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

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

More functions on bitvectors written.

File size: 9.6 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 "hvbox(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 "hvbox(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 "hvbox(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 "hvbox(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 "hvbox(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 "hvbox(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 "hvbox(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 "hvbox(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 "hvbox(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
173ndefinition divide_with_remainder ≝
174  λm, n: Nat.
175    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
176
177(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
178(* Exponentials, and square roots.                                            *)
179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
180
181nlet rec exponential (m: Nat) (n: Nat) on n ≝
182  match n with
183    [ Z ⇒ S (Z)
184    | S o ⇒ m * exponential m o
185    ].
186   
187notation "hvbox(n ^ m)"
188  left associative with precedence 52
189  for @{ 'exponential $n $m }.
190 
191interpretation "Nat exponential" 'exponential n m = (exponential n m).
192
193(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
194(* Greatest common divisor and least common multiple.                         *)
195(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
196
197(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
198(* Lemmas.                                                                    *)
199(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
200
201nlemma less_than_or_equal_zero:
202  ∀n: Nat.
203    Z ≤ n.
204  #n.
205  nelim n.
206  //.
207  #N.
208  napply ltoe_step.
209nqed.
210
211(*
212nlemma less_than_or_equal_injective:
213  ∀m, n: Nat.
214    S m ≤ S n → m ≤ n.
215  #m n.
216  nelim m.
217  #H.
218  napplyS less_than_or_equal_zero.
219  #N H H2.
220  ndestruct.
221
222nlemma less_than_or_equal_zero_equal_zero:
223  ∀m: Nat.
224    m ≤ Z → m = Z.
225  #m.
226  nelim m.
227  //.
228  #N H H2.
229  nnormalize.
230*)
231
232nlemma less_than_or_equal_reflexive:
233  ∀n: Nat.
234    n ≤ n.
235  #n.
236  nelim n.
237  nnormalize.
238  @.
239  #N H.
240  nnormalize.
241  //.
242nqed.
243
244(*
245nlemma less_than_or_equal_succ:
246  ∀m, n: Nat.
247    S m ≤ n → m ≤ n.
248  #m n.
249  nelim m.
250  #H.
251  napplyS less_than_or_equal_zero.
252  #N H H2.
253  //.
254  napplyS H.
255
256
257nlemma less_than_or_equal_transitive:
258  ∀m, n, o: Nat.
259    m ≤ n ∧ n ≤ o → m ≤ o.
260  #m n o.
261  nelim m.
262  #H.
263  napply less_than_or_equal_zero.
264  #N H H2.
265  nnormalize.
266  #;
267*)
268
269nlemma plus_zero:
270  ∀n: Nat.
271    n + Z = n.
272  #n.
273  nelim n.
274  nnormalize.
275  @.
276  #N H.
277  nnormalize.
278  nrewrite > H.
279  @.
280nqed.
281
282nlemma plus_associative:
283  ∀m, n, o: Nat.
284    (m + n) + o = m + (n + o).
285  #m n o.
286  nelim m.
287  nnormalize.
288  @.
289  #N H.
290  nnormalize.
291  nrewrite > H.
292  @.
293nqed.
294
295nlemma succ_plus:
296  ∀m, n: Nat.
297    S(m + n) = m + S(n).
298  #m n.
299  nelim m.
300  nnormalize.
301  @.
302  #N H.
303  nnormalize.
304  nrewrite > H.
305  @.
306nqed.
307
308nlemma succ_plus_succ_zero:
309  ∀n: Nat.
310    S n = plus n (S Z).
311  #n.
312  nelim n.
313  //.
314  #N 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  //.
360nqed.
361
362nlemma multiplication_symmetrical:
363  ∀m, n: Nat.
364    m * n = n * m.
365  #m n.
366  nelim m.
367  nnormalize.
368  nelim n.
369  nnormalize.
370  @.
371  #N H.
372  nnormalize.
373  nrewrite < H.
374  @.
375  #N H.
376  nnormalize.
377  nrewrite > H.
378  napplyS multiplication_succ.
379nqed.
380
381nlemma multiplication_succ_zero_left_neutral:
382  ∀m: Nat.
383    (S Z) * m = m.
384  #m.
385  nelim m.
386  nnormalize.
387  @.
388  #N H.
389  nnormalize.
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  napplyS plus_associative.
417nqed.
418
419nlemma multiplication_distributes_left_plus:
420  ∀m, n, o: Nat.
421    o * (m + n) = o * m + o * n.
422  #m n o.
423  napplyS multiplication_symmetrical.
424nqed.
425
426nlemma mutliplication_associative:
427  ∀m, n, o: Nat.
428    m * (n * o) = (m * n) * o.
429  #m n o.
430  nelim m.
431  nnormalize.
432  @.
433  #N H.
434  nnormalize.
435  nrewrite > H.
436  napplyS multiplication_distributes_right_plus.
437nqed.
438
439nlemma minus_minus:
440  ∀n: Nat.
441    n - n = Z.
442  #n.
443  nelim n.
444  nnormalize.
445  @.
446  #N H.
447  nnormalize.
448  nrewrite > H.
449  @.
450nqed.
451
452(*
453nlemma succ_injective:
454  ∀m, n: Nat.
455    S m = S n → m = n.
456  #m n.
457  nelim m.
458  #H.
459  ninversion H.
460  #H.
461  ndestruct
462
463nlemma plus_minus_associate:
464  ∀m, n, o: Nat.
465    (m + n) - o = m + (n - o).
466  #m n o.
467  nelim m.
468  nnormalize.
469  @.
470  #N H.
471 
472
473nlemma plus_minus_inverses:
474  ∀m, n: Nat.
475    (m + n) - n = m.
476  #m n.
477  nelim m.
478  nnormalize.
479  napply minus_minus.
480  #N H.
481*)
Note: See TracBrowser for help on using the repository browser.