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

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

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

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