lemmes sur Zdiv/Zmod

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

1 files changed, 59 insertions, 15 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index b7876f340..03fb9798a 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -153,8 +153,7 @@ Proof.
 Intros a b; Case a; Case b; Try (Simpl; Intros; Omega).
 Unfold Zdiv_eucl; Intros; Apply Z_div_mod_POS; Trivial.
 
-Intros.
-Absurd `(NEG p) > 0`; [ Generalize (NEG_lt_ZERO p); Omega | Trivial ].
+Intros; Discriminate.
 
 Intros.
 Generalize (Z_div_mod_POS (POS p) H p0).
@@ -177,23 +176,11 @@ Split; Trivial.
 Replace (NEG p0) with `-(POS p0)`; [ Rewrite H1; Ring | Trivial ].
 Generalize (NEG_lt_ZERO p1); Omega.
 
-Intros.
-Absurd `(NEG p)>0`; [ Generalize (NEG_lt_ZERO p); Omega | Omega ].
+Intros; Discriminate.
 Qed.
 
-Theorem Z_div_mod_eq : (a,b:Z)`b > 0` -> `a = b * (Zdiv a b) + (Zmod a b)`.
-Proof.
-Unfold Zdiv Zmod.
-Intros a b Hb.
-Generalize (Z_div_mod a b Hb).
-Pattern (Zdiv_eucl a b).
-Case (Zdiv_eucl); Tauto.
-Save.
-
 (** Existence theorems *)
 
-Set Implicit Arguments.
-
 Theorem Zdiv_eucl_exist : (b:Z)`b > 0` -> (a:Z)
   { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }.
 Proof.
@@ -202,6 +189,8 @@ Exists (Zdiv_eucl a b).
 Exact (Z_div_mod a b Hb).
 Qed.
 
+Implicits Zdiv_eucl_exist.
+
 Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z)
   { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }.
 Proof.
@@ -219,6 +208,61 @@ Rewrite <- Zmult_Zopp_left;Assumption.
 Rewrite Zabs_non_eq;[Assumption|Omega].
 Qed.
 
+Implicits Zdiv_eucl_extended.
+
+(** Auxiliary lemmas about [Zdiv] and [Zmod] *)
+
+Lemma Z_div_mod_eq : (a,b:Z)`b > 0` -> `a = b * (Zdiv a b) + (Zmod a b)`.
+Proof.
+Unfold Zdiv Zmod.
+Intros a b Hb.
+Generalize (Z_div_mod a b Hb).
+Case (Zdiv_eucl); Tauto.
+Save.
+
+Lemma Z_mod_lt : (a,b:Z)`b > 0` -> `0 <= (Zmod a b) < b`.
+Proof.
+Unfold Zmod.
+Intros a b Hb.
+Generalize (Z_div_mod a b Hb).
+Case (Zdiv_eucl a b); Tauto.
+Save.
+
+Lemma Z_div_POS_ge0 : (b:Z)(a:positive)
+  let (q,_) = (Zdiv_eucl_POS a b) in `q >= 0`.
+Proof.
+Induction a; Intros; Simpl.
+Generalize H; Case (Zdiv_eucl_POS p b); Simpl.
+Intros; Case (Zgt_bool b `z0+z0+1`); Simpl; Omega.
+Generalize H; Case (Zdiv_eucl_POS p b); Simpl.
+Intros; Case (Zgt_bool b `z0+z0`); Simpl; Omega.
+Case (Zge_bool b `2`); Simpl; Omega.
+Save.
+
+Lemma Z_div_ge0 : (a,b:Z)`b > 0` -> `a >= 0` -> `(Zdiv a b) >= 0`.
+Proof.
+Intros a b Hb; Unfold Zdiv Zdiv_eucl; Case a; Simpl; Intros.
+Case b; Simpl; Trivial.
+Generalize Hb; Case b; Try Trivial.
+Auto with zarith.
+Intros p0 Hp0; Generalize (Z_div_POS_ge0 (POS p0) p).
+Case (Zdiv_eucl_POS p (POS p0)); Simpl; Tauto.
+Intros; Discriminate.
+Elim H; Trivial.
+Save.
+
+Lemma Z_div_lt : (a,b:Z)`b >= 2` -> `a > 0` -> `(Zdiv a b) < a`.
+Proof.
+Intros. Cut `b > 0`; [Intro Hb | Omega].
+Generalize (Z_div_mod a b Hb).
+Cut `a >= 0`; [Intro Ha | Omega].
+Generalize (Z_div_ge0 a b Hb Ha).
+Unfold Zdiv; Case (Zdiv_eucl a b); Intros q r H1 [H2 H3].
+Cut `a >= 2*q` -> `q < a`; [ Intro h; Apply h; Clear h | Intros; Omega ].
+Apply Zge_trans with `b*q`.
+Omega.
+Auto with zarith.
+Save.
 
 (** Syntax *)