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

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

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File size: 5.6 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 plus_symmetrical:
200  ∀m, n: Nat.
201    m + n = n + m.
202  #m n.
203  nelim m.
204  nnormalize.
205  nelim n.
206  nnormalize.
207  @.
208  #N H.
209  nnormalize.
210  nrewrite < H.
211  @.
212  #N H.
213  nnormalize.
214  nrewrite > H.
215  napplyS succ_plus.
216nqed.
217
218nlemma multiplication_zero_right_neutral:
219  ∀m: Nat.
220    m * Z = Z.
221  #m.
222  nelim m.
223  nnormalize.
224  @.
225  #N H.
226  nnormalize.
227  nrewrite > H.
228  @.
229nqed.
230
231nlemma multiplication_succ:
232  ∀m, n: Nat.
233    m * S(n) = m + (m * n).
234  #m n.
235  nelim m.
236  nnormalize.
237  @.
238  #N H.
239  nnormalize.
240  napplyS plus_symmetrical.
241nqed.
242
243nlemma multiplication_symmetrical:
244  ∀m, n: Nat.
245    m * n = n * m.
246  #m n.
247  nelim m.
248  nnormalize.
249  nelim n.
250  nnormalize.
251  @.
252  #N H.
253  nnormalize.
254  nrewrite < H.
255  @.
256  #N H.
257  nnormalize.
258  nrewrite > H.
259  napplyS multiplication_succ.
260nqed.
261
262nlemma multiplication_succ_zero_left_neutral:
263  ∀m: Nat.
264    (S Z) * m = m.
265  #m.
266  nelim m.
267  nnormalize.
268  @.
269  #N H.
270  nnormalize.
271  napplyS succ_plus.
272nqed.
273
274nlemma multiplication_succ_zero_right_neutral:
275  ∀m: Nat.
276    m * (S Z) = m.
277  #m.
278  nelim m.
279  nnormalize.
280  @.
281  #N H.
282  nnormalize.
283  nrewrite > H.
284  @.
285nqed.
286
287nlemma multiplication_distributes_right_plus:
288  ∀m, n, o: Nat.
289    (m + n) * o = m * o + n * o.
290  #m n o.
291  nelim m.
292  nnormalize.
293  @.
294  #N H.
295  nnormalize.
296  nrewrite > H.
297  napplyS plus_associative.
298nqed.
299
300nlemma multiplication_distributes_left_plus:
301  ∀m, n, o: Nat.
302    o * (m + n) = o * m + o * n.
303  #m n o.
304  napplyS multiplication_symmetrical.
305nqed.
306
307nlemma mutliplication_associative:
308  ∀m, n, o: Nat.
309    m * (n * o) = (m * n) * o.
310  #m n o.
311  nelim m.
312  nnormalize.
313  @.
314  #N H.
315  nnormalize.
316  nrewrite > H.
317  napplyS multiplication_distributes_right_plus.
318nqed.
319
320nlemma minus_minus:
321  ∀n: Nat.
322    n - n = Z.
323  #n.
324  nelim n.
325  nnormalize.
326  @.
327  #N H.
328  nnormalize.
329  nrewrite > H.
330  @.
331nqed.
332
333(*
334nlemma succ_injective:
335  ∀m, n: Nat.
336    S m = S n → m = n.
337  #m n.
338  nelim m.
339  #H.
340  ninversion H.
341  #H.
342  ndestruct
343
344nlemma plus_minus_associate:
345  ∀m, n, o: Nat.
346    (m + n) - o = m + (n - o).
347  #m n o.
348  nelim m.
349  nnormalize.
350  @.
351  #N H.
352 
353
354nlemma plus_minus_inverses:
355  ∀m, n: Nat.
356    (m + n) - n = m.
357  #m n.
358  nelim m.
359  nnormalize.
360  napply minus_minus.
361  #N H.
362*)
Note: See TracBrowser for help on using the repository browser.