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

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

Strengthened typings of get_ and set_index in Vector file.

File size: 10.0 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
209naxiom less_than_or_equal_injective:
210  ∀m, n: Nat.
211    S m ≤ S n → m ≤ n.
212
213(*
214nlemma less_than_or_equal_zero_equal_zero:
215  ∀m: Nat.
216    m ≤ Z → m = Z.
217  #m.
218  nelim m.
219  //.
220  #N H H2.
221  nnormalize.
222*)
223
224nlemma less_than_or_equal_reflexive:
225  ∀n: Nat.
226    n ≤ n.
227  #n.
228  nelim n.
229  nnormalize.
230  @.
231  #N H.
232  nnormalize.
233  //.
234nqed.
235
236(*
237nlemma less_than_or_equal_succ:
238  ∀m, n: Nat.
239    S m ≤ n → m ≤ n.
240  #m n.
241  nelim m.
242  #H.
243  napplyS less_than_or_equal_zero.
244  #N H H2.
245  nrewrite > H.
246  nnormalize.
247
248nlemma less_than_or_equal_transitive:
249  ∀m, n, o: Nat.
250    m ≤ n ∧ n ≤ o → m ≤ o.
251  #m n o.
252  nelim m.
253  #H.
254  napply less_than_or_equal_zero.
255  #N H H2.
256  nnormalize.
257*)
258
259nlemma plus_zero:
260  ∀n: Nat.
261    n + Z = n.
262  #n.
263  nelim n.
264  nnormalize.
265  @.
266  #N H.
267  nnormalize.
268  nrewrite > H.
269  @.
270nqed.
271
272nlemma plus_associative:
273  ∀m, n, o: Nat.
274    (m + n) + o = m + (n + o).
275  #m n o.
276  nelim m.
277  nnormalize.
278  @.
279  #N H.
280  nnormalize.
281  nrewrite > H.
282  @.
283nqed.
284
285nlemma succ_plus:
286  ∀m, n: Nat.
287    S(m + n) = m + S(n).
288  #m n.
289  nelim m.
290  nnormalize.
291  @.
292  #N H.
293  nnormalize.
294  nrewrite > H.
295  @.
296nqed.
297
298nlemma succ_plus_succ_zero:
299  ∀n: Nat.
300    S n = plus n (S Z).
301  #n.
302  nelim n.
303  //.
304  #N H.
305  nnormalize.
306  nrewrite < H.
307  @.
308nqed.
309
310nlemma plus_symmetrical:
311  ∀m, n: Nat.
312    m + n = n + m.
313  #m n.
314  nelim m.
315  nnormalize.
316  nelim n.
317  nnormalize.
318  @.
319  #N H.
320  nnormalize.
321  nrewrite < H.
322  @.
323  #N H.
324  nnormalize.
325  nrewrite > H.
326  napplyS succ_plus.
327nqed.
328
329nlemma multiplication_zero_right_neutral:
330  ∀m: Nat.
331    m * Z = Z.
332  #m.
333  nelim m.
334  nnormalize.
335  @.
336  #N H.
337  nnormalize.
338  nrewrite > H.
339  @.
340nqed.
341
342nlemma multiplication_succ:
343  ∀m, n: Nat.
344    m * S(n) = m + (m * n).
345  #m n.
346  nelim m.
347  nnormalize.
348  @.
349  #N H.
350  nnormalize.
351  nrewrite > H.
352  nrewrite < (plus_associative n N ?).
353  nrewrite > (plus_symmetrical n N).
354  nrewrite > (plus_associative N n ?).
355  @.
356nqed.
357
358nlemma multiplication_symmetrical:
359  ∀m, n: Nat.
360    m * n = n * m.
361  #m n.
362  nelim m.
363  nnormalize.
364  nelim n.
365  nnormalize.
366  @.
367  #N H.
368  nnormalize.
369  nrewrite < H.
370  @.
371  #N H.
372  nnormalize.
373  nrewrite > H.
374  nrewrite > (multiplication_succ ? ?).
375  @.
376nqed.
377
378nlemma multiplication_succ_zero_left_neutral:
379  ∀m: Nat.
380    (S Z) * m = m.
381  #m.
382  nelim m.
383  nnormalize.
384  @.
385  #N H.
386  nnormalize.
387  nrewrite > (succ_plus ? ?).
388  nrewrite < (succ_plus_succ_zero ?).
389  @.
390nqed.
391
392nlemma multiplication_succ_zero_right_neutral:
393  ∀m: Nat.
394    m * (S Z) = m.
395  #m.
396  nelim m.
397  nnormalize.
398  @.
399  #N H.
400  nnormalize.
401  nrewrite > H.
402  @.
403nqed.
404
405nlemma multiplication_distributes_right_plus:
406  ∀m, n, o: Nat.
407    (m + n) * o = m * o + n * o.
408  #m n o.
409  nelim m.
410  nnormalize.
411  @.
412  #N H.
413  nnormalize.
414  nrewrite > H.
415  nrewrite < (plus_associative ? ? ?).
416  @.
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  nelim o.
424  //.
425  #N H.
426  nnormalize.
427  nrewrite > H.
428  nrewrite < (plus_associative ? n (N * n)).
429  nrewrite > (plus_symmetrical (m + N * m) n).
430  nrewrite < (plus_associative n m (N * m)).
431  nrewrite < (plus_symmetrical n m).
432  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
433  @.
434nqed.
435
436nlemma mutliplication_associative:
437  ∀m, n, o: Nat.
438    m * (n * o) = (m * n) * o.
439  #m n o.
440  nelim m.
441  nnormalize.
442  @.
443  #N H.
444  nnormalize.
445  nrewrite > H.
446  nrewrite > (multiplication_distributes_right_plus ? ? ?).
447  @.
448nqed.
449
450nlemma minus_minus:
451  ∀n: Nat.
452    n - n = Z.
453  #n.
454  nelim n.
455  nnormalize.
456  @.
457  #N H.
458  nnormalize.
459  nrewrite > H.
460  @.
461nqed.
462
463(*
464nlemma succ_injective:
465  ∀m, n: Nat.
466    S m = S n → m = n.
467  #m n.
468  nelim m.
469  #H.
470  ninversion H.
471  #H.
472  ndestruct
473
474nlemma plus_minus_associate:
475  ∀m, n, o: Nat.
476    (m + n) - o = m + (n - o).
477  #m n o.
478  nelim m.
479  nnormalize.
480  @.
481  #N H.
482 
483
484nlemma plus_minus_inverses:
485  ∀m, n: Nat.
486    (m + n) - n = m.
487  #m n.
488  nelim m.
489  nnormalize.
490  napply minus_minus.
491  #N H.
492*)
Note: See TracBrowser for help on using the repository browser.