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

Last change on this file since 235 was 234, checked in by mulligan, 10 years ago

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

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