summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Abstract/NZCyclic.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/Numbers/Cyclic/Abstract/NZCyclic.v
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v149
1 files changed, 66 insertions, 83 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 92215ba9..1d5b78ec 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZCyclic.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export NZAxioms.
Require Import BigNumPrelude.
Require Import DoubleType.
@@ -27,21 +25,19 @@ Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
Local Open Scope Z_scope.
-Definition t := w.
-
-Definition NZ_to_Z : t -> Z := znz_to_Z w_op.
-Definition Z_to_NZ : Z -> t := znz_of_Z w_op.
-Local Notation wB := (base w_op.(znz_digits)).
+Local Notation wB := (base ZnZ.digits).
-Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
+Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).
Definition eq (n m : t) := [| n |] = [| m |].
-Definition zero := w_op.(znz_0).
-Definition succ := w_op.(znz_succ).
-Definition pred := w_op.(znz_pred).
-Definition add := w_op.(znz_add).
-Definition sub := w_op.(znz_sub).
-Definition mul := w_op.(znz_mul).
+Definition zero := ZnZ.zero.
+Definition one := ZnZ.one.
+Definition two := ZnZ.succ ZnZ.one.
+Definition succ := ZnZ.succ.
+Definition pred := ZnZ.pred.
+Definition add := ZnZ.add.
+Definition sub := ZnZ.sub.
+Definition mul := ZnZ.mul.
Local Infix "==" := eq (at level 70).
Local Notation "0" := zero.
@@ -51,45 +47,29 @@ Local Infix "+" := add.
Local Infix "-" := sub.
Local Infix "*" := mul.
-Hint Rewrite w_spec.(spec_0) w_spec.(spec_succ) w_spec.(spec_pred)
- w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_sub) : w.
-Ltac wsimpl :=
- unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w.
-Ltac wcongruence := repeat red; intros; wsimpl; congruence.
+Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred
+ ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic.
+Ltac zify :=
+ unfold eq, zero, one, two, succ, pred, add, sub, mul in *;
+ autorewrite with cyclic.
+Ltac zcongruence := repeat red; intros; zify; congruence.
Instance eq_equiv : Equivalence eq.
Proof.
unfold eq. firstorder.
Qed.
-Instance succ_wd : Proper (eq ==> eq) succ.
-Proof.
-wcongruence.
-Qed.
-
-Instance pred_wd : Proper (eq ==> eq) pred.
-Proof.
-wcongruence.
-Qed.
-
-Instance add_wd : Proper (eq ==> eq ==> eq) add.
-Proof.
-wcongruence.
-Qed.
-
-Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
-Proof.
-wcongruence.
-Qed.
+Local Obligation Tactic := zcongruence.
-Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
-Proof.
-wcongruence.
-Qed.
+Program Instance succ_wd : Proper (eq ==> eq) succ.
+Program Instance pred_wd : Proper (eq ==> eq) pred.
+Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
Theorem gt_wB_1 : 1 < wB.
Proof.
-unfold base. apply Zpower_gt_1; unfold Zlt; auto with zarith.
+unfold base. apply Zpower_gt_1; unfold Z.lt; auto with zarith.
Qed.
Theorem gt_wB_0 : 0 < wB.
@@ -97,39 +77,41 @@ Proof.
pose proof gt_wB_1; auto with zarith.
Qed.
+Lemma one_mod_wB : 1 mod wB = 1.
+Proof.
+rewrite Zmod_small. reflexivity. split. auto with zarith. apply gt_wB_1.
+Qed.
+
Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
Proof.
-intro n.
-pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod.
-reflexivity.
-now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
+intro n. rewrite <- one_mod_wB at 2. now rewrite <- Zplus_mod.
Qed.
Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
Proof.
-intro n.
-pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod.
-reflexivity.
-now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
+intro n. rewrite <- one_mod_wB at 2. now rewrite Zminus_mod.
Qed.
Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].
Proof.
-intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z).
+intro n; rewrite Zmod_small. reflexivity. apply ZnZ.spec_to_Z.
Qed.
Theorem pred_succ : forall n, P (S n) == n.
Proof.
-intro n. wsimpl.
+intro n. zify.
rewrite <- pred_mod_wB.
-replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
+replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod.
Qed.
-Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0.
+Theorem one_succ : one == succ zero.
Proof.
-unfold NZ_to_Z, Z_to_NZ. wsimpl.
-rewrite znz_of_Z_correct; auto.
-exact w_spec. split; [auto with zarith |apply gt_wB_0].
+zify; simpl. now rewrite one_mod_wB.
+Qed.
+
+Theorem two_succ : two == succ one.
+Proof.
+reflexivity.
Qed.
Section Induction.
@@ -140,21 +122,22 @@ Hypothesis A0 : A 0.
Hypothesis AS : forall n, A n <-> A (S n).
(* Below, we use only -> direction *)
-Let B (n : Z) := A (Z_to_NZ n).
+Let B (n : Z) := A (ZnZ.of_Z n).
Lemma B0 : B 0.
Proof.
-unfold B. now rewrite Z_to_NZ_0.
+unfold B.
+setoid_replace (ZnZ.of_Z 0) with zero. assumption.
+red; zify. apply ZnZ.of_Z_correct. auto using gt_wB_0 with zarith.
Qed.
Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
Proof.
intros n H1 H2 H3.
-unfold B in *. apply -> AS in H3.
-setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)). assumption.
-wsimpl.
-unfold NZ_to_Z, Z_to_NZ.
-do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]).
+unfold B in *. apply AS in H3.
+setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption.
+zify.
+rewrite 2 ZnZ.of_Z_correct; auto with zarith.
symmetry; apply Zmod_small; auto with zarith.
Qed.
@@ -167,51 +150,51 @@ Qed.
Theorem bi_induction : forall n, A n.
Proof.
-intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)).
-apply B_holds. apply w_spec.(spec_to_Z).
-unfold eq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
-reflexivity.
-exact w_spec.
-apply w_spec.(spec_to_Z).
+intro n. setoid_replace n with (ZnZ.of_Z (ZnZ.to_Z n)).
+apply B_holds. apply ZnZ.spec_to_Z.
+red. symmetry. apply ZnZ.of_Z_correct.
+apply ZnZ.spec_to_Z.
Qed.
End Induction.
Theorem add_0_l : forall n, 0 + n == n.
Proof.
-intro n. wsimpl.
-rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)].
+intro n. zify.
+rewrite Z.add_0_l. apply Zmod_small. apply ZnZ.spec_to_Z.
Qed.
Theorem add_succ_l : forall n m, (S n) + m == S (n + m).
Proof.
-intros n m. wsimpl.
+intros n m. zify.
rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
-rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l.
-rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc.
+rewrite <- (Z.add_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l.
+rewrite (Z.add_comm 1 [| m |]); now rewrite Z.add_assoc.
Qed.
Theorem sub_0_r : forall n, n - 0 == n.
Proof.
-intro n. wsimpl. rewrite Zminus_0_r. apply NZ_to_Z_mod.
+intro n. zify. rewrite Z.sub_0_r. apply NZ_to_Z_mod.
Qed.
Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).
Proof.
-intros n m. wsimpl. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.
+intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.
now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z
- by auto with zarith.
+ by ring.
Qed.
Theorem mul_0_l : forall n, 0 * n == 0.
Proof.
-intro n. wsimpl. now rewrite Zmult_0_l.
+intro n. now zify.
Qed.
Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.
Proof.
-intros n m. wsimpl. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
-now rewrite Zmult_plus_distr_l, Zmult_1_l.
+intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
+now rewrite Z.mul_add_distr_r, Z.mul_1_l.
Qed.
+Definition t := t.
+
End NZCyclicAxiomsMod.