ajout des lemmes Zimmerman

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 143 insertions, 1 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 8ef796eef5..72baafe3ac 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -10,6 +10,8 @@
 
 Require Le.
 Require Lt.
+Require Gt.
+Require Decidable.
 
 Theorem zerop : (n:nat){n=O}+{lt O n}.
 Destruct n; Auto with arith.
@@ -52,3 +54,49 @@ Proof.
 Intros; Elim (lt_eq_lt_dec n m); Auto with arith.
 Intros; Absurd (lt m n); Auto with arith.
 Qed.
+
+(* Proofs of decidability *)
+
+Theorem dec_le:(x,y:nat)(decidable (le x y)).
+Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [
+  Auto with arith
+| Intro; Right; Apply gt_not_le; Assumption].
+Save.
+
+Theorem dec_lt:(x,y:nat)(decidable (lt x y)).
+Intros x y; Unfold lt; Apply dec_le.
+Save.
+
+Theorem dec_gt:(x,y:nat)(decidable (gt x y)).
+Intros x y; Unfold gt; Apply dec_lt.
+Save.
+
+Theorem dec_ge:(x,y:nat)(decidable (ge x y)).
+Intros x y; Unfold ge; Apply dec_le.
+Save.
+
+Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x).
+Intros x y H; Elim (lt_eq_lt_dec x y); [
+  Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption]
+| Auto with arith].
+Save.
+
+
+Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y).
+Intros x y H; Elim (le_gt_dec x y);
+  [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ].
+Save.
+
+Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y).
+Intros x y H; Elim (le_gt_dec x y);
+  [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption].
+Save.
+
+Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y).
+Intros x y H; Exact (not_le y x H).
+Save.
+
+Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y).
+Intros x y H; Exact (not_gt y x H). 
+Save.
+
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 29a9780702..afb5a19844 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -94,3 +94,16 @@ Intros n m; Pattern n m; Apply nat_double_ind; Simpl; Auto with arith.
 Intros; Absurd (lt O O); Trivial with arith.
 Qed.
 Hints Immediate lt_O_minus_lt : arith v62.
+
+Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
+Induction x; Auto with arith.
+Save.
+
+
+Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O.
+Intros y x; Pattern y x ; Apply nat_double_ind; [
+  Simpl; Trivial with arith
+| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n]
+| Simpl; Intros n m H1 H2; Apply H1;
+  Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption].
+Save.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index ff38eef695..e90cec6612 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -10,6 +10,7 @@
 
 Require Export Plus.
 Require Export Minus.
+Require Export Lt.
 
 (**********************************************************)
 (* Multiplication                                         *)
@@ -23,6 +24,12 @@ Elim plus_assoc_l; Elim H; Auto with arith.
 Qed.
 Hints Resolve mult_plus_distr : arith v62.
 
+Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)).
+Proof.
+  Induction n. Trivial.
+  Intros. Simpl. Rewrite (H m p). Apply sym_eq. Apply plus_permute_2_in_4.
+Qed.
+
 Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).
 Proof.
 Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Auto with arith.
@@ -65,3 +72,28 @@ Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
 Intro; Elim mult_sym; Auto with arith.
 Save.
 Hints Resolve mult_n_1 : arith v62.
+
+
+Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)).
+Proof.
+  Induction m. Intros. Simpl. Apply le_n.
+  Intros. Simpl. Apply le_plus_plus. Assumption.
+  Apply H. Assumption.
+Qed.
+Hints Resolve mult_le : arith.
+
+Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)).
+Proof.
+  Induction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
+  Intros. Exact (lt_plus_plus ? ? ? ? H0 (H ? ? H0)).
+Qed.
+
+Hints Resolve mult_lt : arith.
+
+Lemma mult_le_conv_1 : (m,n,p:nat) (le (mult (S m) n) (mult (S m) p)) -> (le n p).
+Proof.
+  Intros. Elim (le_or_lt n p). Trivial.
+  Intro H0. Cut (lt (mult (S m) n) (mult (S m) n)). Intro. Elim (lt_n_n ? H1).
+  Apply le_lt_trans with m:=(mult (S m) p). Assumption.
+  Apply mult_lt. Assumption.
+Qed.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 913d6dd371..5ee33d1563 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,8 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+Require Decidable.
 (* $Id$ *)
 
+
 Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
 Proof.
 Induction n.
@@ -22,3 +24,8 @@ Intros q H'; Elim (H q); Auto.
 Qed.
 
 Hints Resolve O_or_S eq_nat_dec : arith.
+
+Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
+Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
+Save.
+
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 2f96112c38..c070e3645e 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -15,7 +15,7 @@
 Require Le.
 Require Lt.
 
-Lemma plus_sym : (n,m:nat)((plus n m)=(plus m n)).
+Lemma plus_sym : (n,m:nat)(plus n m)=(plus m n).
 Proof.
 Intros n m ; Elim n ; Simpl ; Auto with arith.
 Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
@@ -118,3 +118,45 @@ Proof.
 Intros; Apply lt_le_trans with m; Auto with arith.
 Qed.
 Hints Immediate lt_plus_trans : arith v62.
+
+Lemma le_lt_plus_plus : (n,m,p,q:nat) (le n m)->(lt p q)->(lt (plus n p) (plus m q)).
+Proof.
+  Unfold lt. Intros. Change (le (plus (S n) p) (plus m q)). Rewrite plus_Snm_nSm.
+  Apply le_plus_plus; Assumption.
+Qed.
+
+Lemma lt_le_plus_plus : (n,m,p,q:nat) (lt n m)->(le p q)->(lt (plus n p) (plus m q)).
+Proof.
+  Unfold lt. Intros. Change (le (plus (S n) p) (plus m q)). Apply le_plus_plus; Assumption.
+Qed.
+
+Lemma lt_plus_plus : (n,m,p,q:nat) (lt n m)->(lt p q)->(lt (plus n p) (plus m q)).
+Proof.
+  Intros. Apply lt_le_plus_plus. Assumption.
+  Apply lt_le_weak. Assumption.
+Qed.
+
+
+Lemma plus_is_O : (m,n:nat) (plus m n)=O -> m=O /\ n=O.
+Proof.
+  Destruct m; Auto.
+  Intros. Discriminate H.
+Qed.
+
+Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
+Proof.
+  Destruct m; Auto.
+  Destruct n; Auto.
+  Intros. 
+  Simpl in H. Discriminate H.
+Qed.
+
+Lemma plus_permute_2_in_4 : (a,b,c,d:nat)
+      (plus (plus a b) (plus c d))=(plus (plus a c) (plus b d)).
+Proof.
+  Intros. 
+  Rewrite <- (plus_assoc_l a b (plus c d)). Rewrite (plus_assoc_l b c d).
+  Rewrite (plus_sym b c). Rewrite <- (plus_assoc_l c b d). Apply plus_assoc_l.
+Qed.
+
+