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

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

Fixed Status.ma so that it compiles.

File size: 11.1 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 'mod' 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(* Axioms.                                                                    *)
212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
213
214naxiom plus_minus_inverse_left:
215  ∀m, n: Nat.
216    (m + n) - n = m.
217   
218naxiom less_than_or_equal_monotone:
219  ∀m, n: Nat.
220    m ≤ n → (S m) ≤ (S n).
221   
222naxiom succ_less_than_or_equal_injective:
223  ∀m, n: Nat.
224    (S m) ≤ (S n) → m ≤ n.
225   
226naxiom plus_minus_inverse_right:
227  ∀m, n: Nat.
228    (m - n) + n = m.
229
230naxiom greater_than_b: Nat → Nat → Bool.
231naxiom less_than_b: Nat → Nat → Bool.
232
233naxiom succ_less_than_injective:
234  ∀m, n: Nat.
235    less_than_p (S m) (S n) → m < n.
236   
237naxiom nothing_less_than_Z:
238  ∀m: Nat.
239    ¬(m < Z).
240   
241(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
242(* Lemmas.                                                                    *)
243(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
244   
245nlemma less_than_or_equal_zero:
246  ∀n: Nat.
247    Z ≤ n.
248  #n.
249  nelim n.
250  //.
251  #N.
252  napply ltoe_step.
253nqed.
254
255naxiom less_than_or_equal_injective:
256  ∀m, n: Nat.
257    S m ≤ S n → m ≤ n.
258
259(*
260nlemma less_than_or_equal_zero_equal_zero:
261  ∀m: Nat.
262    m ≤ Z → m = Z.
263  #m.
264  nelim m.
265  //.
266  #N H H2.
267  nnormalize.
268*)
269
270nlemma less_than_or_equal_reflexive:
271  ∀n: Nat.
272    n ≤ n.
273  #n.
274  nelim n.
275  nnormalize.
276  @.
277  #N H.
278  nnormalize.
279  //.
280nqed.
281
282(*
283nlemma less_than_or_equal_succ:
284  ∀m, n: Nat.
285    S m ≤ n → m ≤ n.
286  #m n.
287  nelim m.
288  #H.
289  napplyS less_than_or_equal_zero.
290  #N H H2.
291  nrewrite > H.
292  nnormalize.
293
294nlemma less_than_or_equal_transitive:
295  ∀m, n, o: Nat.
296    m ≤ n ∧ n ≤ o → m ≤ o.
297  #m n o.
298  nelim m.
299  #H.
300  napply less_than_or_equal_zero.
301  #N H H2.
302  nnormalize.
303*)
304
305nlemma plus_zero:
306  ∀n: Nat.
307    n + Z = n.
308  #n.
309  nelim n.
310  nnormalize.
311  @.
312  #N H.
313  nnormalize.
314  nrewrite > H.
315  @.
316nqed.
317
318nlemma plus_associative:
319  ∀m, n, o: Nat.
320    (m + n) + o = m + (n + o).
321  #m n o.
322  nelim m.
323  nnormalize.
324  @.
325  #N H.
326  nnormalize.
327  nrewrite > H.
328  @.
329nqed.
330
331nlemma succ_plus:
332  ∀m, n: Nat.
333    S(m + n) = m + S(n).
334  #m n.
335  nelim m.
336  nnormalize.
337  @.
338  #N H.
339  nnormalize.
340  nrewrite > H.
341  @.
342nqed.
343
344nlemma succ_plus_succ_zero:
345  ∀n: Nat.
346    S n = plus n (S Z).
347  #n.
348  nelim n.
349  //.
350  #N H.
351  nnormalize.
352  nrewrite < H.
353  @.
354nqed.
355
356nlemma plus_symmetrical:
357  ∀m, n: Nat.
358    m + n = n + m.
359  #m n.
360  nelim m.
361  nnormalize.
362  nelim n.
363  nnormalize.
364  @.
365  #N H.
366  nnormalize.
367  nrewrite < H.
368  @.
369  #N H.
370  nnormalize.
371  nrewrite > H.
372  napply succ_plus.
373nqed.
374
375nlemma multiplication_zero_right_neutral:
376  ∀m: Nat.
377    m * Z = Z.
378  #m.
379  nelim m.
380  nnormalize.
381  @.
382  #N H.
383  nnormalize.
384  nrewrite > H.
385  @.
386nqed.
387
388nlemma multiplication_succ:
389  ∀m, n: Nat.
390    m * S(n) = m + (m * n).
391  #m n.
392  nelim m.
393  nnormalize.
394  @.
395  #N H.
396  nnormalize.
397  nrewrite > H.
398  nrewrite < (plus_associative n N ?).
399  nrewrite > (plus_symmetrical n N).
400  nrewrite > (plus_associative N n ?).
401  @.
402nqed.
403
404nlemma multiplication_symmetrical:
405  ∀m, n: Nat.
406    m * n = n * m.
407  #m n.
408  nelim m.
409  nnormalize.
410  nelim n.
411  nnormalize.
412  @.
413  #N H.
414  nnormalize.
415  nrewrite < H.
416  @.
417  #N H.
418  nnormalize.
419  nrewrite > H.
420  nrewrite > (multiplication_succ ? ?).
421  @.
422nqed.
423
424nlemma multiplication_succ_zero_left_neutral:
425  ∀m: Nat.
426    (S Z) * m = m.
427  #m.
428  nelim m.
429  nnormalize.
430  @.
431  #N H.
432  nnormalize.
433  nrewrite > (succ_plus ? ?).
434  nrewrite < (succ_plus_succ_zero ?).
435  @.
436nqed.
437
438nlemma multiplication_succ_zero_right_neutral:
439  ∀m: Nat.
440    m * (S Z) = m.
441  #m.
442  nelim m.
443  nnormalize.
444  @.
445  #N H.
446  nnormalize.
447  nrewrite > H.
448  @.
449nqed.
450
451nlemma multiplication_distributes_right_plus:
452  ∀m, n, o: Nat.
453    (m + n) * o = m * o + n * o.
454  #m n o.
455  nelim m.
456  nnormalize.
457  @.
458  #N H.
459  nnormalize.
460  nrewrite > H.
461  nrewrite < (plus_associative ? ? ?).
462  @.
463nqed.
464
465nlemma multiplication_distributes_left_plus:
466  ∀m, n, o: Nat.
467    o * (m + n) = o * m + o * n.
468  #m n o.
469  nelim o.
470  //.
471  #N H.
472  nnormalize.
473  nrewrite > H.
474  nrewrite < (plus_associative ? n (N * n)).
475  nrewrite > (plus_symmetrical (m + N * m) n).
476  nrewrite < (plus_associative n m (N * m)).
477  nrewrite < (plus_symmetrical n m).
478  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
479  @.
480nqed.
481
482nlemma mutliplication_associative:
483  ∀m, n, o: Nat.
484    m * (n * o) = (m * n) * o.
485  #m n o.
486  nelim m.
487  nnormalize.
488  @.
489  #N H.
490  nnormalize.
491  nrewrite > H.
492  nrewrite > (multiplication_distributes_right_plus ? ? ?).
493  @.
494nqed.
495
496nlemma minus_minus:
497  ∀n: Nat.
498    n - n = Z.
499  #n.
500  nelim n.
501  nnormalize.
502  @.
503  #N H.
504  nnormalize.
505  nrewrite > H.
506  @.
507nqed.
508
509(*
510nlemma succ_injective:
511  ∀m, n: Nat.
512    S m = S n → m = n.
513  #m n.
514  nelim m.
515  #H.
516  ninversion H.
517  #H.
518  ndestruct
519
520nlemma plus_minus_associate:
521  ∀m, n, o: Nat.
522    (m + n) - o = m + (n - o).
523  #m n o.
524  nelim m.
525  nnormalize.
526  @.
527  #N H.
528 
529
530nlemma plus_minus_inverses:
531  ∀m, n: Nat.
532    (m + n) - n = m.
533  #m n.
534  nelim m.
535  nnormalize.
536  napply minus_minus.
537  #N H.
538*)
Note: See TracBrowser for help on using the repository browser.