source: Deliverables/D4.1/Matita/Nat.ma @ 275

Last change on this file since 275 was 275, checked in by mulligan, 10 years ago

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File size: 10.3 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4include "Cartesian.ma".
5include "Bool.ma".
6
7include "Connectives.ma".
8
9(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
10(* The datatype.                                                              *)
11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
12ninductive Nat: Type[0] ≝
13  Z: Nat
14| S: Nat → Nat.
15
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17(* Orderings.                                                                 *)
18(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19
20ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
21  ltoe_refl: less_than_or_equal_p n n
22| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
23
24nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
25  match m with
26    [ Z ⇒ true
27    | S o ⇒
28      match n with
29        [ Z ⇒ false
30        | S p ⇒ less_than_or_equal_b o p
31        ]
32    ].
33   
34notation "hvbox(n break ≤ m)"
35  non associative with precedence 47
36  for @{ 'less_than_or_equal $n $m }.
37 
38interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
39interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
40
41ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
42  λm, n: Nat.
43    n ≤ m.
44
45ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
46  λm, n: Nat.
47    n ≤ m.
48   
49notation "hvbox(n break ≥ m)"
50  non associative with precedence 47
51  for @{ 'greater_than_or_equal $n $m }.
52 
53
54interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
55interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
56
57(* Add Boolean versions.                                                      *)
58ndefinition less_than_p ≝
59  λm: Nat.
60  λn: Nat.
61    less_than_or_equal_p (S m) n.
62   
63notation "hvbox(n break < m)"
64  non associative with precedence 47
65  for @{ 'less_than $n $m }.
66 
67interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
68
69ndefinition greater_than_p ≝
70  λm, n: Nat.
71    n < m.
72   
73notation "hvbox(n break > m)"
74  non associative with precedence 47
75  for @{ 'greater_than $n $m }.
76 
77interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
78
79(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
80(* Addition and subtraction.                                                  *)
81(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
82nlet rec plus (n: Nat) (o: Nat) on n ≝
83  match n with
84    [ Z ⇒ o
85    | S p ⇒ S (plus p o)
86    ].
87   
88notation "hvbox(n break + m)"
89  right associative with precedence 52
90  for @{ 'plus $n $m }.
91 
92interpretation "Nat plus" 'plus n m = (plus n m).
93   
94nlet rec minus (n: Nat) (o: Nat) on n ≝
95  match n with
96    [ Z ⇒ Z
97    | S p ⇒
98      match o with
99        [ Z ⇒ S p
100        | S q ⇒ minus p q
101        ]
102    ].
103   
104notation "hvbox(n break - m)"
105  right associative with precedence 47
106  for @{ 'minus $n $m }.
107 
108interpretation "Nat minus" 'minus n m = (minus n m).
109
110(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
111(* Multiplication, modulus and division.                                      *)
112(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
113   
114nlet rec multiplication (n: Nat) (o: Nat) on n ≝
115  match n with
116    [ Z ⇒ Z
117    | S p ⇒ o + (multiplication p o)
118    ].
119   
120notation "hvbox(n break * m)"
121  right associative with precedence 47
122  for @{ 'multiplication $n $m }.
123 
124interpretation "Nat multiplication" 'times n m = (multiplication n m).
125
126nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
127  match n ≤ p with
128    [ true ⇒ Z
129    | false ⇒
130      match m with
131        [ Z ⇒ Z
132        | (S q) ⇒ S (division_aux q (n - (S p)) p)
133        ]
134    ].
135   
136ndefinition division ≝
137  λm, n: Nat.
138    match n with
139      [ Z ⇒ S m
140      | S o ⇒ division_aux m m o
141      ].
142     
143notation "hvbox(n break ÷ m)"
144  right associative with precedence 47
145  for @{ 'division $n $m }.
146 
147interpretation "Nat division" 'division n m = (division n m).
148     
149nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
150  match n ≤ p with
151    [ true ⇒ n
152    | false ⇒
153      match m with
154        [ Z ⇒ n
155        | S o ⇒ modulus_aux o (n - (S p)) p
156        ]
157    ].
158   
159ndefinition modulus ≝
160  λm, n: Nat.
161    match n with
162      [ Z ⇒ m
163      | S o ⇒ modulus_aux m m o
164      ].
165   
166notation "hvbox(n break % m)"
167  right associative with precedence 47
168  for @{ 'modulus $n $m }.
169 
170interpretation "Nat modulus" 'modulus m n = (modulus m n).
171
172ndefinition divide_with_remainder ≝
173  λm, n: Nat.
174    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
175
176(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
177(* Exponentials, and square roots.                                            *)
178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
179
180nlet rec exponential (m: Nat) (n: Nat) on n ≝
181  match n with
182    [ Z ⇒ S (Z)
183    | S o ⇒ m * exponential m o
184    ].
185   
186notation "hvbox(n ^ m)"
187  left associative with precedence 52
188  for @{ 'exponential $n $m }.
189 
190interpretation "Nat exponential" 'exponential n m = (exponential n m).
191
192nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
193  match m with
194    [ Z ⇒
195      match n with
196        [ Z ⇒ true
197        | _ ⇒ false
198        ]
199    | S o ⇒
200      match n with
201        [ S p ⇒ decidable_equality o p
202        | _ ⇒ false
203        ]
204    ].
205
206(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
207(* Greatest common divisor and least common multiple.                         *)
208(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
209
210(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
211(* Lemmas.                                                                    *)
212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
213
214nlemma less_than_or_equal_zero:
215  ∀n: Nat.
216    Z ≤ n.
217  #n.
218  nelim n.
219  //.
220  #N.
221  napply ltoe_step.
222nqed.
223
224naxiom less_than_or_equal_injective:
225  ∀m, n: Nat.
226    S m ≤ S n → m ≤ n.
227
228(*
229nlemma less_than_or_equal_zero_equal_zero:
230  ∀m: Nat.
231    m ≤ Z → m = Z.
232  #m.
233  nelim m.
234  //.
235  #N H H2.
236  nnormalize.
237*)
238
239nlemma less_than_or_equal_reflexive:
240  ∀n: Nat.
241    n ≤ n.
242  #n.
243  nelim n.
244  nnormalize.
245  @.
246  #N H.
247  nnormalize.
248  //.
249nqed.
250
251(*
252nlemma less_than_or_equal_succ:
253  ∀m, n: Nat.
254    S m ≤ n → m ≤ n.
255  #m n.
256  nelim m.
257  #H.
258  napplyS less_than_or_equal_zero.
259  #N H H2.
260  nrewrite > H.
261  nnormalize.
262
263nlemma less_than_or_equal_transitive:
264  ∀m, n, o: Nat.
265    m ≤ n ∧ n ≤ o → m ≤ o.
266  #m n o.
267  nelim m.
268  #H.
269  napply less_than_or_equal_zero.
270  #N H H2.
271  nnormalize.
272*)
273
274nlemma plus_zero:
275  ∀n: Nat.
276    n + Z = n.
277  #n.
278  nelim n.
279  nnormalize.
280  @.
281  #N H.
282  nnormalize.
283  nrewrite > H.
284  @.
285nqed.
286
287nlemma plus_associative:
288  ∀m, n, o: Nat.
289    (m + n) + o = m + (n + o).
290  #m n o.
291  nelim m.
292  nnormalize.
293  @.
294  #N H.
295  nnormalize.
296  nrewrite > H.
297  @.
298nqed.
299
300nlemma succ_plus:
301  ∀m, n: Nat.
302    S(m + n) = m + S(n).
303  #m n.
304  nelim m.
305  nnormalize.
306  @.
307  #N H.
308  nnormalize.
309  nrewrite > H.
310  @.
311nqed.
312
313nlemma succ_plus_succ_zero:
314  ∀n: Nat.
315    S n = plus n (S Z).
316  #n.
317  nelim n.
318  //.
319  #N H.
320  nnormalize.
321  nrewrite < H.
322  @.
323nqed.
324
325nlemma plus_symmetrical:
326  ∀m, n: Nat.
327    m + n = n + m.
328  #m n.
329  nelim m.
330  nnormalize.
331  nelim n.
332  nnormalize.
333  @.
334  #N H.
335  nnormalize.
336  nrewrite < H.
337  @.
338  #N H.
339  nnormalize.
340  nrewrite > H.
341  napplyS succ_plus.
342nqed.
343
344nlemma multiplication_zero_right_neutral:
345  ∀m: Nat.
346    m * Z = Z.
347  #m.
348  nelim m.
349  nnormalize.
350  @.
351  #N H.
352  nnormalize.
353  nrewrite > H.
354  @.
355nqed.
356
357nlemma multiplication_succ:
358  ∀m, n: Nat.
359    m * S(n) = m + (m * n).
360  #m n.
361  nelim m.
362  nnormalize.
363  @.
364  #N H.
365  nnormalize.
366  nrewrite > H.
367  nrewrite < (plus_associative n N ?).
368  nrewrite > (plus_symmetrical n N).
369  nrewrite > (plus_associative N n ?).
370  @.
371nqed.
372
373nlemma multiplication_symmetrical:
374  ∀m, n: Nat.
375    m * n = n * m.
376  #m n.
377  nelim m.
378  nnormalize.
379  nelim n.
380  nnormalize.
381  @.
382  #N H.
383  nnormalize.
384  nrewrite < H.
385  @.
386  #N H.
387  nnormalize.
388  nrewrite > H.
389  nrewrite > (multiplication_succ ? ?).
390  @.
391nqed.
392
393nlemma multiplication_succ_zero_left_neutral:
394  ∀m: Nat.
395    (S Z) * m = m.
396  #m.
397  nelim m.
398  nnormalize.
399  @.
400  #N H.
401  nnormalize.
402  nrewrite > (succ_plus ? ?).
403  nrewrite < (succ_plus_succ_zero ?).
404  @.
405nqed.
406
407nlemma multiplication_succ_zero_right_neutral:
408  ∀m: Nat.
409    m * (S Z) = m.
410  #m.
411  nelim m.
412  nnormalize.
413  @.
414  #N H.
415  nnormalize.
416  nrewrite > H.
417  @.
418nqed.
419
420nlemma multiplication_distributes_right_plus:
421  ∀m, n, o: Nat.
422    (m + n) * o = m * o + n * o.
423  #m n o.
424  nelim m.
425  nnormalize.
426  @.
427  #N H.
428  nnormalize.
429  nrewrite > H.
430  nrewrite < (plus_associative ? ? ?).
431  @.
432nqed.
433
434nlemma multiplication_distributes_left_plus:
435  ∀m, n, o: Nat.
436    o * (m + n) = o * m + o * n.
437  #m n o.
438  nelim o.
439  //.
440  #N H.
441  nnormalize.
442  nrewrite > H.
443  nrewrite < (plus_associative ? n (N * n)).
444  nrewrite > (plus_symmetrical (m + N * m) n).
445  nrewrite < (plus_associative n m (N * m)).
446  nrewrite < (plus_symmetrical n m).
447  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
448  @.
449nqed.
450
451nlemma mutliplication_associative:
452  ∀m, n, o: Nat.
453    m * (n * o) = (m * n) * o.
454  #m n o.
455  nelim m.
456  nnormalize.
457  @.
458  #N H.
459  nnormalize.
460  nrewrite > H.
461  nrewrite > (multiplication_distributes_right_plus ? ? ?).
462  @.
463nqed.
464
465nlemma minus_minus:
466  ∀n: Nat.
467    n - n = Z.
468  #n.
469  nelim n.
470  nnormalize.
471  @.
472  #N H.
473  nnormalize.
474  nrewrite > H.
475  @.
476nqed.
477
478(*
479nlemma succ_injective:
480  ∀m, n: Nat.
481    S m = S n → m = n.
482  #m n.
483  nelim m.
484  #H.
485  ninversion H.
486  #H.
487  ndestruct
488
489nlemma plus_minus_associate:
490  ∀m, n, o: Nat.
491    (m + n) - o = m + (n - o).
492  #m n o.
493  nelim m.
494  nnormalize.
495  @.
496  #N H.
497 
498
499nlemma plus_minus_inverses:
500  ∀m, n: Nat.
501    (m + n) - n = m.
502  #m n.
503  nelim m.
504  nnormalize.
505  napply minus_minus.
506  #N H.
507*)
Note: See TracBrowser for help on using the repository browser.