Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of Zdiv

Some details: 

 - ZAux.v is the only file left in Ints/Z. The few elements that remain in it
   are rather specific or compatibility oriented. Others parts and files have 
   been either deleted when unused or pushed into some place of ZArith. 
 - Ints/List/ is removed since it was not needed anymore
 - Ints/Tactic.v disappear: some of its tactic were unused, some already in 
   Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict 
   has been added to Tactics.v
 - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
 - A new file Zpow_facts inherits lots of results about Zpower. Placing them 
   into Zpower would have been difficult with respect to compatibility 
   (import of ring)
 - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
 - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) 
 
Now, concerning Zdiv, the behavior when dividing by a negative number is now 
fully proved. When this was possible, existing lemmas has been extended, 
either from strictly positive to non-zero divisor, or even to arbitrary 
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained 
for compatibility. Several lemmas now have shorter proofs (based on unicity 
lemmas). Lemmas are now more or less organized by themes (division and order, 
division and usual operations, etc). Three possible choices of spec for 
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp 
with the current choice of Zdiv/Zmod is now fully covered. A embryo of 
division "a la Ocaml" is given: Odiv and Omod. 




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

1 files changed, 15 insertions, 16 deletions

diff --git a/theories/Ints/num/GenDivn1.v b/theories/Ints/num/GenDivn1.v
index 84bf247f7..7987741da 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Ints/num/GenDivn1.v
@@ -9,8 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import ZDivModAux.
-Require Import ZPowerAux.
+Require Import ZAux.
 Require Import Basic_type.
 Require Import GenBase.
 
@@ -230,7 +229,7 @@ Section GENDIVN1.
      with (2*Zpos (gen_digits w_digits n));auto with zarith.
    replace (2 ^ (Zpos (gen_digits w_digits (S n)) - [|p|])) with
     (2^(Zpos (gen_digits w_digits n) - [|p|])*2^Zpos (gen_digits w_digits n)).
-   rewrite Zdiv_Zmult_compat_r;auto with zarith.
+   rewrite Zdiv_mult_cancel_r;auto with zarith.
    rewrite Zmult_plus_distr_l with (p:=  2^[|p|]). 
    pattern  ([!n|hl!] * 2^[|p|]) at 2;
    rewrite (shift_unshift_mod (Zpos(gen_digits w_digits n))([|p|])([!n|hl!]));
@@ -254,7 +253,7 @@ Section GENDIVN1.
    with (2^Zpos(gen_digits w_digits n) *2^Zpos(gen_digits w_digits n)). 
    rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] +
       [!n|hl!] / 2 ^ (Zpos (gen_digits w_digits n) - [|p|])))).
-   rewrite  Zmod_Zmult_compat_l;auto with zarith.
+   rewrite  Zmult_mod_distr_l;auto with zarith.
    ring. 
    rewrite Zpower_exp;auto with zarith.
    assert (0 < Zpos (gen_digits w_digits n)). unfold Zlt;reflexivity.
@@ -336,7 +335,7 @@ Section GENDIVN1.
   replace (2 ^ (Zpos (gen_digits w_digits (S n)) - Zpos w_digits)) with
    (2^(Zpos (gen_digits w_digits n) - Zpos w_digits) * 
         2^Zpos (gen_digits w_digits n)).
-  rewrite Zdiv_Zmult_compat_r;auto with zarith.
+  rewrite Zdiv_mult_cancel_r;auto with zarith.
   rewrite <- Zpower_exp;auto with zarith.
   replace (Zpos (gen_digits w_digits n) - Zpos w_digits + 
     Zpos (gen_digits w_digits n)) with
@@ -373,7 +372,7 @@ Section GENDIVN1.
    generalize (spec_compare (w_head0 b) w_0); case w_compare;
      rewrite spec_0; intros H2; auto with zarith.
    assert (Hv1: wB/2 <= [|b|]).
-     generalize H0; rewrite H2; rewrite Zpower_exp_0;
+     generalize H0; rewrite H2; rewrite Zpower_0_r;
        rewrite Zmult_1_l; auto.
    assert (Hv2: [|w_0|] < [|b|]).
      rewrite spec_0; auto.
@@ -394,7 +393,7 @@ Section GENDIVN1.
     rewrite (spec_add_mul_div b w_0); auto with zarith.
     rewrite spec_0;rewrite Zdiv_0_l; try omega.
     rewrite Zplus_0_r; rewrite Zmult_comm.
-    rewrite Zmod_def_small; auto with zarith.
+    rewrite Zmod_small; auto with zarith.
    assert (H5 := spec_to_Z (high n a)).
    assert 
     ([|w_add_mul_div (w_head0 b) w_0 (high n a)|]
@@ -407,15 +406,15 @@ Section GENDIVN1.
      apply Zlt_le_trans with wB;auto with zarith.
      pattern wB at 1;replace wB with (wB*1);try ring.
      apply Zmult_le_compat;auto with zarith.
-     assert (H6 := Zpower_lt_0 2 (Zpos w_digits - [|w_head0 b|]));
+     assert (H6 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|]));
        auto with zarith.
-    rewrite Zmod_def_small;auto with zarith.
+    rewrite Zmod_small;auto with zarith.
     apply Zdiv_lt_upper_bound;auto with zarith.
     apply Zlt_le_trans with wB;auto with zarith.
     apply Zle_trans with (2 ^ [|w_head0 b|] * [|b|] * 2).
     rewrite <- wB_div_2; try omega.
     apply Zmult_le_compat;auto with zarith.
-    pattern 2 at 1;rewrite <- Zpower_exp_1.
+    pattern 2 at 1;rewrite <- Zpower_1_r.
     apply Zpower_le_monotone;split;auto with zarith.
    rewrite <- H4 in H0. 
    assert (Hb3: [|w_head0 b|] <= Zpos w_digits); auto with zarith. 
@@ -430,13 +429,13 @@ Section GENDIVN1.
    rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7.
    assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB
      = [!n|a!] / 2^(Zpos (gen_digits w_digits n) - [|w_head0 b|])).
-   rewrite Zmod_def_small;auto with zarith.
+   rewrite Zmod_small;auto with zarith.
    rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith.
    rewrite <- Zpower_exp;auto with zarith.
    replace (Zpos (gen_digits w_digits n) - Zpos w_digits + 
                        (Zpos w_digits - [|w_head0 b|]))
     with (Zpos (gen_digits w_digits n) - [|w_head0 b|]);trivial;ring.
-   assert (H8 := Zpower_lt_0 2  (Zpos w_digits - [|w_head0 b|]));auto with zarith.
+   assert (H8 := Zpower_gt_0 2  (Zpos w_digits - [|w_head0 b|]));auto with zarith.
    split;auto with zarith.
    apply Zle_lt_trans with ([|high n a|]);auto with zarith.
    apply Zdiv_le_upper_bound;auto with zarith.
@@ -451,20 +450,20 @@ Section GENDIVN1.
    rewrite spec_0;rewrite Zmult_0_l;rewrite Zplus_0_l.
    replace (Zpos w_digits - [|w_sub w_zdigits (w_head0 b)|]) 
       with ([|w_head0 b|]).
-   rewrite Zmod_def_small;auto with zarith.
+   rewrite Zmod_small;auto with zarith.
    assert (H9 := spec_to_Z r).
    split;auto with zarith.
    apply Zle_lt_trans with ([|r|]);auto with zarith.
    apply Zdiv_le_upper_bound;auto with zarith.
    pattern ([|r|]) at 1;rewrite <- Zmult_1_r.
    apply Zmult_le_compat;auto with zarith.
-   assert (H10 := Zpower_lt_0 2  ([|w_head0 b|]));auto with zarith.
+   assert (H10 := Zpower_gt_0 2  ([|w_head0 b|]));auto with zarith.
    rewrite spec_sub.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    case (spec_to_Z w_zdigits); auto with zarith.
    rewrite spec_sub.
-   rewrite Zmod_def_small; auto with zarith.
+   rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    case (spec_to_Z w_zdigits); auto with zarith.
   case H7; intros H71 H72.