From 90f9b69fa2c7742722f5a5e72361638a39951aaf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jul 2005 15:46:38 +0000 Subject: [PATCH] some more tests --- helm/matita/tests/clear.ma | 31 ++++++++++++++++++++++++++++++ helm/matita/tests/contradiction.ma | 30 +++++++++++++++++++++++++++++ helm/matita/tests/cut.ma | 24 +++++++++++++++++++++++ helm/matita/tests/decompose.ma | 27 ++++++++++++++++++++++++++ helm/matita/tests/discriminate.ma | 26 +++++++++++++++++++++++++ 5 files changed, 138 insertions(+) create mode 100644 helm/matita/tests/clear.ma create mode 100644 helm/matita/tests/contradiction.ma create mode 100644 helm/matita/tests/cut.ma create mode 100644 helm/matita/tests/decompose.ma create mode 100644 helm/matita/tests/discriminate.ma diff --git a/helm/matita/tests/clear.ma b/helm/matita/tests/clear.ma new file mode 100644 index 000000000..1fe721d59 --- /dev/null +++ b/helm/matita/tests/clear.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tests/clear". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". + + + +theorem stupid: + \forall a: True. + \forall b: 0 = 0. + 0 = 0. +intros 1 [H] . +clear H. +intros 1 [H]. +exact H. +qed. + diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma new file mode 100644 index 000000000..ddd9ac878 --- /dev/null +++ b/helm/matita/tests/contradiction.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tests/contradiction". +alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". +alias id "not" = "cic:/Coq/Init/Logic/not.con". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". + + + +theorem stupid: \forall a:Prop. a \to not a \to 0 = 1. +intros. +letin H \def (H1 H). +contradiction. +qed. + + + diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma new file mode 100644 index 000000000..8ba63bd8b --- /dev/null +++ b/helm/matita/tests/cut.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tests/cut". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". + +theorem stupid: 0 = 0. + cut 0 = 0. + assumption. + reflexivity. + qed. + \ No newline at end of file diff --git a/helm/matita/tests/decompose.ma b/helm/matita/tests/decompose.ma new file mode 100644 index 000000000..48477f3eb --- /dev/null +++ b/helm/matita/tests/decompose.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tests/decompose". +alias symbol "and" (instance 0) = "logical and". +alias symbol "or" (instance 0) = "logical or". + + + +theorem stupid: + \forall a,b,c:Prop. + (a \land c \lor b \land c) \to (c \land (b \lor a)). + intros.decompose H.split.assumption.right.assumption. + split.assumption.left.assumption.qed. + + diff --git a/helm/matita/tests/discriminate.ma b/helm/matita/tests/discriminate.ma new file mode 100644 index 000000000..ca55591ee --- /dev/null +++ b/helm/matita/tests/discriminate.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tests/discriminate". +alias id "not" = "cic:/Coq/Init/Logic/not.con". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". + + +theorem stupid: + 1 = 0 \to (\forall p:Prop. p \to not p). + intros. + discriminate H. + qed. + -- 2.39.2