Email Gateway (Aug 22 2022 at 20:10): Email Gateway (Aug 22 2022 at 20:10):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Dear Isabelle users and experts,
In the rules for submissions to Archives of Formal Proofs, it is written
that "No use of the command smt_oracle". If I well understood, this means
that proofs cannot be done using either "apply smt" or "by smt" (please
correct me if I am wrong). This was also pointed out in Gerwin's Style
Guide (section: "Do not use smt in proofs you need to maintain over longer
time"): http://proofcraft.org/blog/isabelle-style.html
(i) Is there an automatic way to change "smt" by some automatic reasoning
internal to Isabelle, e.g., metis, auto, simp?
(ii) In case of a negative answer for (i), which are the steps "by hand"
recommended for such a task?
Sincerely yours,
José M.
Email Gateway (Aug 22 2022 at 20:10):From: "lammich@in.tum.de" <lammich@in.tum.de>
Hi Jose
Smt can be used, as it replays the proof in the kernel, only smt_oracle is
ruled out.
Best
Peter
Email Gateway (Aug 22 2022 at 20:10):From: Dominique Unruh <unruh@ut.ee>
Hi,
I noticed that until October 2017, the submission instructions for AFP
also contained "No use of the command <code>smt</code>. The result of
this command depends on external tools that are not under our control
and may stop working in the future."
This was removed in commit 48c7802 (afp-devel) by Gerwin Klein.
I am curious why this is no longer a necessity? As I understood, the
reason was not the fact that the proof is not replayed (as in the case
of smt_oracle), but that the behavior of smt depends on Z3, and thus
breaks easily when Z3 changes.
Is my understanding correct? Has this situation changed? Or has merely
the policy changed and the expectation is that smt proofs are just fixed
once Z3 changes make them the smt proofs break?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:10):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Yes, the latter. The policy has changed, because we were observing very few failures of this kind in other Isabelle code where we did not have the restriction, and this has been played out similarly on the AFP since we changed it. We are also changing Z3 versions less often than we used to. I.e. the benefit of allowing smt outweighs the drawbacks.
I should probably update my style guide accordingly as well.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 20:11):From: Lawrence Paulson <lp15@cam.ac.uk>
I still tend to get rid of smt calls, though it’s a chore.
One tip is to use your working smt call to identify the specific instances of the lemmas that you need. So if you have
smt lemma_1 … lemma_n
you can see if it still works with lemma_1 [of a b], where a and b are constants in your problem. Once you’ve done that, then insert
using lemma_1 [of a b]
and try sledgehammer again. You might get a much better proof.
Larry
Last updated: Apr 25 2024 at 20:15 UTC