1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | (* This includes a lot of copied code from arithmetics/Z.ma, so some of the |
---|
16 | comments may no longer be applicable. *) |
---|
17 | |
---|
18 | (*include "arithmetics/compare.ma".*) |
---|
19 | include "utilities/binary/positive.ma". |
---|
20 | |
---|
21 | inductive Z : Type[0] ≝ |
---|
22 | OZ : Z |
---|
23 | | pos : Pos → Z |
---|
24 | | neg : Pos → Z. |
---|
25 | |
---|
26 | (*interpretation "Integers" 'D = Z.*) |
---|
27 | |
---|
28 | definition Z_of_nat ≝ |
---|
29 | λn. match n with |
---|
30 | [ O ⇒ OZ |
---|
31 | | S n ⇒ pos (succ_pos_of_nat n)]. |
---|
32 | |
---|
33 | coercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z. |
---|
34 | |
---|
35 | definition neg_Z_of_nat \def |
---|
36 | λn. match n with |
---|
37 | [ O ⇒ OZ |
---|
38 | | S n ⇒ neg (succ_pos_of_nat n)]. |
---|
39 | |
---|
40 | definition abs ≝ |
---|
41 | λz.match z with |
---|
42 | [ OZ ⇒ O |
---|
43 | | pos n ⇒ nat_of_pos n |
---|
44 | | neg n ⇒ nat_of_pos n]. |
---|
45 | |
---|
46 | definition OZ_test ≝ |
---|
47 | λz.match z with |
---|
48 | [ OZ ⇒ true |
---|
49 | | pos _ ⇒ false |
---|
50 | | neg _ ⇒ false]. |
---|
51 | |
---|
52 | theorem OZ_test_to_Prop : ∀z:Z. |
---|
53 | match OZ_test z with |
---|
54 | [true ⇒ z=OZ |
---|
55 | |false ⇒ z ≠ OZ]. |
---|
56 | #z cases z |
---|
57 | [ @refl |
---|
58 | |*:#z1 @nmk #H destruct] |
---|
59 | qed. |
---|
60 | |
---|
61 | (* discrimination *) |
---|
62 | theorem injective_pos: injective Pos Z pos. |
---|
63 | #n #m #H destruct // |
---|
64 | qed. |
---|
65 | |
---|
66 | (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m |
---|
67 | \def injective_pos. *) |
---|
68 | |
---|
69 | theorem injective_neg: injective Pos Z neg. |
---|
70 | #n #m #H destruct // |
---|
71 | qed. |
---|
72 | |
---|
73 | (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m |
---|
74 | \def injective_neg. *) |
---|
75 | |
---|
76 | theorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n. |
---|
77 | #n @nmk #H destruct; |
---|
78 | qed. |
---|
79 | |
---|
80 | theorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n. |
---|
81 | #n @nmk #H destruct; |
---|
82 | qed. |
---|
83 | |
---|
84 | theorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m. |
---|
85 | #n #m @nmk #H destruct; |
---|
86 | qed. |
---|
87 | |
---|
88 | theorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). |
---|
89 | #x #y cases x; |
---|
90 | [cases y; |
---|
91 | [% // |
---|
92 | |*:#n %2 @nmk #H destruct] |
---|
93 | |#n cases y; |
---|
94 | [%2 @nmk #H destruct; |
---|
95 | |#m cases (decidable_eq_pos n m) #H |
---|
96 | [>H % // |
---|
97 | |%2 @(not_to_not … H) #E destruct @refl |
---|
98 | ] |
---|
99 | |#m %2 @nmk #H destruct] |
---|
100 | |#n cases y; |
---|
101 | [%2 @nmk #H destruct; |
---|
102 | |#m %2 @nmk #H destruct |
---|
103 | |#m cases (decidable_eq_pos n m);#H |
---|
104 | [>H % // |
---|
105 | |%2 @(not_to_not … H) #E destruct @refl |
---|
106 | ]]] |
---|
107 | qed. |
---|
108 | |
---|
109 | definition Zsucc ≝ |
---|
110 | λz. match z with |
---|
111 | [ OZ ⇒ pos one |
---|
112 | | pos n ⇒ pos (succ n) |
---|
113 | | neg n ⇒ |
---|
114 | match n with |
---|
115 | [ one ⇒ OZ |
---|
116 | | _ ⇒ neg (pred n)]]. |
---|
117 | |
---|
118 | definition Zpred ≝ |
---|
119 | λz. match z with |
---|
120 | [ OZ ⇒ neg one |
---|
121 | | pos n ⇒ |
---|
122 | match n with |
---|
123 | [ one ⇒ OZ |
---|
124 | | _ ⇒ pos (pred n)] |
---|
125 | | neg n ⇒ neg (succ n)]. |
---|
126 | |
---|
127 | lemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))). |
---|
128 | //; qed. |
---|
129 | |
---|
130 | theorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z. |
---|
131 | #z cases z; |
---|
132 | [ // |
---|
133 | | #n normalize; cases n; /2/; |
---|
134 | | #n cases n; //; #n' |
---|
135 | >(pred_succ_unfold_hack …) <(succ_pred_n …) //; |
---|
136 | % #H destruct; |
---|
137 | qed. |
---|
138 | |
---|
139 | lemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))). |
---|
140 | //; qed. |
---|
141 | |
---|
142 | theorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z. |
---|
143 | #z cases z |
---|
144 | [ // |
---|
145 | | #n cases n;//; #n' |
---|
146 | >(succ_pred_unfold_hack …) <(succ_pred_n …) //; |
---|
147 | % #H destruct; |
---|
148 | | #n cases n;/3/; |
---|
149 | ] |
---|
150 | qed. |
---|
151 | |
---|
152 | let rec Zle (x:Z) (y:Z) on x : Prop ≝ |
---|
153 | match x with |
---|
154 | [ OZ ⇒ |
---|
155 | match y with |
---|
156 | [ OZ ⇒ True |
---|
157 | | pos m ⇒ True |
---|
158 | | neg m ⇒ False ] |
---|
159 | | pos n ⇒ |
---|
160 | match y with |
---|
161 | [ OZ ⇒ False |
---|
162 | | pos m ⇒ n ≤ m |
---|
163 | | neg m ⇒ False ] |
---|
164 | | neg n ⇒ |
---|
165 | match y with |
---|
166 | [ OZ ⇒ True |
---|
167 | | pos m ⇒ True |
---|
168 | | neg m ⇒ m ≤ n ]]. |
---|
169 | |
---|
170 | interpretation "integer 'less or equal to'" 'leq x y = (Zle x y). |
---|
171 | interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)). |
---|
172 | |
---|
173 | let rec Zlt (x:Z) (y:Z) on x : Prop ≝ |
---|
174 | match x with |
---|
175 | [ OZ ⇒ |
---|
176 | match y with |
---|
177 | [ OZ ⇒ False |
---|
178 | | pos m ⇒ True |
---|
179 | | neg m ⇒ False ] |
---|
180 | | pos n ⇒ |
---|
181 | match y with |
---|
182 | [ OZ ⇒ False |
---|
183 | | pos m ⇒ n<m |
---|
184 | | neg m ⇒ False ] |
---|
185 | | neg n ⇒ |
---|
186 | match y with |
---|
187 | [ OZ ⇒ True |
---|
188 | | pos m ⇒ True |
---|
189 | | neg m ⇒ m<n ]]. |
---|
190 | |
---|
191 | interpretation "integer 'less than'" 'lt x y = (Zlt x y). |
---|
192 | interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)). |
---|
193 | |
---|
194 | theorem irreflexive_Zlt: irreflexive Z Zlt. |
---|
195 | #x cases x |
---|
196 | [@nmk // |
---|
197 | |*:#n @(not_le_succ_n n) (* XXX: auto?? *)] |
---|
198 | qed. |
---|
199 | |
---|
200 | (* transitivity *) |
---|
201 | theorem transitive_Zle : transitive Z Zle. |
---|
202 | #x #y #z cases x |
---|
203 | [cases y |
---|
204 | [// |
---|
205 | |*:#n cases z;//] |
---|
206 | |#n cases y |
---|
207 | [#H cases H |
---|
208 | |(**:#m #Hl cases z;//;*) |
---|
209 | #m #Hl cases z;//;#p #Hr |
---|
210 | @(transitive_le n m p) //; (* XXX: auto??? *) |
---|
211 | |#m #Hl cases Hl] |
---|
212 | |#n cases y |
---|
213 | [#Hl cases z |
---|
214 | [1,2:// |
---|
215 | |#m #Hr cases Hr] |
---|
216 | |#m #Hl cases z; |
---|
217 | [1,2:// |
---|
218 | |#p #Hr cases Hr] |
---|
219 | |#m #Hl cases z;//;#p #Hr |
---|
220 | @(transitive_le p m n) //; (* XXX: auto??? *) ] |
---|
221 | qed. |
---|
222 | |
---|
223 | (* variant trans_Zle: transitive Z Zle |
---|
224 | \def transitive_Zle.*) |
---|
225 | |
---|
226 | theorem transitive_Zlt: transitive Z Zlt. |
---|
227 | #x #y #z cases x |
---|
228 | [cases y |
---|
229 | [// |
---|
230 | |#n cases z |
---|
231 | [#_ #Hr cases Hr |
---|
232 | |// |
---|
233 | |#m #_ #Hr cases Hr] |
---|
234 | |#n #Hl cases Hl] |
---|
235 | |#n cases y |
---|
236 | [#Hl cases Hl |
---|
237 | |#m cases z |
---|
238 | [// |
---|
239 | |#p apply transitive_lt (* XXX: auto??? *) |
---|
240 | |//] |
---|
241 | |#m #Hl cases Hl] |
---|
242 | |#n cases y |
---|
243 | [cases z; |
---|
244 | [1,2:// |
---|
245 | |#m #_ #Hr cases Hr] |
---|
246 | |#m cases z; |
---|
247 | [1,2:// |
---|
248 | |#p #_ #Hr cases Hr] |
---|
249 | |#m cases z |
---|
250 | [1,2:// |
---|
251 | |#p #Hl #Hr apply (transitive_lt … Hr Hl)] |
---|
252 | ] |
---|
253 | ] |
---|
254 | qed. |
---|
255 | |
---|
256 | (* variant trans_Zlt: transitive Z Zlt |
---|
257 | \def transitive_Zlt. |
---|
258 | theorem irrefl_Zlt: irreflexive Z Zlt |
---|
259 | \def irreflexive_Zlt.*) |
---|
260 | |
---|
261 | theorem Zlt_neg_neg_to_lt: |
---|
262 | ∀n,m:Pos. neg n < neg m → m < n. |
---|
263 | //; |
---|
264 | qed. |
---|
265 | |
---|
266 | theorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m. |
---|
267 | //; |
---|
268 | qed. |
---|
269 | |
---|
270 | theorem Zlt_pos_pos_to_lt: |
---|
271 | ∀n,m:Pos. pos n < pos m → n < m. |
---|
272 | //; |
---|
273 | qed. |
---|
274 | |
---|
275 | theorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m. |
---|
276 | //; |
---|
277 | qed. |
---|
278 | |
---|
279 | lemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n. |
---|
280 | #n normalize; <(pred_succ_n n) cases n; //; qed. |
---|
281 | |
---|
282 | theorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y. |
---|
283 | #x #y cases x |
---|
284 | [cases y |
---|
285 | [#H cases H |
---|
286 | |//; |
---|
287 | |#p #H cases H] |
---|
288 | |#n cases y |
---|
289 | [#H cases H |
---|
290 | |#p normalize;// |
---|
291 | |#p #H cases H] |
---|
292 | |#n cases y |
---|
293 | [1,2:cases n;// |
---|
294 | |#p @(pos_cases … n) |
---|
295 | [#H elim (not_le_succ_one p);#H2 @H2 @H (*// *) (* XXX: auto? *) |
---|
296 | |#m >(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *) |
---|
297 | ] |
---|
298 | ] |
---|
299 | ] |
---|
300 | qed. |
---|
301 | |
---|
302 | (*** COMPARE ***) |
---|
303 | |
---|
304 | (* boolean equality *) |
---|
305 | let rec eqZb (x:Z) (y:Z) on x : bool ≝ |
---|
306 | match x with |
---|
307 | [ OZ ⇒ |
---|
308 | match y with |
---|
309 | [ OZ ⇒ true |
---|
310 | | pos q ⇒ false |
---|
311 | | neg q ⇒ false] |
---|
312 | | pos p ⇒ |
---|
313 | match y with |
---|
314 | [ OZ ⇒ false |
---|
315 | | pos q ⇒ eqb p q |
---|
316 | | neg q ⇒ false] |
---|
317 | | neg p ⇒ |
---|
318 | match y with |
---|
319 | [ OZ ⇒ false |
---|
320 | | pos q ⇒ false |
---|
321 | | neg q ⇒ eqb p q]]. |
---|
322 | |
---|
323 | theorem eqZb_to_Prop: |
---|
324 | ∀x,y:Z. |
---|
325 | match eqZb x y with |
---|
326 | [ true ⇒ x=y |
---|
327 | | false ⇒ x ≠ y]. |
---|
328 | #x #y cases x |
---|
329 | [cases y; |
---|
330 | [// |
---|
331 | |@not_eq_OZ_pos (* XXX: auto? *) |
---|
332 | |@not_eq_OZ_neg (* XXX: auto? *)] |
---|
333 | |#n cases y; |
---|
334 | [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/; |
---|
335 | |#m normalize @eqb_elim |
---|
336 | [// |
---|
337 | | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) // |
---|
338 | ] |
---|
339 | |#m @not_eq_pos_neg] |
---|
340 | |#n cases y |
---|
341 | [@nmk #H elim (not_eq_OZ_neg n);#H /2/; |
---|
342 | |#m @nmk #H destruct |
---|
343 | |#m normalize @eqb_elim |
---|
344 | [// |
---|
345 | | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) // |
---|
346 | ] |
---|
347 | ] |
---|
348 | qed. |
---|
349 | |
---|
350 | theorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop. |
---|
351 | (x=y → P true) → (x ≠ y → P false) → P (eqZb x y). |
---|
352 | #x #y #P #HP1 #HP2 |
---|
353 | cut |
---|
354 | (match (eqZb x y) with |
---|
355 | [ true ⇒ x=y |
---|
356 | | false ⇒ x ≠ y] → P (eqZb x y)) |
---|
357 | [cases (eqZb x y);normalize; (* XXX: auto?? *) |
---|
358 | [@HP1 |
---|
359 | |@HP2] |
---|
360 | |#Hcut @Hcut @eqZb_to_Prop] |
---|
361 | qed. |
---|
362 | |
---|
363 | let rec Z_compare (x:Z) (y:Z) : compare ≝ |
---|
364 | match x with |
---|
365 | [ OZ ⇒ |
---|
366 | match y with |
---|
367 | [ OZ ⇒ EQ |
---|
368 | | pos m ⇒ LT |
---|
369 | | neg m ⇒ GT ] |
---|
370 | | pos n ⇒ |
---|
371 | match y with |
---|
372 | [ OZ ⇒ GT |
---|
373 | | pos m ⇒ pos_compare n m |
---|
374 | | neg m ⇒ GT] |
---|
375 | | neg n ⇒ |
---|
376 | match y with |
---|
377 | [ OZ ⇒ LT |
---|
378 | | pos m ⇒ LT |
---|
379 | | neg m ⇒ pos_compare m n ]]. |
---|
380 | |
---|
381 | theorem Z_compare_to_Prop : |
---|
382 | ∀x,y:Z. match (Z_compare x y) with |
---|
383 | [ LT ⇒ x < y |
---|
384 | | EQ ⇒ x=y |
---|
385 | | GT ⇒ y < x]. |
---|
386 | #x #y elim x |
---|
387 | [elim y;//; |
---|
388 | |elim y |
---|
389 | [1,3:// |
---|
390 | |#n #m normalize; |
---|
391 | cut (match (pos_compare m n) with |
---|
392 | [ LT ⇒ m < n |
---|
393 | | EQ ⇒ m = n |
---|
394 | | GT ⇒ n < m ] → |
---|
395 | match (pos_compare m n) with |
---|
396 | [ LT ⇒ (succ m) ≤ n |
---|
397 | | EQ ⇒ pos m = pos n |
---|
398 | | GT ⇒ (succ n) ≤ m]) |
---|
399 | [cases (pos_compare m n);// |
---|
400 | |#Hcut @Hcut @pos_compare_to_Prop] |
---|
401 | ] |
---|
402 | |elim y |
---|
403 | [#n // |
---|
404 | |normalize;// |
---|
405 | |normalize;#n #m |
---|
406 | cut (match (pos_compare n m) with |
---|
407 | [ LT ⇒ n < m |
---|
408 | | EQ ⇒ n = m |
---|
409 | | GT ⇒ m < n] → |
---|
410 | match (pos_compare n m) with |
---|
411 | [ LT ⇒ (succ n) ≤ m |
---|
412 | | EQ ⇒ neg m = neg n |
---|
413 | | GT ⇒ (succ m) ≤ n]) |
---|
414 | [cases (pos_compare n m);// |
---|
415 | |#Hcut @Hcut @pos_compare_to_Prop] |
---|
416 | ] |
---|
417 | ] |
---|
418 | qed. |
---|
419 | |
---|
420 | let rec Zplus (x:Z) (y:Z) on x : Z ≝ |
---|
421 | match x with |
---|
422 | [ OZ ⇒ y |
---|
423 | | pos m ⇒ |
---|
424 | match y with |
---|
425 | [ OZ ⇒ x |
---|
426 | | pos n ⇒ (pos (m + n)) |
---|
427 | | neg n ⇒ |
---|
428 | match pos_compare m n with |
---|
429 | [ LT ⇒ (neg (n-m)) |
---|
430 | | EQ ⇒ OZ |
---|
431 | | GT ⇒ (pos (m-n))] ] |
---|
432 | | neg m ⇒ |
---|
433 | match y with |
---|
434 | [ OZ ⇒ x |
---|
435 | | pos n ⇒ |
---|
436 | match pos_compare m n with |
---|
437 | [ LT ⇒ (pos (n-m)) |
---|
438 | | EQ ⇒ OZ |
---|
439 | | GT ⇒ (neg (m-n))] |
---|
440 | | neg n ⇒ (neg (m + n))] ]. |
---|
441 | |
---|
442 | interpretation "integer plus" 'plus x y = (Zplus x y). |
---|
443 | |
---|
444 | theorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m. |
---|
445 | #n #m cases n |
---|
446 | [// |
---|
447 | |#p cases m |
---|
448 | [normalize;// |
---|
449 | |#m' normalize;>(nat_plus_pos_plus …) >(succ_nat_pos ?) /2/] |
---|
450 | qed. |
---|
451 | |
---|
452 | theorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m. |
---|
453 | //; qed. |
---|
454 | |
---|
455 | theorem Zplus_z_OZ: ∀z:Z. z+OZ = z. |
---|
456 | #z cases z;//; |
---|
457 | qed. |
---|
458 | |
---|
459 | theorem sym_Zplus : ∀x,y:Z. x+y = y+x. |
---|
460 | #x #y cases x |
---|
461 | [>Zplus_z_OZ // |
---|
462 | |#p cases y |
---|
463 | [// |
---|
464 | |// |
---|
465 | |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n |
---|
466 | cases (pos_compare q p);//] |
---|
467 | |#p cases y |
---|
468 | [//; |
---|
469 | |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n |
---|
470 | cases (pos_compare q p);// |
---|
471 | |normalize;//] |
---|
472 | ] |
---|
473 | qed. |
---|
474 | |
---|
475 | theorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z. |
---|
476 | #z cases z |
---|
477 | [// |
---|
478 | |*:#n cases n;//] |
---|
479 | qed. |
---|
480 | |
---|
481 | theorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z. |
---|
482 | #z cases z |
---|
483 | [// |
---|
484 | |*:#n cases n;//] |
---|
485 | qed. |
---|
486 | |
---|
487 | lemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n. |
---|
488 | #n normalize; cases n; /2/; qed. |
---|
489 | |
---|
490 | theorem Zplus_pos_pos: |
---|
491 | ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). |
---|
492 | #n #m @(pos_cases … n) |
---|
493 | [ @(pos_cases … m) //; |
---|
494 | |#p @(pos_cases … m) |
---|
495 | [normalize; <(succ_plus_one …) //; |
---|
496 | |#q >(Zsucc_Zplus_pos_O …) >(Zpred_pos_succ ?) |
---|
497 | normalize; /2/; |
---|
498 | ] |
---|
499 | ] |
---|
500 | qed. |
---|
501 | |
---|
502 | theorem Zplus_pos_neg: |
---|
503 | ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). |
---|
504 | #n #m |
---|
505 | whd in ⊢ (??%%) |
---|
506 | <(pos_compare_S_S …) |
---|
507 | >(minus_S_S …) |
---|
508 | >(minus_S_S …) //; |
---|
509 | qed. |
---|
510 | |
---|
511 | lemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n. |
---|
512 | #A #P #Q #n @succ_elim //; qed. |
---|
513 | |
---|
514 | lemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n. |
---|
515 | #n cases n; //; |
---|
516 | #n' whd in ⊢ (??%?); normalize; <(pred_succ_n …) |
---|
517 | @succ_elim //; qed. |
---|
518 | |
---|
519 | theorem Zplus_neg_pos : |
---|
520 | ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). |
---|
521 | #n #m @(pos_cases … n) @(pos_cases … m) |
---|
522 | [ //; |
---|
523 | | #m' >Zpred_pos_succ |
---|
524 | change in ⊢ (??(??%)?) with (Zsucc (pos m')) |
---|
525 | <Zpred_Zplus_neg_O >Zpred_Zsucc @refl |
---|
526 | | #m' whd in ⊢ (??%%) >pos_compare_S_one normalize; |
---|
527 | >partial_minus_S_one normalize; >pos_nonzero |
---|
528 | <pred_succ_n // |
---|
529 | | #m' #n' whd in ⊢ (??%%) <pos_compare_S_S |
---|
530 | >minus_S_S |
---|
531 | >minus_S_S normalize |
---|
532 | >pos_nonzero |
---|
533 | >pos_nonzero |
---|
534 | <pred_succ_n |
---|
535 | <pred_succ_n |
---|
536 | normalize; //; |
---|
537 | ] qed. |
---|
538 | |
---|
539 | theorem Zplus_neg_neg: |
---|
540 | ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)). |
---|
541 | #n #m @(pos_cases … n) @(pos_cases … m) |
---|
542 | [ 1,2: //; |
---|
543 | | #n' normalize in ⊢ (???(?%?)); |
---|
544 | >(pos_nonzero …) |
---|
545 | <(pred_succ_n …) normalize; //; |
---|
546 | | #m' #n' normalize; >(pos_nonzero …) |
---|
547 | <(pred_succ_n …) normalize; //; |
---|
548 | ] qed. |
---|
549 | |
---|
550 | theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y). |
---|
551 | #x #y cases x |
---|
552 | [cases y |
---|
553 | [// |
---|
554 | |#n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) // |
---|
555 | |#p <(Zsucc_Zplus_pos_O …) //] |
---|
556 | |cases y;/2/; #p >(sym_Zplus ? (Zpred OZ)) |
---|
557 | <Zpred_Zplus_neg_O //; |
---|
558 | |cases y |
---|
559 | [#n <(sym_Zplus ??) <(sym_Zplus (Zpred OZ) ?) |
---|
560 | <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc ?) // |
---|
561 | |*:/2/] |
---|
562 | qed. |
---|
563 | |
---|
564 | theorem Zplus_Zsucc_pos_pos : |
---|
565 | ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). |
---|
566 | #n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //; |
---|
567 | qed. |
---|
568 | |
---|
569 | theorem Zplus_Zsucc_pos_neg: |
---|
570 | ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). |
---|
571 | #n #m |
---|
572 | @(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))) |
---|
573 | [#n1 elim n1 |
---|
574 | [// |
---|
575 | |*:#n2 #IH elim n2;//] |
---|
576 | |#n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) |
---|
577 | >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) |
---|
578 | >(Zpred_Zsucc …) /2/ |
---|
579 | |#n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH |
---|
580 | <(Zplus_pos_neg …) //] |
---|
581 | qed. |
---|
582 | |
---|
583 | theorem Zplus_Zsucc_neg_neg : |
---|
584 | ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m). |
---|
585 | #n #m |
---|
586 | @(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))) |
---|
587 | [@pos_elim |
---|
588 | [// |
---|
589 | |#n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //] |
---|
590 | | #n' normalize; |
---|
591 | >(pos_nonzero …) |
---|
592 | <(pred_succ_n …) normalize; |
---|
593 | <(succ_plus_one …) |
---|
594 | <(succ_plus_one …) >(pos_nonzero …) //; |
---|
595 | | #n' #m' #IH normalize; |
---|
596 | >(pos_nonzero …) normalize; |
---|
597 | <(pluss_succn_m …) |
---|
598 | >(pos_nonzero …) //; |
---|
599 | ] |
---|
600 | qed. |
---|
601 | |
---|
602 | lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m. |
---|
603 | #n #m whd in ⊢ (??%%) <pos_compare_S_S |
---|
604 | >minus_S_S >minus_S_S |
---|
605 | //; qed. |
---|
606 | |
---|
607 | |
---|
608 | theorem Zplus_Zsucc_neg_pos: |
---|
609 | ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). |
---|
610 | #n #m |
---|
611 | @(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m))) |
---|
612 | [@pos_elim |
---|
613 | [// |
---|
614 | |#n2 #IH normalize; >(pos_nonzero …) normalize; |
---|
615 | >(partial_minus_S_one …) //] |
---|
616 | | #n' |
---|
617 | >(sym_Zplus …) |
---|
618 | <(Zsucc_Zplus_pos_O …) |
---|
619 | >(sym_Zplus …) |
---|
620 | <(Zsucc_Zplus_pos_O …) //; |
---|
621 | |#n' #m' #IH |
---|
622 | >(neg_pos_succ …) //; |
---|
623 | ] qed. |
---|
624 | |
---|
625 | theorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y). |
---|
626 | #x #y cases x |
---|
627 | [cases y;//;(*#n normalize;cases n;//;*) |
---|
628 | |*:#n cases y;//;#m @Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)] |
---|
629 | qed. |
---|
630 | |
---|
631 | theorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y). |
---|
632 | #x #y cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)) |
---|
633 | [>(Zsucc_Zpred ?) // |
---|
634 | |#Hcut >Hcut >(Zplus_Zsucc ??) //] |
---|
635 | qed. |
---|
636 | |
---|
637 | lemma eq_rect_Type0_r: |
---|
638 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
639 | #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption. |
---|
640 | qed. |
---|
641 | |
---|
642 | theorem associative_Zplus: associative Z Zplus. |
---|
643 | (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*) |
---|
644 | #x #y #z cases x |
---|
645 | [// |
---|
646 | |@pos_elim |
---|
647 | [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //; |
---|
648 | |#n1 #IH |
---|
649 | >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?) |
---|
650 | >(Zplus_Zsucc ((pos n1)+y) ?) //] |
---|
651 | |@pos_elim |
---|
652 | [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //; |
---|
653 | |#n1 #IH |
---|
654 | >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?) |
---|
655 | >(Zplus_Zpred ((neg n1)+y) ?) //] |
---|
656 | ] |
---|
657 | qed. |
---|
658 | |
---|
659 | (* variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) |
---|
660 | \def associative_Zplus. *) |
---|
661 | |
---|
662 | (* Zopp *) |
---|
663 | definition Zopp : Z → Z ≝ |
---|
664 | λx:Z. match x with |
---|
665 | [ OZ ⇒ OZ |
---|
666 | | pos n ⇒ neg n |
---|
667 | | neg n ⇒ pos n ]. |
---|
668 | |
---|
669 | interpretation "integer unary minus" 'uminus x = (Zopp x). |
---|
670 | |
---|
671 | theorem eq_OZ_Zopp_OZ : OZ = (- OZ). |
---|
672 | //; |
---|
673 | qed. |
---|
674 | |
---|
675 | theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y. |
---|
676 | #x #y cases x |
---|
677 | [cases y;// |
---|
678 | |*:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//] |
---|
679 | qed. |
---|
680 | |
---|
681 | theorem Zopp_Zopp: ∀x:Z. --x = x. |
---|
682 | #x cases x;//; |
---|
683 | qed. |
---|
684 | |
---|
685 | theorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ. |
---|
686 | #x cases x |
---|
687 | [// |
---|
688 | |*:#n whd in ⊢ (??%?) >pos_compare_n_n //] |
---|
689 | qed. |
---|
690 | |
---|
691 | theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x). |
---|
692 | #x #z #y #H |
---|
693 | <(Zplus_z_OZ z) <(Zplus_z_OZ y) |
---|
694 | <(Zplus_Zopp x) |
---|
695 | <(associative_Zplus ???) <(associative_Zplus ???) |
---|
696 | //; |
---|
697 | qed. |
---|
698 | |
---|
699 | theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y). |
---|
700 | #x #z #y #H |
---|
701 | @(injective_Zplus_l x) |
---|
702 | <(sym_Zplus ??) |
---|
703 | //; |
---|
704 | qed. |
---|
705 | |
---|
706 | (* minus *) |
---|
707 | definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y). |
---|
708 | |
---|
709 | interpretation "integer minus" 'minus x y = (Zminus x y). |
---|
710 | |
---|
711 | |
---|
712 | |
---|
713 | definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n). |
---|
714 | definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n). |
---|
715 | definition two_p : Z → Z ≝ |
---|
716 | λz.match z with |
---|
717 | [ OZ ⇒ pos one |
---|
718 | | pos p ⇒ pos (two_power_pos p) |
---|
719 | | neg _ ⇒ OZ (* same fib as Coq *) |
---|
720 | ]. |
---|