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
(************************************************************************)
11
(*i $Id: NPeano.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
18
Module NPeanoAxiomsMod <: NAxiomsSig.
19
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
20
Module Export NZAxiomsMod <: NZAxiomsSig.
23
Definition NZeq := (@eq nat).
25
Definition NZsucc := S.
26
Definition NZpred := pred.
27
Definition NZadd := plus.
28
Definition NZsub := minus.
29
Definition NZmul := mult.
31
Theorem NZeq_equiv : equiv nat NZeq.
35
reflexivity proved by (proj1 NZeq_equiv)
36
symmetry proved by (proj2 (proj2 NZeq_equiv))
37
transitivity proved by (proj1 (proj2 NZeq_equiv))
40
(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq"
41
then the theorem generated for succ_wd below is forall x, succ x = succ x,
42
which does not match the axioms in NAxiomsSig *)
44
Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
49
Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
54
Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
59
Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
64
Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
70
forall A : nat -> Prop, predicate_wd (@eq nat) A ->
71
A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
73
intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
76
Theorem NZpred_succ : forall n : nat, pred (S n) = n.
81
Theorem NZadd_0_l : forall n : nat, 0 + n = n.
86
Theorem NZadd_succ_l : forall n m : nat, (S n) + m = S (n + m).
91
Theorem NZsub_0_r : forall n : nat, n - 0 = n.
93
intro n; now destruct n.
96
Theorem NZsub_succ_r : forall n m : nat, n - (S m) = pred (n - m).
98
intros n m; induction n m using nat_double_ind; simpl; auto. apply NZsub_0_r.
101
Theorem NZmul_0_l : forall n : nat, 0 * n = 0.
106
Theorem NZmul_succ_l : forall n m : nat, S n * m = n * m + m.
108
intros n m; now rewrite plus_comm.
113
Definition NZlt := lt.
114
Definition NZle := le.
115
Definition NZmin := min.
116
Definition NZmax := max.
118
Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
120
unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
123
Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
125
unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
128
Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
133
Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
138
Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.
142
intro H; destruct H as [H | H].
143
now apply lt_le_weak. rewrite H; apply le_refl.
146
Theorem NZlt_irrefl : forall n : nat, ~ (n < n).
151
Theorem NZlt_succ_r : forall n m : nat, n < S m <-> n <= m.
153
intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm].
156
Theorem NZmin_l : forall n m : nat, n <= m -> NZmin n m = n.
161
Theorem NZmin_r : forall n m : nat, m <= n -> NZmin n m = m.
166
Theorem NZmax_l : forall n m : nat, m <= n -> NZmax n m = n.
171
Theorem NZmax_r : forall n m : nat, n <= m -> NZmax n m = m.
178
Definition recursion : forall A : Type, A -> (nat -> A -> A) -> nat -> A :=
179
fun A : Type => nat_rect (fun _ => A).
180
Implicit Arguments recursion [A].
182
Theorem succ_neq_0 : forall n : nat, S n <> 0.
184
intros; discriminate.
187
Theorem pred_0 : pred 0 = 0.
192
Theorem recursion_wd : forall (A : Type) (Aeq : relation A),
193
forall a a' : A, Aeq a a' ->
194
forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' ->
195
forall n n' : nat, n = n' ->
196
Aeq (recursion a f n) (recursion a' f' n').
198
unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
201
Theorem recursion_0 :
202
forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a.
207
Theorem recursion_succ :
208
forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
209
Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f ->
210
forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
212
induction n; simpl; auto.
217
(* Now we apply the largest property functor *)
219
Module Export NPeanoSubPropMod := NSubPropFunct NPeanoAxiomsMod.