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

Last change on this file since 352 was 352, checked in by mulligan, 9 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.