nouveau module Zdiv

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

5 files changed, 290 insertions, 151 deletions

diff --git a/.depend.coq b/.depend.coq
index 8ac9788a17..d3c97df3de 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -115,6 +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/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/Makefile b/Makefile
index f184b937f2..cf254a4fa1 100644
--- a/Makefile
+++ b/Makefile
@@ -410,7 +410,8 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/ZArith_dec.vo  theories/ZArith/fast_integer.vo \
 	 theories/ZArith/Zmisc.vo       theories/ZArith/zarith_aux.vo \
 	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
-	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo
+	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
+	 theories/ZArith/Zdiv.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index ef479c8310..815d22ebf6 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -150,8 +150,6 @@ Apply Zcompare_Zmult_right; Assumption.
 Save.
 
 
-Section diveucl.
-
 Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. 
 NewDestruct x.
 Left ; Split with ZERO; Reflexivity.
@@ -215,141 +213,6 @@ Omega.
 Simpl; Omega.
 Save.
 
-Lemma Zdiv_eucl_POS : (b:Z)`b > 0` -> (p:positive)
-  { qr:Z*Z | let (q,r)=qr in `(POS p)=b*q+r` /\ `0 <= r < b` }.
-
-Induction p.
-
-(* p => (xI p) *)
-(* Notez l'utilisation des nouveaux patterns Intro *)
-Intros p' ((q,r), (Hrec1, Hrec2)).
-Elim (Z_lt_ge_dec `2*r+1` b); 
-[ Exists `(2*q, 2*r+1)`;
-  Rewrite POS_xI;
-  Rewrite Hrec1;
-  Split; 
-  [ Rewrite Zmult_Zplus_distr; 
-    Rewrite Zplus_assoc_l;
-    Rewrite (Zmult_permute b `2`);
-    Reflexivity
-  | Omega ]
-| Exists `(2*q+1, 2*r+1-b)`;
-  Rewrite POS_xI;
-  Rewrite Hrec1;
-  Split; 
-  [ Do 2 Rewrite Zmult_Zplus_distr; 
-    Unfold Zminus;
-    Do 2 Rewrite Zplus_assoc_l;
-    Rewrite <- (Zmult_permute `2` b);
-    Generalize `b*q`; Intros; Omega
-  | Omega ]
-].
-
-(* p => (xO p) *)
-Intros p' ((q,r), (Hrec1, Hrec2)).
-Elim (Z_lt_ge_dec `2*r` b); 
-[ Exists `(2*q,2*r)`;
-  Rewrite POS_xO;
-  Rewrite Hrec1;
-  Split; 
-  [ Rewrite Zmult_Zplus_distr; 
-    Rewrite (Zmult_permute b `2`);
-    Reflexivity
-  | Omega ]
-| Exists `(2*q+1, 2*r-b)`;
-  Rewrite POS_xO;
-  Rewrite Hrec1;
-  Split; 
-  [ Do 2 Rewrite Zmult_Zplus_distr; 
-    Unfold Zminus;
-    Rewrite <- (Zmult_permute `2` b);
-    Generalize `b*q`; Intros; Omega
-  | Omega ]
-].
-(* xH *)
-Elim (Z_le_gt_dec `2` b);
-[ Exists `(0,1)`; Omega
-| Exists `(1,0)`; Omega 
-].
-Save.
-
-Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z)
-  { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }.
-NewDestruct a;
-
-[ (* a=0 *) Exists `(0,0)`; Omega
-| (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto
-| (* a = (NEG p) *) Intros; Elim (Zdiv_eucl_POS H p);
-  Intros (q,r) (Hp1, Hp2);
-  Elim (Z_le_gt_dec r `0`); 
-  [ Exists `(-q,0)`; Split;
-    [ Apply Zopp_intro; Simpl; Rewrite Hp1;
-      Rewrite Zero_right; 
-      Rewrite <- Zopp_Zmult;
-      Rewrite Zmult_Zopp_Zopp;
-      Generalize `b*q`; Intro; Omega 
-    | Omega
-    ]
-  | Exists `(-(q+1),b-r)`; Split;
-    [ Apply Zopp_intro;
-      Unfold Zminus; Simpl; Rewrite Hp1;
-      Repeat Rewrite Zopp_Zplus;
-      Repeat Rewrite <- Zopp_Zmult;
-      Rewrite Zmult_Zplus_distr;
-      Rewrite Zmult_Zopp_Zopp;
-      Rewrite Zplus_assoc_r;
-      Apply f_equal with f:=[c:Z]`b*q+c`;
-      Omega
-    | Omega ]
-  ]
-].
-Save.
-
-Definition Zdiv [a,b:Z] : Z :=
-  Cases (Z_gt_le_dec b `0`) of
-    (left bpos) => let (qr,_) = (Zdiv_eucl bpos a) in 
-                   let (q,_) = qr in q
-  | (right _) => `0` end.
-
-Definition Zmod [a,b:Z] : Z :=
-  Cases (Z_gt_le_dec b `0`) of
-    (left bpos) => let (qr,_) = (Zdiv_eucl bpos a) in 
-                   let (_,r) = qr in r
-  | (right _) => `0` end.
-
-Lemma Z_div_mod : (a,b:Z)`b > 0` -> `a = (Zdiv a b)*b + (Zmod a b)`.
-Proof.
-Intros; Unfold Zdiv Zmod; Case (Z_gt_le_dec b `0`); Simpl; Intros.
-Case (Zdiv_eucl z a); Simpl; Induction x; Intros. 
-Rewrite <- Zmult_sym; Tauto.
-Absurd `b > 0`; Omega.
-Save.
-
-Lemma Z_mod_bounds : (a,b:Z)`b > 0` -> `0 <= (Zmod a b) < b`.
-Proof.
-Intros; Unfold Zdiv Zmod; Case (Z_gt_le_dec b `0`); Simpl; Intros.
-Case (Zdiv_eucl z a); Simpl; Induction x; Intros; Omega. 
-Absurd `b > 0`; Omega.
-Save.
-
-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.
-Intros b Hb a.
-Elim (Z_le_gt_dec `0` b);Intro Hb'.
-Cut `b>0`;[Intro Hb''|Omega].
-Rewrite Zabs_eq;[Apply Zdiv_eucl;Assumption|Assumption].
-Cut `-b>0`;[Intro Hb''|Omega].
-Elim (Zdiv_eucl Hb'' a);Intros qr.
-Elim qr;Intros q r Hqr.
-Exists (pair ? ? `-q` r).
-Elim Hqr;Intros.
-Split.
-Rewrite <- Zmult_Zopp_left;Assumption.
-Rewrite Zabs_non_eq;[Assumption|Omega].
-Save.
-
-End diveucl.
 
 (** Two more induction principles over [Z]. *)
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
new file mode 100644
index 0000000000..75894ffa34
--- /dev/null
+++ b/theories/ZArith/Zdiv.v
@@ -0,0 +1,238 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(* Contribution by Claude Marché and Xavier Urbain *)
+
+(**
+
+Euclidean Division
+
+Defines first of function that allows Coq to normalize. 
+Then only after proves the main required property.
+
+*)
+
+Require ZArith.
+Require Omega.
+Require ZArithRing.
+
+(**
+
+  Euclidean division of a positive by a integer 
+  (that is supposed to be positive).
+
+  total function than returns an arbitrary value when
+  divisor is not positive
+  
+*)
+
+Fixpoint Zdiv_eucl_POS [a:positive] : Z -> Z*Z := [b:Z]
+ Cases a of
+ | xH => if `(Zge_bool b 2)` then `(0,1)` else `(1,0)` 
+ | (xO a') => 
+    let (q,r) = (Zdiv_eucl_POS a' b) in 
+    if `(Zgt_bool b (r+r))` then `(q+q,r+r)` else `(q+q+1,r+r-b)`
+ | (xI a') =>
+    let (q,r) = (Zdiv_eucl_POS a' b) in 
+    if `(Zgt_bool b (r+r+1))` then `(q+q,r+r+1)` else `(q+q+1,r+r+1-b)`
+ end.
+
+
+(**
+
+  Euclidean division of integers.
+ 
+  Total function than returns (0,0) when dividing by 0. 
+
+*) 
+    
+(* 
+
+  The pseudo-code is:
+  
+  if b = 0 : (0,0)
+ 
+  if b <> 0 and a = 0 : (0,0)
+
+  if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in 
+                       if r = 0 then (-q,0) else (-(q+1),b-r)
+
+  if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r)
+
+  if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in 
+                       if r = 0 then (-q,0) else (-(q+1),b+r)
+
+*)
+
+Definition Zdiv_eucl [a,b:Z] : Z*Z :=
+  Cases a b of
+  | ZERO _  => `(0,0)`
+  | _ ZERO  => `(0,0)`
+  | (POS a') (POS _) => (Zdiv_eucl_POS a' b)
+  | (NEG a') (POS _) => 
+      let (q,r) = (Zdiv_eucl_POS a' b) in 
+      Cases r of 
+      | ZERO => `(-q,0)`
+      | _    => `(-(q+1),b-r)`
+      end
+  | (NEG a') (NEG b') => 
+	 let (q,r) = (Zdiv_eucl_POS a' (POS b')) in `(q,-r)`
+  | (POS a') (NEG b') =>
+      let (q,r) = (Zdiv_eucl_POS a' (POS b')) in 
+      Cases r of 
+      | ZERO => `(-q,0)`
+      | _    => `(-(q+1),b+r)`
+      end
+    end.
+
+
+(** Division and modulo are projections of [Zdiv_eucl] *)
+     
+Definition Zdiv [a,b:Z] : Z := let (q,_) = (Zdiv_eucl a b) in q.
+
+Definition Zmod [a,b:Z] : Z := let (_,r) = (Zdiv_eucl a b) in r. 
+
+(* Tests:
+
+Eval Compute in `(Zdiv_eucl 7 3)`. 
+
+Eval Compute in `(Zdiv_eucl (-7) 3)`.
+
+Eval Compute in `(Zdiv_eucl 7 (-3))`.
+
+Eval Compute in `(Zdiv_eucl (-7) (-3))`.
+
+*)
+
+
+(**
+
+  Main division theorem. 
+
+  First a lemma for positive
+
+*)
+
+Lemma Z_div_mod_POS : (b:Z)`b > 0` -> (a:positive)
+  let (q,r)=(Zdiv_eucl_POS a b) in `(POS a) = b*q + r`/\`0<=r<b`.
+Proof.
+Induction a; Simpl.
+Intro p.
+Case (Zdiv_eucl_POS p b).
+Intros q r H1.
+Decompose [and] H1.
+Generalize (Zgt_cases b `r+r+1`).
+Case (Zgt_bool b `r+r+1`); 
+(Rewrite POS_xI; Rewrite H0; Split ; [ Ring | Omega ]).
+
+Intros p.
+Case (Zdiv_eucl_POS p b).
+Intros q r H1.
+Decompose [and] H1.
+Generalize (Zgt_cases b `r+r`).
+Case (Zgt_bool b `r+r`);
+(Rewrite POS_xO; Rewrite H0; Split ; [ Ring | Omega ]).
+
+Generalize (Zge_cases b `2`).
+Case (Zge_bool b `2`); 
+(Intros; Split; [Ring | Omega ]).
+Omega.
+Save.
+
+
+
+Theorem Z_div_mod : (a,b:Z)`b > 0` -> 
+  let (q,r) = (Zdiv_eucl a b) in `a = b*q + r` /\ `0<=r<b`.
+Proof.
+Intros a b; Case a; Case b.
+Simpl; Omega.
+Simpl; Intros; Omega.
+Simpl; Intros; Omega.
+Simpl; Intros; Omega.
+Unfold Zdiv_eucl; Intros; Apply Z_div_mod_POS; Trivial.
+
+Intros.
+Absurd `(NEG p) > 0`.
+Generalize (NEG_lt_ZERO p).
+Omega.
+Assumption.
+
+Intros; Absurd `0>0`.
+Unfold Zgt; Simpl.
+Discriminate.
+Assumption.
+
+Intros.
+Generalize (Z_div_mod_POS (POS p) H p0).
+Unfold Zdiv_eucl.
+Case (Zdiv_eucl_POS p0 (POS p)).
+Intros z z0.
+Case z0.
+
+Intros [H1 H2].
+Split.
+Replace (NEG p0) with `-(POS p0)`.
+Rewrite H1.
+Ring.
+Trivial.
+Trivial.
+
+Intros p1 [H1 H2].
+Split.
+Replace (NEG p0) with `-(POS p0)`.
+Rewrite H1.
+Ring.
+Trivial.
+Generalize (POS_gt_ZERO p1); Omega.
+
+Intros p1 [H1 H2].
+Split.
+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.
+Save.
+
+
+(** Existence theorems *)
+
+Implicit Arguments On.
+
+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.
+Intros b Hb a.
+Exists (Zdiv_eucl a b).
+Exact (Z_div_mod a b Hb).
+Save.
+
+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.
+Intros b Hb a.
+Elim (Z_le_gt_dec `0` b);Intro Hb'.
+Cut `b>0`;[Intro Hb''|Omega].
+Rewrite Zabs_eq;[Apply Zdiv_eucl_exist;Assumption|Assumption].
+Cut `-b>0`;[Intro Hb''|Omega].
+Elim (Zdiv_eucl_exist Hb'' a);Intros qr.
+Elim qr;Intros q r Hqr.
+Exists (pair ? ? `-q` r).
+Elim Hqr;Intros.
+Split.
+Rewrite <- Zmult_Zopp_left;Assumption.
+Rewrite Zabs_non_eq;[Assumption|Omega].
+Save.
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 7e3fae23e8..396ef8e5ae 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -63,13 +63,44 @@ Lemma NEG_add : (p,p':positive)`(NEG (add p p'))=(NEG p)+(NEG p')`.
 Induction p; Induction p'; Simpl; Auto with arith.
 Save.
 
-Definition Zle_bool := [x,y:Z]Case `x ?= y` of true true false end.
-Definition Zge_bool := [x,y:Z]Case `x ?= y` of true false true end.
-Definition Zlt_bool := [x,y:Z]Case `x ?= y` of false true false end.
-Definition Zgt_bool := [x,y:Z]Case ` x ?= y` of false false true end.
-Definition Zeq_bool := [x,y:Z]Cases `x ?= y` of EGAL => true | _ => false end.
-Definition Zneq_bool := [x,y:Z]Cases `x ?= y` of EGAL =>false | _ => true end.
+(** Boolean comparisons *)
+
+Definition Zle_bool := 
+  [x,y:Z]Cases `x ?= y` of SUPERIEUR => false | _ => true end.
+Definition Zge_bool := 
+  [x,y:Z]Cases `x ?= y` of INFERIEUR => false | _ => true end.
+Definition Zlt_bool := 
+  [x,y:Z]Cases `x ?= y` of INFERIEUR => true | _ => false end.
+Definition Zgt_bool := 
+  [x,y:Z]Cases ` x ?= y` of SUPERIEUR => true | _ => false end.
+Definition Zeq_bool := 
+  [x,y:Z]Cases `x ?= y` of EGAL => true | _ => false end.
+Definition Zneq_bool := 
+  [x,y:Z]Cases `x ?= y` of EGAL => false | _ => true end.
+
+Lemma Zle_cases : (x,y:Z)if (Zle_bool x y) then `x<=y` else `x>y`.
+Proof.
+Intros x y; Unfold Zle_bool Zle Zgt.
+Case (Zcompare x y); Auto; Discriminate.
+Save.
+
+Lemma Zlt_cases : (x,y:Z)if (Zlt_bool x y) then `x<y` else `x>=y`.
+Proof.
+Intros x y; Unfold Zlt_bool Zlt Zge.
+Case (Zcompare x y); Auto; Discriminate.
+Save.
 
+Lemma Zge_cases : (x,y:Z)if (Zge_bool x y) then `x>=y` else `x<y`.
+Proof.
+Intros x y; Unfold Zge_bool Zge Zlt.
+Case (Zcompare x y); Auto; Discriminate.
+Save.
+
+Lemma Zgt_cases : (x,y:Z)if (Zgt_bool x y) then `x>y` else `x<=y`.
+Proof.
+Intros x y; Unfold Zgt_bool Zgt Zle.
+Case (Zcompare x y); Auto; Discriminate.
+Save.
 
 End numbers.
 
@@ -158,12 +189,13 @@ End iterate.
 
 Section arith.
 
-Lemma ZERO_le_POS : (p:positive) `0 <= (POS p)`.
-Intro; Unfold Zle; Unfold Zcompare; Discriminate.
+Lemma POS_gt_ZERO : (p:positive) `(POS p) > 0`.
+Unfold Zgt; Trivial.
 Save.
 
-Lemma POS_gt_ZERO : (p:positive) `(POS p) > 0`.
-Intro; Unfold Zgt; Simpl; Trivial with arith.
+(* weaker but useful (in [Zpower] for instance) *)
+Lemma ZERO_le_POS : (p:positive) `0 <= (POS p)`.
+Intro; Unfold Zle; Unfold Zcompare; Discriminate.
 Save.
 
 Lemma Zlt_ZERO_pred_le_ZERO : (x:Z) `0 < x` -> `0 <= (Zpred x)`.
@@ -174,6 +206,11 @@ Apply Zlt_gt.
 Assumption.
 Save.
 
+Lemma NEG_lt_ZERO : (p:positive)`(NEG p) < 0`.
+Unfold Zlt; Trivial.
+Save.
+
+
 (** [Zeven], [Zodd], [Zdiv2] and their related properties *)
 
 Definition Zeven := 
@@ -423,9 +460,8 @@ Save.
 
 Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y).
 Proof.
-  Unfold Zle_bool Zle. Intros x y. Unfold not. Case (Zcompare x y). Intros. Discriminate H0.
-  Intros. Discriminate H0.
-  Intro. Discriminate H.
+  Unfold Zle_bool Zle. Intros x y. Unfold not. 
+  Case (Zcompare x y); Intros; Discriminate.
 Qed.
 
 Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true.