diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 141 |
1 files changed, 62 insertions, 79 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 92215ba9..c52cbe10 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-2010 *) (* \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,41 +47,25 @@ 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. @@ -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,25 +150,23 @@ 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 Zplus_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. @@ -193,25 +174,27 @@ 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 Zminus_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. +intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. now rewrite Zmult_plus_distr_l, Zmult_1_l. Qed. +Definition t := t. + End NZCyclicAxiomsMod. |