From 81b43e348e0c3e61114900d1e1df058ecc68cd90 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 20 Apr 2007 15:39:16 +0000 Subject: [PATCH] A new test on some non punctuation tacticals. --- helm/software/matita/tests/tacticals.ma | 50 +++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 helm/software/matita/tests/tacticals.ma diff --git a/helm/software/matita/tests/tacticals.ma b/helm/software/matita/tests/tacticals.ma new file mode 100644 index 000000000..a44e80a86 --- /dev/null +++ b/helm/software/matita/tests/tacticals.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tacticals". + +inductive myand (A, B: Prop) : Prop \def + | myconj : ∀a:A.∀b:B. myand A B. + +lemma prova: + ∀A,B,C,D:Prop.∀a:A.∀b:B.∀c:C.∀d:D.myand (myand A B) (myand C D). + intros; try (apply myconj); try assumption; try (apply myconj); + try assumption. +qed. + +lemma prova2: + ∀A,B,C,D:Prop.∀a:A.∀b:B.∀c:C.∀d:D.myand (myand A B) (myand C D). + intros; progress (apply myconj; apply myconj); + solve [assumption]. +qed. + +lemma prova3: + ∀A,B,C,D:Prop.∀a:A.∀b:B.∀c:C.∀d:D.myand (myand A B) (myand C D). + intros; repeat first [ assumption | apply myconj]. +qed. + +lemma prova4: + ∀A,B,C,D:Prop.∀a:A.∀b:B.∀c:C.∀d:D.myand (myand A B) (myand C D). + intros; + repeat apply myconj; + assumption. +qed. + +lemma prova6: + ∀A,B,C,D:Prop.∀a:A.∀b:B.∀c:C.∀d:D.myand (myand A B) (myand C D). + intros; apply myconj; + [1:repeat (constructor 1; try assumption) + |2:repeat (constructor 1; try assumption) + ] +qed. \ No newline at end of file -- 2.39.2