← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Numbers/Cyclic/Abstract/NZCyclic.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Numbers/Cyclic/Abstract/NZCyclic.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
(*                      Evgeny Makarov, INRIA, 2007                     *)
 
9
(************************************************************************)
 
10
 
 
11
(*i $Id: NZCyclic.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
 
12
 
 
13
Require Export NZAxioms.
 
14
Require Import BigNumPrelude.
 
15
Require Import DoubleType.
 
16
Require Import CyclicAxioms.
 
17
 
 
18
(** * From [CyclicType] to [NZAxiomsSig] *)
 
19
 
 
20
(** A [Z/nZ] representation given by a module type [CyclicType] 
 
21
    implements [NZAxiomsSig], e.g. the common properties between 
 
22
    N and Z with no ordering. Notice that the [n] in [Z/nZ] is 
 
23
    a power of 2.
 
24
*)
 
25
 
 
26
Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
 
27
 
 
28
Open Local Scope Z_scope.
 
29
 
 
30
Definition NZ := w.
 
31
 
 
32
Definition NZ_to_Z : NZ -> Z := znz_to_Z w_op.
 
33
Definition Z_to_NZ : Z -> NZ := znz_of_Z w_op.
 
34
Notation Local wB := (base w_op.(znz_digits)).
 
35
 
 
36
Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
 
37
 
 
38
Definition NZeq (n m : NZ) := [| n |] = [| m |].
 
39
Definition NZ0 := w_op.(znz_0).
 
40
Definition NZsucc := w_op.(znz_succ).
 
41
Definition NZpred := w_op.(znz_pred).
 
42
Definition NZadd := w_op.(znz_add).
 
43
Definition NZsub := w_op.(znz_sub).
 
44
Definition NZmul := w_op.(znz_mul).
 
45
 
 
46
Theorem NZeq_equiv : equiv NZ NZeq.
 
47
Proof.
 
48
unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto.
 
49
now transitivity [| y |].
 
50
Qed.
 
51
 
 
52
Add Relation NZ NZeq
 
53
 reflexivity proved by (proj1 NZeq_equiv)
 
54
 symmetry proved by (proj2 (proj2 NZeq_equiv))
 
55
 transitivity proved by (proj1 (proj2 NZeq_equiv))
 
56
as NZeq_rel.
 
57
 
 
58
Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 
59
Proof.
 
60
unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
 
61
Qed.
 
62
 
 
63
Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
 
64
Proof.
 
65
unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
 
66
Qed.
 
67
 
 
68
Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
 
69
Proof.
 
70
unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
 
71
now rewrite H1, H2.
 
72
Qed.
 
73
 
 
74
Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
 
75
Proof.
 
76
unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
 
77
now rewrite H1, H2.
 
78
Qed.
 
79
 
 
80
Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
 
81
Proof.
 
82
unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
 
83
now rewrite H1, H2.
 
84
Qed.
 
85
 
 
86
Delimit Scope IntScope with Int.
 
87
Bind Scope IntScope with NZ.
 
88
Open Local Scope IntScope.
 
89
Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
 
90
Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 
91
Notation "0" := NZ0 : IntScope.
 
92
Notation S x := (NZsucc x).
 
93
Notation P x := (NZpred x).
 
94
(*Notation "1" := (S 0) : IntScope.*)
 
95
Notation "x + y" := (NZadd x y) : IntScope.
 
96
Notation "x - y" := (NZsub x y) : IntScope.
 
97
Notation "x * y" := (NZmul x y) : IntScope.
 
98
 
 
99
Theorem gt_wB_1 : 1 < wB.
 
100
Proof.
 
101
unfold base. 
 
102
apply Zpower_gt_1; unfold Zlt; auto with zarith.
 
103
Qed.
 
104
 
 
105
Theorem gt_wB_0 : 0 < wB.
 
106
Proof.
 
107
pose proof gt_wB_1; auto with zarith.
 
108
Qed.
 
109
 
 
110
Lemma NZsucc_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
 
111
Proof.
 
112
intro n.
 
113
pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod.
 
114
reflexivity.
 
115
now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
 
116
Qed.
 
117
 
 
118
Lemma NZpred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
 
119
Proof.
 
120
intro n.
 
121
pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod.
 
122
reflexivity.
 
123
now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
 
124
Qed.
 
125
 
 
126
Lemma NZ_to_Z_mod : forall n : NZ, [| n |] mod wB = [| n |].
 
127
Proof.
 
128
intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z).
 
129
Qed.
 
130
 
 
131
Theorem NZpred_succ : forall n : NZ, P (S n) == n.
 
132
Proof.
 
133
intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ).
 
134
rewrite <- NZpred_mod_wB.
 
135
replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
 
136
Qed.
 
137
 
 
138
Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int.
 
139
Proof.
 
140
unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct.
 
141
symmetry; apply w_spec.(spec_0).
 
142
exact w_spec. split; [auto with zarith |apply gt_wB_0].
 
143
Qed.
 
144
 
 
145
Section Induction.
 
146
 
 
147
Variable A : NZ -> Prop.
 
148
Hypothesis A_wd : predicate_wd NZeq A.
 
149
Hypothesis A0 : A 0.
 
150
Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
 
151
 
 
152
Add Morphism A with signature NZeq ==> iff as A_morph.
 
153
Proof. apply A_wd. Qed.
 
154
 
 
155
Let B (n : Z) := A (Z_to_NZ n).
 
156
 
 
157
Lemma B0 : B 0.
 
158
Proof.
 
159
unfold B. now rewrite Z_to_NZ_0.
 
160
Qed.
 
161
 
 
162
Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
 
163
Proof.
 
164
intros n H1 H2 H3.
 
165
unfold B in *. apply -> AS in H3.
 
166
setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZeq. assumption.
 
167
unfold NZeq. rewrite w_spec.(spec_succ).
 
168
unfold NZ_to_Z, Z_to_NZ.
 
169
do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]).
 
170
symmetry; apply Zmod_small; auto with zarith.
 
171
Qed.
 
172
 
 
173
Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.
 
174
Proof.
 
175
intros n [H1 H2].
 
176
apply Zbounded_induction with wB.
 
177
apply B0. apply BS. assumption. assumption.
 
178
Qed.
 
179
 
 
180
Theorem NZinduction : forall n : NZ, A n.
 
181
Proof.
 
182
intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq.
 
183
apply B_holds. apply w_spec.(spec_to_Z).
 
184
unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
 
185
reflexivity.
 
186
exact w_spec.
 
187
apply w_spec.(spec_to_Z).
 
188
Qed.
 
189
 
 
190
End Induction.
 
191
 
 
192
Theorem NZadd_0_l : forall n : NZ, 0 + n == n.
 
193
Proof.
 
194
intro n; unfold NZadd, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
 
195
rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)].
 
196
Qed.
 
197
 
 
198
Theorem NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 
199
Proof.
 
200
intros n m; unfold NZadd, NZsucc, NZeq. rewrite w_spec.(spec_add).
 
201
do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add).
 
202
rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
 
203
rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l.
 
204
rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc.
 
205
Qed.
 
206
 
 
207
Theorem NZsub_0_r : forall n : NZ, n - 0 == n.
 
208
Proof.
 
209
intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub).
 
210
rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod.
 
211
Qed.
 
212
 
 
213
Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m).
 
214
Proof.
 
215
intros n m; unfold NZsub, NZsucc, NZpred, NZeq.
 
216
rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub).
 
217
rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r.
 
218
rewrite Zminus_mod_idemp_l.
 
219
now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith.
 
220
Qed.
 
221
 
 
222
Theorem NZmul_0_l : forall n : NZ, 0 * n == 0.
 
223
Proof.
 
224
intro n; unfold NZmul, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul).
 
225
rewrite w_spec.(spec_0). now rewrite Zmult_0_l.
 
226
Qed.
 
227
 
 
228
Theorem NZmul_succ_l : forall n m : NZ, (S n) * m == n * m + m.
 
229
Proof.
 
230
intros n m; unfold NZmul, NZsucc, NZadd, NZeq. rewrite w_spec.(spec_mul).
 
231
rewrite w_spec.(spec_add), w_spec.(spec_mul), w_spec.(spec_succ).
 
232
rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
 
233
now rewrite Zmult_plus_distr_l, Zmult_1_l.
 
234
Qed.
 
235
 
 
236
End NZCyclicAxiomsMod.