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

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

Test commit.

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