From: Enrico Tassi Date: Fri, 29 Sep 2006 12:48:07 +0000 (+0000) Subject: added tests for auto X-Git-Tag: 0.4.95@7852~973 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=206c348a9a9900ee3a485a71ac2b10ebd54e6dd8;p=helm.git added tests for auto --- diff --git a/matita/tests/makefile b/matita/tests/makefile index 39d64a952..c4568230e 100644 --- a/matita/tests/makefile +++ b/matita/tests/makefile @@ -1,6 +1,6 @@ H=@ -RT_BASEDIR=../ +RT_BASEDIR=/home/tassi/helm/software/matita/ OPTIONS=-bench MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) @@ -9,25 +9,29 @@ CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) devel:=$(shell basename `pwd`) +ifneq "$(SRC)" "" + XXX=SRC=$(SRC) +endif + all: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) clean: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) cleanall: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all all.opt opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) clean.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) cleanall.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all %.mo: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ %.mo.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ preall: - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) diff --git a/matita/tests/paramodulation/irratsqrt2.ma b/matita/tests/paramodulation/irratsqrt2.ma new file mode 100644 index 000000000..0eac7556e --- /dev/null +++ b/matita/tests/paramodulation/irratsqrt2.ma @@ -0,0 +1,160 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/paramodulation/irratsqrt2/". + +include "nat/times.ma". +include "nat/minus.ma". + +theorem prova : + \forall n,m:nat. + \forall P:nat \to Prop. + \forall H:P (S (S O)). + \forall H:P (S (S (S O))). + \forall H1: \forall x.P x \to O = x. + O = S (S (S (S (S O)))). + intros. + auto. + qed. + +theorem example2: +\forall x: nat. (x+S O)*(x-S O) = x*x - S O. +intro; +apply (nat_case x); + [ auto timeout = 1.|intro.auto timeout = 1.] +qed. + +theorem irratsqrt2_byhand: + \forall A:Set. + \forall m:A \to A \to A. + \forall divides: A \to A \to Prop. + \forall o,a,b,two:A. + \forall H1:\forall x.m o x = x. + \forall H1:\forall x.m x o = x. + \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. + \forall H1:\forall x.m x o = x. + \forall H2:\forall x,y.m x y = m y x. + \forall H3:\forall x,y,z. m x y = m x z \to y = z. + (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) + \forall H4:\forall x,y.(divides x y \to (\exists z.m x z = y)). + \forall H4:\forall x,y,z.m x z = y \to divides x y. + \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y. + \forall H5:m a a = m two (m b b). + \forall H6:\forall x.divides x a \to divides x b \to x = o. + two = o. + intros. + cut (divides two a); + [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.] + |elim (H6 ? ? Hcut). + cut (divides two b); + [ apply (H10 ? Hcut Hcut1). + | elim (H8 b b);[assumption.|assumption| + apply (H7 ? ? (m a1 a1)); + apply (H5 two ? ?);rewrite < H9. + rewrite < H11.rewrite < H2. + apply eq_f.rewrite > H2.rewrite > H4.reflexivity. + ] + ] + ] +qed. + +theorem irratsqrt2_byhand': + \forall A:Set. + \forall m,f:A \to A \to A. + \forall divides: A \to A \to Prop. + \forall o,a,b,two:A. + \forall H1:\forall x.m o x = x. + \forall H1:\forall x.m x o = x. + \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. + \forall H1:\forall x.m x o = x. + \forall H2:\forall x,y.m x y = m y x. + \forall H3:\forall x,y,z. m x y = m x z \to y = z. + (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) + \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). + \forall H4:\forall x,y,z.m x z = y \to divides x y. + \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y. + \forall H5:m a a = m two (m b b). + \forall H6:\forall x.divides x a \to divides x b \to x = o. + two = o. + intros. + cut (divides two a); + [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.] + |(*elim (H6 ? ? Hcut). *) + cut (divides two b); + [ apply (H10 ? Hcut Hcut1). + | elim (H8 b b);[assumption.|assumption| + + apply (H7 ? ? (m (f two a) (f two a))); + apply (H5 two ? ?); + rewrite < H9. + rewrite < (H6 two a Hcut) in \vdash (? ? ? %). + rewrite < H2.apply eq_f. + rewrite < H4 in \vdash (? ? ? %). + rewrite > H2.reflexivity. + ] + ] + ] +qed. + +theorem irratsqrt2: + \forall A:Set. + \forall m,f:A \to A \to A. + \forall divides: A \to A \to Prop. + \forall o,a,b,two:A. + \forall H1:\forall x.m o x = x. + \forall H1:\forall x.m x o = x. + \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. + \forall H1:\forall x.m x o = x. + \forall H2:\forall x,y.m x y = m y x. + \forall H3:\forall x,y,z. m x y = m x z \to y = z. + (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) + \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). + \forall H4:\forall x,y,z.m x z = y \to divides x y. + \forall H4:\forall x.divides two (m x x) \to divides two x. + \forall H5:m a a = m two (m b b). + \forall H6:\forall x.divides x a \to divides x b \to x = o. + two = o. +intros. +auto depth = 5 timeout = 180. +qed. + +(* time: 146s *) + + +(* intermediate attempts + + cut (divides two a);[| + (* apply H8;apply (H7 two (m a a) (m b b));symmetry;assumption. *) + auto depth = 4 width = 3 use_paramod = false. ] + (*auto depth = 5.*) + + apply H10; + [ assumption. + |(*auto depth = 4.*) apply H8; + (*auto.*) + apply (H7 ? ? (m (f two a) (f two a))); + apply (H5 two ? ?); + cut ((\lambda x:A.m x (m two ?)=m x (m b b))?); + [|||simplify; + auto paramodulation. + (*auto.*) + rewrite < H9. + rewrite < (H6 two a Hcut) in \vdash (? ? ? %). + rewrite < H2.apply eq_f. + rewrite < H4 in \vdash (? ? ? %). + rewrite > H2.reflexivity. + ] + +qed. +*)