Gergely Buday (Jun 12 2023 at 15:53): Gergely Buday (Jun 12 2023 at 15:53):Sometimes the metis call Sledgehammer suggests is displayed in purple when copied to the proof, meaning that the underlying process is working, so the metis call went into an infinite loop.
What can I do in this situation, how can I figure out what had gone wrong, and how can I fix it?
Manuel Eberl (Jun 13 2023 at 09:45):I see three possibilities of what might cause this:
One, there is a bug somewhere in sledgehammer (e.g. in one of its translations from HOL to simpler logics. That's probably something that should be investigated by the Sledgehammer team.
Two, there is a bug in the external prover that found the "proof" and the "proof" is actally wrong. But I'm not sure if that could really cause this issue, because then I would expect Sledgehammer not to give you that "metis" call in the first place.
Three, something is going wrong in the Sledgehammer part where it converts a proof found by one of the external provers to a metis call. I'm never quite sure whether it is expected that this might happen in some cases or whether it is an actual bug.
I think it is probably best to ask one of the Sledgehammer experts like Jasmin Blanchette about this.
As for how you can fix it, well, if it suggests more than one proof to you (which is often the case) then you can try one of the others that it suggests to you. If not then I suggest you proceed in the same way that you would if it gave you no proof: try to break the goal up into smaller, simpler steps and see if it can do those. Or just do the entire proof "by hand".
But note that unless the proof it found is actually rubbish (due to e.g. a soundness bug in the translation or the external prover), the fact names occurring in the metis call often give you valuable information about what facts are actually crucial to the proof, often even enough to easily do the proof by hand. Just look at the list of facts it mentions, kick out all the ones whose content is "obvious" stuff like "n + 0 = n", and the remaining ones are probably the important ones.
Gergely Buday (Jun 13 2023 at 10:06):@Manuel Eberl after using the definition of id, Sledgehammer came up with a simp add proof, and that worked flawlessly. Something around metis is fishy, probably in Sledgehammer.
Manuel Eberl (Jun 13 2023 at 10:06):In that case please do try sending a minimal working example to Jasmin.
Manuel Eberl (Jun 13 2023 at 10:07):Could be a higher-order translation issue. Perhaps there's a lambda in there somewhere that confuses Sledgehammer. Just speculation.
Gergely Buday (Jun 13 2023 at 10:28):@Manuel Eberl I sent a problem report to him.
Mathias Fleury (Jun 13 2023 at 15:34):Most likely, the problem is that no proof method works and metis is the default method
Mathias Fleury (Jun 13 2023 at 15:35):@Martin Desharnais accidentally removed the time out that was marked before (and will be again in the next release)
Mathias Fleury (Jun 13 2023 at 15:35):(or maybe he was not responsible for that, but he is the current expert :-))
Martin Desharnais (Jun 15 2023 at 08:12):Mathias is correct, a metis proof is usually suggested when proof reconstruction as a mean to provide the list of lemmas to the user. It used to be stated explicitly that proof reconstruction failed, but the message was accidentally removed last year. It was noticed a few months later and is already back in the development version of Isabelle; so users can expect it back in Isabelle version 2023 at the end of the summer.
Manuel Eberl (Jun 16 2023 at 07:30):Just out of curiosity: why does sledgehammer not try to use the proofs found by the ATPs to construct an Isabelle proof instead of trying to find a new proof from scratch?
Manuel Eberl (Jun 16 2023 at 07:32):Is it too complicated to translate those proofs back given the logic encodings sledgehammer uses? Or is it simply not worth the effort because the current approach works almost all the time?
Manuel Eberl (Jun 16 2023 at 07:32):Would this be a viable option given strong higher-other ATPs?
Mathias Fleury (Jun 16 2023 at 08:00):this is done in two ways:
- direct checking of the proof : that is the approach used by smt (for veriT and z3)
- usage of the steps : used to produce the Isar proof that Sledgehammer suggests
Mathias Fleury (Jun 16 2023 at 08:03):The direct checking was never extended from SMT solvers to superposition, partly because the steps are more complicated to check (E can produce proof steps that even E is not able to check)
Mathias Fleury (Jun 16 2023 at 08:05):But it requires a lot of work from the SMT developers to produce usable proofs
Last updated: Apr 28 2024 at 04:17 UTC