Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def

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

3 files changed, 27 insertions, 21 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index f19baf4d1..0e54c453b 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -88,7 +88,7 @@ Theorem div_unique_pos:
 Proof. intros; apply div_unique with r; auto. Qed.
 
 Theorem div_unique_neg:
- forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b.
+ forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b.
 Proof. intros; apply div_unique with r; auto. Qed.
 
 Theorem mod_unique:
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 8e53e4d62..173a8f177 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Zquot.
+Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import NSig.
 Require Import ZSig.
@@ -503,22 +503,28 @@ Module Make (N:NType) <: ZType.
 
  Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
  Proof.
-  intros [x|x] [y|y]; simpl; symmetry;
-   rewrite N.spec_div, ?Zquot_opp_r, ?Zquot_opp_l, ?Zopp_involutive;
-   rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
+  intros [x|x] [y|y]; simpl; symmetry; rewrite N.spec_div;
+  (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *)
+  destruct (Z.eq_dec (N.to_Z y) 0) as [EQ|NEQ];
+    try (rewrite EQ; now destruct (N.to_Z x));
+  rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd;
+  trivial; apply Z.quot_div_nonneg;
+   generalize (N.spec_pos x) (N.spec_pos y); Z.order.
  Qed.
 
  Lemma spec_rem : forall x y,
-   to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
+   to_Z (rem x y) = Z.rem (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold rem. rewrite spec_eqb, spec_0.
   case Z.eqb_spec; intros Hy.
-  now rewrite Hy, Zrem_0_r.
+  (* Nota: we rely here on [Z.rem a 0 = a] *)
+  rewrite Hy. now destruct (to_Z x).
   destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
-   rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
-   try rewrite Z.eq_opp_l, Z.opp_0 in Hy;
-   rewrite Zrem_Zmod_pos; generalize (N.spec_pos x) (N.spec_pos y);
-   Z.order.
+   rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy;
+   rewrite N.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive,
+    ?Z.opp_inj_wd;
+   trivial; apply Z.rem_mod_nonneg;
+    generalize (N.spec_pos x) (N.spec_pos y); Z.order.
  Qed.
 
  Definition gcd x y :=
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 6facd3c3a..390b52ebe 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -10,7 +10,7 @@ Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
-Module ZTypeIsZAxioms (Import Z : ZType').
+Module ZTypeIsZAxioms (Import ZZ : ZType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
@@ -53,7 +53,7 @@ Qed.
 
 Section Induction.
 
-Variable A : Z.t -> Prop.
+Variable A : ZZ.t -> Prop.
 Hypothesis A_wd : Proper (eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (succ n).
@@ -173,7 +173,7 @@ Proof.
  intros. zify. apply Z.compare_antisym.
 Qed.
 
-Include BoolOrderFacts Z Z Z [no inline].
+Include BoolOrderFacts ZZ ZZ ZZ [no inline].
 
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
@@ -388,23 +388,23 @@ Program Instance rem_wd : Proper (eq==>eq==>eq) rem.
 
 Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b.
 Proof.
-intros a b _. zify. apply Z_quot_rem_eq.
+intros a b. zify. apply Z.quot_rem.
 Qed.
 
 Theorem rem_bound_pos :
  forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b.
 Proof.
-intros a b. zify. intros. now apply Zrem_bound.
+intros a b. zify. apply Z.rem_bound_pos.
 Qed.
 
 Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b).
 Proof.
-intros a b _. zify. apply Zrem_opp_l.
+intros a b. zify. apply Z.rem_opp_l.
 Qed.
 
 Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b.
 Proof.
-intros a b _. zify. apply Zrem_opp_r.
+intros a b. zify. apply Z.rem_opp_r.
 Qed.
 
 (** Gcd *)
@@ -520,6 +520,6 @@ Qed.
 
 End ZTypeIsZAxioms.
 
-Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: OrderFunctions Z <: HasMinMax Z
- := Z <+ ZTypeIsZAxioms.
+Module ZType_ZAxioms (ZZ : ZType)
+ <: ZAxiomsSig <: OrderFunctions ZZ <: HasMinMax ZZ
+ := ZZ <+ ZTypeIsZAxioms.