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