Stream: Beginner Questions

Topic: "It suffices to show..."

John Hughes (May 11 2025 at 13:07):

Proofs in math books often start with "to prove X, it suffices to show Y, because ...", followed by a quick proof that Y implies X. The remainder of the proof then tries to show Y. This is more or less one step of a 'backward' proof.

I've tried to mimic this in Isabelle (using presume) , avoiding the need to show that Y implies X by including it as an assumption, and similarly avoiding the proof that something implies Y by including that as another assumption.

lemma suffices_example:
  fixes A B C
  assumes a1: "A ∧ B ⟹ D"
  assumes a2: "D ⟹ C"
  shows "A ∧  B ⟹ C"
proof -
  presume ph: D
  show ?thesis using ph a2  by blast
  show q: "A ∧ B ⟹ D" using a1 by blast

When I get to the end of this attempted proof, I end up in a state where this is A ∧ B ⟹ D and the goal is A ∧ B ⟹ D as well. Frankly, I thought that the last line I wrote would complete the proof, but .. well, it didn't. But I don't know what to do at this point to complete the proof. Can someone suggest how this might be done?

Mathias Fleury (May 11 2025 at 13:49):

you are missing a next before the second show

John Hughes (May 11 2025 at 13:59):

Thanks! That indeed fixes the problem.

But what does that "next" actually do? All it appears to do in the proof-state panel is remove "D" as "this". Is there some richer visualization of the state that would let me understand more of what's going on?

After the first "show" the goal shown in the proof-state changes, and I set about "show"ing the newly-displayed goal. Is there some way I could have known this wasn't enough? (As a beginning user, it's pretty frustrating to have "this" and "goal" look identical, but be unable to progress!)

Mathias Fleury (May 11 2025 at 14:01):

It cleans the assumptions

Mathias Fleury (May 11 2025 at 14:02):

the second show you have still has D has assumption, which you do not want

Mathias Fleury (May 11 2025 at 14:04):

I stumbled on the missing next by accident. I actually have no clue how you are supposed to know…

Mathias Fleury (May 11 2025 at 14:04):

Actually the show should not have worked in the first place but I don't really know why it did

John Hughes (May 11 2025 at 14:16):

Thank you. The fact that you, as a pretty experienced user, have no idea how I was supposed to know is some comfort to me. The proof in its revised form

lemma suffices_example:
  fixes A B C
  assumes a1: "A ∧ B ⟹ D"
  assumes a2: "D ⟹ C"
  shows "A ∧  B ⟹ C"
proof -
  presume ph: D
  show ?thesis using ph a2  by blast
next
  show q: "A ∧ B ⟹ D" using a1 by blast
qed

actually makes some sense to me, esp. when you say that "next" clears the assumptions. Now part 1 says "if you assume D, you can prove the result, so I'm going to change the goal to say "assumptions imply D",
and part 2 (after the next) gets rid of the assumption that D is true, but the goal remains. So now I prove that the actual assumptions (in the lemma-statement) imply D, and I'm done.

I'm not sure if that's what's actually going on, but it makes enough sense for me to proceed.

Last updated: Jun 21 2025 at 01:46 UTC