From 87a3d3854f447e67e7671b9035eb768a906aff2a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Apr 2006 12:08:32 +0000 Subject: [PATCH] added another interesting problem for paramodulation --- matita/tests/group.ma | 51 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 matita/tests/group.ma diff --git a/matita/tests/group.ma b/matita/tests/group.ma new file mode 100644 index 000000000..a9a55b9cf --- /dev/null +++ b/matita/tests/group.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "legacy/coq.ma". + +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". +alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con". +alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con". +alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con". + + +theorem self: + \forall A:Set. + \forall f,g:A \to A. + \forall H:(\forall x,y:A. x = y). + \forall H:(\forall x,y,z:A. f x = y). + \forall x,y:A. x=y. +intros.auto paramodulation. +qed. + +theorem GRP049_simple: + \forall A:Set. + \forall inv: A \to A. + \forall mult: A \to A \to A. + \forall H: (\forall x,y,z:A.mult z (inv (mult (inv (mult (inv (mult z y)) x)) (inv (mult y (mult (inv y) y))))) = x). + \forall a,b:A. mult (inv a) a = mult (inv b) b. +intros.auto paramodulation; exact a. +qed. + +theorem GRP049 : + \forall A:Set. + \forall inv: A \to A. + \forall mult: A \to A \to A. + \forall H: (\forall x,y,z:A.mult z (inv (mult (inv (mult (inv (mult z y)) x)) (inv (mult y (mult (inv y) y))))) = x). + \forall a,b:A. mult a (inv a)= mult b (inv b). +intros.auto paramodulation. +qed. -- 2.39.2