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

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

Changes to get directory to compile.

File size: 10.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).
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 ≝
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, n: Nat.
60    m ≤ n ∧ ¬(m = n).
61   
62notation "hvbox(n break < m)"
63  non associative with precedence 47
64  for @{ 'less_than $n $m }.
65 
66interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
67
68ndefinition greater_than_p ≝
69  λm, n: Nat.
70    n < m.
71   
72notation "hvbox(n break > m)"
73  non associative with precedence 47
74  for @{ 'greater_than $n $m }.
75 
76interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
77
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
79(* Addition and subtraction.                                                  *)
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
81nlet rec plus (n: Nat) (o: Nat) on n ≝
82  match n with
83    [ Z ⇒ o
84    | S p ⇒ S (plus p o)
85    ].
86   
87notation "hvbox(n break + m)"
88  right associative with precedence 52
89  for @{ 'plus $n $m }.
90 
91interpretation "Nat plus" 'plus n m = (plus n m).
92   
93nlet rec minus (n: Nat) (o: Nat) on n ≝
94  match n with
95    [ Z ⇒ Z
96    | S p ⇒
97      match o with
98        [ Z ⇒ S p
99        | S q ⇒ minus p q
100        ]
101    ].
102   
103notation "hvbox(n break - m)"
104  right associative with precedence 47
105  for @{ 'minus $n $m }.
106 
107interpretation "Nat minus" 'minus n m = (minus n m).
108
109(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
110(* Multiplication, modulus and division.                                      *)
111(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
112   
113nlet rec multiplication (n: Nat) (o: Nat) on n ≝
114  match n with
115    [ Z ⇒ Z
116    | S p ⇒ o + (multiplication p o)
117    ].
118   
119notation "hvbox(n break * m)"
120  right associative with precedence 47
121  for @{ 'multiplication $n $m }.
122 
123interpretation "Nat multiplication" 'times n m = (multiplication n m).
124
125nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
126  match n ≤ p with
127    [ True ⇒ Z
128    | False ⇒
129      match m with
130        [ Z ⇒ Z
131        | (S q) ⇒ S (division_aux q (n - (S p)) p)
132        ]
133    ].
134   
135ndefinition division ≝
136  λm, n: Nat.
137    match n with
138      [ Z ⇒ S m
139      | S o ⇒ division_aux m m o
140      ].
141     
142notation "hvbox(n break ÷ m)"
143  right associative with precedence 47
144  for @{ 'division $n $m }.
145 
146interpretation "Nat division" 'division n m = (division n m).
147     
148nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
149  match n ≤ p with
150    [ True ⇒ n
151    | False ⇒
152      match m with
153        [ Z ⇒ n
154        | S o ⇒ modulus_aux o (n - (S p)) p
155        ]
156    ].
157   
158ndefinition modulus ≝
159  λm, n: Nat.
160    match n with
161      [ Z ⇒ m
162      | S o ⇒ modulus_aux m m o
163      ].
164   
165notation "hvbox(n break % m)"
166  right associative with precedence 47
167  for @{ 'modulus $n $m }.
168 
169interpretation "Nat modulus" 'modulus m n = (modulus m n).
170
171ndefinition divide_with_remainder ≝
172  λm, n: Nat.
173    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
174
175(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
176(* Exponentials, and square roots.                                            *)
177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
178
179nlet rec exponential (m: Nat) (n: Nat) on n ≝
180  match n with
181    [ Z ⇒ S (Z)
182    | S o ⇒ m * exponential m o
183    ].
184   
185notation "hvbox(n ^ m)"
186  left associative with precedence 52
187  for @{ 'exponential $n $m }.
188 
189interpretation "Nat exponential" 'exponential n m = (exponential n m).
190
191(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
192(* Greatest common divisor and least common multiple.                         *)
193(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
194
195(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
196(* Lemmas.                                                                    *)
197(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
198
199nlemma less_than_or_equal_zero:
200  ∀n: Nat.
201    Z ≤ n.
202  #n.
203  nelim n.
204  //.
205  #N.
206  napply ltoe_step.
207nqed.
208
209(*
210nlemma less_than_or_equal_injective:
211  ∀m, n: Nat.
212    S m ≤ S n → m ≤ n.
213  #m n.
214  nelim m.
215  #H.
216  napplyS less_than_or_equal_zero.
217  #N H H2.
218  ndestruct.
219
220nlemma less_than_or_equal_zero_equal_zero:
221  ∀m: Nat.
222    m ≤ Z → m = Z.
223  #m.
224  nelim m.
225  //.
226  #N H H2.
227  nnormalize.
228*)
229
230nlemma less_than_or_equal_reflexive:
231  ∀n: Nat.
232    n ≤ n.
233  #n.
234  nelim n.
235  nnormalize.
236  @.
237  #N H.
238  nnormalize.
239  //.
240nqed.
241
242(*
243nlemma less_than_or_equal_succ:
244  ∀m, n: Nat.
245    S m ≤ n → m ≤ n.
246  #m n.
247  nelim m.
248  #H.
249  napplyS less_than_or_equal_zero.
250  #N H H2.
251  //.
252  napplyS H.
253
254
255nlemma less_than_or_equal_transitive:
256  ∀m, n, o: Nat.
257    m ≤ n ∧ n ≤ o → m ≤ o.
258  #m n o.
259  nelim m.
260  #H.
261  napply less_than_or_equal_zero.
262  #N H H2.
263  nnormalize.
264  #;
265*)
266
267nlemma plus_zero:
268  ∀n: Nat.
269    n + Z = n.
270  #n.
271  nelim n.
272  nnormalize.
273  @.
274  #N H.
275  nnormalize.
276  nrewrite > H.
277  @.
278nqed.
279
280nlemma plus_associative:
281  ∀m, n, o: Nat.
282    (m + n) + o = m + (n + o).
283  #m n o.
284  nelim m.
285  nnormalize.
286  @.
287  #N H.
288  nnormalize.
289  nrewrite > H.
290  @.
291nqed.
292
293nlemma succ_plus:
294  ∀m, n: Nat.
295    S(m + n) = m + S(n).
296  #m n.
297  nelim m.
298  nnormalize.
299  @.
300  #N H.
301  nnormalize.
302  nrewrite > H.
303  @.
304nqed.
305
306nlemma succ_plus_succ_zero:
307  ∀n: Nat.
308    S n = plus n (S Z).
309  #n.
310  nelim n.
311  //.
312  #N H.
313  nnormalize.
314  nrewrite < H.
315  @.
316nqed.
317
318nlemma plus_symmetrical:
319  ∀m, n: Nat.
320    m + n = n + m.
321  #m n.
322  nelim m.
323  nnormalize.
324  nelim n.
325  nnormalize.
326  @.
327  #N H.
328  nnormalize.
329  nrewrite < H.
330  @.
331  #N H.
332  nnormalize.
333  nrewrite > H.
334  napplyS succ_plus.
335nqed.
336
337nlemma multiplication_zero_right_neutral:
338  ∀m: Nat.
339    m * Z = Z.
340  #m.
341  nelim m.
342  nnormalize.
343  @.
344  #N H.
345  nnormalize.
346  nrewrite > H.
347  @.
348nqed.
349
350nlemma multiplication_succ:
351  ∀m, n: Nat.
352    m * S(n) = m + (m * n).
353  #m n.
354  nelim m.
355  nnormalize.
356  @.
357  #N H.
358  nnormalize.
359  nrewrite > H.
360  nrewrite < (plus_associative n N ?).
361  nrewrite > (plus_symmetrical n N).
362  nrewrite > (plus_associative N n ?).
363  @.
364nqed.
365
366nlemma multiplication_symmetrical:
367  ∀m, n: Nat.
368    m * n = n * m.
369  #m n.
370  nelim m.
371  nnormalize.
372  nelim n.
373  nnormalize.
374  @.
375  #N H.
376  nnormalize.
377  nrewrite < H.
378  @.
379  #N H.
380  nnormalize.
381  nrewrite > H.
382  nrewrite > (multiplication_succ ? ?).
383  @.
384nqed.
385
386nlemma multiplication_succ_zero_left_neutral:
387  ∀m: Nat.
388    (S Z) * m = m.
389  #m.
390  nelim m.
391  nnormalize.
392  @.
393  #N H.
394  nnormalize.
395  nrewrite > (succ_plus ? ?).
396  nrewrite < (succ_plus_succ_zero ?).
397  @.
398nqed.
399
400nlemma multiplication_succ_zero_right_neutral:
401  ∀m: Nat.
402    m * (S Z) = m.
403  #m.
404  nelim m.
405  nnormalize.
406  @.
407  #N H.
408  nnormalize.
409  nrewrite > H.
410  @.
411nqed.
412
413nlemma multiplication_distributes_right_plus:
414  ∀m, n, o: Nat.
415    (m + n) * o = m * o + n * o.
416  #m n o.
417  nelim m.
418  nnormalize.
419  @.
420  #N H.
421  nnormalize.
422  nrewrite > H.
423  nrewrite < (plus_associative ? ? ?).
424  @.
425nqed.
426
427nlemma multiplication_distributes_left_plus:
428  ∀m, n, o: Nat.
429    o * (m + n) = o * m + o * n.
430  #m n o.
431  nelim o.
432  //.
433  #N H.
434  nnormalize.
435  nrewrite > H.
436  nrewrite < (plus_associative ? n (N * n)).
437  nrewrite > (plus_symmetrical (m + N * m) n).
438  nrewrite < (plus_associative n m (N * m)).
439  nrewrite < (plus_symmetrical n m).
440  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
441  @.
442nqed.
443
444nlemma mutliplication_associative:
445  ∀m, n, o: Nat.
446    m * (n * o) = (m * n) * o.
447  #m n o.
448  nelim m.
449  nnormalize.
450  @.
451  #N H.
452  nnormalize.
453  nrewrite > H.
454  nrewrite > (multiplication_distributes_right_plus ? ? ?).
455  @.
456nqed.
457
458nlemma minus_minus:
459  ∀n: Nat.
460    n - n = Z.
461  #n.
462  nelim n.
463  nnormalize.
464  @.
465  #N H.
466  nnormalize.
467  nrewrite > H.
468  @.
469nqed.
470
471(*
472nlemma succ_injective:
473  ∀m, n: Nat.
474    S m = S n → m = n.
475  #m n.
476  nelim m.
477  #H.
478  ninversion H.
479  #H.
480  ndestruct
481
482nlemma plus_minus_associate:
483  ∀m, n, o: Nat.
484    (m + n) - o = m + (n - o).
485  #m n o.
486  nelim m.
487  nnormalize.
488  @.
489  #N H.
490 
491
492nlemma plus_minus_inverses:
493  ∀m, n: Nat.
494    (m + n) - n = m.
495  #m n.
496  nelim m.
497  nnormalize.
498  napply minus_minus.
499  #N H.
500*)
Note: See TracBrowser for help on using the repository browser.