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

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

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

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