]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/Coq/Init/Peano.mma
components: arity, csuba
[helm.git] / matita / matita / contribs / procedural / Coq / Init / Peano.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "Coq.ma".
18
19 (*#***********************************************************************)
20
21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
22
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
24
25 (*   \VV/  **************************************************************)
26
27 (*    //   *      This file is distributed under the terms of the       *)
28
29 (*         *       GNU Lesser General Public License Version 2.1        *)
30
31 (*#***********************************************************************)
32
33 (*i $Id: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
34
35 (*#* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
36
37 (*#* This module defines the following operations on natural numbers :
38     - predecessor [pred]
39     - addition [plus]
40     - multiplication [mult]
41     - less or equal order [le]
42     - less [lt]
43     - greater or equal [ge]
44     - greater [gt]
45
46    This module states various lemmas and theorems about natural numbers,
47    including Peano's axioms of arithmetic (in Coq, these are in fact provable)
48    Case analysis on [nat] and induction on [nat * nat] are provided too *)
49
50 include "Init/Notations.ma".
51
52 include "Init/Datatypes.ma".
53
54 include "Init/Logic.ma".
55
56 (* UNEXPORTED
57 Open Scope nat_scope.
58 *)
59
60 inline procedural "cic:/Coq/Init/Peano/eq_S.con" as definition.
61
62 (* UNEXPORTED
63 Hint Resolve (f_equal S): v62.
64 *)
65
66 (* UNEXPORTED
67 Hint Resolve (f_equal (A:=nat)): core.
68 *)
69
70 (*#* The predecessor function *)
71
72 inline procedural "cic:/Coq/Init/Peano/pred.con" as definition.
73
74 (* UNEXPORTED
75 Hint Resolve (f_equal pred): v62.
76 *)
77
78 inline procedural "cic:/Coq/Init/Peano/pred_Sn.con" as theorem.
79
80 inline procedural "cic:/Coq/Init/Peano/eq_add_S.con" as theorem.
81
82 (* UNEXPORTED
83 Hint Immediate eq_add_S: core v62.
84 *)
85
86 (*#* A consequence of the previous axioms *)
87
88 inline procedural "cic:/Coq/Init/Peano/not_eq_S.con" as theorem.
89
90 (* UNEXPORTED
91 Hint Resolve not_eq_S: core v62.
92 *)
93
94 inline procedural "cic:/Coq/Init/Peano/IsSucc.con" as definition.
95
96 inline procedural "cic:/Coq/Init/Peano/O_S.con" as theorem.
97
98 (* UNEXPORTED
99 Hint Resolve O_S: core v62.
100 *)
101
102 inline procedural "cic:/Coq/Init/Peano/n_Sn.con" as theorem.
103
104 (* UNEXPORTED
105 Hint Resolve n_Sn: core v62.
106 *)
107
108 (*#* Addition *)
109
110 inline procedural "cic:/Coq/Init/Peano/plus.con" as definition.
111
112 (* UNEXPORTED
113 Hint Resolve (f_equal2 plus): v62.
114 *)
115
116 (* UNEXPORTED
117 Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
118 *)
119
120 (* NOTATION
121 Infix "+" := plus : nat_scope.
122 *)
123
124 inline procedural "cic:/Coq/Init/Peano/plus_n_O.con" as lemma.
125
126 (* UNEXPORTED
127 Hint Resolve plus_n_O: core v62.
128 *)
129
130 inline procedural "cic:/Coq/Init/Peano/plus_O_n.con" as lemma.
131
132 inline procedural "cic:/Coq/Init/Peano/plus_n_Sm.con" as lemma.
133
134 (* UNEXPORTED
135 Hint Resolve plus_n_Sm: core v62.
136 *)
137
138 inline procedural "cic:/Coq/Init/Peano/plus_Sn_m.con" as lemma.
139
140 (*#* Multiplication *)
141
142 inline procedural "cic:/Coq/Init/Peano/mult.con" as definition.
143
144 (* UNEXPORTED
145 Hint Resolve (f_equal2 mult): core v62.
146 *)
147
148 (* NOTATION
149 Infix "*" := mult : nat_scope.
150 *)
151
152 inline procedural "cic:/Coq/Init/Peano/mult_n_O.con" as lemma.
153
154 (* UNEXPORTED
155 Hint Resolve mult_n_O: core v62.
156 *)
157
158 inline procedural "cic:/Coq/Init/Peano/mult_n_Sm.con" as lemma.
159
160 (* UNEXPORTED
161 Hint Resolve mult_n_Sm: core v62.
162 *)
163
164 (*#* Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
165
166 inline procedural "cic:/Coq/Init/Peano/minus.con" as definition.
167
168 (* NOTATION
169 Infix "-" := minus : nat_scope.
170 *)
171
172 (*#* Definition of the usual orders, the basic properties of [le] and [lt] 
173     can be found in files Le and Lt *)
174
175 (*#* An inductive definition to define the order *)
176
177 inline procedural "cic:/Coq/Init/Peano/le.ind".
178
179 (* NOTATION
180 Infix "<=" := le : nat_scope.
181 *)
182
183 (* UNEXPORTED
184 Hint Constructors le: core v62.
185 *)
186
187 (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
188
189 inline procedural "cic:/Coq/Init/Peano/lt.con" as definition.
190
191 (* UNEXPORTED
192 Hint Unfold lt: core v62.
193 *)
194
195 (* NOTATION
196 Infix "<" := lt : nat_scope.
197 *)
198
199 inline procedural "cic:/Coq/Init/Peano/ge.con" as definition.
200
201 (* UNEXPORTED
202 Hint Unfold ge: core v62.
203 *)
204
205 (* NOTATION
206 Infix ">=" := ge : nat_scope.
207 *)
208
209 inline procedural "cic:/Coq/Init/Peano/gt.con" as definition.
210
211 (* UNEXPORTED
212 Hint Unfold gt: core v62.
213 *)
214
215 (* NOTATION
216 Infix ">" := gt : nat_scope.
217 *)
218
219 (* NOTATION
220 Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
221 *)
222
223 (* NOTATION
224 Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
225 *)
226
227 (* NOTATION
228 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
229 *)
230
231 (* NOTATION
232 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
233 *)
234
235 (*#* Pattern-Matching on natural numbers *)
236
237 inline procedural "cic:/Coq/Init/Peano/nat_case.con" as theorem.
238
239 (*#* Principle of double induction *)
240
241 inline procedural "cic:/Coq/Init/Peano/nat_double_ind.con" as theorem.
242
243 (*#* Notations *)
244