From d73bd6d966d4aeb509a3cf776708d55560464ec2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 15:11:08 +0000 Subject: [PATCH] New tactic: unfold. --- helm/matita/tests/unfold.ma | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 helm/matita/tests/unfold.ma diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma new file mode 100644 index 000000000..ff68d5fd1 --- /dev/null +++ b/helm/matita/tests/unfold.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold". + +alias symbol "plus" (instance 0) = "Coq's natural plus". +definition myplus \def \lambda x,y. x+y. + +lemma lem: \forall n. S (n + n) = (S n) + n. + intro; reflexivity. +qed. + +theorem trivial: \forall n. S (myplus n n) = (S n) + n. + unfold myplus. + intro. + rewrite > lem. + reflexivity. +qed. \ No newline at end of file -- 2.39.2