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;#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.
80 ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
84 ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
88 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
92 ##|##*:#n;@2;#H;ndestruct]
95 ##|#m;ncases (decidable_eq_nat n m);#H;
97 ##|@2;#H2;napply H;ndestruct;//]
98 ##|#m;@2;#H;ndestruct]
101 ##|#m;@2;#H;ndestruct
102 ##|#m;ncases (decidable_eq_nat n m);#H;
104 ##|@2;#H2;napply H;ndestruct;//]##]##]
123 | neg n ⇒ neg (S n)].
125 ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
131 ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
133 ##[##2:#n;ncases n;//
137 ndefinition Zle : Z → Z → Prop ≝
156 interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
157 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
159 ndefinition Zlt : Z → Z → Prop ≝
178 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
179 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
181 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
184 ##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
188 ntheorem transitive_Zle : transitive Z Zle.
192 ##|##*:#n;ncases z;//]
195 ##|(*##*:#m;#Hl;ncases z;//;*)
196 #m;#Hl;ncases z;//;#p;#Hr;
197 napply (transitive_le n m p);//; (* XXX: auto??? *)
206 ##|#m;#Hl;ncases z;//;#p;#Hr;
207 napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
210 (* variant trans_Zle: transitive Z Zle
211 \def transitive_Zle.*)
213 ntheorem transitive_Zlt: transitive Z Zlt.
220 ##|#m;#_;#Hr;ncases Hr]
226 ##|#p;napply transitive_lt (* XXX: auto??? *)
232 ##|#m;#_;#Hr;ncases Hr]
235 ##|#p;#_;#Hr;ncases Hr]
238 ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
243 (* variant trans_Zlt: transitive Z Zlt
245 theorem irrefl_Zlt: irreflexive Z Zlt
246 \def irreflexive_Zlt.*)
248 ntheorem Zlt_neg_neg_to_lt:
249 ∀n,m:nat. neg n < neg m → m < n.
253 ntheorem lt_to_Zlt_neg_neg: ∀n,m:nat.m < n → neg n < neg m.
257 ntheorem Zlt_pos_pos_to_lt:
258 ∀n,m:nat. pos n < pos m → n < m.
262 ntheorem lt_to_Zlt_pos_pos: ∀n,m:nat.n < m → pos n < pos m.
266 ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
278 ##|#p;ncases n;nnormalize;
279 ##[napply not_le_Sn_O (* XXX: auto? *)
280 ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
287 (* boolean equality *)
288 ndefinition eqZb : Z → Z → bool ≝
307 ntheorem eqZb_to_Prop:
315 ##|napply not_eq_OZ_pos (* XXX: auto? *)
316 ##|napply not_eq_OZ_neg (* XXX: auto? *)]
318 ##[#H;napply not_eq_OZ_pos;//;
319 ##|#m;napply eqb_elim;
321 ##|#H;#H2;napply H;ndestruct;//]
322 ##|#m;napply not_eq_pos_neg]
324 ##[#H;napply not_eq_OZ_neg;//;
326 ##|#m;napply eqb_elim;
328 ##|#H;#H2;napply H;ndestruct;//]
333 ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
334 (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
337 (match (eqZb x y) with
339 | false ⇒ x ≠ y] → P (eqZb x y))
340 ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
343 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
346 ndefinition Z_compare : Z → Z → compare ≝
357 | pos m ⇒ nat_compare n m
363 | neg m ⇒ nat_compare m n ]].
365 ntheorem Z_compare_to_Prop :
366 ∀x,y:Z. match (Z_compare x y) with
375 ncut (match (nat_compare m n) with
379 match (nat_compare m n) with
383 ##[ncases (nat_compare m n);//
384 ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
390 ncut (match (nat_compare n m) with
394 match (nat_compare n m) with
398 ##[ncases (nat_compare n m);//
399 ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
404 ndefinition Zplus : Z → Z → Z ≝
410 | pos n ⇒ (pos (pred ((S m)+(S n))))
412 match nat_compare m n with
413 [ LT ⇒ (neg (pred (n-m)))
415 | GT ⇒ (pos (pred (m-n)))] ]
420 match nat_compare m n with
421 [ LT ⇒ (pos (pred (n-m)))
423 | GT ⇒ (neg (pred (m-n)))]
424 | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
426 interpretation "integer plus" 'plus x y = (Zplus x y).
428 ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
436 ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
440 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
442 ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
444 ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
448 ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
449 ncases (nat_compare q p);//]
452 ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
453 ncases (nat_compare q p);//
458 ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg O)+z.
461 ##|##*:#n;ncases n;//]
464 ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos O)+z.
467 ##|##*:#n;ncases n;//]
470 ntheorem Zplus_pos_pos:
471 ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
476 nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_O ?); (* XXX yet again *)
478 ##|#q;nnormalize;nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_Sm ??);//]
482 ntheorem Zplus_pos_neg:
483 ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
487 ntheorem Zplus_neg_pos :
488 ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
489 #n;#m;ncases n;ncases m;//;
492 ntheorem Zplus_neg_neg:
493 ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
496 ##|#p;ncases m;nnormalize;
497 ##[nrewrite > (plus_n_Sm ??);//
498 ##|#q;nrewrite > (plus_n_Sm ??);//]
502 ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
506 ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
510 ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
511 nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
515 ntheorem Zplus_Zsucc_pos_pos :
516 ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
520 ntheorem Zplus_Zsucc_pos_neg:
521 ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
523 napply (nat_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
526 ##|#n2;#IH;nelim n2;//]
528 ##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nelim IH;//]
531 ntheorem Zplus_Zsucc_neg_neg :
532 ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
534 napply (nat_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
537 ##|#n2;#IH;nelim n2;//]
541 ntheorem Zplus_Zsucc_neg_pos:
542 ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
544 napply (nat_elim2 (λn,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
547 ##|#n2;#IH;nelim n2;//]
549 ##|#n1;#m1;#IH;nrewrite < IH;nrewrite < (Zplus_neg_pos ? (S m1));//]
552 ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
554 ##[ncases y;//;#n;nnormalize;ncases n;//;
555 ##|##*:#n;ncases y;//]
558 ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
559 #x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
560 ##[nrewrite > (Zsucc_Zpred ?);//
561 ##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//]
564 ntheorem associative_Zplus: associative Z Zplus.
565 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
569 ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
571 nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
572 nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
574 ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
576 nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
577 nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
581 (* variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z)
582 \def associative_Zplus. *)
585 ndefinition Zopp : Z → Z ≝
591 interpretation "integer unary minus" 'uminus x = (Zopp x).
593 ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
597 ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
600 ##|##*:#n;ncases y;//;#m;nnormalize;napply nat_compare_elim;nnormalize;//]
603 ntheorem Zopp_Zopp: ∀x:Z. --x = x.
607 ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
610 ##|##*:#n;nnormalize;nrewrite > (nat_compare_n_n ?);//]
613 ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
615 nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
616 nrewrite < (Zplus_Zopp x);
617 nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
621 ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
623 napply (injective_Zplus_l x);
624 nrewrite < (sym_Zplus ??);
629 ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
631 interpretation "integer minus" 'minus x y = (Zminus x y).