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

Last change on this file since 234 was 234, checked in by mulligan, 9 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.