Hello. Metis can prove «(λx m. x ≤ m) = (λx m. x < SUC m)» using arithmeticTheory.LESS_EQ_IFF_LESS_SUC, but if the left hand side and right hand instead appear as the operands of a combination then it no longer works. The same behavior applies to “PROVE_TAC”.
> TAC_PROOF (([], “(λx m. x ≤ m) = (λx m. x < SUC m)”), METIS_TAC
[arithmeticTheory.LESS_EQ_IFF_LESS_SUC]);
metis: r[+0+5]+0+0+1+0+0+1#
val it = ⊢ (λx m. x ≤ m) = (λx m. x < SUC m): thm
> TAC_PROOF (([], “f (λx m. x ≤ m) = f (λx m. x < SUC m)”), METIS_TAC
[arithmeticTheory.LESS_EQ_IFF_LESS_SUC]);
<<HOL message: inventing new type variable names: 'a>>
metis: r[+0+7]+0+0+0+0+0+0+0!
Exception-
HOL_ERR
{message = "no solution found", origin_function = "FOL_FIND",
origin_structure = "folTools"} raised
> TAC_PROOF (([], “f (λx m. x ≤ m) = f (λx m. x < SUC m)”),
metisTools.HO_METIS_TAC [arithmeticTheory.LESS_EQ_IFF_LESS_SUC]);
<<HOL message: inventing new type variable names: 'a>>
metis: r[+0+7]+0+0+0+0+0+0+0!
Exception-
HOL_ERR
{message = "no solution found", origin_function = "FOL_FIND",
origin_structure = "folTools"} raised
This is a reduced test case to show the problem. Obviously I could use
the simplifier here, but in general Metis and MESON seem to be unable to
use equality of lambda terms to complete a proof and thus they fail for
some otherwise simple use cases that occur in practice. What should I do
about this?
Thanks.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
