aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-28 23:29:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-28 23:29:59 +0000
commit2941378aee6586bcff9f8a117f11e5c5c2327607 (patch)
tree9bb45db9aa55e2a63ddd7c8b700a0a99277b67eb /theories/Numbers
parent0f96f620f5ca1ccf02439bb868d223ae4aa9f2d2 (diff)
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
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivFloor.v2
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v26
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v20
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.