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

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

Changes from this morning: Bool / Prop division = nightmare.

File size: 5.7 KB
Line 
1include "Cartesian.ma".
2include "Maybe.ma".
3include "Bool.ma".
4
5include "logic/pts.ma".
6include "Plogic/equality.ma".
7include "Plogic/connectives.ma".
8
9ninductive Nat: Type[0] ≝
10  Z: Nat
11| S: Nat → Nat.
12
13nlet rec plus (n: Nat) (o: Nat) on n ≝
14  match n with
15    [ Z ⇒ o
16    | S p ⇒ S (plus p o)
17    ].
18   
19notation "n break + m"
20  right associative with precedence 52
21  for @{ 'plus $n $m }.
22 
23interpretation "Nat plus" 'plus n m = (plus n m).
24   
25nlet rec minus (n: Nat) (o: Nat) on n ≝
26  match n with
27    [ Z ⇒ Z
28    | S p ⇒
29      match o with
30        [ Z ⇒ S p
31        | S q ⇒ minus p q
32        ]
33    ].
34   
35notation "n break - m"
36  right associative with precedence 47
37  for @{ 'minus $n $m }.
38 
39interpretation "Nat minus" 'minus n m = (minus n m).
40   
41nlet rec multiplication (n: Nat) (o: Nat) on n ≝
42  match n with
43    [ Z ⇒ Z
44    | S p ⇒ o + (multiplication p o)
45    ].
46   
47notation "n break * m"
48  right associative with precedence 47
49  for @{ 'multiplication $n $m }.
50 
51interpretation "Nat multiplication" 'times n m = (multiplication n m).
52
53ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
54  ltoe_refl: less_than_or_equal_p n n
55| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
56
57nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m ≝
58  match m with
59    [ Z ⇒ True
60    | S o ⇒
61      match n with
62        [ Z ⇒ False
63        | S p ⇒ less_than_or_equal_b o p
64        ]
65    ].
66   
67notation "n break ≤ m"
68  non associative with precedence 47
69  for @{ 'less_than_or_equal $n $m }.
70 
71interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
72interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
73
74ndefinition less_than_p ≝
75  λm, n: Nat.
76    m ≤ n ∧ ¬(m = n).
77   
78notation "n break < m"
79  non associative with precedence 47
80  for @{ 'less_than $n $m }.
81 
82interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
83
84(*
85nlet rec greatest_common_divisor (m: Nat) (n: Nat) on n ≝
86  match n with
87    [ Z ⇒ m
88    | S o ⇒ greatest_common_divisor n (modulus m n)
89    ].
90*)
91
92nlemma less_than_or_equal_zero:
93  ∀n: Nat.
94    Z ≤ n.
95  #n.
96  nelim n.
97  //.
98  #N.
99  //.
100nqed.
101
102(*
103nlemma less_than_or_equal_injective:
104  ∀m, n: Nat.
105    S m ≤ S n → m ≤ n.
106  #m n.
107  nelim m.
108  #H.
109  napplyS less_than_or_equal_zero.
110  #N H H2.
111  ndestruct.
112
113nlemma less_than_or_equal_zero_equal_zero:
114  ∀m: Nat.
115    m ≤ Z → m = Z.
116  #m.
117  nelim m.
118  //.
119  #N H H2.
120  nnormalize.
121*)
122
123nlemma less_than_or_equal_reflexive:
124  ∀n: Nat.
125    n ≤ n.
126  #n.
127  nelim n.
128  nnormalize.
129  @.
130  #N H.
131  nnormalize.
132  //.
133nqed.
134
135(*
136nlemma less_than_or_equal_succ:
137  ∀m, n: Nat.
138    S m ≤ n → m ≤ n.
139  #m n.
140  nelim m.
141  #H.
142  napplyS less_than_or_equal_zero.
143  #N H H2.
144  //.
145  napplyS H.
146
147
148nlemma less_than_or_equal_transitive:
149  ∀m, n, o: Nat.
150    m ≤ n ∧ n ≤ o → m ≤ o.
151  #m n o.
152  nelim m.
153  #H.
154  napply less_than_or_equal_zero.
155  #N H H2.
156  nnormalize.
157  #;
158*)
159
160nlemma plus_zero:
161  ∀n: Nat.
162    n + Z = n.
163  #n.
164  nelim n.
165  nnormalize.
166  @.
167  #N H.
168  nnormalize.
169  nrewrite > H.
170  @.
171nqed.
172
173nlemma plus_associative:
174  ∀m, n, o: Nat.
175    (m + n) + o = m + (n + o).
176  #m n o.
177  nelim m.
178  nnormalize.
179  @.
180  #N H.
181  nnormalize.
182  nrewrite > H.
183  @.
184nqed.
185
186nlemma succ_plus:
187  ∀m, n: Nat.
188    S(m + n) = m + S(n).
189  #m n.
190  nelim m.
191  nnormalize.
192  @.
193  #N H.
194  nnormalize.
195  nrewrite > H.
196  @.
197nqed.
198
199nlemma succ_plus_succ_zero:
200  ∀n: Nat.
201    S n = plus n (S Z).
202  #n.
203  nelim n.
204  //.
205  #N H.
206  //.
207nqed.
208
209nlemma plus_symmetrical:
210  ∀m, n: Nat.
211    m + n = n + m.
212  #m n.
213  nelim m.
214  nnormalize.
215  nelim n.
216  nnormalize.
217  @.
218  #N H.
219  nnormalize.
220  nrewrite < H.
221  @.
222  #N H.
223  nnormalize.
224  nrewrite > H.
225  napplyS succ_plus.
226nqed.
227
228nlemma multiplication_zero_right_neutral:
229  ∀m: Nat.
230    m * Z = Z.
231  #m.
232  nelim m.
233  nnormalize.
234  @.
235  #N H.
236  nnormalize.
237  nrewrite > H.
238  @.
239nqed.
240
241nlemma multiplication_succ:
242  ∀m, n: Nat.
243    m * S(n) = m + (m * n).
244  #m n.
245  nelim m.
246  nnormalize.
247  @.
248  #N H.
249  nnormalize.
250  //.
251nqed.
252
253nlemma multiplication_symmetrical:
254  ∀m, n: Nat.
255    m * n = n * m.
256  #m n.
257  nelim m.
258  nnormalize.
259  nelim n.
260  nnormalize.
261  @.
262  #N H.
263  nnormalize.
264  nrewrite < H.
265  @.
266  #N H.
267  nnormalize.
268  nrewrite > H.
269  napplyS multiplication_succ.
270nqed.
271
272nlemma multiplication_succ_zero_left_neutral:
273  ∀m: Nat.
274    (S Z) * m = m.
275  #m.
276  nelim m.
277  nnormalize.
278  @.
279  #N H.
280  nnormalize.
281  //.
282nqed.
283
284nlemma multiplication_succ_zero_right_neutral:
285  ∀m: Nat.
286    m * (S Z) = m.
287  #m.
288  nelim m.
289  nnormalize.
290  @.
291  #N H.
292  nnormalize.
293  nrewrite > H.
294  @.
295nqed.
296
297nlemma multiplication_distributes_right_plus:
298  ∀m, n, o: Nat.
299    (m + n) * o = m * o + n * o.
300  #m n o.
301  nelim m.
302  nnormalize.
303  @.
304  #N H.
305  nnormalize.
306  nrewrite > H.
307  napplyS plus_associative.
308nqed.
309
310nlemma multiplication_distributes_left_plus:
311  ∀m, n, o: Nat.
312    o * (m + n) = o * m + o * n.
313  #m n o.
314  napplyS multiplication_symmetrical.
315nqed.
316
317nlemma mutliplication_associative:
318  ∀m, n, o: Nat.
319    m * (n * o) = (m * n) * o.
320  #m n o.
321  nelim m.
322  nnormalize.
323  @.
324  #N H.
325  nnormalize.
326  nrewrite > H.
327  napplyS multiplication_distributes_right_plus.
328nqed.
329
330nlemma minus_minus:
331  ∀n: Nat.
332    n - n = Z.
333  #n.
334  nelim n.
335  nnormalize.
336  @.
337  #N H.
338  nnormalize.
339  nrewrite > H.
340  @.
341nqed.
342
343(*
344nlemma succ_injective:
345  ∀m, n: Nat.
346    S m = S n → m = n.
347  #m n.
348  nelim m.
349  #H.
350  ninversion H.
351  #H.
352  ndestruct
353
354nlemma plus_minus_associate:
355  ∀m, n, o: Nat.
356    (m + n) - o = m + (n - o).
357  #m n o.
358  nelim m.
359  nnormalize.
360  @.
361  #N H.
362 
363
364nlemma plus_minus_inverses:
365  ∀m, n: Nat.
366    (m + n) - n = m.
367  #m n.
368  nelim m.
369  nnormalize.
370  napply minus_minus.
371  #N H.
372*)
Note: See TracBrowser for help on using the repository browser.