helm/software/matita/tests/paramodulation/boolean_algebra.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "coq.ma".
  18
  19 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  20 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
  21 alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
  22 alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
  23 alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
  24
  25 definition bool_algebra \def
  26   \lambda A:Set.
  27   \lambda one:A.
  28   \lambda zero:A.
  29   \lambda add: A \to A \to A.
  30   \lambda mult: A \to A \to A.
  31   \lambda inv: A \to A.
  32   (\forall x:A. (add x (inv x)) = one)\land
  33   (\forall x:A. (mult x (inv x)) = zero)\land
  34   (\forall x:A. (mult x one) = x)\land
  35   (\forall x:A. (add x zero) = x)\land
  36   (\forall x,y,z:A.(mult x (add y z)) = (add (mult x y) (mult x z)))\land
  37   (\forall x,y,z:A.(add x (mult y z)) = (mult (add x y) (add x z)))\land
  38   (\forall x,y:A.(mult x y) = (mult y x))\land
  39   (\forall x,y:A.(add x y) = (add y x)).
  40
  41 (*
  42 theorem SKK:
  43   \forall A:Set.
  44   \forall app: A \to A \to A.
  45   \forall K:A.
  46   \forall S:A.
  47   \forall H1: (\forall x,y:A.(app (app K x) y) = x).
  48   \forall H2: (\forall x,y,z:A.
  49     (app (app (app S x) y) z) = (app (app x z) (app y z))).
  50   \forall x:A.
  51     (app (app (app S K) K) x) = x.
  52 intros.auto paramodulation.
  53 qed.
  54 *)
  55 (*
  56 theorem bool1:
  57   \forall A: Set.
  58   \forall one,zero: A.
  59   \forall add,mult: A \to A \to A.
  60   \forall inv: A \to A.
  61   \forall H: bool_algebra A one zero add mult inv.
  62   (inv zero) = one.
  63 intros.
  64 unfold bool_algebra in H.
  65 decompose
  66 auto paramodulation.
  67 qed.
  68 *)
  69 (*
  70 theorem bool2:
  71   \forall A: Set.
  72   \forall one,zero: A.
  73   \forall add,mult: A \to A \to A.
  74   \forall inv: A \to A.
  75   \forall H: bool_algebra A one zero add mult inv.
  76   \forall x:A. (mult x zero) = zero.
  77 intros.
  78 unfold bool_algebra in H.
  79 decompose
  80 auto paramodulation.
  81 qed.
  82 *)
  83 (*
  84 theorem bool3:
  85   \forall A: Set.
  86   \forall one,zero: A.
  87   \forall add,mult: A \to A \to A.
  88   \forall inv: A \to A.
  89   \forall H: bool_algebra A one zero add mult inv.
  90   \forall x:A. (inv (inv x)) = x.
  91 intros.
  92 unfold bool_algebra in H.
  93 decompose
  94 auto paramodulation.
  95 qed.
  96 *)
  97 (*
  98 theorem bool266:
  99   \forall A: Set.
 100   \forall one,zero: A.
 101   \forall add,mult: A \to A \to A.
 102   \forall inv: A \to A.
 103   \forall H: bool_algebra A one zero add mult inv.
 104   \forall x,y:A. (mult x (add (inv x) y)) = (mult x y).
 105 intros.
 106 unfold bool_algebra in H.
 107 decompose
 108 auto paramodulation.
 109 qed.
 110 *)
 111 (*
 112 theorem bool507:
 113   \forall A: Set.
 114   \forall one,zero: A.
 115   \forall add,mult: A \to A \to A.
 116   \forall inv: A \to A.
 117   \forall H: bool_algebra A one zero add mult inv.
 118   \forall x,y:A. zero = (mult x (mult (inv x) y)).
 119 intros.
 120 unfold bool_algebra in H.
 121 decompose
 122 auto paramodulation.
 123 qed.
 124 *)
 125 (*
 126 theorem bool515:
 127   \forall A: Set.
 128   \forall one,zero: A.
 129   \forall add,mult: A \to A \to A.
 130   \forall inv: A \to A.
 131   \forall H: bool_algebra A one zero add mult inv.
 132   \forall x,y:A. zero = mult (inv x) (mult x y).
 133 intros.
 134 unfold bool_algebra in H.
 135 decompose
 136 auto paramodulation.
 137 qed.
 138 *)
 139 (*
 140 theorem bool304:
 141   \forall A: Set.
 142   \forall one,zero: A.
 143   \forall add,mult: A \to A \to A.
 144   \forall inv: A \to A.
 145   \forall H: bool_algebra A one zero add mult inv.
 146   \forall x,y:A. x = (mult (add y x) x).
 147 intros.
 148 unfold bool_algebra in H.
 149 decompose
 150 auto paramodulation.
 151 qed.
 152 *)
 153 (*
 154 theorem bool531:
 155   \forall A: Set.
 156   \forall one,zero: A.
 157   \forall add,mult: A \to A \to A.
 158   \forall inv: A \to A.
 159   \forall H: bool_algebra A one zero add mult inv.
 160   \forall x,y:A. zero = (mult (inv (add x y)) y).
 161 intros.
 162 unfold bool_algebra in H.
 163 decompose
 164 auto paramodulation.
 165 qed.
 166 *)
 167 (*
 168 theorem bool253:
 169   \forall A: Set.
 170   \forall one,zero: A.
 171   \forall add,mult: A \to A \to A.
 172   \forall inv: A \to A.
 173   \forall H: bool_algebra A one zero add mult inv.
 174   \forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y).
 175 intros.
 176 unfold bool_algebra in H.
 177 decompose
 178 auto paramodulation.
 179 qed.
 180 *)
 181 (*
 182 theorem bool557:
 183   \forall A: Set.
 184   \forall one,zero: A.
 185   \forall add,mult: A \to A \to A.
 186   \forall inv: A \to A.
 187   \forall H: bool_algebra A one zero add mult inv.
 188   \forall x,y:A.
 189     inv x =  (add (inv x) (inv (add y x))).
 190 intros.
 191 unfold bool_algebra in H.
 192 decompose
 193 auto paramodulation.
 194 qed.
 195 *)
 196 (*
 197 theorem bool609:
 198   \forall A: Set.
 199   \forall one,zero: A.
 200   \forall add,mult: A \to A \to A.
 201   \forall inv: A \to A.
 202   \forall H: bool_algebra A one zero add mult inv.
 203   \forall x,y:A.
 204     inv x =  (add (inv (add y x)) (inv x)).
 205 intros.
 206 unfold bool_algebra in H.
 207 decompose
 208 auto paramodulation.
 209 qed.
 210 *)
 211 (*
 212 theorem bool260:
 213   \forall A: Set.
 214   \forall one,zero: A.
 215   \forall add,mult: A \to A \to A.
 216   \forall inv: A \to A.
 217   \forall H: bool_algebra A one zero add mult inv.
 218   \forall x,y,z:A.
 219     add x (mult x y) = mult x (add x y).
 220 intros.
 221 unfold bool_algebra in H.
 222 decompose
 223 auto paramodulation.
 224 qed.
 225 *)
 226 (*
 227 theorem bool276:
 228   \forall A: Set.
 229   \forall one,zero: A.
 230   \forall add,mult: A \to A \to A.
 231   \forall inv: A \to A.
 232   \forall H: bool_algebra A one zero add mult inv.
 233   \forall x,y,z,u:A.
 234     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u))).
 235 intros.
 236 unfold bool_algebra in H.
 237 decompose
 238 auto paramodulation.
 239 qed.
 240 *)
 241 (*
 242 theorem bool250:
 243   \forall A: Set.
 244   \forall one,zero: A.
 245   \forall add,mult: A \to A \to A.
 246   \forall inv: A \to A.
 247   \forall H: bool_algebra A one zero add mult inv.
 248   \forall x,y,z:A.
 249     add x (mult y z) = mult (add y x) (add x z).
 250 intros.
 251 unfold bool_algebra in H.
 252 decompose
 253 auto paramodulation.
 254 qed.
 255 *)
 256 (*
 257 theorem bool756minimal:
 258   \forall A:Set.
 259   \forall add: A \to A \to A.
 260   \forall mult: A \to A \to A.
 261   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 262   \forall hint1: (\forall x,y,z,u:A.
 263     add y (add x (mult x u)) = (add (mult (add x y) z) (add x (mult y u)))).
 264   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
 265   \forall x,y,z:A.
 266     add x (add y (mult y z)) = add x (add y (mult x z)).
 267 intros.
 268 auto paramodulation.
 269 qed.
 270 *)
 271 (*
 272 theorem bool756simplified:
 273   \forall A:Set.
 274   \forall add: A \to A \to A.
 275   \forall mult: A \to A \to A.
 276   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 277   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 278   \forall hint1: (\forall x,y,z,u:A.
 279     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
 280   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
 281   \forall hint3: (\forall x,y,z:A.
 282     add x (mult y z) = mult (add y x) (add x z)).
 283   \forall hint4: (\forall x,y:A.
 284     add x (mult x y) = mult x (add x y)).
 285   \forall x,y,z:A.
 286     add x (add y (mult y z)) = add x (add y (mult x z)).
 287 intros.
 288 auto paramodulation.
 289 qed.
 290 *)
 291 (*
 292 theorem bool756:
 293   \forall A:Set.
 294   \forall one:A.
 295   \forall zero:A.
 296   \forall add: A \to A \to A.
 297   \forall mult: A \to A \to A.
 298   \forall inv: A \to A.
 299   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 300   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 301   \forall d1: (\forall x,y,z:A.
 302               (add x (mult y z)) = (mult (add x y) (add x z))).
 303   \forall d2: (\forall x,y,z:A.
 304               (mult x (add y z)) = (add (mult x y) (mult x z))).
 305   \forall i1: (\forall x:A. (add x zero) = x).
 306   \forall i2: (\forall x:A. (mult x one) = x).
 307   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 308   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 309   \forall hint1: (\forall x,y,z,u:A.
 310     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
 311   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
 312   \forall hint3: (\forall x,y,z:A.
 313     add x (mult y z) = mult (add y x) (add x z)).
 314   \forall hint4: (\forall x,y:A.
 315     add x (mult x y) = mult x (add x y)).
 316   \forall x,y,z:A.
 317     add x y = add x (add y (mult x z)).
 318 intros;
 319 cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
 320 [auto paramodulation
 321 |auto paramodulation]
 322 qed.
 323 *)
 324 (*
 325 theorem bool756full:
 326   \forall A: Set.
 327   \forall one,zero: A.
 328   \forall add,mult: A \to A \to A.
 329   \forall inv: A \to A.
 330   \forall H: bool_algebra A one zero add mult inv.
 331   \forall x,y,z:A.
 332     add x y = add x (add y (mult x z)).
 333 intros.
 334 unfold bool_algebra in H.
 335 decompose
 336 auto paramodulation.
 337 qed.
 338 *)
 339 (*
 340 theorem bool1164:
 341   \forall A: Set.
 342   \forall one,zero: A.
 343   \forall add,mult: A \to A \to A.
 344   \forall inv: A \to A.
 345   \forall H: bool_algebra A one zero add mult inv.
 346   \forall x,y,z:A.
 347     (add x y) = (add (add x (mult y z)) y).
 348 intros.
 349 unfold bool_algebra in H.
 350 decompose
 351 auto paramodulation.
 352 qed.
 353 *)
 354 (*
 355 theorem bool1230:
 356   \forall A: Set.
 357   \forall one,zero: A.
 358   \forall add,mult: A \to A \to A.
 359   \forall inv: A \to A.
 360   \forall H: bool_algebra A one zero add mult inv.
 361   \forall A:Set.
 362   \forall one:A.
 363   \forall zero:A.
 364   \forall add: A \to A \to A.
 365   \forall mult: A \to A \to A.
 366   \forall inv: A \to A.
 367   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 368   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 369   \forall d1: (\forall x,y,z:A.
 370               (add x (mult y z)) = (mult (add x y) (add x z))).
 371   \forall d2: (\forall x,y,z:A.
 372               (mult x (add y z)) = (add (mult x y) (mult x z))).
 373   \forall i1: (\forall x:A. (add x zero) = x).
 374   \forall i2: (\forall x:A. (mult x one) = x).
 375   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 376   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 377   \forall x,y,z:A.
 378   \forall c1z: (\forall x:A.(add x z) = (add z x)).
 379     add (add x y) z = add (add x y) (add z y).
 380 intros.
 381 auto paramodulation.
 382 qed.
 383 *)
 384 (*
 385 theorem bool1230:
 386   \forall A: Set.
 387   \forall one,zero: A.
 388   \forall add,mult: A \to A \to A.
 389   \forall inv: A \to A.
 390   \forall H: bool_algebra A one zero add mult inv.
 391   \forall x,y,z:A.
 392     add (add x y) z = add (add x y) (add z y).
 393 intros.
 394 unfold bool_algebra in H.
 395 decompose
 396 auto paramodulation.
 397 qed.
 398 *)
 399 (*
 400 theorem bool1372:
 401   \forall A: Set.
 402   \forall one,zero: A.
 403   \forall add,mult: A \to A \to A.
 404   \forall inv: A \to A.
 405   \forall H: bool_algebra A one zero add mult inv.
 406   \forall x,y,z:A.
 407     add x (add y z) = add (add x z) y.
 408 intros.
 409 unfold bool_algebra in H.
 410 decompose
 411 auto paramodulation.
 412 qed.
 413 *)
 414 (*
 415 theorem bool381:
 416   \forall A: Set.
 417   \forall one,zero: A.
 418   \forall add,mult: A \to A \to A.
 419   \forall inv: A \to A.
 420   \forall H: bool_algebra A one zero add mult inv.
 421   \forall x,y:A.
 422       add (inv x) y = add (mult x y) (inv x).
 423 intros.
 424 unfold bool_algebra in H.
 425 decompose
 426 auto paramodulation.
 427 qed.
 428 *)
 429 (*
 430 theorem bool5hint1:
 431   \forall A:Set.
 432   \forall one:A.
 433   \forall zero:A.
 434   \forall add: A \to A \to A.
 435   \forall mult: A \to A \to A.
 436   \forall inv: A \to A.
 437   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 438   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 439   \forall d1: (\forall x,y,z:A.
 440               (add x (mult y z)) = (mult (add x y) (add x z))).
 441   \forall d2: (\forall x,y,z:A.
 442               (mult x (add y z)) = (add (mult x y) (mult x z))).
 443   \forall i1: (\forall x:A. (add x zero) = x).
 444   \forall i2: (\forall x:A. (mult x one) = x).
 445   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 446   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 447   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
 448   \forall hint1735:(\forall x,y:A. add (inv (add x y)) x = add x (inv y)).
 449   \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
 450   \forall x,y:A.
 451     (inv (mult x y)) = (add (inv x) (inv y)).
 452 intros.
 453 auto paramodulation.
 454 qed.
 455 *)
 456 (*
 457 theorem bool5hint2:
 458   \forall A:Set.
 459   \forall one:A.
 460   \forall zero:A.
 461   \forall add: A \to A \to A.
 462   \forall mult: A \to A \to A.
 463   \forall inv: A \to A.
 464   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 465   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 466   \forall d1: (\forall x,y,z:A.
 467               (add x (mult y z)) = (mult (add x y) (add x z))).
 468   \forall d2: (\forall x,y,z:A.
 469               (mult x (add y z)) = (add (mult x y) (mult x z))).
 470   \forall i1: (\forall x:A. (add x zero) = x).
 471   \forall i2: (\forall x:A. (mult x one) = x).
 472   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 473   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 474   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
 475   \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
 476   \forall x,y:A.
 477     (inv (mult x y)) = (add (inv x) (inv y)).
 478 intros.
 479 auto paramodulation.
 480 qed.
 481 *)
 482 (*
 483 theorem bool5hint3:
 484   \forall A:Set.
 485   \forall one:A.
 486   \forall zero:A.
 487   \forall add: A \to A \to A.
 488   \forall mult: A \to A \to A.
 489   \forall inv: A \to A.
 490   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 491   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 492   \forall d1: (\forall x,y,z:A.
 493               (add x (mult y z)) = (mult (add x y) (add x z))).
 494   \forall d2: (\forall x,y,z:A.
 495               (mult x (add y z)) = (add (mult x y) (mult x z))).
 496   \forall i1: (\forall x:A. (add x zero) = x).
 497   \forall i2: (\forall x:A. (mult x one) = x).
 498   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 499   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 500   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
 501   \forall hint609:(\forall x,y:A. inv x = add (inv (add y x)) (inv x)).
 502   \forall x,y:A.
 503     (inv (mult x y)) = (add (inv x) (inv y)).
 504 intros.
 505 auto paramodulation.
 506 qed.
 507 *)
 508 theorem bool5:
 509   \forall A: Set.
 510   \forall one,zero: A.
 511   \forall add,mult: A \to A \to A.
 512   \forall inv: A \to A.
 513   \forall H: bool_algebra A one zero add mult inv.
 514   \forall x,y:A.
 515     (inv (mult x y)) = (add (inv x) (inv y)).
 516 intros.
 517 unfold bool_algebra in H.
 518 decompose.
 519 autobatch paramodulation timeout=120.
 520 qed.