Email Gateway (Aug 22 2022 at 10:28): Email Gateway (Aug 22 2022 at 10:28):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi all,
I've noticed after enabling auto-Sledgehammer that it (and friends like Nitpick) run on all the
lemmas in any file you open. So, for example, when you open a previously worked on theory,
Sledgehammer starts attacking lemmas that already have completed proofs. This isn't a large
impediment, but I just wanted to suggest that perhaps this behaviour could be improved on in future
by noticing the completed proof.
If there's a way to alter this behaviour that I have overlooked, please let me know and apologies
for the noise.
Thanks,
Matt
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 22 2022 at 10:30):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
There is actually a good use for this in some cases: autosledgehammer is extremely good at pointing out redundant lemmas.
Going through larger proof updates recently, I was able to remove quite a few proofs that were duplicates or close duplicates, which autosledgehammer had highlighted for me.
So maybe this should be configurable, at least.
Ideally autosledgehammer would recognise lemmas that are already solved by a one-liner and always skip those. And autosolve skip those that are already solved by a single rule application with one of the rules it is suggesting. But that’s probably a lot of proof text analysis for something that doesn’t really want to know about any of that.
Cheers,
Gerwin
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 22 2022 at 10:31):From: Lars Noschinski <noschinl@in.tum.de>
I'd like autosolve to skip non-lemma proof-obligations (for example
those of sublocale); at least if these have a successful proof.
-- Lars
Last updated: Apr 24 2024 at 01:07 UTC