diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-15 17:36:08 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-15 17:36:08 +0000 |
commit | cd279a01c50c9a5a236ff360709c569be08a5c80 (patch) | |
tree | f84e2710bdf333f371e4a55c3371d62b74b25311 /theories/Arith/Min.v | |
parent | fa806c8c70d2318cc8674b6546763e6d6346afbf (diff) |
Ajout d'un fichier Max dans Arith, et enrichissement du Min.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Min.v')
-rwxr-xr-x | theories/Arith/Min.v | 35 |
1 files changed, 33 insertions, 2 deletions
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. |