diff options
Diffstat (limited to 'theories/Numbers/Integer/TreeMod/ZTreeMod.v')
| -rw-r--r-- | theories/Numbers/Integer/TreeMod/ZTreeMod.v | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v index 7479868e9..2d63a22fa 100644 --- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v +++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v @@ -16,7 +16,7 @@ Notation Local wB := (base w_op.(znz_digits)). Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99). -Definition NZE (n m : NZ) := [| n |] = [| m |]. +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). @@ -24,51 +24,51 @@ Definition NZplus := w_op.(znz_add). Definition NZminus := w_op.(znz_sub). Definition NZtimes := w_op.(znz_mul). -Theorem NZE_equiv : equiv NZ NZE. +Theorem NZE_equiv : equiv NZ NZeq. Proof. -unfold equiv, reflexive, symmetric, transitive, NZE; repeat split; intros; auto. +unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto. now transitivity [| y |]. Qed. -Add Relation NZ NZE +Add Relation NZ NZeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Proof. -unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. +unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. Qed. -Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Proof. -unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. +unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. Qed. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. Proof. -unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). now rewrite H1, H2. Qed. -Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. +Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. Proof. -unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). now rewrite H1, H2. Qed. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. Proof. -unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). now rewrite H1, H2. Qed. Delimit Scope IntScope with Int. Bind Scope IntScope with NZ. Open Local Scope IntScope. -Notation "x == y" := (NZE x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ NZE x y) (at level 70) : 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'" := NZsucc : IntScope. Notation "'P'" := NZpred : IntScope. @@ -110,14 +110,14 @@ Qed. Theorem NZpred_succ : forall n : NZ, P (S n) == n. Proof. -intro n; unfold NZsucc, NZpred, NZE. rewrite w_spec.(spec_pred), w_spec.(spec_succ). +intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ). rewrite <- NZpred_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. Proof. -unfold NZE, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct. +unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct. symmetry; apply w_spec.(spec_0). exact w_spec. split; [auto with zarith |apply gt_wB_0]. Qed. @@ -125,11 +125,11 @@ Qed. Section Induction. Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZE A. +Hypothesis A_wd : predicate_wd NZeq 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 NZE ==> iff as A_morph. +Add Morphism A with signature NZeq ==> iff as A_morph. Proof A_wd. Let B (n : Z) := A (Z_to_NZ n). @@ -143,8 +143,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 NZE. assumption. -unfold NZE. rewrite w_spec.(spec_succ). +setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZeq. assumption. +unfold NZeq. rewrite w_spec.(spec_succ). unfold NZ_to_Z, Z_to_NZ. do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]). symmetry; apply Zmod_def_small; auto with zarith. @@ -159,9 +159,9 @@ Qed. Theorem NZinduction : forall n : NZ, A n. Proof. -intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZE. +intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq. apply B_holds. apply w_spec.(spec_to_Z). -unfold NZE, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. +unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. reflexivity. exact w_spec. apply w_spec.(spec_to_Z). @@ -171,13 +171,13 @@ End Induction. Theorem NZplus_0_l : forall n : NZ, 0 + n == n. Proof. -intro n; unfold NZplus, NZ0, NZE. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). +intro n; unfold NZplus, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). rewrite Zplus_0_l. rewrite Zmod_def_small; [reflexivity | apply w_spec.(spec_to_Z)]. Qed. Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). Proof. -intros n m; unfold NZplus, NZsucc, NZE. rewrite w_spec.(spec_add). +intros n m; unfold NZplus, 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. rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l; [ |apply gt_wB_0]. @@ -186,13 +186,13 @@ Qed. Theorem NZminus_0_r : forall n : NZ, n - 0 == n. Proof. -intro n; unfold NZminus, NZ0, NZE. rewrite w_spec.(spec_sub). +intro n; unfold NZminus, NZ0, NZeq. rewrite w_spec.(spec_sub). rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). Proof. -intros n m; unfold NZminus, NZsucc, NZpred, NZE. +intros n m; unfold NZminus, 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; [ | apply gt_wB_0]. rewrite Zminus_mod_idemp_l; [ | apply gt_wB_0]. @@ -201,13 +201,13 @@ Qed. Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0. Proof. -intro n; unfold NZtimes, NZ0, NZ, NZE. rewrite w_spec.(spec_mul). +intro n; unfold NZtimes, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul). rewrite w_spec.(spec_0). now rewrite Zmult_0_r. Qed. Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. Proof. -intros n m; unfold NZtimes, NZsucc, NZplus, NZE. rewrite w_spec.(spec_mul). +intros n m; unfold NZtimes, NZsucc, NZplus, NZeq. rewrite w_spec.(spec_mul). rewrite w_spec.(spec_add). rewrite w_spec.(spec_mul). rewrite w_spec.(spec_succ). rewrite Zplus_mod_idemp_l; [ | apply gt_wB_0]. rewrite Zmult_mod_idemp_r; [ | apply gt_wB_0]. rewrite Zmult_plus_distr_r. now rewrite Zmult_1_r. |