]> matita.cs.unibo.it Git - helm.git/blob - matita/tests/naiveparamod.ma
restored the good factorization file
[helm.git] / 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.