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

Last change on this file since 246 was 246, checked in by mulligan, 9 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
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4include "Cartesian.ma".
5include "Bool.ma".
6
7include "Connectives.ma".
8
9(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
10(* The datatype.                                                              *)
11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
12ninductive Nat: Type[0] ≝
13  Z: Nat
14| S: Nat → Nat.
15
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   
34notation "hvbox(n break ≤ m)"
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   
49notation "hvbox(n break ≥ m)"
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   
62notation "hvbox(n break < m)"
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   
72notation "hvbox(n break > m)"
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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
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   
87notation "hvbox(n break + m)"
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   
103notation "hvbox(n break - m)"
104  right associative with precedence 47
105  for @{ 'minus $n $m }.
106 
107interpretation "Nat minus" 'minus n m = (minus n m).
108
109(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
110(* Multiplication, modulus and division.                                      *)
111(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
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   
119notation "hvbox(n break * m)"
120  right associative with precedence 47
121  for @{ 'multiplication $n $m }.
122 
123interpretation "Nat multiplication" 'times n m = (multiplication n m).
124
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)
132        ]
133    ].
134   
135ndefinition division ≝
136  λm, n: Nat.
137    match n with
138      [ Z ⇒ S m
139      | S o ⇒ division_aux m m o
140      ].
141     
142notation "hvbox(n break ÷ m)"
143  right associative with precedence 47
144  for @{ 'division $n $m }.
145 
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 ≝
159  λm, n: Nat.
160    match n with
161      [ Z ⇒ m
162      | S o ⇒ modulus_aux m m o
163      ].
164   
165notation "hvbox(n break % m)"
166  right associative with precedence 47
167  for @{ 'modulus $n $m }.
168 
169interpretation "Nat modulus" 'modulus m n = (modulus m n).
170
171ndefinition divide_with_remainder ≝
172  λm, n: Nat.
173    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
174
175(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
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(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
192(* Greatest common divisor and least common multiple.                         *)
193(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
194
195(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
196(* Lemmas.                                                                    *)
197(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
198
199nlemma less_than_or_equal_zero:
200  ∀n: Nat.
201    Z ≤ n.
202  #n.
203  nelim n.
204  //.
205  #N.
206  napply ltoe_step.
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
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
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
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
335nlemma multiplication_zero_right_neutral:
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.
357  //.
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.
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.
388  //.
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.