I'm afraid there is no solution to this problem whereby automatic tools will
make lots of progress. First order reasoners such as PROVE_TAC and METIS_TAC
try to do a little in this area (converting lambda-expressions to terms
involving combinators for example), but this only goes so far, and also makes
it hard to see what one should additionally provide to prime the provers. In
your case, the underlying goal might end up being
f (<=) = f (\x. B ((<) x) SUC)
= f (S (B B (<)) (K SUC))
Where B is actually combin$o. Given this, the supposedly relevant theorem
relating < and <= isn't going to apply. You could try giving METIS FUN_EQ_THM
as an argument I suppose.
Michael
On 27/3/18, 04:56, "Mario Xerxes Castelán Castro" <[email protected]>
wrote:
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.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
