diff options
| -rw-r--r-- | .depend | 118 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rwxr-xr-x | theories/Arith/Max.v | 85 | ||||
| -rwxr-xr-x | theories/Arith/Min.v | 35 |
4 files changed, 178 insertions, 62 deletions
@@ -24,6 +24,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/indtypes.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi \ @@ -46,8 +48,6 @@ library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ library/opaque.cmi: kernel/closure.cmi kernel/environ.cmi kernel/names.cmi \ kernel/safe_typing.cmi library/summary.cmi: kernel/names.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -225,18 +225,18 @@ toplevel/recordobj.cmi: library/nametab.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ library/nametab.cmi proofs/proof_type.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -419,24 +419,32 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp_control.cmo: lib/pp_control.cmi -lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi library/global.cmi library/impargs.cmi \ kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \ @@ -517,14 +525,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ @@ -1112,15 +1112,15 @@ tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi lib/explore.cmi proofs/logic.cmi \ kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/termops.cmi lib/util.cmi + proofs/proof_type.cmi kernel/reduction.cmi parsing/search.cmi \ + kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx lib/explore.cmx proofs/logic.cmx \ kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/termops.cmx lib/util.cmx + proofs/proof_type.cmx kernel/reduction.cmx parsing/search.cmx \ + kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \ tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \ @@ -1327,12 +1327,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coqdep_lexer.cmo: config/coq_config.cmi -tools/coqdep_lexer.cmx: config/coq_config.cmx -tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo -tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx +tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo +tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ @@ -1511,6 +1511,16 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ @@ -1557,28 +1567,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ library/declare.cmi pretyping/detyping.cmi kernel/indtypes.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ @@ -1591,6 +1579,18 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \ lib/util.cmx contrib/correctness/pcic.cmi +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -2027,14 +2027,6 @@ contrib/interface/pbp.cmx: parsing/coqlib.cmx contrib/interface/ctast.cmx \ kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -2055,6 +2047,14 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/interface/showproof.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2151,6 +2151,8 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi library/nameops.cmi \ @@ -2171,8 +2173,6 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \ contrib/xml/xmlcommand.cmx -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo contrib/correctness/psyntax.cmo: parsing/grammar.cma contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo @@ -384,7 +384,7 @@ ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.vo \ theories/Arith/Mult.vo theories/Arith/Even.vo \ theories/Arith/EqNat.vo theories/Arith/Peano_dec.vo \ theories/Arith/Euclid.vo theories/Arith/Plus.vo \ - theories/Arith/Wf_nat.vo \ + theories/Arith/Wf_nat.vo theories/Arith/Max.vo \ # theories/Arith/Div.vo BOOLVO=theories/Bool/Bool.vo theories/Bool/IfProp.vo \ diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v new file mode 100755 index 000000000..5ef1ba445 --- /dev/null +++ b/theories/Arith/Max.v @@ -0,0 +1,85 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +Require Arith. + +(**************************************************************************) +(* maximum of two natural numbers *) +(**************************************************************************) + +Fixpoint max [n:nat] : nat -> nat := +[m:nat]Cases n m of + O _ => m + | (S n') O => n + | (S n') (S m') => (S (max n' m')) + end. + +(* Simplifications of max *) + + +Lemma max_SS : (n,m:nat)((S (max n m))=(max (S n) (S m))). +Proof. +Auto with arith. +Qed. + +Lemma max_sym : (n,m:nat)(max n m)=(max m n). +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Qed. + +(* max and le *) + +Lemma max_l : (n,m:nat)(le m n)->(max n m)=n. +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Qed. + +Lemma max_r : (n,m:nat)(le n m)->(max n m)=m. +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Qed. + +Lemma le_max_l : (n,m:nat)(le n (max n m)). +Proof. +NewInduction n; Intros; Simpl; Auto with arith. +Elim m; Intros; Simpl; Auto with arith. +Qed. + +Lemma le_max_r : (n,m:nat)(le m (max n m)). +Proof. +NewInduction n; Simpl; Auto with arith. +NewInduction m; Simpl; Auto with arith. +Qed. +Hints Resolve max_r max_l le_max_l le_max_r: arith v62. + + +(* max n m is equal to n or m *) + +Lemma max_dec : (n,m:nat){(max n m)=n}+{(max n m)=m}. +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Elim (IHn m);Intro H;Elim H;Auto. +Qed. + +Lemma max_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (max n m)). +Proof. +NewInduction n; Simpl; Auto with arith. +NewInduction m; Intros; Simpl; Auto with arith. +Pattern (max n m); Apply IHn ; Auto with arith. +Qed. + +Lemma max_case2 : (n,m:nat)(P:nat->Prop)(P n)->(P m)->(P (max n m)). +Proof. +NewInduction n; Simpl; Auto with arith. +NewInduction m; Intros; Simpl; Auto with arith. +Pattern (max n m); Apply IHn ; Auto with arith. +Qed. + + diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index a38329c34..56d254c48 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -21,30 +21,61 @@ Fixpoint min [n:nat] : nat -> nat := | (S n') (S m') => (S (min n' m')) end. +(* Simplifications of min *) + Lemma min_SS : (n,m:nat)((S (min n m))=(min (S n) (S m))). Proof. Auto with arith. Qed. +Lemma min_sym : (n,m:nat)(min n m)=(min m n). +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Qed. + +(* min and le *) + +Lemma min_l : (n,m:nat)(le n m)->(min n m)=n. +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Qed. + +Lemma min_r : (n,m:nat)(le m n)->(min n m)=m. +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Qed. + Lemma le_min_l : (n,m:nat)(le (min n m) n). Proof. NewInduction n; Intros; Simpl; Auto with arith. Elim m; Intros; Simpl; Auto with arith. Qed. -Hints Resolve le_min_l : arith v62. Lemma le_min_r : (n,m:nat)(le (min n m) m). Proof. NewInduction n; Simpl; Auto with arith. NewInduction m; Simpl; Auto with arith. Qed. -Hints Resolve le_min_r : arith v62. +Hints Resolve min_l min_r le_min_l le_min_r : arith v62. (* min n m is equal to n or m *) +Lemma min_dec : (n,m:nat){(min n m)=n}+{(min n m)=m}. +Proof. +NewInduction n;NewInduction m;Simpl;Auto with arith. +Elim (IHn m);Intro H;Elim H;Auto. +Qed. + Lemma min_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (min n m)). Proof. NewInduction n; Simpl; Auto with arith. NewInduction m; Intros; Simpl; Auto with arith. Pattern (min n m); Apply IHn ; Auto with arith. Qed. + +Lemma min_case2 : (n,m:nat)(P:nat->Prop)(P n)->(P m)->(P (min n m)). +Proof. +NewInduction n; Simpl; Auto with arith. +NewInduction m; Intros; Simpl; Auto with arith. +Pattern (min n m); Apply IHn ; Auto with arith. +Qed. |