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

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

Commit to restore deleted file.

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