diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 173 |
1 files changed, 77 insertions, 96 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index fb3f0cef..517e48ad 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NZCyclic.v 11238 2008-07-19 09:34:03Z herbelin $ i*) +(*i $Id$ i*) Require Export NZAxioms. Require Import BigNumPrelude. @@ -17,89 +17,79 @@ Require Import CyclicAxioms. (** * From [CyclicType] to [NZAxiomsSig] *) -(** A [Z/nZ] representation given by a module type [CyclicType] - implements [NZAxiomsSig], e.g. the common properties between - N and Z with no ordering. Notice that the [n] in [Z/nZ] is +(** A [Z/nZ] representation given by a module type [CyclicType] + implements [NZAxiomsSig], e.g. the common properties between + N and Z with no ordering. Notice that the [n] in [Z/nZ] is a power of 2. *) Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig. -Open Local Scope Z_scope. +Local Open Scope Z_scope. -Definition NZ := w. +Definition t := w. -Definition NZ_to_Z : NZ -> Z := znz_to_Z w_op. -Definition Z_to_NZ : Z -> NZ := znz_of_Z w_op. -Notation Local wB := (base w_op.(znz_digits)). +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)). -Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99). +Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99). -Definition NZeq (n m : NZ) := [| n |] = [| m |]. -Definition NZ0 := w_op.(znz_0). -Definition NZsucc := w_op.(znz_succ). -Definition NZpred := w_op.(znz_pred). -Definition NZadd := w_op.(znz_add). -Definition NZsub := w_op.(znz_sub). -Definition NZmul := w_op.(znz_mul). +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). -Theorem NZeq_equiv : equiv NZ NZeq. -Proof. -unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto. -now transitivity [| y |]. -Qed. +Local Infix "==" := eq (at level 70). +Local Notation "0" := zero. +Local Notation S := succ. +Local Notation P := pred. +Local Infix "+" := add. +Local Infix "-" := sub. +Local Infix "*" := mul. -Add Relation NZ NZeq - reflexivity proved by (proj1 NZeq_equiv) - symmetry proved by (proj2 (proj2 NZeq_equiv)) - transitivity proved by (proj1 (proj2 NZeq_equiv)) -as NZeq_rel. +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. -Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Instance eq_equiv : Equivalence eq. Proof. -unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. +unfold eq. firstorder. Qed. -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Instance succ_wd : Proper (eq ==> eq) succ. Proof. -unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. +wcongruence. Qed. -Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Instance pred_wd : Proper (eq ==> eq) pred. Proof. -unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). -now rewrite H1, H2. +wcongruence. Qed. -Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Instance add_wd : Proper (eq ==> eq ==> eq) add. Proof. -unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). -now rewrite H1, H2. +wcongruence. Qed. -Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Instance sub_wd : Proper (eq ==> eq ==> eq) sub. Proof. -unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). -now rewrite H1, H2. +wcongruence. Qed. -Delimit Scope IntScope with Int. -Bind Scope IntScope with NZ. -Open Local Scope IntScope. -Notation "x == y" := (NZeq x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. -Notation "0" := NZ0 : IntScope. -Notation S x := (NZsucc x). -Notation P x := (NZpred x). -(*Notation "1" := (S 0) : IntScope.*) -Notation "x + y" := (NZadd x y) : IntScope. -Notation "x - y" := (NZsub x y) : IntScope. -Notation "x * y" := (NZmul x y) : IntScope. +Instance mul_wd : Proper (eq ==> eq ==> eq) mul. +Proof. +wcongruence. +Qed. 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 Zlt; auto with zarith. Qed. Theorem gt_wB_0 : 0 < wB. @@ -107,7 +97,7 @@ Proof. pose proof gt_wB_1; auto with zarith. Qed. -Lemma NZsucc_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB. +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. @@ -115,7 +105,7 @@ reflexivity. now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]]. Qed. -Lemma NZpred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB. +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. @@ -123,34 +113,32 @@ reflexivity. now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]]. Qed. -Lemma NZ_to_Z_mod : forall n : NZ, [| n |] mod wB = [| n |]. +Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |]. Proof. intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z). Qed. -Theorem NZpred_succ : forall n : NZ, P (S n) == n. +Theorem pred_succ : forall n, P (S n) == n. Proof. -intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ). -rewrite <- NZpred_mod_wB. +intro n. wsimpl. +rewrite <- pred_mod_wB. replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod. Qed. -Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int. +Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0. Proof. -unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct. -symmetry; apply w_spec.(spec_0). +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]. Qed. Section Induction. -Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZeq A. +Variable A : t -> Prop. +Hypothesis A_wd : Proper (eq ==> iff) A. Hypothesis A0 : A 0. -Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *) - -Add Morphism A with signature NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. +Hypothesis AS : forall n, A n <-> A (S n). + (* Below, we use only -> direction *) Let B (n : Z) := A (Z_to_NZ n). @@ -163,8 +151,8 @@ 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)) using relation NZeq. assumption. -unfold NZeq. rewrite w_spec.(spec_succ). +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]). symmetry; apply Zmod_small; auto with zarith. @@ -177,11 +165,11 @@ apply Zbounded_induction with wB. apply B0. apply BS. assumption. assumption. Qed. -Theorem NZinduction : forall n : NZ, A n. +Theorem bi_induction : forall n, A n. Proof. -intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq. +intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)). apply B_holds. apply w_spec.(spec_to_Z). -unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. +unfold eq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. reflexivity. exact w_spec. apply w_spec.(spec_to_Z). @@ -189,47 +177,40 @@ Qed. End Induction. -Theorem NZadd_0_l : forall n : NZ, 0 + n == n. +Theorem add_0_l : forall n, 0 + n == n. Proof. -intro n; unfold NZadd, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). +intro n. wsimpl. rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)]. Qed. -Theorem NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). +Theorem add_succ_l : forall n m, (S n) + m == S (n + m). Proof. -intros n m; unfold NZadd, NZsucc, NZeq. rewrite w_spec.(spec_add). -do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add). -rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. +intros n m. wsimpl. +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. Qed. -Theorem NZsub_0_r : forall n : NZ, n - 0 == n. +Theorem sub_0_r : forall n, n - 0 == n. Proof. -intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub). -rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. +intro n. wsimpl. rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. -Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Theorem sub_succ_r : forall n m, n - (S m) == P (n - m). Proof. -intros n m; unfold NZsub, NZsucc, NZpred, NZeq. -rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). -rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r. -rewrite Zminus_mod_idemp_l. -now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith. +intros n m. wsimpl. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l. +now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z + by auto with zarith. Qed. -Theorem NZmul_0_l : forall n : NZ, 0 * n == 0. +Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intro n; unfold NZmul, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul). -rewrite w_spec.(spec_0). now rewrite Zmult_0_l. +intro n. wsimpl. now rewrite Zmult_0_l. Qed. -Theorem NZmul_succ_l : forall n m : NZ, (S n) * m == n * m + m. +Theorem mul_succ_l : forall n m, (S n) * m == n * m + m. Proof. -intros n m; unfold NZmul, NZsucc, NZadd, NZeq. rewrite w_spec.(spec_mul). -rewrite w_spec.(spec_add), w_spec.(spec_mul), w_spec.(spec_succ). -rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. +intros n m. wsimpl. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. now rewrite Zmult_plus_distr_l, Zmult_1_l. Qed. |