waynee95 (Oct 12 2022 at 20:55): waynee95 (Oct 12 2022 at 20:55):I have ran into this situation a few times where sledgehammer allegedly finds a proof using metis or smt and upon inserting it, it will stay red and won't terminate.
How can this be interpreted? Does that mean the statement is provable but it takes a long time and therefor needs more intermediate steps/information.
Or does that maybe mean it's not provable and the "found proof" is wrong?
Lukas Stevens (Oct 12 2022 at 20:56):Normally, this means that the smt solver found a proof but the replay mechanism recommends a proof that doesn't work.
waynee95 (Oct 12 2022 at 20:57):@Lukas Stevens I see
Mathias Fleury (Oct 13 2022 at 04:20):Normally sledgehammer provides you some timing information (like 1.5s), what does it say in such cases?
Mathias Fleury (Oct 13 2022 at 04:22):Lukas Stevens said:
Normally, this means that the smt solver found a proof but the replay mechanism recommends a proof that doesn't work.
sledgehammer should mark such cases as timed out.
Mathias Fleury (Oct 13 2022 at 04:24):By default running tactics are purple and failed ones are red. If you see a failed smt or metis tactic, you should also see an error message. Is there one?
Lukas Stevens (Oct 13 2022 at 09:03):Mathias Fleury said:
Lukas Stevens said:
Normally, this means that the smt solver found a proof but the replay mechanism recommends a proof that doesn't work.
sledgehammer should mark such cases as timed out.
It also sometimes happens that the proof just fails.
Mathias Fleury (Oct 13 2022 at 09:07):yeah true
Mathias Fleury (Oct 13 2022 at 09:08):BTW if you get errors in the reconstruction of smt, I take bug reports
waynee95 (Oct 14 2022 at 08:25):I think I have an explanation why I ran into that issue. The proof method generated by sledgehammer made use of an auxiliary lemma which was stubbed with a sorry which turned out to be faulty and doesn't hold.
So that's why the proof replay didn't work I assume because the auxiliary lemma was false.
Manuel Eberl (Oct 14 2022 at 11:12):That should not be a problem. A sorried theorem is a theorem like any other for tools such as sledgehammer. (Except that if it does not hold, sometimes sledgehammer manages to realise that you can actually prove False from it and will tell you so.)
Last updated: Apr 20 2024 at 08:16 UTC