helm/matita/tests/SK.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 set "baseuri" "cic:/matita/SK/".
  16
  17 include "legacy/coq.ma".
  18 alias symbol "eq" = "Coq's leibnitz's equality".
  19
  20 theorem SKK:
  21   \forall A:Set.
  22   \forall app: A \to A \to A.
  23   \forall K:A.
  24   \forall S:A.
  25   \forall H1: (\forall x,y:A.(app (app K x) y) = x).
  26   \forall H2: (\forall x,y,z:A.
  27     (app (app (app S x) y) z) = (app (app x z) (app y z))).
  28   \forall x:A.
  29     (app (app (app S K) K) x) = x.
  30 intros.auto paramodulation.
  31 qed.
  32
  33 theorem bool1:
  34   \forall A:Set.
  35   \forall one:A.
  36   \forall zero:A.
  37   \forall add: A \to A \to A.
  38   \forall mult: A \to A \to A.
  39   \forall inv: A \to A.
  40   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  41   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  42   \forall d1: (\forall x,y,z:A.
  43               (add x (mult y z)) = (mult (add x y) (add x z))).
  44   \forall d2: (\forall x,y,z:A.
  45               (mult x (add y z)) = (add (mult x y) (mult x z))).
  46   \forall i1: (\forall x:A. (add x zero) = x).
  47   \forall i2: (\forall x:A. (mult x one) = x).
  48   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  49   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  50   (inv zero) = one.
  51 intros.auto paramodulation.
  52 qed.
  53
  54 theorem bool2:
  55   \forall A:Set.
  56   \forall one:A.
  57   \forall zero:A.
  58   \forall add: A \to A \to A.
  59   \forall mult: A \to A \to A.
  60   \forall inv: A \to A.
  61   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  62   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  63   \forall d1: (\forall x,y,z:A.
  64               (add x (mult y z)) = (mult (add x y) (add x z))).
  65   \forall d2: (\forall x,y,z:A.
  66               (mult x (add y z)) = (add (mult x y) (mult x z))).
  67   \forall i1: (\forall x:A. (add x zero) = x).
  68   \forall i2: (\forall x:A. (mult x one) = x).
  69   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  70   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  71   \forall x:A. (mult x zero) = zero.
  72 intros.auto paramodulation.
  73 qed.
  74
  75 theorem bool3:
  76   \forall A:Set.
  77   \forall one:A.
  78   \forall zero:A.
  79   \forall add: A \to A \to A.
  80   \forall mult: A \to A \to A.
  81   \forall inv: A \to A.
  82   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  83   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  84   \forall d1: (\forall x,y,z:A.
  85               (add x (mult y z)) = (mult (add x y) (add x z))).
  86   \forall d2: (\forall x,y,z:A.
  87               (mult x (add y z)) = (add (mult x y) (mult x z))).
  88   \forall i1: (\forall x:A. (add x zero) = x).
  89   \forall i2: (\forall x:A. (mult x one) = x).
  90   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  91   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  92   \forall x:A. (inv (inv x)) = x.
  93 intros.auto paramodulation.
  94 qed.
  95
  96 theorem bool2:
  97   \forall A:Set.
  98   \forall one:A.
  99   \forall zero:A.
 100   \forall add: A \to A \to A.
 101   \forall mult: A \to A \to A.
 102   \forall inv: A \to A.
 103   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 104   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 105   \forall d1: (\forall x,y,z:A.
 106               (add x (mult y z)) = (mult (add x y) (add x z))).
 107   \forall d2: (\forall x,y,z:A.
 108               (mult x (add y z)) = (add (mult x y) (mult x z))).
 109   \forall i1: (\forall x:A. (add x zero) = x).
 110   \forall i2: (\forall x:A. (mult x one) = x).
 111   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 112   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 113   \forall x,y:A.
 114     (inv (mult x y)) = (add (inv x) (inv y)).
 115 intros.auto paramodulation.
 116 qed.