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

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

less axioms

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