Re: [isabelle] Auto sledgehammer fails to find proofs sledgehammer finds.



Hi David,

> However, the (marginally) more complex lemma:
> 
>    lemma "length xs > 0 ⟹ hd (rev xs) = last  xs"
> 
> fails to provide any automatic sledgehammer results, despite the fact
> that it can be solved quickly by explicitly writing:
> 
>    sledgehammer [provers=e,timeout=1.0]
> 
> which gives the results:
> 
>    "e": Try this: by (metis hd_rev length_0_conv less_numeral_extra(3)) (11 ms).
> 
> Is this expected behaviour (for example, because the latter does time
> slicing which enables it to find proofs that the former does not), or
> could there be a deeper problem here?

Thanks for the report. I was able to reproduce what you describe on my machine with Isabelle2013-RC1. Doubling the timeout to 4 s doesn't seem to help. Hence this would suggest it has something to do with the slicing or the otherwise reduced nature of Auto Sledgehammer.

However, with the current repository version (fcb7bbbe3799), it finds the proof as expected, even with the lower, default timeout (2 s). In addition, with the current "isabelle-release" version (782e430e6a83), which includes several Sledgehammer-related changes by both Makarius and myself that could make a difference here, it also works as expected. So I would simply recommend that you give it a try in the RC2 once it is available to confirm that the problem is gone for you too.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.