Ajout lemmes; independance vis a vis noms variables liees

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

1 files changed, 59 insertions, 20 deletions

diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index d3d3efac1..a4968b418 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -10,7 +10,8 @@
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Arith.
-Require fast_integer.
+Require BinPos.
+Require BinInt.
 Require Zorder.
 
 V7only [Import nat_scope.].
@@ -20,33 +21,84 @@ Open Local Scope Z_scope.
 (** Properties of absolute value *)
 
 Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
-NewDestruct x; Auto with arith.
+Intro x; NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
 
 Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
 Proof.
-NewDestruct x; Auto with arith.
+Intro x; NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
 
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_Zopp: (z : Z)  (Zabs (Zopp z)) = (Zabs z).
+Proof.
+Intros z; Case z; Simpl; Auto.
+Qed.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_intro: (P : ?) (z : Z) (P (Zopp z)) -> (P z) ->  (P (Zabs z)).
+Intros P z; Case z; Simpl; Auto.
+Qed.
+
 Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
 Proof.
-NewDestruct x;Auto with arith.
+Intro x; NewDestruct x;Auto with arith.
 Defined.
 
 Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
-NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Intro x; NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Qed.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_eq_case:
+ (z1, z2 : Z) (Zabs z1) = (Zabs z2) ->  z1 = z2 \/ z1 = (Zopp z2).
+Proof.
+Intros z1 z2; Case z1; Case z2; Simpl; Auto; Try (Intros; Discriminate);
+ Intros p1 p2 H1; Injection H1; (Intros H2; Rewrite H2); Auto.
 Qed.
 
+(** Triangular inequality *)
+
+Hints Local Resolve Zle_NEG_POS :zarith.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_triangle:
+ (z1, z2 : Z)  (Zle (Zabs (Zplus z1 z2)) (Zplus (Zabs z1) (Zabs z2))).
+Proof.
+Intros z1 z2; Case z1; Case z2; Try (Simpl; Auto with zarith; Fail).
+Intros p1 p2;
+ Apply Zabs_intro
+      with P := [x : ?]  (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1))));
+ Try Rewrite Zopp_Zplus; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Intros p1 p2;
+ Apply Zabs_intro
+      with P := [x : ?]  (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1))));
+ Try Rewrite Zopp_Zplus; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Qed.
+
+(** Absolute value and multiplication *)
+
 Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
 Proof.
-NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith.
 Qed.
 
 Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x.
 Proof.
-NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Qed.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_Zmult:
+ (z1, z2 : Z)  (Zabs (Zmult z1 z2)) = (Zmult (Zabs z1) (Zabs z2)).
+Proof.
+Intros z1 z2; Case z1; Case z2; Simpl; Auto.
 Qed.
 
 (** absolute value in nat is compatible with order *)
@@ -70,16 +122,3 @@ Compute. Intro H0. Discriminate H0. Intuition.
 
 Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition.
 Qed.
-
-Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n).
-Proof.
-Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus;
-Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n);
-Apply Zlt_reg_l; Assumption.
-Qed.
-
-Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n).
-Proof.
-Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l;
-Rewrite Zplus_sym;Exact H.
-Qed.