From bc23e49033b5f369ddc0d56e1c740c6f00de7ed7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Sep 2006 15:58:44 +0000 Subject: [PATCH] ... --- matita/tests/naiveparamod.ma | 47 ++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 matita/tests/naiveparamod.ma diff --git a/matita/tests/naiveparamod.ma b/matita/tests/naiveparamod.ma new file mode 100644 index 000000000..37011c733 --- /dev/null +++ b/matita/tests/naiveparamod.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/". + +include "logic/equality.ma". + +inductive TT : Prop \def II:TT. + +theorem prova1: + \forall A,B,C:Prop. + \forall S:Set. + \forall a:B -> A. + \forall w:B \to Prop. + \forall h:(A -> \forall x:B. w x -> TT -> C). + \forall b:B. + \forall s:S. + \forall wb:w b. (* ASK ANDREA: what if b1 *) + C. + intros (A B C S a w h b wb). + (* exact (h s (a b) b wb II). *) + auto width = 5 depth = 3. (* look at h parameters! *) + qed. + +(* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *) +theorem prova2: + \forall A,B,C:Prop. (* SE METTO SET NON VA *) + \forall a:B -> A. + \forall h:A -> B -> A = B. + (* \forall h:A -> C -> A = B. *) + \forall b:B. + A=B. + intros. + auto paramodulation. + try assumption. + qed. -- 2.39.2