helm/software/matita/tests/paramodulation/irratsqrt2.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 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/times.ma".
  18 include "nat/minus.ma".
  19
  20 theorem prova :
  21   \forall n,m:nat.
  22   \forall P:nat \to Prop.
  23   \forall H:P (S (S O)).
  24   \forall H:P (S (S (S O))).
  25   \forall H1: \forall x.P x \to O = x.
  26    O = S (S (S (S (S O)))).
  27    intros.
  28    autobatch.
  29  qed.
  30
  31 theorem example2:
  32 \forall x: nat. (x+S O)*(x-S O) = x*x - S O.
  33 intro;
  34 apply (nat_case x);
  35  [ autobatch timeout = 1.|intro.autobatch timeout = 1.]
  36 qed.
  37
  38 theorem irratsqrt2_byhand:
  39   \forall A:Set.
  40   \forall m:A \to A \to A.
  41   \forall divides: A \to A \to Prop.
  42   \forall o,a,b,two:A.
  43   \forall H1:\forall x.m o x = x.
  44   \forall H1:\forall x.m x o = x.
  45   \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z.
  46   \forall H1:\forall x.m x o = x.
  47   \forall H2:\forall x,y.m x y = m y x.
  48   \forall H3:\forall x,y,z. m x y = m x z \to y = z.
  49   (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *)
  50   \forall H4:\forall x,y.(divides x y \to (\exists z.m x z = y)).
  51   \forall H4:\forall x,y,z.m x z = y \to divides x y.
  52   \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y.
  53   \forall H5:m a a = m two (m b b).
  54   \forall H6:\forall x.divides x a \to divides x b \to x = o.
  55   two = o.
  56   intros.
  57   cut (divides two a);
  58     [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.autobatch.]
  59     |elim (H6 ? ? Hcut).
  60      cut (divides two b);
  61        [ apply (H10 ? Hcut Hcut1).
  62        | elim (H8 b b);[assumption.|assumption|
  63          apply (H7 ? ? (m a1 a1));
  64          apply (H5 two ? ?);rewrite < H9.
  65          rewrite < H11.rewrite < H2.
  66          apply eq_f.rewrite > H2.rewrite > H4.reflexivity.
  67          ]
  68          ]
  69          ]
  70 qed.
  71
  72 theorem irratsqrt2_byhand':
  73   \forall A:Set.
  74   \forall m,f:A \to A \to A.
  75   \forall divides: A \to A \to Prop.
  76   \forall o,a,b,two:A.
  77   \forall H1:\forall x.m o x = x.
  78   \forall H1:\forall x.m x o = x.
  79   \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z.
  80   \forall H1:\forall x.m x o = x.
  81   \forall H2:\forall x,y.m x y = m y x.
  82   \forall H3:\forall x,y,z. m x y = m x z \to y = z.
  83   (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *)
  84   \forall H4:\forall x,y.(divides x y \to m x (f x y) = y).
  85   \forall H4:\forall x,y,z.m x z = y \to divides x y.
  86   \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y.
  87   \forall H5:m a a = m two (m b b).
  88   \forall H6:\forall x.divides x a \to divides x b \to x = o.
  89   two = o.
  90   intros.
  91   cut (divides two a);
  92     [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.autobatch.]
  93     |(*elim (H6 ? ? Hcut). *)
  94      cut (divides two b);
  95        [ apply (H10 ? Hcut Hcut1).
  96        | elim (H8 b b);[assumption.|assumption|
  97
  98          apply (H7 ? ? (m (f two a) (f two a)));
  99          apply (H5 two ? ?);
 100          rewrite < H9.
 101          rewrite < (H6 two a Hcut) in \vdash (? ? ? %).
 102          rewrite < H2.apply eq_f.
 103          rewrite < H4 in \vdash (? ? ? %).
 104          rewrite > H2.reflexivity.
 105          ]
 106          ]
 107          ]
 108 qed.
 109
 110 theorem irratsqrt2:
 111   \forall A:Set.
 112   \forall m,f:A \to A \to A.
 113   \forall divides: A \to A \to Prop.
 114   \forall o,a,b,two:A.
 115   \forall H1:\forall x.m o x = x.
 116   \forall H1:\forall x.m x o = x.
 117   \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z.
 118   \forall H1:\forall x.m x o = x.
 119   \forall H2:\forall x,y.m x y = m y x.
 120   \forall H3:\forall x,y,z. m x y = m x z \to y = z.
 121   (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *)
 122   \forall H4:\forall x,y.(divides x y \to m x (f x y) = y).
 123   \forall H4:\forall x,y,z.m x z = y \to divides x y.
 124   \forall H4:\forall x.divides two (m x x) \to divides two x.
 125   \forall H5:m a a = m two (m b b).
 126   \forall H6:\forall x.divides x a \to divides x b \to x = o.
 127   two = o.
 128 intros.
 129 autobatch depth = 5 timeout = 180.
 130 qed.
 131
 132 (* time: 146s *)
 133
 134
 135 (* intermediate attempts
 136
 137   cut (divides two a);[|
 138     (* apply H8;apply (H7 two (m a a) (m b b));symmetry;assumption. *)
 139     autobatch depth = 4 width = 3 use_paramod = false. ]
 140   (*autobatch depth = 5.*)
 141
 142   apply H10;
 143   [ assumption.
 144   |(*autobatch depth = 4.*) apply H8;
 145          (*autobatch.*)
 146          apply (H7 ? ? (m (f two a) (f two a)));
 147          apply (H5 two ? ?);
 148          cut ((\lambda x:A.m x (m two ?)=m x (m b b))?);
 149          [|||simplify;
 150          autobatch paramodulation.
 151          (*autobatch new.*)
 152          rewrite < H9.
 153          rewrite < (H6 two a Hcut) in \vdash (? ? ? %).
 154          rewrite < H2.apply eq_f.
 155          rewrite < H4 in \vdash (? ? ? %).
 156          rewrite > H2.reflexivity.
 157   ]
 158
 159 qed.
 160 *)