helm/matita/tests/match.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/tests/".
  16
  17
  18 inductive True: Prop \def
  19 I : True.
  20
  21 inductive False: Prop \def .
  22
  23 definition Not: Prop \to Prop \def
  24 \lambda A. (A \to False).
  25
  26 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
  27 intros. elim (H1 H).
  28 qed.
  29
  30 inductive And (A,B:Prop) : Prop \def
  31     conj : A \to B \to (And A B).
  32
  33 theorem proj1: \forall A,B:Prop. (And A B) \to A.
  34 intros. elim H. assumption.
  35 qed.
  36
  37 theorem proj2: \forall A,B:Prop. (And A B) \to A.
  38 intros. elim H. assumption.
  39 qed.
  40
  41 inductive Or (A,B:Prop) : Prop \def
  42      or_introl : A \to (Or A B)
  43    | or_intror : B \to (Or A B).
  44
  45 inductive ex (A:Type) (P:A \to Prop) : Prop \def
  46     ex_intro: \forall x:A. P x \to ex A P.
  47
  48 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
  49     ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
  50
  51 inductive eq (A:Type) (x:A) : A \to Prop \def
  52     refl_equal : eq A x x.
  53
  54 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y  \to eq A y x.
  55 intros. elim H. apply refl_equal.
  56 qed.
  57
  58 theorem trans_eq : \forall A:Type.
  59 \forall x,y,z:A. eq A x y  \to eq A y z \to eq A x z.
  60 intros.elim H1.assumption.
  61 qed.
  62
  63 theorem f_equal: \forall  A,B:Type.\forall f:A\to B.
  64 \forall x,y:A. eq A x y \to eq B (f x) (f y).
  65 intros.elim H.apply refl_equal.
  66 qed.
  67
  68 theorem f_equal2: \forall  A,B,C:Type.\forall f:A\to B \to C.
  69 \forall x1,x2:A. \forall y1,y2:B.
  70 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
  71 intros.elim H1.elim H.apply refl_equal.
  72 qed.
  73
  74 inductive nat : Set \def
  75   | O : nat
  76   | S : nat \to nat.
  77
  78 definition pred: nat \to nat \def
  79 \lambda n:nat. match n with
  80 [ O \Rightarrow  O
  81 | (S u) \Rightarrow u ].
  82
  83 theorem pred_Sn : \forall n:nat.
  84 (eq nat n (pred (S n))).
  85 intros.apply refl_equal.
  86 qed.
  87
  88 theorem injective_S : \forall n,m:nat.
  89 (eq nat (S n) (S m)) \to (eq nat n m).
  90 intros.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))).
  91 apply f_equal. assumption.
  92 qed.
  93
  94 theorem not_eq_S  : \forall n,m:nat.
  95 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
  96 intros. simplify.intros.
  97 apply H.apply injective_S.assumption.
  98 qed.
  99
 100 definition not_zero : nat \to Prop \def
 101 \lambda n: nat.
 102   match n with
 103   [ O \Rightarrow False
 104   | (S p) \Rightarrow True ].
 105
 106 theorem O_S : \forall n:nat. Not (eq nat O (S n)).
 107 intros.simplify.intros.
 108 cut (not_zero O).exact Hcut.elim (sym_eq ? ? ? H).
 109 exact I.
 110 qed.
 111
 112 theorem n_Sn : \forall n:nat. Not (eq nat n (S n)).
 113 intros.elim n.apply O_S.apply not_eq_S.assumption.
 114 qed.
 115
 116
 117 let rec plus n m \def
 118  match n with
 119  [ O \Rightarrow m
 120  | (S p) \Rightarrow S (plus p m) ].
 121
 122 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
 123 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 124 qed.
 125
 126 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n  m)) (plus n (S m)).
 127 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 128 qed.
 129
 130 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
 131 intros.elim n.simplify.apply plus_n_O.
 132 simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm.
 133 qed.
 134
 135 theorem assoc_plus:
 136 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
 137 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 138 qed.
 139
 140 let rec times n m \def
 141  match n with
 142  [ O \Rightarrow O
 143  | (S p) \Rightarrow (plus m (times p m)) ].
 144
 145 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 146 intros.elim n.simplify.apply refl_equal.simplify.assumption.
 147 qed.
 148
 149 theorem times_n_Sm :
 150 \forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
 151 intros.elim n.simplify.apply refl_equal.
 152 simplify.apply f_equal.elim H.
 153 apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq.
 154 apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)).
 155 apply f_equal2.
 156 apply sym_plus.apply refl_equal.apply assoc_plus.
 157 qed.
 158
 159 theorem sym_times :
 160 \forall n,m:nat. eq nat (times n m) (times m n).
 161 intros.elim n.simplify.apply times_n_O.
 162 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 163 qed.
 164
 165 let rec minus n m \def
 166  match n with
 167  [ O \Rightarrow O
 168  | (S p) \Rightarrow
 169         match m with
 170         [O \Rightarrow (S p)
 171         | (S q) \Rightarrow minus p q ]].
 172
 173 theorem nat_case :
 174 \forall n:nat.\forall P:nat \to Prop.
 175 P O \to  (\forall m:nat. P (S m)) \to P n.
 176 intros.elim n.assumption.apply H1.
 177 qed.
 178
 179 theorem nat_double_ind :
 180 \forall R:nat \to nat \to Prop.
 181 (\forall n:nat. R O n) \to
 182 (\forall n:nat. R (S n) O) \to
 183 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 184 intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
 185 apply nat_case m1.apply H1.intros.apply H2. apply H3.
 186 qed.
 187
 188 inductive bool : Set \def
 189   | true : bool
 190   | false : bool.
 191
 192 definition notn : bool \to bool \def
 193 \lambda b:bool.
 194  match b with
 195  [ true \Rightarrow false
 196  | false \Rightarrow true ].
 197
 198 definition andb : bool \to bool \to bool\def
 199 \lambda b1,b2:bool.
 200  match b1 with
 201  [ true \Rightarrow
 202         match b2 with [true \Rightarrow true | false \Rightarrow false]
 203  | false \Rightarrow false ].
 204
 205 definition orb : bool \to bool \to bool\def
 206 \lambda b1,b2:bool.
 207  match b1 with
 208  [ true \Rightarrow
 209         match b2 with [true \Rightarrow true | false \Rightarrow false]
 210  | false \Rightarrow false ].
 211
 212 definition if_then_else : bool \to Prop \to Prop \to Prop \def
 213 \lambda b:bool.\lambda P,Q:Prop.
 214 match b with
 215 [ true \Rightarrow P
 216 | false  \Rightarrow Q].
 217
 218 inductive le (n:nat) : nat \to Prop \def
 219   | le_n : le n n
 220   | le_S : \forall m:nat. le n m \to le n (S m).
 221
 222 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
 223 intros.
 224 elim H1.assumption.
 225 apply le_S.assumption.
 226 qed.
 227
 228 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
 229 intros.elim H.
 230 apply le_n.apply le_S.assumption.
 231 qed.
 232
 233 theorem le_O_n : \forall n:nat. le O n.
 234 intros.elim n.apply le_n.apply le_S. assumption.
 235 qed.
 236
 237 theorem le_n_Sn : \forall n:nat. le n (S n).
 238 intros. apply le_S.apply le_n.
 239 qed.
 240
 241 theorem le_pred_n : \forall n:nat. le (pred n) n.
 242 intros.elim n.simplify.apply le_n.simplify.
 243 apply le_n_Sn.
 244 qed.
 245
 246 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
 247 intros.elim H.exact I.exact I.
 248 qed.
 249
 250 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 251 intros.simplify.intros.apply not_zero_le ? O H.
 252 qed.
 253
 254 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
 255 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
 256 elim n.apply refl_equal.apply False_ind.apply  (le_Sn_O ? H2).
 257 qed.
 258
 259 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
 260 intros.cut le (pred (S n)) (pred (S m)).exact Hcut.
 261 elim H.apply le_n.apply trans_le ? (pred x).assumption.
 262 apply le_pred_n.
 263 qed.
 264
 265 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
 266 intros.elim n.apply le_Sn_O.simplify.intros.
 267 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
 268 qed.
 269
 270 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 271 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 272 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
 273 intros.whd.intros.
 274 apply le_n_O_eq.assumption.
 275 intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption.
 276 intros.whd.intros.apply f_equal.apply H2.
 277 apply le_S_n.assumption.
 278 apply le_S_n.assumption.
 279 qed.
 280
 281 let rec leb n m \def
 282     match n with
 283     [ O \Rightarrow true
 284     | (S p) \Rightarrow
 285         match m with
 286         [ O \Rightarrow false
 287         | (S q) \Rightarrow leb p q]].
 288
 289 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 290 intros.
 291 apply (nat_double_ind
 292 (\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
 293 simplify.intros.apply le_O_n.
 294 simplify.exact le_Sn_O.
 295 intros 2.simplify.elim (leb n1 m1).
 296 simplify.apply le_n_S.apply H.
 297 simplify.intros.apply H.apply le_S_n.assumption.
 298 qed.
 299
 300 inductive Z : Set \def
 301   OZ : Z
 302 | pos : nat \to Z
 303 | neg : nat \to Z.
 304
 305 definition Z_of_nat \def
 306 \lambda n. match n with
 307 [ O \Rightarrow  OZ
 308 | (S n)\Rightarrow  pos n].
 309
 310 coercion Z_of_nat.
 311
 312 definition neg_Z_of_nat \def
 313 \lambda n. match n with
 314 [ O \Rightarrow  OZ
 315 | (S n)\Rightarrow  neg n].
 316
 317 definition absZ \def
 318 \lambda z.
 319  match z with
 320 [ OZ \Rightarrow O
 321 | (pos n) \Rightarrow n
 322 | (neg n) \Rightarrow n].
 323
 324 definition OZ_testb \def
 325 \lambda z.
 326 match z with
 327 [ OZ \Rightarrow true
 328 | (pos n) \Rightarrow false
 329 | (neg n) \Rightarrow false].
 330
 331 theorem OZ_discr :
 332 \forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)).
 333 intros.elim z.simplify.apply refl_equal.
 334 simplify.intros.
 335 cut match neg e with
 336 [ OZ \Rightarrow True
 337 | (pos n) \Rightarrow False
 338 | (neg n) \Rightarrow False].
 339 apply Hcut. elim (sym_eq ? ? ? H).simplify.exact I.
 340 simplify.intros.
 341 cut match pos e with
 342 [ OZ \Rightarrow True
 343 | (pos n) \Rightarrow False
 344 | (neg n) \Rightarrow False].
 345 apply Hcut. elim (sym_eq ? ? ? H).simplify.exact I.
 346 qed.
 347
 348 definition Zsucc \def
 349 \lambda z. match z with
 350 [ OZ \Rightarrow pos O
 351 | (pos n) \Rightarrow pos (S n)
 352 | (neg n) \Rightarrow
 353           match n with
 354           [ O \Rightarrow OZ
 355           | (S p) \Rightarrow neg p]].
 356
 357 definition Zpred \def
 358 \lambda z. match z with
 359 [ OZ \Rightarrow neg O
 360 | (pos n) \Rightarrow
 361           match n with
 362           [ O \Rightarrow OZ
 363           | (S p) \Rightarrow pos p]
 364 | (neg n) \Rightarrow neg (S n)].
 365
 366 theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
 367 intros.elim z.apply refl_equal.
 368 elim e.apply refl_equal.
 369 apply refl_equal.
 370 apply refl_equal.
 371 qed.
 372
 373 theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
 374 intros.elim z.apply refl_equal.
 375 apply refl_equal.
 376 elim e.apply refl_equal.
 377 apply refl_equal.
 378 qed.
 379
 380 inductive compare :Set \def
 381 | LT : compare
 382 | EQ : compare
 383 | GT : compare.
 384
 385 let rec nat_compare n m: compare \def
 386 match n with
 387 [ O \Rightarrow
 388     match m with
 389       [ O \Rightarrow EQ
 390       | (S q) \Rightarrow LT ]
 391 | (S p) \Rightarrow
 392     match m with
 393       [ O \Rightarrow GT
 394       | (S q) \Rightarrow nat_compare p q]].
 395
 396 definition compare_invert: compare \to compare \def
 397   \lambda c.
 398     match c with
 399       [ LT \Rightarrow GT
 400       | EQ \Rightarrow EQ
 401       | GT \Rightarrow LT ].
 402
 403 theorem nat_compare_invert: \forall n,m:nat.
 404 eq compare (nat_compare n m) (compare_invert (nat_compare m n)).
 405 intros.
 406 apply nat_double_ind (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))).
 407 intros.elim n1.simplify.apply refl_equal.
 408 simplify.apply refl_equal.
 409 intro.elim n1.simplify.apply refl_equal.
 410 simplify.apply refl_equal.
 411 intros.simplify.elim H.apply refl_equal.
 412 qed.
 413
 414 let rec Zplus x y : Z \def
 415   match x with
 416     [ OZ \Rightarrow y
 417     | (pos m) \Rightarrow
 418         match y with
 419          [ OZ \Rightarrow x
 420          | (pos n) \Rightarrow (pos (S (plus m n)))
 421          | (neg n) \Rightarrow
 422               match nat_compare m n with
 423                 [ LT \Rightarrow (neg (pred (minus n m)))
 424                 | EQ \Rightarrow OZ
 425                 | GT \Rightarrow (pos (pred (minus m n)))]]
 426     | (neg m) \Rightarrow
 427         match y with
 428          [ OZ \Rightarrow x
 429          | (pos n) \Rightarrow
 430               match nat_compare m n with
 431                 [ LT \Rightarrow (pos (pred (minus n m)))
 432                 | EQ \Rightarrow OZ
 433                 | GT \Rightarrow (neg (pred (minus m n)))]
 434          | (neg n) \Rightarrow (neg (S (plus m n)))]].
 435
 436 theorem Zplus_z_O:  \forall z:Z. eq Z (Zplus z OZ) z.
 437 intro.elim z.
 438 simplify.apply refl_equal.
 439 simplify.apply refl_equal.
 440 simplify.apply refl_equal.
 441 qed.
 442
 443 theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
 444 intros.elim x.simplify.elim (sym_eq ? ? ? (Zplus_z_O y)).apply refl_equal.
 445 elim y.simplify.reflexivity.
 446 simplify.elim (sym_plus e e1).apply refl_equal.
 447 simplify.elim (sym_eq ? ? ?(nat_compare_invert e e1)).
 448 simplify.elim nat_compare e1 e.simplify.apply refl_equal.
 449 simplify. apply refl_equal.
 450 simplify. apply refl_equal.
 451 elim y.simplify.reflexivity.
 452 simplify.elim (sym_eq ? ? ?(nat_compare_invert e e1)).
 453 simplify.elim nat_compare e1 e.simplify.apply refl_equal.
 454 simplify. apply refl_equal.
 455 simplify. apply refl_equal.
 456 simplify.elim (sym_plus e1 e).apply refl_equal.
 457 qed.
 458
 459 theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
 460 intros.elim z.
 461 simplify.apply refl_equal.
 462 simplify.apply refl_equal.
 463 elim e.simplify.apply refl_equal.
 464 simplify.apply refl_equal.
 465 qed.
 466
 467 theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
 468 intros.elim z.
 469 simplify.apply refl_equal.
 470 elim e.simplify.apply refl_equal.
 471 simplify.apply refl_equal.
 472 simplify.apply refl_equal.
 473 qed.
 474
 475 theorem Zplus_succ_pred_pp :
 476 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
 477 intros.
 478 elim n.elim m.
 479 simplify.apply refl_equal.
 480 simplify.apply refl_equal.
 481 elim m.
 482 simplify.elim (plus_n_O ?).apply refl_equal.
 483 simplify.elim (plus_n_Sm ? ?).apply refl_equal.
 484 qed.
 485
 486 theorem Zplus_succ_pred_pn :
 487 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
 488 intros.apply refl_equal.
 489 qed.
 490
 491 theorem Zplus_succ_pred_np :
 492 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
 493 intros.
 494 elim n.elim m.
 495 simplify.apply refl_equal.
 496 simplify.apply refl_equal.
 497 elim m.
 498 simplify.apply refl_equal.
 499 simplify.apply refl_equal.
 500 qed.
 501
 502 theorem Zplus_succ_pred_nn:
 503 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
 504 intros.
 505 elim n.elim m.
 506 simplify.apply refl_equal.
 507 simplify.apply refl_equal.
 508 elim m.
 509 simplify.elim (plus_n_Sm ? ?).apply refl_equal.
 510 simplify.elim (sym_eq ? ? ? (plus_n_Sm ? ?)).apply refl_equal.
 511 qed.
 512
 513 theorem Zplus_succ_pred:
 514 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
 515 intros.
 516 elim x. elim y.
 517 simplify.apply refl_equal.
 518 simplify.apply refl_equal.
 519 elim (Zsucc_pos ?).elim (sym_eq ? ? ? (Zsucc_pred ?)).apply refl_equal.
 520 elim y.elim sym_Zplus ? ?.elim sym_Zplus (Zpred OZ) ?.
 521 elim (Zpred_neg ?).elim (sym_eq ? ? ? (Zpred_succ ?)).
 522 simplify.apply refl_equal.
 523 apply Zplus_succ_pred_nn.
 524 apply Zplus_succ_pred_np.
 525 elim y.simplify.apply refl_equal.
 526 apply Zplus_succ_pred_pn.
 527 apply Zplus_succ_pred_pp.
 528 qed.
 529
 530 theorem Zsucc_plus_pp :
 531 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 532 intros.apply refl_equal.
 533 qed.
 534
 535 theorem Zsucc_plus_pn :
 536 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 537 intros.
 538 apply nat_double_ind
 539 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 540 intros.elim n1.
 541 simplify. apply refl_equal.
 542 elim e.simplify. apply refl_equal.
 543 simplify. apply refl_equal.
 544 intros. elim n1.
 545 simplify. apply refl_equal.
 546 simplify.apply refl_equal.
 547 intros.
 548 elim (Zplus_succ_pred_pn ? m1).
 549 elim H.apply refl_equal.
 550 qed.
 551
 552 theorem Zsucc_plus_nn :
 553 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 554 intros.
 555 apply nat_double_ind
 556 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 557 intros.elim n1.
 558 simplify. apply refl_equal.
 559 elim e.simplify. apply refl_equal.
 560 simplify. apply refl_equal.
 561 intros. elim n1.
 562 simplify. apply refl_equal.
 563 simplify.apply refl_equal.
 564 intros.
 565 elim (Zplus_succ_pred_nn ? m1).
 566 apply refl_equal.
 567 qed.
 568
 569 theorem Zsucc_plus_np :
 570 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 571 intros.
 572 apply nat_double_ind
 573 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 574 intros.elim n1.
 575 simplify. apply refl_equal.
 576 elim e.simplify. apply refl_equal.
 577 simplify. apply refl_equal.
 578 intros. elim n1.
 579 simplify. apply refl_equal.
 580 simplify.apply refl_equal.
 581 intros.
 582 elim H.
 583 elim (Zplus_succ_pred_np ? (S m1)).
 584 apply refl_equal.
 585 qed.
 586
 587
 588 theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
 589 intros.elim x.elim y.
 590 simplify. apply refl_equal.
 591 elim (Zsucc_pos ?).apply refl_equal.
 592 simplify.apply refl_equal.
 593 elim y.elim sym_Zplus ? ?.elim sym_Zplus OZ ?.simplify.apply refl_equal.
 594 apply Zsucc_plus_nn.
 595 apply Zsucc_plus_np.
 596 elim y.
 597 elim (sym_Zplus OZ ?).apply refl_equal.
 598 apply Zsucc_plus_pn.
 599 apply Zsucc_plus_pp.
 600 qed.
 601
 602 theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 603 intros.
 604 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
 605 elim (sym_eq ? ? ? Hcut).
 606 elim (sym_eq ? ? ? (Zsucc_plus ? ?)).
 607 elim (sym_eq ? ? ? (Zpred_succ ?)).
 608 apply refl_equal.
 609 elim (sym_eq ? ? ? (Zsucc_pred ?)).
 610 apply refl_equal.
 611 qed.
 612
 613 theorem assoc_Zplus :
 614 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
 615 intros.elim x.simplify.apply refl_equal.
 616 elim e.elim (Zpred_neg (Zplus y z)).
 617 elim (Zpred_neg y).
 618 elim (Zpred_plus ? ?).
 619 apply refl_equal.
 620 elim (sym_eq ? ? ? (Zpred_plus (neg e1) ?)).
 621 elim (sym_eq ? ? ? (Zpred_plus (neg e1) ?)).
 622 elim (sym_eq ? ? ? (Zpred_plus (Zplus (neg e1) y) ?)).
 623 apply f_equal.assumption.
 624 elim e.elim (Zsucc_pos ?).
 625 elim (Zsucc_pos ?).
 626 apply (sym_eq ? ? ? (Zsucc_plus ? ?)) .
 627 elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)).
 628 elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)).
 629 elim (sym_eq ? ? ? (Zsucc_plus (Zplus (pos e1) y) ?)).
 630 apply f_equal.assumption.
 631 qed.
 632
 633
 634