1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
22 interpretation "Integers" 'Z = Z.
24 ndefinition Z_of_nat ≝
29 ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
31 ndefinition neg_Z_of_nat \def
36 nlemma pos_n_eq_S_n : ∀n : nat.pos n = S n.
52 ntheorem OZ_test_to_Prop : ∀z:Z.
58 ##|##*:#z1;napply nmk;#H;ndestruct]
62 ntheorem injective_pos: injective nat Z pos.
63 #n;#m;#H;ndestruct;//;
66 (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
67 \def injective_pos. *)
69 ntheorem injective_neg: injective nat Z neg.
70 #n;#m;#H;ndestruct;//;
73 (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
74 \def injective_neg. *)
76 ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n.
77 #n;napply nmk;#H;ndestruct;
80 ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
81 #n;napply nmk;#H;ndestruct;
84 ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
85 #n;#m;napply nmk;#H;ndestruct;
88 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
92 ##|##*:#n;@2;napply nmk;#H;ndestruct]
94 ##[@2;napply nmk;#H;ndestruct;
95 ##|#m;ncases (decidable_eq_nat n m);#H;
97 ##|@2;napply nmk;#H2;nelim H;
98 (* bug if you don't introduce H3 *)#H3;ndestruct;
100 ##|#m;@2;napply nmk;#H;ndestruct]
102 ##[@2;napply nmk;#H;ndestruct;
103 ##|#m;@2;napply nmk;#H;ndestruct
104 ##|#m;ncases (decidable_eq_nat n m);#H;
106 ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
126 | neg n ⇒ neg (S n)].
128 ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
134 ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
136 ##[##2:#n;ncases n;//
140 ndefinition Zle : Z → Z → Prop ≝
159 interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
160 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
162 ndefinition Zlt : Z → Z → Prop ≝
181 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
182 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
184 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
187 ##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
191 ntheorem transitive_Zle : transitive Z Zle.
195 ##|##*:#n;ncases z;//]
198 ##|(*##*:#m;#Hl;ncases z;//;*)
199 #m;#Hl;ncases z;//;#p;#Hr;
200 napply (transitive_le n m p);//; (* XXX: auto??? *)
209 ##|#m;#Hl;ncases z;//;#p;#Hr;
210 napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
213 (* variant trans_Zle: transitive Z Zle
214 \def transitive_Zle.*)
216 ntheorem transitive_Zlt: transitive Z Zlt.
223 ##|#m;#_;#Hr;ncases Hr]
229 ##|#p;napply transitive_lt (* XXX: auto??? *)
235 ##|#m;#_;#Hr;ncases Hr]
238 ##|#p;#_;#Hr;ncases Hr]
241 ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
246 (* variant trans_Zlt: transitive Z Zlt
248 theorem irrefl_Zlt: irreflexive Z Zlt
249 \def irreflexive_Zlt.*)
251 ntheorem Zlt_neg_neg_to_lt:
252 ∀n,m:nat. neg n < neg m → m < n.
256 ntheorem lt_to_Zlt_neg_neg: ∀n,m:nat.m < n → neg n < neg m.
260 ntheorem Zlt_pos_pos_to_lt:
261 ∀n,m:nat. pos n < pos m → n < m.
265 ntheorem lt_to_Zlt_pos_pos: ∀n,m:nat.n < m → pos n < pos m.
269 ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
281 ##|#p;ncases n;nnormalize;
282 ##[#H;nelim (not_le_Sn_O p);#H2;napply H2;//; (* XXX: auto? *)
283 ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
290 (* boolean equality *)
291 ndefinition eqZb : Z → Z → bool ≝
310 ntheorem eqZb_to_Prop:
318 ##|napply not_eq_OZ_pos (* XXX: auto? *)
319 ##|napply not_eq_OZ_neg (* XXX: auto? *)]
321 ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
322 ##|#m;napply eqb_elim;
324 ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
325 ##|#m;napply not_eq_pos_neg]
327 ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
328 ##|#m;napply nmk;#H;ndestruct
329 ##|#m;napply eqb_elim;
331 ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
336 ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
337 (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
340 (match (eqZb x y) with
342 | false ⇒ x ≠ y] → P (eqZb x y))
343 ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
346 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
349 include "arithmetics/compare.ma".
351 ndefinition Z_compare : Z → Z → compare ≝
362 | pos m ⇒ nat_compare n m
368 | neg m ⇒ nat_compare m n ]].
370 ntheorem Z_compare_to_Prop :
371 ∀x,y:Z. match (Z_compare x y) with
380 ncut (match (nat_compare m n) with
384 match (nat_compare m n) with
388 ##[ncases (nat_compare m n);//
389 ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
395 ncut (match (nat_compare n m) with
399 match (nat_compare n m) with
403 ##[ncases (nat_compare n m);//
404 ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
409 ndefinition Zplus : Z → Z → Z ≝
415 | pos n ⇒ (pos (pred ((S m)+(S n))))
417 match nat_compare m n with
418 [ LT ⇒ (neg (pred (n-m)))
420 | GT ⇒ (pos (pred (m-n)))] ]
425 match nat_compare m n with
426 [ LT ⇒ (pos (pred (n-m)))
428 | GT ⇒ (neg (pred (m-n)))]
429 | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
431 interpretation "integer plus" 'plus x y = (Zplus x y).
433 ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
441 ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
445 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
447 ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
449 ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
453 ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
454 ncases (nat_compare q p);//]
457 ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
458 ncases (nat_compare q p);//
463 ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg O)+z.
466 ##|##*:#n;ncases n;//]
469 ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos O)+z.
472 ##|##*:#n;ncases n;//]
475 ntheorem Zplus_pos_pos:
476 ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
481 nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_O ?); (* XXX yet again *)
483 ##|#q;nnormalize;nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_Sm ??);//]
487 ntheorem Zplus_pos_neg:
488 ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
492 ntheorem Zplus_neg_pos :
493 ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
494 #n;#m;ncases n;ncases m;//;
497 ntheorem Zplus_neg_neg:
498 ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
501 ##|#p;ncases m;nnormalize;
502 ##[nrewrite > (plus_n_Sm ??);//
503 ##|#q;nrewrite > (plus_n_Sm ??);//]
507 ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
511 ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
515 ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
516 nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
520 ntheorem Zplus_Zsucc_pos_pos :
521 ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
525 ntheorem Zplus_Zsucc_pos_neg:
526 ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
528 napply (nat_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
531 ##|#n2;#IH;nelim n2;//]
533 ##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nelim IH;//]
536 ntheorem Zplus_Zsucc_neg_neg :
537 ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
539 napply (nat_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
542 ##|#n2;#IH;nelim n2;//]
546 ntheorem Zplus_Zsucc_neg_pos:
547 ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
549 napply (nat_elim2 (λn,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
552 ##|#n2;#IH;nelim n2;//]
554 ##|#n1;#m1;#IH;nrewrite < IH;nrewrite < (Zplus_neg_pos ? (S m1));//]
557 ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
559 ##[ncases y;//;#n;nnormalize;ncases n;//;
560 ##|##*:#n;ncases y;//]
563 ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
564 #x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
565 ##[nrewrite > (Zsucc_Zpred ?);//
566 ##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]
569 ntheorem associative_Zplus: associative Z Zplus.
570 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
574 ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
576 nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
577 nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
579 ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
581 nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
582 nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
586 (* variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z)
587 \def associative_Zplus. *)
590 ndefinition Zopp : Z → Z ≝
596 interpretation "integer unary minus" 'uminus x = (Zopp x).
598 ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
602 ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
605 ##|##*:#n;ncases y;//;#m;nnormalize;napply nat_compare_elim;nnormalize;//]
608 ntheorem Zopp_Zopp: ∀x:Z. --x = x.
612 ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
615 ##|##*:#n;nnormalize;nrewrite > (nat_compare_n_n ?);//]
618 ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
620 nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
621 nrewrite < (Zplus_Zopp x);
622 nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
626 ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
628 napply (injective_Zplus_l x);
629 nrewrite < (sym_Zplus ??);
634 ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
636 interpretation "integer minus" 'minus x y = (Zminus x y).