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

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

Fixed segmentation fault in Nat.ma, added get_index and renamed previous get_index to get_index_weak in List.ma.

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