1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Require Export NZAxioms.
Require Import BigNumPrelude.
Require Import DoubleType.
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 power of 2.
*)
Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
Open Local Scope Z_scope.
Definition NZ := 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)).
Notation Local "[| 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).
Theorem NZeq_equiv : equiv NZ NZeq.
Proof.
unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto.
now transitivity [| y |].
Qed.
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.
Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
Proof.
unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
Qed.
Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
Proof.
unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
Qed.
Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
Proof.
unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
now rewrite H1, H2.
Qed.
Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
Proof.
unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
now rewrite H1, H2.
Qed.
Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
Proof.
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" := (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.
Theorem gt_wB_1 : 1 < wB.
Proof.
unfold base.
apply Zpower_gt_1; unfold Zlt; auto with zarith.
Qed.
Theorem gt_wB_0 : 0 < wB.
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.
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]].
Qed.
Lemma NZpred_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]].
Qed.
Lemma NZ_to_Z_mod : forall n : NZ, [| 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.
Proof.
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 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.
Section Induction.
Variable A : NZ -> Prop.
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 NZeq ==> iff as A_morph.
Proof. apply A_wd. Qed.
Let B (n : Z) := A (Z_to_NZ n).
Lemma B0 : B 0.
Proof.
unfold B. now rewrite Z_to_NZ_0.
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)) 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_small; auto with zarith.
Qed.
Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.
Proof.
intros n [H1 H2].
apply Zbounded_induction with wB.
apply B0. apply BS. assumption. assumption.
Qed.
Theorem NZinduction : forall n : NZ, A n.
Proof.
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 NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
reflexivity.
exact w_spec.
apply w_spec.(spec_to_Z).
Qed.
End Induction.
Theorem NZadd_0_l : forall n : NZ, 0 + n == n.
Proof.
intro n; unfold NZadd, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
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).
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.
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.
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.
Qed.
Theorem NZsub_succ_r : forall n m : NZ, 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.
Qed.
Theorem NZmul_0_l : forall n : NZ, 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.
Qed.
Theorem NZmul_succ_l : forall n m : NZ, (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.
now rewrite Zmult_plus_distr_l, Zmult_1_l.
Qed.
End NZCyclicAxiomsMod.
|
