matita/tests/naiveparamod.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/test/".
  16
  17 include "logic/equality.ma".
  18
  19 inductive TT : Prop \def II:TT.
  20
  21 theorem prova1:
  22   \forall A,B,C:Prop.
  23   \forall S:Set.
  24   \forall a:B -> A.
  25   \forall w:B \to Prop.
  26   \forall h:(A -> \forall x:B. w x -> TT -> C).
  27   \forall b:B.
  28   \forall s:S.
  29   \forall wb:w b. (* ASK ANDREA: what if b1 *)
  30   C.
  31   intros (A B C S a w h b wb).
  32   (* exact (h s (a b) b wb II). *)
  33   auto width = 5 depth = 3. (* look at h parameters! *)
  34   qed.
  35
  36 (* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *)
  37 theorem prova2:
  38   \forall A,B,C:Prop. (* SE METTO SET NON VA *)
  39   \forall a:B -> A.
  40   \forall h:A -> B -> A = B.
  41   (* \forall h:A -> C -> A = B. *)
  42   \forall b:B.
  43   A=B.
  44   intros.
  45   auto paramodulation.
  46   try assumption.
  47   qed.