helm/software/matita/nlibrary/arithmetics/Z.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16
  17 ninductive Z : Type ≝
  18   OZ : Z
  19 | pos : nat → Z
  20 | neg : nat → Z.
  21
  22 interpretation "Integers" 'Z = Z.
  23
  24 ndefinition Z_of_nat ≝
  25 λn. match n with
  26 [ O ⇒ OZ
  27 | S n ⇒ pos n].
  28
  29 ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.
  30
  31 ndefinition neg_Z_of_nat \def
  32 λn. match n with
  33 [ O ⇒ OZ
  34 | S n ⇒ neg n].
  35
  36 nlemma pos_n_eq_S_n : ∀n : nat.pos n = S n.
  37 //.
  38 nqed.
  39
  40 ndefinition abs ≝
  41 λz.match z with
  42 [ OZ ⇒ O
  43 | pos n ⇒ S n
  44 | neg n ⇒ S n].
  45
  46 ndefinition OZ_test ≝
  47 λz.match z with
  48 [ OZ ⇒ true
  49 | pos _ ⇒ false
  50 | neg _ ⇒ false].
  51
  52 ntheorem OZ_test_to_Prop : ∀z:Z.
  53   match OZ_test z with
  54   [true ⇒ z=OZ
  55   |false ⇒ z ≠ OZ].
  56 #z;ncases z
  57 ##[napply refl
  58 ##|##*:#z1;napply nmk;#H;ndestruct]
  59 nqed.
  60
  61 (* discrimination *)
  62 ntheorem injective_pos: injective nat Z pos.
  63 #n;#m;#H;ndestruct;//;
  64 nqed.
  65
  66 (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
  67 \def injective_pos. *)
  68
  69 ntheorem injective_neg: injective nat Z neg.
  70 #n;#m;#H;ndestruct;//;
  71 nqed.
  72
  73 (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
  74 \def injective_neg. *)
  75
  76 ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n.
  77 #n;napply nmk;#H;ndestruct;
  78 nqed.
  79
  80 ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
  81 #n;napply nmk;#H;ndestruct;
  82 nqed.
  83
  84 ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
  85 #n;#m;napply nmk;#H;ndestruct;
  86 nqed.
  87
  88 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
  89 #x;#y;ncases x;
  90 ##[ncases y;
  91    ##[@;//
  92    ##|##*:#n;@2;napply nmk;#H;ndestruct]
  93 ##|#n;ncases y;
  94    ##[@2;napply nmk;#H;ndestruct;
  95    ##|#m;ncases (decidable_eq_nat n m);#H;
  96       ##[nrewrite > H;@;//
  97       ##|@2;napply nmk;#H2;nelim H;
  98          (* bug if you don't introduce H3 *)#H3;ndestruct;
  99          napply H3;@]
 100    ##|#m;@2;napply nmk;#H;ndestruct]
 101 ##|#n;ncases y;
 102    ##[@2;napply nmk;#H;ndestruct;
 103    ##|#m;@2;napply nmk;#H;ndestruct
 104    ##|#m;ncases (decidable_eq_nat n m);#H;
 105       ##[nrewrite > H;@;//
 106       ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
 107          napply H3;@]##]##]
 108 nqed.
 109
 110 ndefinition Zsucc ≝
 111 λz. match z with
 112 [ OZ ⇒ pos O
 113 | pos n ⇒ pos (S n)
 114 | neg n ⇒
 115           match n with
 116           [ O ⇒ OZ
 117           | S p ⇒ neg p]].
 118
 119 ndefinition Zpred ≝
 120 λz. match z with
 121 [ OZ ⇒ neg O
 122 | pos n ⇒
 123           match n with
 124           [ O ⇒ OZ
 125           | S p ⇒ pos p]
 126 | neg n ⇒ neg (S n)].
 127
 128 ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
 129 #z;ncases z;
 130 ##[##1,2://
 131 ##|#n;ncases n;//]
 132 nqed.
 133
 134 ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
 135 #z;ncases z
 136 ##[##2:#n;ncases n;//
 137 ##|##*://]
 138 nqed.
 139
 140 ndefinition Zle : Z → Z → Prop ≝
 141 λx,y:Z.
 142   match x with
 143   [ OZ ⇒
 144     match y with
 145     [ OZ ⇒ True
 146     | pos m ⇒ True
 147     | neg m ⇒ False ]
 148   | pos n ⇒
 149     match y with
 150     [ OZ ⇒ False
 151     | pos m ⇒ n ≤ m
 152     | neg m ⇒ False ]
 153   | neg n ⇒
 154     match y with
 155     [ OZ ⇒ True
 156     | pos m ⇒ True
 157     | neg m ⇒ m ≤ n ]].
 158
 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)).
 161
 162 ndefinition Zlt : Z → Z → Prop ≝
 163 λx,y:Z.
 164   match x with
 165   [ OZ ⇒
 166     match y with
 167     [ OZ ⇒ False
 168     | pos m ⇒ True
 169     | neg m ⇒ False ]
 170   | pos n ⇒
 171     match y with
 172     [ OZ ⇒ False
 173     | pos m ⇒ n<m
 174     | neg m ⇒ False ]
 175   | neg n ⇒
 176     match y with
 177     [ OZ ⇒ True
 178     | pos m ⇒ True
 179     | neg m ⇒ m<n ]].
 180
 181 interpretation "integer 'less than'" 'lt x y = (Zlt x y).
 182 interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
 183
 184 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
 185 #x;ncases x
 186 ##[napply nmk;//
 187 ##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
 188 nqed.
 189
 190 (* transitivity *)
 191 ntheorem transitive_Zle : transitive Z Zle.
 192 #x;#y;#z;ncases x
 193 ##[ncases y
 194    ##[//
 195    ##|##*:#n;ncases z;//]
 196 ##|#n;ncases y
 197    ##[#H;ncases H
 198    ##|(*##*:#m;#Hl;ncases z;//;*)
 199       #m;#Hl;ncases z;//;#p;#Hr;
 200       napply (transitive_le n m p);//; (* XXX: auto??? *)
 201    ##|#m;#Hl;ncases Hl]
 202 ##|#n;ncases y
 203    ##[#Hl;ncases z
 204       ##[##1,2://
 205       ##|#m;#Hr;ncases Hr]
 206    ##|#m;#Hl;ncases z;
 207       ##[##1,2://
 208       ##|#p;#Hr;ncases Hr]
 209    ##|#m;#Hl;ncases z;//;#p;#Hr;
 210       napply (transitive_le p m n);//; (* XXX: auto??? *) ##]
 211 nqed.
 212
 213 (* variant trans_Zle: transitive Z Zle
 214 \def transitive_Zle.*)
 215
 216 ntheorem transitive_Zlt: transitive Z Zlt.
 217 #x;#y;#z;ncases x
 218 ##[ncases y
 219    ##[//
 220    ##|#n;ncases z
 221       ##[#_;#Hr;ncases Hr
 222       ##|//
 223       ##|#m;#_;#Hr;ncases Hr]
 224    ##|#n;#Hl;ncases Hl]
 225 ##|#n;ncases y
 226    ##[#Hl;ncases Hl
 227    ##|#m;ncases z
 228       ##[//
 229       ##|#p;napply transitive_lt (* XXX: auto??? *)
 230       ##|//##]
 231    ##|#m;#Hl;ncases Hl]
 232 ##|#n;ncases y
 233    ##[ncases z;
 234       ##[##1,2://
 235       ##|#m;#_;#Hr;ncases Hr]
 236    ##|#m;ncases z;
 237       ##[##1,2://
 238       ##|#p;#_;#Hr;ncases Hr]
 239    ##|#m;ncases z
 240       ##[##1,2://
 241       ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)]
 242    ##]
 243 ##]
 244 nqed.
 245
 246 (* variant trans_Zlt: transitive Z Zlt
 247 \def transitive_Zlt.
 248 theorem irrefl_Zlt: irreflexive Z Zlt
 249 \def irreflexive_Zlt.*)
 250
 251 ntheorem Zlt_neg_neg_to_lt:
 252   ∀n,m:nat. neg n < neg m → m < n.
 253 //;
 254 nqed.
 255
 256 ntheorem lt_to_Zlt_neg_neg: ∀n,m:nat.m < n → neg n < neg m.
 257 //;
 258 nqed.
 259
 260 ntheorem Zlt_pos_pos_to_lt:
 261   ∀n,m:nat. pos n < pos m → n < m.
 262 //;
 263 nqed.
 264
 265 ntheorem lt_to_Zlt_pos_pos: ∀n,m:nat.n < m → pos n < pos m.
 266 //;
 267 nqed.
 268
 269 ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
 270 #x;#y;ncases x
 271 ##[ncases y
 272    ##[#H;ncases H
 273    ##|//;
 274    ##|#p;#H;ncases H]
 275 ##|#n;ncases y
 276    ##[#H;ncases H
 277    ##|#p;nnormalize;//
 278    ##|#p;#H;ncases H]
 279 ##|#n;ncases y
 280    ##[##1,2:ncases n;//
 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? *)]
 284    ##]
 285 ##]
 286 nqed.
 287
 288 (*** COMPARE ***)
 289
 290 (* boolean equality *)
 291 ndefinition eqZb : Z → Z → bool ≝
 292 λx,y:Z.
 293   match x with
 294   [ OZ ⇒
 295       match y with
 296         [ OZ ⇒ true
 297         | pos q ⇒ false
 298         | neg q ⇒ false]
 299   | pos p ⇒
 300       match y with
 301         [ OZ ⇒ false
 302         | pos q ⇒ eqb p q
 303         | neg q ⇒ false]
 304   | neg p ⇒
 305       match y with
 306         [ OZ ⇒ false
 307         | pos q ⇒ false
 308         | neg q ⇒ eqb p q]].
 309
 310 ntheorem eqZb_to_Prop:
 311   ∀x,y:Z.
 312     match eqZb x y with
 313     [ true ⇒ x=y
 314     | false ⇒ x ≠ y].
 315 #x;#y;ncases x
 316 ##[ncases y;
 317    ##[//
 318    ##|napply not_eq_OZ_pos (* XXX: auto? *)
 319    ##|napply not_eq_OZ_neg (* XXX: auto? *)]
 320 ##|#n;ncases y;
 321    ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
 322    ##|#m;napply eqb_elim;
 323       ##[//
 324       ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
 325    ##|#m;napply not_eq_pos_neg]
 326 ##|#n;ncases y
 327    ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
 328    ##|#m;napply nmk;#H;ndestruct
 329    ##|#m;napply eqb_elim;
 330       ##[//
 331       ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
 332    ##]
 333 ##]
 334 nqed.
 335
 336 ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
 337   (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
 338 #x;#y;#P;#HP1;#HP2;
 339 ncut
 340 (match (eqZb x y) with
 341 [ true ⇒ x=y
 342 | false ⇒ x ≠ y] → P (eqZb x y))
 343 ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *)
 344    ##[napply HP1
 345    ##|napply HP2]
 346 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
 347 nqed.
 348
 349 include "arithmetics/compare.ma".
 350
 351 ndefinition Z_compare : Z → Z → compare ≝
 352 λx,y:Z.
 353   match x with
 354   [ OZ ⇒
 355     match y with
 356     [ OZ ⇒ EQ
 357     | pos m ⇒ LT
 358     | neg m ⇒ GT ]
 359   | pos n ⇒
 360     match y with
 361     [ OZ ⇒ GT
 362     | pos m ⇒ nat_compare n m
 363     | neg m ⇒ GT]
 364   | neg n ⇒
 365     match y with
 366     [ OZ ⇒ LT
 367     | pos m ⇒ LT
 368     | neg m ⇒ nat_compare m n ]].
 369
 370 ntheorem Z_compare_to_Prop :
 371 ∀x,y:Z. match (Z_compare x y) with
 372 [ LT ⇒ x < y
 373 | EQ ⇒ x=y
 374 | GT ⇒ y < x].
 375 #x;#y;nelim x
 376 ##[nelim y;//;
 377 ##|nelim y
 378    ##[##1,3://
 379    ##|#n;#m;nnormalize;
 380       ncut (match (nat_compare m n) with
 381       [ LT ⇒ m < n
 382       | EQ ⇒ m = n
 383       | GT ⇒ n < m ] →
 384       match (nat_compare m n) with
 385       [ LT ⇒ S m  ≤ n
 386       | EQ ⇒ pos m = pos n
 387       | GT ⇒ S n  ≤ m])
 388       ##[ncases (nat_compare m n);//
 389       ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
 390    ##]
 391 ##|nelim y
 392    ##[#n;//
 393    ##|nnormalize;//
 394    ##|nnormalize;#n;#m;
 395       ncut (match (nat_compare n m) with
 396         [ LT ⇒ n < m
 397         | EQ ⇒ n = m
 398         | GT ⇒ m < n] →
 399       match (nat_compare n m) with
 400       [ LT ⇒ S n ≤ m
 401       | EQ ⇒ neg m = neg n
 402       | GT ⇒ S m ≤ n])
 403       ##[ncases (nat_compare n m);//
 404       ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
 405    ##]
 406 ##]
 407 nqed.
 408
 409 ndefinition Zplus : Z → Z → Z ≝
 410   λx,y. match x with
 411     [ OZ ⇒ y
 412     | pos m ⇒
 413         match y with
 414          [ OZ ⇒ x
 415          | pos n ⇒ (pos (pred ((S m)+(S n))))
 416          | neg n ⇒
 417               match nat_compare m n with
 418                 [ LT ⇒ (neg (pred (n-m)))
 419                 | EQ ⇒ OZ
 420                 | GT ⇒ (pos (pred (m-n)))] ]
 421     | neg m ⇒
 422         match y with
 423          [ OZ ⇒ x
 424          | pos n ⇒
 425               match nat_compare m n with
 426                 [ LT ⇒ (pos (pred (n-m)))
 427                 | EQ ⇒ OZ
 428                 | GT ⇒ (neg (pred (m-n)))]
 429          | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
 430
 431 interpretation "integer plus" 'plus x y = (Zplus x y).
 432
 433 ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
 434 #n;#m;ncases n
 435 ##[//
 436 ##|#p;ncases m
 437    ##[nnormalize;//
 438    ##|//]
 439 nqed.
 440
 441 ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
 442 #z;ncases z;//;
 443 nqed.
 444
 445 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
 446
 447 ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x.
 448 #x;#y;ncases x;
 449 ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);//
 450 ##|#p;ncases y
 451    ##[//
 452    ##|nnormalize;//
 453    ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
 454       ncases (nat_compare q p);//]
 455 ##|#p;ncases y
 456    ##[//;
 457    ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*);
 458       ncases (nat_compare q p);//
 459    ##|nnormalize;//]
 460 ##]
 461 nqed.
 462
 463 ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg O)+z.
 464 #z;ncases z
 465 ##[//
 466 ##|##*:#n;ncases n;//]
 467 nqed.
 468
 469 ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos O)+z.
 470 #z;ncases z
 471 ##[//
 472 ##|##*:#n;ncases n;//]
 473 nqed.
 474
 475 ntheorem Zplus_pos_pos:
 476   ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
 477 #n;#m;ncases n
 478 ##[ncases m;//
 479 ##|#p;ncases m
 480    ##[nnormalize;
 481       nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_O ?); (* XXX yet again *)
 482       //
 483    ##|#q;nnormalize;nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_Sm ??);//]
 484 ##]
 485 nqed.
 486
 487 ntheorem Zplus_pos_neg:
 488   ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
 489 //;
 490 nqed.
 491
 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;//;
 495 nqed.
 496
 497 ntheorem Zplus_neg_neg:
 498   ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
 499 #n;#m;ncases n
 500 ##[ncases m;//
 501 ##|#p;ncases m;nnormalize;
 502    ##[nrewrite > (plus_n_Sm ??);//
 503    ##|#q;nrewrite > (plus_n_Sm ??);//]
 504 ##]
 505 nqed.
 506
 507 ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
 508 #x;#y;ncases x
 509 ##[ncases y
 510    ##[//
 511    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
 512    ##|//]
 513 ##|ncases y;/2/;
 514 ##|ncases y
 515    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
 516       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
 517    ##|##*://]
 518 nqed.
 519
 520 ntheorem Zplus_Zsucc_pos_pos :
 521   ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
 522 //;
 523 nqed.
 524
 525 ntheorem Zplus_Zsucc_pos_neg:
 526   ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
 527 #n;#m;
 528 napply (nat_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
 529 ##[#n1;nelim n1
 530    ##[//
 531    ##|#n2;#IH;nelim n2;//]
 532 ##|//
 533 ##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nelim IH;//]
 534 nqed.
 535
 536 ntheorem Zplus_Zsucc_neg_neg :
 537   ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 538 #n;#m;
 539 napply (nat_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
 540 ##[#n1;nelim n1
 541    ##[//
 542    ##|#n2;#IH;nelim n2;//]
 543 ##|##*://]
 544 nqed.
 545
 546 ntheorem Zplus_Zsucc_neg_pos:
 547   ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 548 #n;#m;
 549 napply (nat_elim2 (λn,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
 550 ##[#n1;nelim n1
 551    ##[//
 552    ##|#n2;#IH;nelim n2;//]
 553 ##|//
 554 ##|#n1;#m1;#IH;nrewrite < IH;nrewrite < (Zplus_neg_pos ? (S m1));//]
 555 nqed.
 556
 557 ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
 558 #x;#y;ncases x
 559 ##[ncases y;//;#n;nnormalize;ncases n;//;
 560 ##|##*:#n;ncases y;//]
 561 nqed.
 562
 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 ??);//]
 567 nqed.
 568
 569 ntheorem associative_Zplus: associative Z Zplus.
 570 (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
 571 #x;#y;#z;ncases x
 572 ##[//
 573 ##|#n;nelim n
 574    ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//;
 575    ##|#n1;#IH;
 576       nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?);
 577       nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//]
 578 ##|#n;nelim n
 579    ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//;
 580    ##|#n1;#IH;
 581       nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?);
 582       nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//]
 583 ##]
 584 nqed.
 585
 586 (* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
 587 \def associative_Zplus. *)
 588
 589 (* Zopp *)
 590 ndefinition Zopp : Z → Z ≝
 591   λx:Z. match x with
 592   [ OZ ⇒ OZ
 593   | pos n ⇒ neg n
 594   | neg n ⇒ pos n ].
 595
 596 interpretation "integer unary minus" 'uminus x = (Zopp x).
 597
 598 ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ).
 599 //;
 600 nqed.
 601
 602 ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
 603 #x;#y;ncases x
 604 ##[ncases y;//
 605 ##|##*:#n;ncases y;//;#m;nnormalize;napply nat_compare_elim;nnormalize;//]
 606 nqed.
 607
 608 ntheorem Zopp_Zopp: ∀x:Z. --x = x.
 609 #x;ncases x;//;
 610 nqed.
 611
 612 ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
 613 #x;ncases x
 614 ##[//
 615 ##|##*:#n;nnormalize;nrewrite > (nat_compare_n_n ?);//]
 616 nqed.
 617
 618 ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
 619 #x;#z;#y;#H;
 620 nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y);
 621 nrewrite < (Zplus_Zopp x);
 622 nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???);
 623 //;
 624 nqed.
 625
 626 ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
 627 #x;#z;#y;#H;
 628 napply (injective_Zplus_l x);
 629 nrewrite < (sym_Zplus ??);
 630 //;
 631 nqed.
 632
 633 (* minus *)
 634 ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).
 635
 636 interpretation "integer minus" 'minus x y = (Zminus x y).