Thanks.
On 28/03/18 05:00, michael.norr...@data61.csiro.au wrote:
> 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" <marioxcc...@yandex.com>
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
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
