Alex Weisberger (Sep 09 2023 at 01:02): Alex Weisberger (Sep 09 2023 at 01:02):Recently I've ran into a few cases where I prove a proposition, but it's only true vacuously because the assumptions aren't satisfiable. Of course, we have to be careful about defining assumptions for this reason. But, this is a big problem practically, since detecting such assumptions is not always trivial.
So, does anyone have any advice for how to a) detect this scenario or b) prove that this isn't the case? I read Gerwin Klein's Isabell style guide a while back where he mentions this pitfall, and recommends proving that a theorem's assumptions are satisfiable. Is that the best thing to do?
Wenda Li (Sep 09 2023 at 08:15):To detect inconsistent assumptions, perhaps we can attempt to prove False using Sledgehammer. Showing assumptions are satisfiable is much harder -- not sure if there is a systematic way. Nitpick?
Alex Weisberger (Sep 09 2023 at 12:25):Nitpick has been working really well to show that a theorem is false, but I wouldn't know how to use it to check the satisfiability of assumptions.
Wenda Li (Sep 09 2023 at 12:42):Might be a bit simplistic, but I was thinking that we can substitute False for the actual conclusion and then call nitpick:
lemma "x<(1::real) ⟹ False"
nitpick
If a counterexample can be found, then the assumption is satisfiable (in the example above we can have x=0 to satisfy the assumption).
Alex Weisberger (Sep 09 2023 at 12:56):That's a really good idea.
Yutaka Nagashima (Sep 24 2023 at 21:35):Alex Weisberger said:
Recently I've ran into a few cases where I prove a proposition, but it's only true vacuously because the assumptions aren't satisfiable. Of course, we have to be careful about defining assumptions for this reason. But, this is a big problem practically, since detecting such assumptions is not always trivial.
So, does anyone have any advice for how to a) detect this scenario or b) prove that this isn't the case? I read Gerwin Klein's Isabell style guide a while back where he mentions this pitfall, and recommends proving that a theorem's assumptions are satisfiable. Is that the best thing to do?
Hi Alex,
I hope you're doing well!
I once faced a challenge similar to yours when I was trying to produce numerous conjectures algorithmically. I noticed that most of these conjectures turned out to be 'vacuously' false. Naturally, I aimed to filter out such 'vacuously' correct conjectures.
To tackle this, I extracted premises from these conjectures using Logic.strip_imp_prems and then integrated them into a proof state. Following that, I used Quickcheck and Nitpick on the proof state.
For your situation, you might consider creating a new proposition by merging the premises into a single term using meta-conjunction.
One thing to note: while this method worked for me, it did require a bit of ML-level programming, especially the first time around. If you have only a small number of problems, Wenda's approach seems more suitable to me.
Here's a link that might be helpful:
GitHub Link
I hope this helps, and I'm here if you have any more questions!
Best,
Yutaka
Last updated: Dec 21 2024 at 12:33 UTC