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, 10 insertions, 12 deletions

diff --git a/theories/Ints/num/GenBase.v b/theories/Ints/num/GenBase.v
index 6b6376b69..a9936f1dd 100644
--- a/theories/Ints/num/GenBase.v
+++ b/theories/Ints/num/GenBase.v
@@ -10,8 +10,6 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import ZAux.
-Require Import ZDivModAux.
-Require Import ZPowerAux.
 Require Import Basic_type.
 Require Import JMeq.
 
@@ -188,7 +186,7 @@ Section GenBase.
 
   Lemma lt_0_wB : 0 < wB.
   Proof. 
-   unfold base;apply Zpower_lt_0. unfold Zlt;reflexivity.
+   unfold base;apply Zpower_gt_0. unfold Zlt;reflexivity.
    unfold Zle;intros H;discriminate H.
   Qed.
 
@@ -208,7 +206,7 @@ Section GenBase.
   Proof.
    assert (H:= wB_pos);rewrite wwB_wBwB;rewrite <-(Zmult_1_r 1).
    rewrite Zpower_2.
-   apply Zmult_lt_compat;(split;[unfold Zlt;reflexivity|trivial]).
+   apply Zmult_lt_compat2;(split;[unfold Zlt;reflexivity|trivial]).
    apply Zlt_le_weak;trivial. 
   Qed.
 
@@ -217,11 +215,11 @@ Section GenBase.
    clear spec_w_0 w_0 spec_w_1 w_1 spec_w_Bm1 w_Bm1 spec_w_WW spec_w_0W 
     spec_to_Z;unfold base.
    assert (2 ^ Zpos w_digits = 2 * (2 ^ (Zpos w_digits - 1))).
-   pattern 2 at 2; rewrite <- Zpower_exp_1.
+   pattern 2 at 2; rewrite <- Zpower_1_r.
    rewrite <- Zpower_exp; auto with zarith.
-   eq_tac; auto with zarith.
+   f_equal; auto with zarith.
    case w_digits; compute; intros; discriminate.
-   rewrite H; eq_tac; auto with zarith.
+   rewrite H; f_equal; auto with zarith.
    rewrite Zmult_comm; apply Z_div_mult; auto with zarith.
   Qed.
 
@@ -239,17 +237,17 @@ Section GenBase.
    (z*wB + [|x|]) mod wwB = (z mod wB)*wB + [|x|].
   Proof.
    intros z x.
-   rewrite Zmod_plus. 2:apply lt_0_wwB.
+   rewrite Zplus_mod. 
    pattern wwB at 1;rewrite wwB_wBwB; rewrite Zpower_2.
    rewrite Zmult_mod_distr_r;try apply lt_0_wB.
-   rewrite (Zmod_def_small [|x|]).
-   apply Zmod_def_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z.
+   rewrite (Zmod_small [|x|]).
+   apply Zmod_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z.
    apply Z_mod_lt;apply Zlt_gt;apply lt_0_wB.
    destruct (spec_to_Z x);split;trivial.
    change [|x|] with (0*wB+[|x|]). rewrite wwB_wBwB.
    rewrite Zpower_2;rewrite <- (Zplus_0_r (wB*wB));apply beta_lex_inv.
    apply lt_0_wB. apply spec_to_Z. split;[apply Zle_refl | apply lt_0_wB].
-  Qed.
+ Qed.
 
   Lemma wB_div : forall x y, ([|x|] * wB + [|y|]) / wB = [|x|].
   Proof.
@@ -321,7 +319,7 @@ Section GenBase.
   apply Zmult_le_compat; auto with zarith.
   apply Zle_trans with wB; auto with zarith.
   unfold base.
-  rewrite <- (ZAux.Zpower_exp_0 2).
+  rewrite <- (Zpower_0_r 2).
   apply Zpower_le_monotone2; auto with zarith.
   unfold base; auto with zarith.
   Qed.