← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.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/Integer/SpecViaZ/ZSigZAxioms.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
 
 
9
(*i $Id: ZSigZAxioms.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
10
 
 
11
Require Import ZArith.
 
12
Require Import ZAxioms.
 
13
Require Import ZSig.
 
14
 
 
15
(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
16
 
 
17
Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
 
18
 
 
19
Delimit Scope IntScope with Int.
 
20
Bind Scope IntScope with Z.t.
 
21
Open Local Scope IntScope.
 
22
Notation "[ x ]" := (Z.to_Z x) : IntScope.
 
23
Infix "=="  := Z.eq (at level 70) : IntScope.
 
24
Notation "0" := Z.zero : IntScope.
 
25
Infix "+" := Z.add : IntScope.
 
26
Infix "-" := Z.sub : IntScope.
 
27
Infix "*" := Z.mul : IntScope.
 
28
Notation "- x" := (Z.opp x) : IntScope.
 
29
 
 
30
Hint Rewrite 
 
31
 Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
 
32
 Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec.
 
33
 
 
34
Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec.
 
35
 
 
36
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 
37
Module Export NZAxiomsMod <: NZAxiomsSig.
 
38
 
 
39
Definition NZ := Z.t.
 
40
Definition NZeq := Z.eq.
 
41
Definition NZ0 := Z.zero.
 
42
Definition NZsucc := Z.succ.
 
43
Definition NZpred := Z.pred.
 
44
Definition NZadd := Z.add.
 
45
Definition NZsub := Z.sub.
 
46
Definition NZmul := Z.mul.
 
47
 
 
48
Theorem NZeq_equiv : equiv Z.t Z.eq.
 
49
Proof.
 
50
repeat split; repeat red; intros; auto; congruence.
 
51
Qed.
 
52
 
 
53
Add Relation Z.t Z.eq
 
54
 reflexivity proved by (proj1 NZeq_equiv)
 
55
 symmetry proved by (proj2 (proj2 NZeq_equiv))
 
56
 transitivity proved by (proj1 (proj2 NZeq_equiv))
 
57
 as NZeq_rel.
 
58
 
 
59
Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
 
60
Proof.
 
61
intros; zsimpl; f_equal; assumption.
 
62
Qed.
 
63
 
 
64
Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd.
 
65
Proof.
 
66
intros; zsimpl; f_equal; assumption.
 
67
Qed.
 
68
 
 
69
Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd.
 
70
Proof.
 
71
intros; zsimpl; f_equal; assumption.
 
72
Qed.
 
73
 
 
74
Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd.
 
75
Proof.
 
76
intros; zsimpl; f_equal; assumption.
 
77
Qed.
 
78
 
 
79
Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd.
 
80
Proof.
 
81
intros; zsimpl; f_equal; assumption.
 
82
Qed.
 
83
 
 
84
Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n.
 
85
Proof.
 
86
intros; zsimpl; auto with zarith.
 
87
Qed.
 
88
 
 
89
Section Induction.
 
90
 
 
91
Variable A : Z.t -> Prop.
 
92
Hypothesis A_wd : predicate_wd Z.eq A.
 
93
Hypothesis A0 : A 0.
 
94
Hypothesis AS : forall n, A n <-> A (Z.succ n). 
 
95
 
 
96
Add Morphism A with signature Z.eq ==> iff as A_morph.
 
97
Proof. apply A_wd. Qed.
 
98
 
 
99
Let B (z : Z) := A (Z.of_Z z).
 
100
 
 
101
Lemma B0 : B 0.
 
102
Proof.
 
103
unfold B; simpl.
 
104
rewrite <- (A_wd 0); auto.
 
105
zsimpl; auto.
 
106
Qed.
 
107
 
 
108
Lemma BS : forall z : Z, B z -> B (z + 1).
 
109
Proof.
 
110
intros z H.
 
111
unfold B in *. apply -> AS in H.
 
112
setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto.
 
113
zsimpl; auto.
 
114
Qed.
 
115
 
 
116
Lemma BP : forall z : Z, B z -> B (z - 1).
 
117
Proof.
 
118
intros z H.
 
119
unfold B in *. rewrite AS.
 
120
setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto.
 
121
zsimpl; auto with zarith.
 
122
Qed.
 
123
 
 
124
Lemma B_holds : forall z : Z, B z.
 
125
Proof.
 
126
intros; destruct (Z_lt_le_dec 0 z).
 
127
apply natlike_ind; auto with zarith.
 
128
apply B0.
 
129
intros; apply BS; auto.
 
130
replace z with (-(-z))%Z in * by (auto with zarith).
 
131
remember (-z)%Z as z'.
 
132
pattern z'; apply natlike_ind.
 
133
apply B0.
 
134
intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto.
 
135
subst z'; auto with zarith.
 
136
Qed.
 
137
 
 
138
Theorem NZinduction : forall n, A n.
 
139
Proof.
 
140
intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)).
 
141
apply B_holds.
 
142
zsimpl; auto.
 
143
Qed.
 
144
 
 
145
End Induction.
 
146
 
 
147
Theorem NZadd_0_l : forall n, 0 + n == n.
 
148
Proof.
 
149
intros; zsimpl; auto with zarith.
 
150
Qed.
 
151
 
 
152
Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
 
153
Proof.
 
154
intros; zsimpl; auto with zarith.
 
155
Qed.
 
156
 
 
157
Theorem NZsub_0_r : forall n, n - 0 == n.
 
158
Proof.
 
159
intros; zsimpl; auto with zarith.
 
160
Qed.
 
161
 
 
162
Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
 
163
Proof.
 
164
intros; zsimpl; auto with zarith.
 
165
Qed.
 
166
 
 
167
Theorem NZmul_0_l : forall n, 0 * n == 0.
 
168
Proof.
 
169
intros; zsimpl; auto with zarith.
 
170
Qed.
 
171
 
 
172
Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
 
173
Proof.
 
174
intros; zsimpl; ring.
 
175
Qed.
 
176
 
 
177
End NZAxiomsMod.
 
178
 
 
179
Definition NZlt := Z.lt.
 
180
Definition NZle := Z.le.
 
181
Definition NZmin := Z.min.
 
182
Definition NZmax := Z.max.
 
183
 
 
184
Infix "<=" := Z.le : IntScope.
 
185
Infix "<" := Z.lt : IntScope.
 
186
 
 
187
Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z.
 
188
Proof.
 
189
 intros; generalize (Z.spec_compare x y).
 
190
 destruct (Z.compare x y); auto.
 
191
 intros H; rewrite H; symmetry; apply Zcompare_refl.
 
192
Qed.
 
193
 
 
194
Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
 
195
Proof.
 
196
 intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition.
 
197
Qed.
 
198
 
 
199
Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
 
200
Proof.
 
201
 intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition.
 
202
Qed.
 
203
 
 
204
Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y].
 
205
Proof.
 
206
 intros; unfold Z.min, Zmin.
 
207
 rewrite spec_compare_alt; destruct Zcompare; auto.
 
208
Qed.
 
209
 
 
210
Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y].
 
211
Proof.
 
212
 intros; unfold Z.max, Zmax.
 
213
 rewrite spec_compare_alt; destruct Zcompare; auto.
 
214
Qed.
 
215
 
 
216
Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
 
217
Proof. 
 
218
intros x x' Hx y y' Hy.
 
219
rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
 
220
Qed.
 
221
 
 
222
Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
 
223
Proof.
 
224
intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
 
225
Qed.
 
226
 
 
227
Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd.
 
228
Proof.
 
229
intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition.
 
230
Qed.
 
231
 
 
232
Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd.
 
233
Proof.
 
234
intros; red; rewrite 2 spec_min; congruence.
 
235
Qed.
 
236
 
 
237
Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd.
 
238
Proof.
 
239
intros; red; rewrite 2 spec_max; congruence.
 
240
Qed.
 
241
 
 
242
Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 
243
Proof.
 
244
intros.
 
245
unfold Z.eq; rewrite spec_lt, spec_le; omega.
 
246
Qed.
 
247
 
 
248
Theorem NZlt_irrefl : forall n, ~ n < n.
 
249
Proof.
 
250
intros; rewrite spec_lt; auto with zarith.
 
251
Qed.
 
252
 
 
253
Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
 
254
Proof.
 
255
intros; rewrite spec_lt, spec_le, Z.spec_succ; omega.
 
256
Qed.
 
257
 
 
258
Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n.
 
259
Proof.
 
260
intros n m; unfold Z.eq; rewrite spec_le, spec_min.
 
261
generalize (Zmin_spec [n] [m]); omega.
 
262
Qed.
 
263
 
 
264
Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m.
 
265
Proof.
 
266
intros n m; unfold Z.eq; rewrite spec_le, spec_min.
 
267
generalize (Zmin_spec [n] [m]); omega.
 
268
Qed.
 
269
 
 
270
Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n.
 
271
Proof.
 
272
intros n m; unfold Z.eq; rewrite spec_le, spec_max.
 
273
generalize (Zmax_spec [n] [m]); omega.
 
274
Qed.
 
275
 
 
276
Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m.
 
277
Proof.
 
278
intros n m; unfold Z.eq; rewrite spec_le, spec_max.
 
279
generalize (Zmax_spec [n] [m]); omega.
 
280
Qed.
 
281
 
 
282
End NZOrdAxiomsMod.
 
283
 
 
284
Definition Zopp := Z.opp.
 
285
 
 
286
Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd.
 
287
Proof.
 
288
intros; zsimpl; auto with zarith.
 
289
Qed.
 
290
 
 
291
Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n.
 
292
Proof.
 
293
red; intros; zsimpl; auto with zarith.
 
294
Qed.
 
295
 
 
296
Theorem Zopp_0 : - 0 == 0.
 
297
Proof.
 
298
red; intros; zsimpl; auto with zarith.
 
299
Qed.
 
300
 
 
301
Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n).
 
302
Proof.
 
303
intros; zsimpl; auto with zarith.
 
304
Qed.
 
305
 
 
306
End ZSig_ZAxioms.