From a97fe0b74f4442f934b60fc34ff843789c299481 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 9 Jul 2005 07:56:59 +0000 Subject: [PATCH] New test suite for generalize. The last test fails because of a weakness of apply. --- helm/matita/tests/generalize.ma | 36 +++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 helm/matita/tests/generalize.ma diff --git a/helm/matita/tests/generalize.ma b/helm/matita/tests/generalize.ma new file mode 100644 index 000000000..a6e56ef3e --- /dev/null +++ b/helm/matita/tests/generalize.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/generalize". + +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "plus" (instance 0) = "natural plus". +alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con". +alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". + +(* This tests is for the case of a pattern that contains metavariables *) +theorem t: \forall x. x + 4 = 4 + x. + intro. + generalize in match (S ?). + intro; apply plus_comm. +qed. + +(* This test used to fail because x was used in the wrong context *) +(* Once this was fixed it still did not work since apply is not *) +(* able to solve a goal that ends in a product. *) +theorem test2: \forall x. x + 4 = 4 + x. + generalize in match 4. + exact plus_comm. +qed. \ No newline at end of file -- 2.39.2