Email Gateway (Aug 19 2022 at 12:20): Email Gateway (Aug 19 2022 at 12:20):From: David Greenaway <david.greenaway@nicta.com.au>
[[ Originally posted to the Isabelle 2013-1 RC1 issue tracker. Re-posting
to Isabelle-users by request of Makarius. ]]
Hi all,
In Isabelle/jEdit, when "Auto Sledgehammer" is enabled, typing:
lemma "2 + 2 = (4::nat)"
quickly gives a proof in the output window:
Auto Sledgehammer ("e") found a proof: by (metis numeral_Bit0).
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?
(Isabelle 2013-RC1, running under 64-bit Ubuntu 13.04, with Unity.)
Thanks so much,
David
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 12:21):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi David,
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
Last updated: Nov 21 2024 at 12:39 UTC