nouveaux lemmes dans Zdiv (Claude Marche)

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

3 files changed, 100 insertions, 1 deletions

diff --git a/.depend.coq b/.depend.coq
index d3c97df3de..ae6d159b39 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -115,7 +115,7 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
-theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo
+theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 20309ab069..2ce09a752d 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -249,3 +249,20 @@ Rewrite Zopp_Zopp;Intros.
 Elim (H `|m|`);Intros;Auto with zarith.
 Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
 Qed.
+
+(** To do case analysis over the sign of [z] *) 
+
+Unset Implicit Arguments.
+
+Lemma Zcases : (x:Z)(P:Prop)
+ (`x=0`->P)->
+ (`x>0`->P)->
+ (`x<0`->P)->P.
+Proof.
+Intros x P Hzero Hpos Hneg.
+Induction x.
+Apply Hzero; Trivial.
+Apply Hpos; Apply POS_gt_ZERO.
+Apply Hneg; Apply NEG_lt_ZERO.
+Save.
+
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 03fb9798ab..7cbf21ae3b 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -22,6 +22,7 @@ Then only after proves the main required property.
 Require Export ZArith.
 Require Omega.
 Require ZArithRing.
+Require Zcomplements.
 
 (**
 
@@ -284,3 +285,84 @@ Syntax constr
       [ << (ZEXPR <<(Zmod $n1 $n2)>>) >> ]
       	 -> [ (ZEXPR $n1):E "%" [0 0] (ZEXPR $n2):L ]
 .
+
+(** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)
+
+Lemma Z_div_ge : (a,b,c:Z)`c > 0`->`a >= b`->`a/c >= b/c`.
+Proof.
+Intros a b c cPos aGeb.
+Generalize (Z_div_mod_eq a c cPos).
+Generalize (Z_mod_lt a c cPos).
+Generalize (Z_div_mod_eq b c cPos).
+Generalize (Z_mod_lt b c cPos).
+Intros.
+Elim (Z_ge_lt_dec `a/c` `b/c`); Trivial.
+Intro.
+Absurd `b-a >= 1`.
+Omega.
+Rewrite -> H0.
+Rewrite -> H2.
+Assert `c*(b/c)+b%c-(c*(a/c)+a%c) = c*(b/c - a/c) + b%c - a%c`.
+Ring.
+Rewrite H3.
+Assert `c*(b/c-a/c) >= c*1`.
+Apply Zge_Zmult_pos_left.
+Omega.
+Omega.
+Assert `c*1=c`.
+Ring.
+Omega.
+Save.
+
+Lemma Z_mod_plus : (a,b,c:Z)`c > 0`->`(a+b*c)%c = a%c`.
+Proof.
+Intros a b c cPos.
+Generalize (Z_div_mod_eq a c cPos).
+Generalize (Z_mod_lt a c cPos).
+Generalize (Z_div_mod_eq `a+b*c` c cPos).
+Generalize (Z_mod_lt `a+b*c` c cPos).
+Intros.
+
+Assert `(a+b*c)%c - a%c = c*(b+a/c - (a+b*c)/c)`.
+Replace `(a+b*c)%c` with `a+b*c - c*((a+b*c)/c)`.
+Replace `a%c` with `a - c*(a/c)`.
+Ring.
+Omega.
+Omega.
+LetTac q := `b+a/c-(a+b*c)/c`.
+Apply (Zcases q); Intros.
+Assert `c*q=0`.
+Rewrite H4; Ring.
+Rewrite H5 in H3.
+Omega.
+
+Assert `c*q >= c`.
+Pattern 2 c; Replace c with `c*1`.
+Apply Zge_Zmult_pos_left; Omega.
+Ring.
+Omega.
+
+Assert `c*q <= -c`.
+Replace `-c` with `c*(-1)`.
+Apply Zle_Zmult_pos_left; Omega.
+Ring.
+Omega.
+Save.
+
+Lemma Z_div_plus : (a,b,c:Z)`c > 0`->`(a+b*c)/c = a/c+b`.
+Proof.
+Intros a b c cPos.
+Generalize (Z_div_mod_eq a c cPos).
+Generalize (Z_mod_lt a c cPos).
+Generalize (Z_div_mod_eq `a+b*c` c cPos).
+Generalize (Z_mod_lt `a+b*c` c cPos).
+Intros.
+Apply Zmult_reg_left with 1:=cPos.
+Replace `c*((a+b*c)/c)` with `a+b*c-(a+b*c)%c`.
+Rewrite (Z_mod_plus a b c cPos).
+Pattern 1 a; Rewrite H2.
+Ring.
+Pattern 1 `a+b*c`; Rewrite H0.
+Ring.
+Save.
+