Email Gateway (May 04 2022 at 11:44): Email Gateway (May 04 2022 at 11:44):From: Szymon Antoniak <sa394197@students.mimuw.edu.pl>
Hello,
How does adding premises to Sledgehammer work? As I understand it, there are two phases to ledgehammer: first, premise selection, which is done by feeding a lot of premises+current goal to external provers; if some prover manages to show the goal with the use of some subset of the premises, it then returns a message that the proof is possible, along with the list of premises. Then, Isabelle tries to recreate the proof in metis, using that list of premises.
Anyway, I'm curious about what adding premises to sledgehammer does. If we do "by sledgehammer add: my_lemma", does my_lemma get added to the premise selection stage, or the proof reconstruction stage? I am under the impression that we add to the premise selection stage, since there's a line in the sledgehammer that says
The specified facts then replace the least relevant facts that would otherwise be included; the other selected facts remain the same.
This makes me think that we add to the premise pool before we call the provers, and our chosen premise may or may not be returned as relevant if some prover succeeds. Is this the case, or do our added premises get added post factum to the list of premises supplied to metis, assuming some prover succeeded?
Best,
Szymon
Email Gateway (May 12 2022 at 07:43):From: Jasmin Blanchette <cl-isabelle-users@lists.cam.ac.uk>
Dear Szymon,
I'm not sure I understand 100% what you ask, but I will explain how premises work in Sledgehammer, hoping this answers your question.
There are two ways to supply custom lemmas as premises to Sledgehammer: the "using" syntax and the parenthesis syntax (e.g. "sledgehammer (add_comm le_def)" if you call Sledgehammer directly).
With the "using" syntax, this is a general Isabelle syntax that Sledgehammer honors, but also other tools. If you keep the "using" there, these premises will be passed to "metis" or any other command invocation generated by Sledgehammer. You might want to try to manually remove the premises one by one and see if the "metis" (or other) call succeeds without.
With the other syntax, the premises are not passed to "metis" (or other). They are only passed to Sledgehammer.
I hope this helps.
Cheers,
Jasmin
Last updated: Jul 15 2022 at 23:21 UTC