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

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

Strange problem with matita and the Maybe file? Cannot find Maybe.ng.

File size: 9.0 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4include "Cartesian.ma".
5include "Bool.ma".
6
7include "logic/pts.ma".
8include "Plogic/equality.ma".
9include "Plogic/connectives.ma".
10
11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
12(* The datatype.                                                              *)
13(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
14ninductive Nat: Type[0] ≝
15  Z: Nat
16| S: Nat → Nat.
17
18(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
19(* Orderings.                                                                 *)
20(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
21
22ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
23  ltoe_refl: less_than_or_equal_p n n
24| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
25
26nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
27  match m with
28    [ Z ⇒ True
29    | S o ⇒
30      match n with
31        [ Z ⇒ False
32        | S p ⇒ less_than_or_equal_b o p
33        ]
34    ].
35   
36notation "n break ≤ m"
37  non associative with precedence 47
38  for @{ 'less_than_or_equal $n $m }.
39 
40interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
41interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
42
43ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
44  λm, n: Nat.
45    n ≤ m.
46
47ndefinition greater_than_or_equal_b ≝
48  λm, n: Nat.
49    n ≤ m.
50   
51notation "n break ≥ m"
52  non associative with precedence 47
53  for @{ 'greater_than_or_equal $n $m }.
54 
55
56interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
57interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
58
59(* Add Boolean versions.                                                      *)
60ndefinition less_than_p ≝
61  λm, n: Nat.
62    m ≤ n ∧ ¬(m = n).
63   
64notation "n break < m"
65  non associative with precedence 47
66  for @{ 'less_than $n $m }.
67 
68interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
69
70ndefinition greater_than_p ≝
71  λm, n: Nat.
72    n < m.
73   
74notation "n break > m"
75  non associative with precedence 47
76  for @{ 'greater_than $n $m }.
77 
78interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
79
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
81(* Addition and subtraction.                                                  *)
82(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
83nlet rec plus (n: Nat) (o: Nat) on n ≝
84  match n with
85    [ Z ⇒ o
86    | S p ⇒ S (plus p o)
87    ].
88   
89notation "n break + m"
90  right associative with precedence 52
91  for @{ 'plus $n $m }.
92 
93interpretation "Nat plus" 'plus n m = (plus n m).
94   
95nlet rec minus (n: Nat) (o: Nat) on n ≝
96  match n with
97    [ Z ⇒ Z
98    | S p ⇒
99      match o with
100        [ Z ⇒ S p
101        | S q ⇒ minus p q
102        ]
103    ].
104   
105notation "n break - m"
106  right associative with precedence 47
107  for @{ 'minus $n $m }.
108 
109interpretation "Nat minus" 'minus n m = (minus n m).
110
111(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
112(* Multiplication, modulus and division.                                      *)
113(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
114   
115nlet rec multiplication (n: Nat) (o: Nat) on n ≝
116  match n with
117    [ Z ⇒ Z
118    | S p ⇒ o + (multiplication p o)
119    ].
120   
121notation "n break * m"
122  right associative with precedence 47
123  for @{ 'multiplication $n $m }.
124 
125interpretation "Nat multiplication" 'times n m = (multiplication n m).
126
127nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
128  match n ≤ p with
129    [ True ⇒ Z
130    | False ⇒
131      match m with
132        [ Z ⇒ Z
133        | (S q) ⇒ S (division_aux q (n - (S p)) p)
134        ]
135    ].
136   
137ndefinition division ≝
138  λm, n: Nat.
139    match n with
140      [ Z ⇒ S m
141      | S o ⇒ division_aux m m o
142      ].
143     
144notation "n break ÷ m"
145  right associative with precedence 47
146  for @{ 'division $n $m }.
147 
148interpretation "Nat division" 'division n m = (division n m).
149     
150nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
151  match n ≤ p with
152    [ True ⇒ n
153    | False ⇒
154      match m with
155        [ Z ⇒ n
156        | S o ⇒ modulus_aux o (n - (S p)) p
157        ]
158    ].
159   
160ndefinition modulus ≝
161  λm, n: Nat.
162    match n with
163      [ Z ⇒ m
164      | S o ⇒ modulus_aux m m o
165      ].
166   
167notation "n break % m"
168  right associative with precedence 47
169  for @{ 'modulus $n $m }.
170 
171interpretation "Nat modulus" 'modulus m n = (modulus m n).
172
173(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
174(* Greatest common divisor and least common multiple.                         *)
175(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
176
177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
178(* Lemmas.                                                                    *)
179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
180
181nlemma less_than_or_equal_zero:
182  ∀n: Nat.
183    Z ≤ n.
184  #n.
185  nelim n.
186  //.
187  #N.
188  napply ltoe_step.
189nqed.
190
191(*
192nlemma less_than_or_equal_injective:
193  ∀m, n: Nat.
194    S m ≤ S n → m ≤ n.
195  #m n.
196  nelim m.
197  #H.
198  napplyS less_than_or_equal_zero.
199  #N H H2.
200  ndestruct.
201
202nlemma less_than_or_equal_zero_equal_zero:
203  ∀m: Nat.
204    m ≤ Z → m = Z.
205  #m.
206  nelim m.
207  //.
208  #N H H2.
209  nnormalize.
210*)
211
212nlemma less_than_or_equal_reflexive:
213  ∀n: Nat.
214    n ≤ n.
215  #n.
216  nelim n.
217  nnormalize.
218  @.
219  #N H.
220  nnormalize.
221  //.
222nqed.
223
224(*
225nlemma less_than_or_equal_succ:
226  ∀m, n: Nat.
227    S m ≤ n → m ≤ n.
228  #m n.
229  nelim m.
230  #H.
231  napplyS less_than_or_equal_zero.
232  #N H H2.
233  //.
234  napplyS H.
235
236
237nlemma less_than_or_equal_transitive:
238  ∀m, n, o: Nat.
239    m ≤ n ∧ n ≤ o → m ≤ o.
240  #m n o.
241  nelim m.
242  #H.
243  napply less_than_or_equal_zero.
244  #N H H2.
245  nnormalize.
246  #;
247*)
248
249nlemma plus_zero:
250  ∀n: Nat.
251    n + Z = n.
252  #n.
253  nelim n.
254  nnormalize.
255  @.
256  #N H.
257  nnormalize.
258  nrewrite > H.
259  @.
260nqed.
261
262nlemma plus_associative:
263  ∀m, n, o: Nat.
264    (m + n) + o = m + (n + o).
265  #m n o.
266  nelim m.
267  nnormalize.
268  @.
269  #N H.
270  nnormalize.
271  nrewrite > H.
272  @.
273nqed.
274
275nlemma succ_plus:
276  ∀m, n: Nat.
277    S(m + n) = m + S(n).
278  #m n.
279  nelim m.
280  nnormalize.
281  @.
282  #N H.
283  nnormalize.
284  nrewrite > H.
285  @.
286nqed.
287
288nlemma succ_plus_succ_zero:
289  ∀n: Nat.
290    S n = plus n (S Z).
291  #n.
292  nelim n.
293  //.
294  #N H.
295  //.
296nqed.
297
298nlemma plus_symmetrical:
299  ∀m, n: Nat.
300    m + n = n + m.
301  #m n.
302  nelim m.
303  nnormalize.
304  nelim n.
305  nnormalize.
306  @.
307  #N H.
308  nnormalize.
309  nrewrite < H.
310  @.
311  #N H.
312  nnormalize.
313  nrewrite > H.
314  napplyS succ_plus.
315nqed.
316
317nlemma multiplication_zero_right_neutral:
318  ∀m: Nat.
319    m * Z = Z.
320  #m.
321  nelim m.
322  nnormalize.
323  @.
324  #N H.
325  nnormalize.
326  nrewrite > H.
327  @.
328nqed.
329
330nlemma multiplication_succ:
331  ∀m, n: Nat.
332    m * S(n) = m + (m * n).
333  #m n.
334  nelim m.
335  nnormalize.
336  @.
337  #N H.
338  nnormalize.
339  //.
340nqed.
341
342nlemma multiplication_symmetrical:
343  ∀m, n: Nat.
344    m * n = n * m.
345  #m n.
346  nelim m.
347  nnormalize.
348  nelim n.
349  nnormalize.
350  @.
351  #N H.
352  nnormalize.
353  nrewrite < H.
354  @.
355  #N H.
356  nnormalize.
357  nrewrite > H.
358  napplyS multiplication_succ.
359nqed.
360
361nlemma multiplication_succ_zero_left_neutral:
362  ∀m: Nat.
363    (S Z) * m = m.
364  #m.
365  nelim m.
366  nnormalize.
367  @.
368  #N H.
369  nnormalize.
370  //.
371nqed.
372
373nlemma multiplication_succ_zero_right_neutral:
374  ∀m: Nat.
375    m * (S Z) = m.
376  #m.
377  nelim m.
378  nnormalize.
379  @.
380  #N H.
381  nnormalize.
382  nrewrite > H.
383  @.
384nqed.
385
386nlemma multiplication_distributes_right_plus:
387  ∀m, n, o: Nat.
388    (m + n) * o = m * o + n * o.
389  #m n o.
390  nelim m.
391  nnormalize.
392  @.
393  #N H.
394  nnormalize.
395  nrewrite > H.
396  napplyS plus_associative.
397nqed.
398
399nlemma multiplication_distributes_left_plus:
400  ∀m, n, o: Nat.
401    o * (m + n) = o * m + o * n.
402  #m n o.
403  napplyS multiplication_symmetrical.
404nqed.
405
406nlemma mutliplication_associative:
407  ∀m, n, o: Nat.
408    m * (n * o) = (m * n) * o.
409  #m n o.
410  nelim m.
411  nnormalize.
412  @.
413  #N H.
414  nnormalize.
415  nrewrite > H.
416  napplyS multiplication_distributes_right_plus.
417nqed.
418
419nlemma minus_minus:
420  ∀n: Nat.
421    n - n = Z.
422  #n.
423  nelim n.
424  nnormalize.
425  @.
426  #N H.
427  nnormalize.
428  nrewrite > H.
429  @.
430nqed.
431
432(*
433nlemma succ_injective:
434  ∀m, n: Nat.
435    S m = S n → m = n.
436  #m n.
437  nelim m.
438  #H.
439  ninversion H.
440  #H.
441  ndestruct
442
443nlemma plus_minus_associate:
444  ∀m, n, o: Nat.
445    (m + n) - o = m + (n - o).
446  #m n o.
447  nelim m.
448  nnormalize.
449  @.
450  #N H.
451 
452
453nlemma plus_minus_inverses:
454  ∀m, n: Nat.
455    (m + n) - n = m.
456  #m n.
457  nelim m.
458  nnormalize.
459  napply minus_minus.
460  #N H.
461*)
Note: See TracBrowser for help on using the repository browser.