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
(************************************************************************)
9
(*i $Id: NSigNAxioms.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
11
Require Import ZArith.
13
Require Import NAxioms.
16
(** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
18
Module NSig_NAxioms (N:NType) <: NAxiomsSig.
20
Delimit Scope IntScope with Int.
21
Bind Scope IntScope with N.t.
22
Open Local Scope IntScope.
23
Notation "[ x ]" := (N.to_Z x) : IntScope.
24
Infix "==" := N.eq (at level 70) : IntScope.
25
Notation "0" := N.zero : IntScope.
26
Infix "+" := N.add : IntScope.
27
Infix "-" := N.sub : IntScope.
28
Infix "*" := N.mul : IntScope.
30
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
31
Module Export NZAxiomsMod <: NZAxiomsSig.
34
Definition NZeq := N.eq.
35
Definition NZ0 := N.zero.
36
Definition NZsucc := N.succ.
37
Definition NZpred := N.pred.
38
Definition NZadd := N.add.
39
Definition NZsub := N.sub.
40
Definition NZmul := N.mul.
42
Theorem NZeq_equiv : equiv N.t N.eq.
44
repeat split; repeat red; intros; auto; congruence.
48
reflexivity proved by (proj1 NZeq_equiv)
49
symmetry proved by (proj2 (proj2 NZeq_equiv))
50
transitivity proved by (proj1 (proj2 NZeq_equiv))
53
Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
55
unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto.
58
Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd.
61
generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0).
62
destruct N.eq_bool; rewrite N.spec_0; intros.
63
rewrite 2 N.spec_pred0; congruence.
64
rewrite 2 N.spec_pred; f_equal; auto; try omega.
67
Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd.
69
unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
72
Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd.
74
unfold N.eq; intros x x' Hx y y' Hy.
75
destruct (Z_lt_le_dec [x] [y]).
76
rewrite 2 N.spec_sub0; f_equal; congruence.
77
rewrite 2 N.spec_sub; f_equal; congruence.
80
Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd.
82
unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto.
85
Theorem NZpred_succ : forall n, N.pred (N.succ n) == n.
88
rewrite N.spec_pred; rewrite N.spec_succ.
90
generalize (N.spec_pos n); omega.
93
Definition N_of_Z z := N.of_N (Zabs_N z).
97
Variable A : N.t -> Prop.
98
Hypothesis A_wd : predicate_wd N.eq A.
100
Hypothesis AS : forall n, A n <-> A (N.succ n).
102
Add Morphism A with signature N.eq ==> iff as A_morph.
103
Proof. apply A_wd. Qed.
105
Let B (z : Z) := A (N_of_Z z).
109
unfold B, N_of_Z; simpl.
110
rewrite <- (A_wd 0); auto.
111
red; rewrite N.spec_0, N.spec_of_N; auto.
114
Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1).
117
unfold B in *. apply -> AS in H2.
118
setoid_replace (N_of_Z (z + 1)) with (N.succ (N_of_Z z)); auto.
119
unfold N.eq. rewrite N.spec_succ.
121
rewrite 2 N.spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith.
124
Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z.
126
exact (natlike_ind B B0 BS).
129
Theorem NZinduction : forall n, A n.
131
intro n. setoid_replace n with (N_of_Z (N.to_Z n)).
132
apply B_holds. apply N.spec_pos.
134
rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
140
Theorem NZadd_0_l : forall n, 0 + n == n.
142
intros; red; rewrite N.spec_add, N.spec_0; auto with zarith.
145
Theorem NZadd_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
147
intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith.
150
Theorem NZsub_0_r : forall n, n - 0 == n.
152
intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith.
156
Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
159
destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H].
160
rewrite N.spec_sub0; auto.
161
rewrite N.spec_succ in H.
162
rewrite N.spec_pred0; auto.
163
destruct (Z_eq_dec [n] [m]).
164
rewrite N.spec_sub; auto with zarith.
165
rewrite N.spec_sub0; auto with zarith.
167
rewrite N.spec_sub, N.spec_succ in *; auto.
168
rewrite N.spec_pred, N.spec_sub; auto with zarith.
169
rewrite N.spec_sub; auto with zarith.
172
Theorem NZmul_0_l : forall n, 0 * n == 0.
175
rewrite N.spec_mul, N.spec_0; auto with zarith.
178
Theorem NZmul_succ_l : forall n m, (N.succ n) * m == n * m + m.
181
rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring.
186
Definition NZlt := N.lt.
187
Definition NZle := N.le.
188
Definition NZmin := N.min.
189
Definition NZmax := N.max.
191
Infix "<=" := N.le : IntScope.
192
Infix "<" := N.lt : IntScope.
194
Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z.
196
intros; generalize (N.spec_compare x y).
197
destruct (N.compare x y); auto.
198
intros H; rewrite H; symmetry; apply Zcompare_refl.
201
Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
203
intros; unfold N.lt, Zlt; rewrite spec_compare_alt; intuition.
206
Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
208
intros; unfold N.le, Zle; rewrite spec_compare_alt; intuition.
211
Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y].
213
intros; unfold N.min, Zmin.
214
rewrite spec_compare_alt; destruct Zcompare; auto.
217
Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y].
219
intros; unfold N.max, Zmax.
220
rewrite spec_compare_alt; destruct Zcompare; auto.
223
Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
225
intros x x' Hx y y' Hy.
226
rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
229
Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.
231
intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition.
234
Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd.
236
intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition.
239
Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd.
241
intros; red; rewrite 2 spec_min; congruence.
244
Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd.
246
intros; red; rewrite 2 spec_max; congruence.
249
Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
252
unfold N.eq; rewrite spec_lt, spec_le; omega.
255
Theorem NZlt_irrefl : forall n, ~ n < n.
257
intros; rewrite spec_lt; auto with zarith.
260
Theorem NZlt_succ_r : forall n m, n < (N.succ m) <-> n <= m.
262
intros; rewrite spec_lt, spec_le, N.spec_succ; omega.
265
Theorem NZmin_l : forall n m, n <= m -> N.min n m == n.
267
intros n m; unfold N.eq; rewrite spec_le, spec_min.
268
generalize (Zmin_spec [n] [m]); omega.
271
Theorem NZmin_r : forall n m, m <= n -> N.min n m == m.
273
intros n m; unfold N.eq; rewrite spec_le, spec_min.
274
generalize (Zmin_spec [n] [m]); omega.
277
Theorem NZmax_l : forall n m, m <= n -> N.max n m == n.
279
intros n m; unfold N.eq; rewrite spec_le, spec_max.
280
generalize (Zmax_spec [n] [m]); omega.
283
Theorem NZmax_r : forall n m, n <= m -> N.max n m == m.
285
intros n m; unfold N.eq; rewrite spec_le, spec_max.
286
generalize (Zmax_spec [n] [m]); omega.
291
Theorem pred_0 : N.pred 0 == 0.
293
red; rewrite N.spec_pred0; rewrite N.spec_0; auto.
296
Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
297
Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
298
Implicit Arguments recursion [A].
300
Theorem recursion_wd :
301
forall (A : Type) (Aeq : relation A),
302
forall a a' : A, Aeq a a' ->
303
forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' ->
304
forall x x' : N.t, x == x' ->
305
Aeq (recursion a f x) (recursion a' f' x').
307
unfold fun2_wd, N.eq, fun2_eq.
308
intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
311
rewrite <- Exx'; clear x' Exx'.
312
replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
313
induction (Zabs_nat [x]).
315
rewrite N_of_S, 2 Nrect_step; auto.
316
destruct [x]; simpl; auto.
317
change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
318
change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
321
Theorem recursion_0 :
322
forall (A : Type) (a : A) (f : N.t -> A -> A), recursion a f 0 = a.
324
intros A a f; unfold recursion, N.to_N; rewrite N.spec_0; simpl; auto.
327
Theorem recursion_succ :
328
forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
329
Aeq a a -> fun2_wd N.eq Aeq Aeq f ->
330
forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)).
332
unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n.
333
replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)).
337
rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
340
fold (recursion a f n).
341
apply recursion_wd; auto.
347
change ([n]+1)%Z with (Zsucc [n]).
350
rewrite 2 Z_of_N_abs.
351
rewrite 2 Zabs_eq; auto.
352
generalize (N.spec_pos n); auto with zarith.
353
apply N.spec_pos; auto.
added
removed
theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
