Report de lemmes de Znumtheory dans Zabs ou BinInt

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

4 files changed, 48 insertions, 29 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 14aa0dec10..b5fa6694ba 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -639,6 +639,16 @@ Intros x y z H; Apply simpl_times_r with z:=z.
 Rewrite times_sym with x:=x; Rewrite times_sym with x:=y; Assumption.
 Qed.
 
+(** Inversion of multiplication *)
+
+Lemma times_one_inversion_l : (x,y:positive) (times x y)=xH -> x=xH.
+Proof.
+Intros x y; NewDestruct x; Simpl.
+ NewDestruct y; Intro; Discriminate.
+ Intro; Discriminate.
+ Reflexivity.
+Qed.
+
 (**********************************************************************)
 (** Properties of comparison on binary positive numbers *)
 
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index e6257b243d..81cf647701 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -752,6 +752,15 @@ Qed.
 
 V7only [Unset Implicit Arguments.].
 
+Lemma Zmult_1_inversion_l : 
+ (x,y:Z) (Zmult x y)=(POS xH) -> x=(POS xH) \/ x=(NEG xH).
+Proof.
+Intros x y; NewDestruct x as [|p|p]; Intro; [ Discriminate | Left | Right ];
+  (NewDestruct y as [|q|q]; Try Discriminate;
+  Simpl in H; Injection H; Clear H; Intro H;
+  Rewrite times_one_inversion_l with 1:=H; Reflexivity).
+Qed.
+
 (** Multiplication and Opposite *)
 
 Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y).
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index a4968b4187..27c72c4d15 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -13,6 +13,8 @@ Require Arith.
 Require BinPos.
 Require BinInt.
 Require Zorder.
+Require Zsyntax.
+Require ZArith_dec.
 
 V7only [Import nat_scope.].
 Open Local Scope Z_scope.
@@ -37,6 +39,18 @@ Proof.
 Intros z; Case z; Simpl; Auto.
 Qed.
 
+(** Proving a property of the absolute value by cases *)
+
+Lemma Zabs_ind : 
+  (P:Z->Prop)(x:Z)(`x >= 0` -> (P x)) -> (`x <= 0` -> (P `-x`)) ->
+  (P `|x|`).
+Proof.
+Intros P x H H0; Elim (Z_lt_ge_dec x `0`); Intro.
+Assert `x<=0`. Apply Zlt_le_weak; Assumption.
+Rewrite Zabs_non_eq. Apply H0. Assumption. Assumption.
+Rewrite Zabs_eq. Apply H; Assumption. Apply Zge_le. Assumption.
+Save.
+
 V7only [ (* From Zdivides *) ].
 Theorem Zabs_intro: (P : ?) (z : Z) (P (Zopp z)) -> (P z) ->  (P (Zabs z)).
 Intros P z; Case z; Simpl; Auto.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 7a25df242b..dfe1c31fda 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -136,17 +136,12 @@ Hints Resolve Zdivide_plus Zdivide_opp Zdivide_opp_rev
 Lemma Zmult_one : 
  (x,y:Z) `x>=0` -> `x*y=1` -> `x=1`.
 Proof.
-Intros.
-Assert `x<>0`.
- Intro; Subst; Auto with zarith.
-Assert `y>0`.
- Apply (Zmult_gt x y); Auto with zarith.
-Elim (Z_lt_ge_dec `1` x); [ Intros | Auto with zarith ].
-Elim (Z_lt_ge_dec `1` y); Intros.
-Assert `x*y >= 2*1`.
- Apply Zge_Zmult_pos_compat; Omega.
-Auto with zarith.
-Assert y=1; Subst; Auto with zarith.
+Intros x y H H0; NewDestruct (Zmult_1_inversion_l ? ? H0) as [Hpos|Hneg].
+  Assumption.
+  Rewrite Hneg in H; Simpl in H.
+  Contradiction (Zle_not_lt `0` `-1`).
+    Apply Zge_le; Assumption.
+    Apply NEG_lt_ZERO.
 Save.
 
 (** Only [1] and [-1] divide [1]. *)
@@ -183,15 +178,6 @@ Save.
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 
-Lemma Zabs_ind : 
-  (P:Z->Prop)(x:Z)(`x >= 0` -> (P x)) -> (`x <= 0` -> (P `-x`)) ->
-  (P `|x|`).
-Proof.
-Intros; Elim (Z_lt_ge_dec x `0`); Intro. 
-Rewrite Zabs_non_eq. Apply H0; Omega. Omega.
-Rewrite Zabs_eq. Apply H; Assumption. Omega.
-Save.
-
 Lemma Zdivide_bounds : (a,b:Z) (a|b) -> `b<>0` -> `|a| <= |b|`.
 Proof.
 Induction 1; Intros.
@@ -353,7 +339,7 @@ Inductive Bezout [a,b,d:Z] : Prop :=
 Lemma gcd_bezout : (a,b,d:Z) (gcd a b d) -> (Bezout a b d).
 Proof.
 Intros a b d Hgcd.
-Elim (euclid a b); Intros.
+Elim (euclid a b); Intros u v d0 e g.
 Generalize (gcd_uniqueness_apart_sign a b d d0 Hgcd g).
 Intro H; Elim H; Clear H; Intros.
 Apply Bezout_intro with u v.
@@ -366,7 +352,7 @@ Save.
 
 Lemma gcd_mult : (a,b,c,d:Z) (gcd a b d) -> (gcd `c*a` `c*b` `c*d`).
 Proof.
-Induction 1; Constructor; Intuition.
+Intros a b c d; Induction 1; Constructor; Intuition.
 Elim (gcd_bezout a b d H); Intros.
 Elim H3; Intros.
 Elim H4; Intros.
@@ -430,11 +416,11 @@ Defined.
 Definition Zgcd := [a,b:Z](let (g,_) = (Zgcd_spec a b) in g).
 
 Lemma Zgcd_is_pos : (a,b:Z)`(Zgcd a b) >=0`.
-Intros; Unfold Zgcd; Case (Zgcd_spec a b); Tauto.
+Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto.
 Qed.
 
 Lemma Zgcd_is_gcd : (a,b:Z)(gcd a b (Zgcd a b)).
-Intros; Unfold Zgcd; Case (Zgcd_spec a b); Tauto.
+Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto.
 Qed.
 
 (** * Relative primality *)
@@ -488,7 +474,7 @@ Lemma rel_prime_cross_prod :
   (a,b,c,d:Z) (rel_prime a b) -> (rel_prime c d) -> `b>0` -> `d>0` -> 
   `a*d = b*c` -> (a=c /\ b=d).
 Proof.
-Intros.
+Intros a b c d; Intros.
 Elim (Zdivide_antisym b d).
 Split; Auto with zarith.
 Rewrite H4 in H3.
@@ -510,7 +496,7 @@ Save.
 
 Lemma gcd_rel_prime : 
  (a,b,g:Z)`b>0` -> `g>=0`-> (gcd a b g) -> (rel_prime `a/g` `b/g`).
-Intros.
+Intros a b g; Intros.
 Assert `g <> 0`.
  Intro.
  Elim H1; Intros. 
@@ -598,14 +584,14 @@ Hints Resolve prime_rel_prime : zarith.
 (** [Zdivide] can be expressed using [Zmod]. *)
 
 Lemma Zmod_Zdivide : (a,b:Z) `b>0` -> `a%b = 0` -> (b|a).
-Intros. 
+Intros a b H H0.
 Apply Zdivide_intro with `(a/b)`.
 Pattern 1 a; Rewrite (Z_div_mod_eq a b H).
 Rewrite H0; Ring.
 Save.
 
 Lemma Zdivide_Zmod : (a,b:Z) `b>0` -> (b|a) -> `a%b = 0`.
-Destruct 2; Intros; Subst.
+Intros a b; Destruct 2; Intros; Subst.
 Change `q*b` with `0+q*b`.
 Rewrite Z_mod_plus; Auto.
 Save.
@@ -635,7 +621,7 @@ Save.
 Lemma prime_mult : 
   (p:Z) (prime p) -> (a,b:Z) (p | `a*b`) -> (p | a) \/ (p | b).
 Proof.
-Induction 1; Intros.
+Intro p; Induction 1; Intros.
 Case (Zdivide_dec p a); Intuition.
 Right; Apply Gauss with a; Auto with zarith.
 Save.