Chengsong Tan (Aug 31 2024 at 12:14): Chengsong Tan (Aug 31 2024 at 12:14):Dear All,
I have an Isabelle(2024) tool I want to share with you.
super_sketch-1.zip
In my project I had the problem of having to prove lemmas with
hundreds of subgoals and it was a bit cumbersome to have to
invoke Sledgehammer on each of them one-by-one. I solved my
problem with some ML code that extends Florian Haftmann's sketch
command. In the attached code, I implemented a super_sketch
command that outlines the proof skeleton but also invokes
sledgehammer on each subgoal and collects the proof suggestions.
Since it was quite helpful to me, I attach the code. Maybe others
might like to play with such a command as well. Super_sketch should
work "plug-and-play" by just including a theory and then invoking
the super_sketch command whenever there are many subgoals to be
solved by sledgehammer. There is a simple theory about regular
languages that illustrate how super_sketch works.
Note however, this code is just an experiment. The results are
necessarily non-deterministic as super_sketch calls the external
sledgehammer provers and they might reply with proofs in any
shape or order. Also sometimes the proof suggested by super_sketch
does not "reconstruct" unlike a manual invocation of sledgehammer
on the same goal. Also, when the number of subgoals goes up to
over a few hundred, the prover just grinds to a halt.
If someone knows why and can suggest a fix, I
would be very grateful. I am also happy to receive any feedback
how super_sketch works and any improvements.
Best wishes,
Chengsong Tan
Wenda Li (Sep 02 2024 at 13:20):Thanks for developing such a tool. Will surely give it a shot later on!
Last updated: Dec 21 2024 at 12:33 UTC