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/Max.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/Max.v')
-rwxr-xr-x | theories/Arith/Max.v | 85 |
1 files changed, 85 insertions, 0 deletions
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. + + |