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

Last change on this file since 289 was 277, checked in by sacerdot, 9 years ago

Bugs fixed in definition of sub8_with_carrier.

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