Re: [Hol-info] Unexpected failure to considerate equality of lambda terms in Metis and MESON

2018-03-28 Thread Mario Xerxes Castelán Castro 
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"  
> 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]);
> <>
> 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]);
> <>
> 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

Re: [Hol-info] Unexpected failure to considerate equality of lambda terms in Metis and MESON

2018-03-28 Thread Michael.Norrish 
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"  
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]);
<>
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]);
<>
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

[Hol-info] Unexpected failure to considerate equality of lambda terms in Metis and MESON

2018-03-26 Thread Mario Xerxes Castelán Castro 
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]);
<>
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]);
<>
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