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

Last change on this file since 351 was 351, checked in by mulligan, 9 years ago

No more axioms but the paralogisms.

File size: 14.4 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).
39
40notation "hvbox(n break ≲ m)"
41  non associative with precedence 47
42  for @{ 'less_than_or_equalb $n $m }.
43
44interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m).
45
46
47ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
48  λm, n: Nat.
49    n ≤ m.
50
51ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
52  λm, n: Nat.
53    less_than_or_equal_b n m.
54   
55notation "hvbox(n break ≥ m)"
56  non associative with precedence 47
57  for @{ 'greater_than_or_equal $n $m }.
58 
59
60interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
61
62notation "hvbox(n break ≳ m)"
63  non associative with precedence 47
64  for @{ 'greater_than_or_equalb $n $m }.
65
66interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m).
67
68
69(* Add Boolean versions.                                                      *)
70ndefinition less_than_p ≝
71  λm: Nat.
72  λn: Nat.
73    less_than_or_equal_p (S m) n.
74   
75notation "hvbox(n break < m)"
76  non associative with precedence 47
77  for @{ 'less_than $n $m }.
78 
79interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
80
81ndefinition greater_than_p ≝
82  λm, n: Nat.
83    n < m.
84   
85notation "hvbox(n break > m)"
86  non associative with precedence 47
87  for @{ 'greater_than $n $m }.
88 
89interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
90
91nlet rec less_than_b (m: Nat) (n: Nat) on m ≝
92  match m with
93    [ Z ⇒
94      match n with
95        [ Z ⇒ false
96        | S o ⇒ true
97        ]
98    | S o ⇒
99      match n with
100        [ Z ⇒ false
101        | S p ⇒ less_than_b o p
102        ]
103    ].
104
105(* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *)
106
107ndefinition greater_than_b ≝
108  λm, n: Nat.
109    less_than_b n m.
110   
111(* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *)
112
113(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
114(* Addition and subtraction.                                                  *)
115(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
116nlet rec plus (n: Nat) (o: Nat) on n ≝
117  match n with
118    [ Z ⇒ o
119    | S p ⇒ S (plus p o)
120    ].
121   
122notation "hvbox(n break + m)"
123  right associative with precedence 52
124  for @{ 'plus $n $m }.
125 
126interpretation "Nat plus" 'plus n m = (plus n m).
127   
128nlet rec minus (n: Nat) (o: Nat) on n ≝
129  match n with
130    [ Z ⇒ Z
131    | S p ⇒
132      match o with
133        [ Z ⇒ S p
134        | S q ⇒ minus p q
135        ]
136    ].
137   
138notation "hvbox(n break - m)"
139  right associative with precedence 47
140  for @{ 'minus $n $m }.
141 
142interpretation "Nat minus" 'minus n m = (minus n m).
143
144(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
145(* Multiplication, modulus and division.                                      *)
146(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
147   
148nlet rec multiplication (n: Nat) (o: Nat) on n ≝
149  match n with
150    [ Z ⇒ Z
151    | S p ⇒ o + (multiplication p o)
152    ].
153   
154notation "hvbox(n break * m)"
155  right associative with precedence 47
156  for @{ 'multiplication $n $m }.
157 
158interpretation "Nat multiplication" 'times n m = (multiplication n m).
159
160nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
161  match less_than_or_equal_b n p with
162    [ true ⇒ Z
163    | false ⇒
164      match m with
165        [ Z ⇒ Z
166        | (S q) ⇒ S (division_aux q (n - (S p)) p)
167        ]
168    ].
169   
170ndefinition division ≝
171  λm, n: Nat.
172    match n with
173      [ Z ⇒ S m
174      | S o ⇒ division_aux m m o
175      ].
176     
177notation "hvbox(n break ÷ m)"
178  right associative with precedence 47
179  for @{ 'division $n $m }.
180 
181interpretation "Nat division" 'division n m = (division n m).
182     
183nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
184  match less_than_or_equal_b n p with
185    [ true ⇒ n
186    | false ⇒
187      match m with
188        [ Z ⇒ n
189        | S o ⇒ modulus_aux o (n - (S p)) p
190        ]
191    ].
192   
193ndefinition modulus ≝
194  λm, n: Nat.
195    match n with
196      [ Z ⇒ m
197      | S o ⇒ modulus_aux m m o
198      ].
199   
200notation "hvbox(n break 'mod' m)"
201  right associative with precedence 47
202  for @{ 'modulus $n $m }.
203 
204interpretation "Nat modulus" 'modulus m n = (modulus m n).
205
206ndefinition divide_with_remainder ≝
207  λm, n: Nat.
208    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
209
210(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
211(* Exponentials, and square roots.                                            *)
212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
213
214nlet rec exponential (m: Nat) (n: Nat) on n ≝
215  match n with
216    [ Z ⇒ S (Z)
217    | S o ⇒ m * exponential m o
218    ].
219   
220notation "hvbox(n ^ m)"
221  left associative with precedence 52
222  for @{ 'exponential $n $m }.
223 
224interpretation "Nat exponential" 'exponential n m = (exponential n m).
225
226nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝
227  match m with
228    [ Z ⇒
229      match n with
230        [ Z ⇒ true
231        | _ ⇒ false
232        ]
233    | S o ⇒
234      match n with
235        [ S p ⇒ eq_n o p
236        | _ ⇒ false
237        ]
238    ].
239
240(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
241(* Greatest common divisor and least common multiple.                         *)
242(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
243
244(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
245(* Axioms.                                                                    *)
246(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
247
248(*naxiom plus_minus_inverse_left:
249  ∀m, n: Nat.
250    (m + n) - n = m.
251*)
252 
253ntheorem less_than_or_equal_monotone:
254  ∀m, n: Nat.
255    m ≤ n → (S m) ≤ (S n).
256 #m n H; nelim H; /2/.
257nqed.
258
259nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l.
260 #n m l H H1; nelim H1; /2/.
261nqed.
262
263ntheorem less_than_or_equal_injective:
264  ∀m, n: Nat.
265    (S m) ≤ (S n) → m ≤ n.
266 #m n H;
267 nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]);
268 napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]);
269 nnormalize; /3/.
270nqed.
271   
272ntheorem succ_less_than_injective:
273  ∀m, n: Nat.
274    less_than_p (S m) (S n) → m < n.
275 /2/.
276nqed.
277
278nlemma not_less_than_S_Z:
279 ∀m,n: Nat. S m ≤ n → ¬ (n = Z).
280 #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ]
281nqed.
282
283ntheorem nothing_less_than_Z:
284  ∀m: Nat.
285    ¬(m < Z).
286 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
287nqed.
288
289   
290(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
291(* Lemmas.                                                                    *)
292(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
293   
294nlemma less_than_or_equal_zero:
295  ∀n: Nat.
296    Z ≤ n.
297  #n.
298  nelim n.
299  //.
300  #N.
301  napply ltoe_step.
302nqed.
303
304(*
305nlemma less_than_or_equal_zero_equal_zero:
306  ∀m: Nat.
307    m ≤ Z → m = Z.
308  #m.
309  nelim m.
310  //.
311  #N H H2.
312  nnormalize.
313*)
314
315nlemma less_than_or_equal_reflexive:
316  ∀n: Nat.
317    n ≤ n.
318  #n.
319  nelim n.
320  nnormalize.
321  @.
322  #N H.
323  nnormalize.
324  //.
325nqed.
326
327(*
328nlemma less_than_or_equal_succ:
329  ∀m, n: Nat.
330    S m ≤ n → m ≤ n.
331  #m n.
332  nelim m.
333  #H.
334  napplyS less_than_or_equal_zero.
335  #N H H2.
336  nrewrite > H.
337  nnormalize.
338
339nlemma less_than_or_equal_transitive:
340  ∀m, n, o: Nat.
341    m ≤ n ∧ n ≤ o → m ≤ o.
342  #m n o.
343  nelim m.
344  #H.
345  napply less_than_or_equal_zero.
346  #N H H2.
347  nnormalize.
348*)
349
350nlemma plus_zero:
351  ∀n: Nat.
352    n + Z = n.
353  #n.
354  nelim n.
355  nnormalize.
356  @.
357  #N H.
358  nnormalize.
359  nrewrite > H.
360  @.
361nqed.
362
363nlemma plus_associative:
364  ∀m, n, o: Nat.
365    (m + n) + o = m + (n + o).
366  #m n o.
367  nelim m.
368  nnormalize.
369  @.
370  #N H.
371  nnormalize.
372  nrewrite > H.
373  @.
374nqed.
375
376nlemma succ_plus:
377  ∀m, n: Nat.
378    S(m + n) = m + S(n).
379  #m n.
380  nelim m.
381  nnormalize.
382  @.
383  #N H.
384  nnormalize.
385  nrewrite > H.
386  @.
387nqed.
388
389nlemma succ_plus_succ_zero:
390  ∀n: Nat.
391    S n = plus n (S Z).
392  #n.
393  nelim n.
394  //.
395  #N H.
396  nnormalize.
397  nrewrite < H.
398  @.
399nqed.
400
401nlemma plus_symmetrical:
402  ∀m, n: Nat.
403    m + n = n + m.
404  #m n.
405  nelim m.
406  nnormalize.
407  nelim n.
408  nnormalize.
409  @.
410  #N H.
411  nnormalize.
412  nrewrite < H.
413  @.
414  #N H.
415  nnormalize.
416  nrewrite > H.
417  napply succ_plus.
418nqed.
419
420nlemma multiplication_zero_right_neutral:
421  ∀m: Nat.
422    m * Z = Z.
423  #m.
424  nelim m.
425  nnormalize.
426  @.
427  #N H.
428  nnormalize.
429  nrewrite > H.
430  @.
431nqed.
432
433nlemma multiplication_succ:
434  ∀m, n: Nat.
435    m * S(n) = m + (m * n).
436  #m n.
437  nelim m.
438  nnormalize.
439  @.
440  #N H.
441  nnormalize.
442  nrewrite > H.
443  nrewrite < (plus_associative n N ?).
444  nrewrite > (plus_symmetrical n N).
445  nrewrite > (plus_associative N n ?).
446  @.
447nqed.
448
449nlemma multiplication_symmetrical:
450  ∀m, n: Nat.
451    m * n = n * m.
452  #m n.
453  nelim m.
454  nnormalize.
455  nelim n.
456  nnormalize.
457  @.
458  #N H.
459  nnormalize.
460  nrewrite < H.
461  @.
462  #N H.
463  nnormalize.
464  nrewrite > H.
465  nrewrite > (multiplication_succ ? ?).
466  @.
467nqed.
468
469nlemma multiplication_succ_zero_left_neutral:
470  ∀m: Nat.
471    (S Z) * m = m.
472  #m.
473  nelim m.
474  nnormalize.
475  @.
476  #N H.
477  nnormalize.
478  nrewrite > (succ_plus ? ?).
479  nrewrite < (succ_plus_succ_zero ?).
480  @.
481nqed.
482
483nlemma multiplication_succ_zero_right_neutral:
484  ∀m: Nat.
485    m * (S Z) = m.
486  #m.
487  nelim m.
488  nnormalize.
489  @.
490  #N H.
491  nnormalize.
492  nrewrite > H.
493  @.
494nqed.
495
496nlemma multiplication_distributes_right_plus:
497  ∀m, n, o: Nat.
498    (m + n) * o = m * o + n * o.
499  #m n o.
500  nelim m.
501  nnormalize.
502  @.
503  #N H.
504  nnormalize.
505  nrewrite > H.
506  nrewrite < (plus_associative ? ? ?).
507  @.
508nqed.
509
510nlemma multiplication_distributes_left_plus:
511  ∀m, n, o: Nat.
512    o * (m + n) = o * m + o * n.
513  #m n o.
514  nelim o.
515  //.
516  #N H.
517  nnormalize.
518  nrewrite > H.
519  nrewrite < (plus_associative ? n (N * n)).
520  nrewrite > (plus_symmetrical (m + N * m) n).
521  nrewrite < (plus_associative n m (N * m)).
522  nrewrite < (plus_symmetrical n m).
523  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
524  @.
525nqed.
526
527nlemma mutliplication_associative:
528  ∀m, n, o: Nat.
529    m * (n * o) = (m * n) * o.
530  #m n o.
531  nelim m.
532  nnormalize.
533  @.
534  #N H.
535  nnormalize.
536  nrewrite > H.
537  nrewrite > (multiplication_distributes_right_plus ? ? ?).
538  @.
539nqed.
540
541nlemma minus_minus:
542  ∀n: Nat.
543    n - n = Z.
544  #n.
545  nelim n.
546  nnormalize.
547  @.
548  #N H.
549  nnormalize.
550  nrewrite > H.
551  @.
552nqed.
553
554
555nlemma succ_injective:
556  ∀m, n: Nat.
557    S m = S n → m = n.
558  #m n H;
559  napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with
560           [refl ⇒ ? ]);
561  @;
562nqed.
563
564ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'.
565 //;
566nqed.
567
568ntheorem plus_minus_inverse_right:
569  ∀m, n: Nat.
570   n ≤ m → (m - n) + n = m.
571 #m; nelim m
572  [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1);
573    #K; ncases (K H3)
574  | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/;
575    #w; nrewrite < succ_plus; /4/. ##]
576nqed.
577
578(*
579
580nlemma plus_minus_associate:
581  ∀m, n, o: Nat.
582    (m + n) - o = m + (n - o).
583  #m n o.
584  nelim m.
585  nnormalize.
586  @.
587  #N H.
588 
589
590nlemma plus_minus_inverses:
591  ∀m, n: Nat.
592    (m + n) - n = m.
593  #m n.
594  nelim m.
595  nnormalize.
596  napply minus_minus.
597  #N H.
598*)
599
600ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n.
601 #m; nelim m; //; #y H1 z; ncases z; nnormalize
602  [ #H; ndestruct | /3/ ]
603nqed.
604
605ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n).
606 #m; nelim m; nnormalize
607  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
608    [ #H; ndestruct | /3/ ] /2/.
609nqed.
610
611ndefinition less_than_or_equal_b_elim:
612 ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
613  P (less_than_or_equal_b m n).
614 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
615 nlapply (less_than_or_equal_b_complete m n);
616 ncases (less_than_or_equal_b m n); /3/.
617nqed.
618
619ndefinition greater_than_or_equal_b_elim:
620 ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) →
621  P (greater_than_or_equal_b m n).
622 #m n; napply less_than_or_equal_b_elim;
623nqed.
624
625ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n.
626 #m; nelim m
627  [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ]
628##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K;
629    napply less_than_or_equal_monotone; napply H; napply K ]
630nqed.
631
632ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n).
633 #m; nelim m
634  [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct
635  | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/.
636nqed.
637
638ndefinition less_than_b_elim:
639 ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) →
640  P (less_than_b m n).
641 #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n);
642 ncases (less_than_b m n); /3/.
643nqed.
644
645ndefinition greater_than_b_elim:
646 ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) →
647  P (greater_than_b m n).
648 #m n; napply less_than_b_elim.
649nqed.
Note: See TracBrowser for help on using the repository browser.