matita/contribs/library_auto/auto/Z/plus.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 set "baseuri" "cic:/matita/library_autobatch/Z/plus".
  16
  17 include "auto/Z/z.ma".
  18 include "auto/nat/minus.ma".
  19
  20 definition Zplus :Z \to Z \to Z \def
  21 \lambda x,y.
  22   match x with
  23     [ OZ \Rightarrow y
  24     | (pos m) \Rightarrow
  25         match y with
  26          [ OZ \Rightarrow x
  27          | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
  28          | (neg n) \Rightarrow
  29               match nat_compare m n with
  30                 [ LT \Rightarrow (neg (pred (n-m)))
  31                 | EQ \Rightarrow OZ
  32                 | GT \Rightarrow (pos (pred (m-n)))] ]
  33     | (neg m) \Rightarrow
  34         match y with
  35          [ OZ \Rightarrow x
  36          | (pos n) \Rightarrow
  37               match nat_compare m n with
  38                 [ LT \Rightarrow (pos (pred (n-m)))
  39                 | EQ \Rightarrow OZ
  40                 | GT \Rightarrow (neg (pred (m-n)))]
  41          | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
  42
  43 (*CSC: the URI must disappear: there is a bug now *)
  44 interpretation "integer plus" 'plus x y = (cic:/matita/library_autobatch/Z/plus/Zplus.con x y).
  45
  46 theorem Zplus_z_OZ:  \forall z:Z. z+OZ = z.
  47 intro.
  48 elim z;autobatch.
  49   (*simplify;reflexivity.*)
  50 qed.
  51
  52 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
  53
  54 theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
  55 intros.
  56 elim x
  57 [ autobatch
  58   (*rewrite > Zplus_z_OZ.
  59   reflexivity*)
  60 | elim y
  61   [ autobatch
  62     (*simplify.
  63     reflexivity*)
  64   | simplify.
  65     autobatch
  66     (*rewrite < plus_n_Sm.
  67     rewrite < plus_n_Sm.
  68     rewrite < sym_plus.
  69     reflexivity*)
  70   | simplify.
  71     rewrite > nat_compare_n_m_m_n.
  72     simplify.
  73     elim nat_compare;autobatch
  74     (*[ simplify.
  75       reflexivity
  76     | simplify.
  77       reflexivity
  78     | simplify.
  79       reflexivity
  80     ]*)
  81   ]
  82 | elim y
  83   [ autobatch
  84     (*simplify.
  85     reflexivity*)
  86   | simplify.
  87     rewrite > nat_compare_n_m_m_n.
  88     simplify.
  89     elim nat_compare;autobatch
  90     (*[ simplify.
  91       reflexivity
  92     | simplify.
  93       reflexivity
  94     | simplify.
  95       reflexivity
  96     ]*)
  97   | simplify.
  98     autobatch
  99     (*rewrite < plus_n_Sm.
 100     rewrite < plus_n_Sm.
 101     rewrite < sym_plus.
 102     reflexivity*)
 103   ]
 104 ]
 105 qed.
 106
 107 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
 108 intros.
 109 elim z
 110 [ autobatch
 111   (*simplify.
 112   reflexivity*)
 113 | elim n;autobatch
 114   (*[ simplify.
 115     reflexivity
 116   | simplify.
 117     reflexivity
 118   ]*)
 119 | simplify.
 120   reflexivity
 121 ]
 122 qed.
 123
 124 theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
 125 intros.
 126 elim z
 127 [ autobatch
 128   (*simplify.
 129   reflexivity*)
 130 | autobatch
 131   (*simplify.
 132   reflexivity*)
 133 | elim n;autobatch
 134   (*[ simplify.
 135     reflexivity
 136   | simplify.
 137     reflexivity
 138   ]*)
 139 ]
 140 qed.
 141
 142 theorem Zplus_pos_pos:
 143 \forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
 144 intros.
 145 elim n
 146 [ elim m;autobatch
 147   (*[ simplify.
 148     reflexivity
 149   | simplify.
 150     reflexivity
 151   ]*)
 152 | elim m
 153   [ autobatch
 154     (*simplify.
 155     rewrite < plus_n_Sm.
 156     rewrite < plus_n_O.
 157     reflexivity*)
 158   | simplify.
 159     autobatch
 160     (*rewrite < plus_n_Sm.
 161     rewrite < plus_n_Sm.
 162     reflexivity*)
 163   ]
 164 ]
 165 qed.
 166
 167 theorem Zplus_pos_neg:
 168 \forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
 169 intros.
 170 reflexivity.
 171 qed.
 172
 173 theorem Zplus_neg_pos :
 174 \forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
 175 intros.
 176 elim n
 177 [ elim m;autobatch
 178   (*[ simplify.
 179     reflexivity
 180   | simplify.
 181     reflexivity
 182   ]*)
 183 | elim m;autobatch
 184   (*[ simplify.
 185     reflexivity
 186   | simplify.
 187     reflexivity
 188   ]*)
 189 ]
 190 qed.
 191
 192 theorem Zplus_neg_neg:
 193 \forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
 194 intros.
 195 elim n
 196 [ autobatch
 197   (*elim m
 198   [ simplify.
 199     reflexivity
 200   | simplify.
 201     reflexivity
 202   ]*)
 203 | elim m
 204   [ autobatch
 205     (*simplify.
 206     rewrite > plus_n_Sm.
 207     reflexivity*)
 208   | simplify.
 209     autobatch
 210     (*rewrite > plus_n_Sm.
 211     reflexivity*)
 212   ]
 213 ]
 214 qed.
 215
 216 theorem Zplus_Zsucc_Zpred:
 217 \forall x,y. x+y = (Zsucc x)+(Zpred y).
 218 intros.
 219 elim x
 220 [ autobatch
 221   (*elim y
 222   [ simplify.
 223     reflexivity
 224   | rewrite < Zsucc_Zplus_pos_O.
 225     rewrite > Zsucc_Zpred.
 226     reflexivity
 227   | simplify.
 228     reflexivity
 229   ]*)
 230 | elim y;autobatch
 231   (*[ simplify.
 232     reflexivity
 233   | apply Zplus_pos_pos
 234   | apply Zplus_pos_neg
 235   ]*)
 236 | elim y;autobatch
 237   (*[ rewrite < sym_Zplus.
 238     rewrite < (sym_Zplus (Zpred OZ)).
 239     rewrite < Zpred_Zplus_neg_O.
 240     rewrite > Zpred_Zsucc.
 241     simplify.
 242     reflexivity
 243   | apply Zplus_neg_pos
 244   | rewrite < Zplus_neg_neg.
 245     reflexivity
 246   ]*)
 247 ]
 248 qed.
 249
 250 theorem Zplus_Zsucc_pos_pos :
 251 \forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
 252 intros.
 253 reflexivity.
 254 qed.
 255
 256 theorem Zplus_Zsucc_pos_neg:
 257 \forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
 258 intros.
 259 apply (nat_elim2
 260 (\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
 261 [ intro.
 262   elim n1;autobatch
 263   (*[ simplify.
 264     reflexivity
 265   | elim n2; simplify; reflexivity
 266   ]*)
 267 | intros.
 268   autobatch
 269   (*elim n1;simplify;reflexivity*)
 270 | intros.
 271   rewrite < (Zplus_pos_neg ? m1).
 272   elim H.
 273   reflexivity
 274 ]
 275 qed.
 276
 277 theorem Zplus_Zsucc_neg_neg :
 278 \forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 279 intros.
 280 apply (nat_elim2
 281 (\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
 282 [ intros.
 283   autobatch
 284   (*elim n1
 285   [ simplify.
 286     reflexivity
 287   | elim n2;simplify;reflexivity
 288   ]*)
 289 | intros.
 290   autobatch
 291   (*elim n1;simplify;reflexivity*)
 292 | intros.
 293   autobatch.
 294   (*rewrite < (Zplus_neg_neg ? m1).
 295   reflexivity*)
 296 ]
 297 qed.
 298
 299 theorem Zplus_Zsucc_neg_pos:
 300 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 301 intros.
 302 apply (nat_elim2
 303 (\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
 304 [ intros.
 305   autobatch
 306   (*elim n1
 307   [ simplify.
 308     reflexivity
 309   | elim n2;simplify;reflexivity
 310   ]*)
 311 | intros.
 312   autobatch
 313   (*elim n1;simplify;reflexivity*)
 314 | intros.
 315   autobatch
 316   (*rewrite < H.
 317   rewrite < (Zplus_neg_pos ? (S m1)).
 318   reflexivity*)
 319 ]
 320 qed.
 321
 322 theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
 323 intros.
 324 elim x
 325 [ autobatch
 326   (*elim y
 327   [ simplify.
 328     reflexivity
 329   | simplify.
 330     reflexivity
 331   | rewrite < Zsucc_Zplus_pos_O.
 332     reflexivity
 333   ]*)
 334 | elim y;autobatch
 335   (*[ rewrite < (sym_Zplus OZ).
 336     reflexivity
 337   | apply Zplus_Zsucc_pos_pos
 338   | apply Zplus_Zsucc_pos_neg
 339   ]*)
 340 | elim y;autobatch
 341   (*[ rewrite < sym_Zplus.
 342     rewrite < (sym_Zplus OZ).
 343     simplify.
 344     reflexivity
 345   | apply Zplus_Zsucc_neg_pos
 346   | apply Zplus_Zsucc_neg_neg
 347   ]*)
 348 ]
 349 qed.
 350
 351 theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
 352 intros.
 353 cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y));autobatch.
 354 (*[ rewrite > Hcut.
 355   rewrite > Zplus_Zsucc.
 356   rewrite > Zpred_Zsucc.
 357   reflexivity
 358 | rewrite > Zsucc_Zpred.
 359   reflexivity
 360 ]*)
 361 qed.
 362
 363
 364 theorem associative_Zplus: associative Z Zplus.
 365 change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)).
 366 (* simplify. *)
 367 intros.
 368 elim x
 369 [ autobatch
 370   (*simplify.
 371   reflexivity*)
 372 | elim n
 373   [ rewrite < Zsucc_Zplus_pos_O.
 374     autobatch
 375     (*rewrite < Zsucc_Zplus_pos_O.
 376     rewrite > Zplus_Zsucc.
 377     reflexivity*)
 378   | rewrite > (Zplus_Zsucc (pos n1)).
 379     rewrite > (Zplus_Zsucc (pos n1)).
 380     autobatch
 381     (*rewrite > (Zplus_Zsucc ((pos n1)+y)).
 382     apply eq_f.
 383     assumption*)
 384   ]
 385 | elim n
 386   [ rewrite < (Zpred_Zplus_neg_O (y+z)).
 387     autobatch
 388     (*rewrite < (Zpred_Zplus_neg_O y).
 389     rewrite < Zplus_Zpred.
 390     reflexivity*)
 391   | rewrite > (Zplus_Zpred (neg n1)).
 392     rewrite > (Zplus_Zpred (neg n1)).
 393     autobatch
 394     (*rewrite > (Zplus_Zpred ((neg n1)+y)).
 395     apply eq_f.
 396     assumption*)
 397   ]
 398 ]
 399 qed.
 400
 401 variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
 402 \def associative_Zplus.
 403
 404 (* Zopp *)
 405 definition Zopp : Z \to Z \def
 406 \lambda x:Z. match x with
 407 [ OZ \Rightarrow OZ
 408 | (pos n) \Rightarrow (neg n)
 409 | (neg n) \Rightarrow (pos n) ].
 410
 411 (*CSC: the URI must disappear: there is a bug now *)
 412 interpretation "integer unary minus" 'uminus x = (cic:/matita/library_autobatch/Z/plus/Zopp.con x).
 413
 414 theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
 415 intros.
 416 elim x
 417 [ elim y;autobatch
 418   (*simplify;reflexivity*)
 419 | elim y
 420   [ autobatch
 421     (*simplify.
 422     reflexivity*)
 423   | autobatch
 424     (*simplify.
 425     reflexivity*)
 426   | simplify.
 427     apply nat_compare_elim;
 428       intro;autobatch (*simplify;reflexivity*)
 429   ]
 430 | elim y
 431   [ autobatch
 432     (*simplify.
 433     reflexivity*)
 434   | simplify.
 435     apply nat_compare_elim;
 436       intro;autobatch
 437         (*simplify;reflexivity*)
 438   | autobatch
 439     (*simplify.
 440     reflexivity*)
 441   ]
 442 ]
 443 qed.
 444
 445 theorem Zopp_Zopp: \forall x:Z. --x = x.
 446 intro.
 447 elim x;reflexivity.
 448 qed.
 449
 450 theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ.
 451 intro.
 452 elim x
 453 [ apply refl_eq
 454 | simplify.
 455   rewrite > nat_compare_n_n.
 456   autobatch
 457   (*simplify.
 458   apply refl_eq*)
 459 | simplify.
 460   rewrite > nat_compare_n_n.
 461   autobatch
 462   (*simplify.
 463   apply refl_eq*)
 464 ]
 465 qed.
 466
 467 (* minus *)
 468 definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
 469
 470 interpretation "integer minus" 'minus x y = (cic:/matita/library_autobatch/Z/plus/Zminus.con x y).