Stream: Beginner Questions

Topic: Why are these lemmas different and not legal?

Sebastian Davidson (May 01 2025 at 00:14):

I've having trouble getting a grasp on how to use the Isar part of Isabelle. So far, I've got this lemma working:

lemma "A ∧ B ⟹ B ∧ A"
proof
  assume "A ∧ B" thus "B" ..
next
  assume "A ∧ B" thus "A" ..
qed

But it doesn't work when I try this:

lemma "A ∧ B ⟹ B ∧ A"
proof
  assume ab: "A ∧ B"
  then have ba: "B ∧ A"
  proof
    from ab have a: "A" ..
    from ab have b: "B" ..
    from a b show "B ∧ A" by (auto)
  qed
qed

Nor does this work, even though I copied it from an Isar manual.

lemma assumes "A ∧ B" shows "B ∧ A"
proof
  assume "A ∧ B"
  from this have "B" ..
  moreover have "A" ..
  ultimately show "B ∧ A"
qed

Is Isar not Isabelle/Isar? What ways would be the right ways to write the equivalent of the first lemma in Isabelle?

Mathias Fleury (May 01 2025 at 05:30):

In the second, it should be show ba not have ba and proof -

Mathias Fleury (May 01 2025 at 05:32):

With only proof, look at the state panel: the conjunction was already split, so you need to also split the show

Mathias Fleury (May 01 2025 at 05:33):

For the last one:

- you assume something that is not in the context for proof. Either using assms before the out-most proof or give it a name, remove the assume and use the name instead of this.
- same issue splitting of the goal
- at the point have "A" ..the assume is not in the context anymore. have "A" using ‹A ∧ B› .. works however

Sebastian Davidson (May 01 2025 at 15:49):

Thanks for the response. Now I see how you're meant to write it. What does adding the - at the end of proof mean, by the way?
For the last one, I thought that moreover was meant for using the same context as the last thing you said, so you wouldn't have to restate the assumption "A ∧B" and then ultimately was to combine them. Since that seems not to be the case, how should you use it?
Also, any tips on remembering what keywords do, and connecting it to how Isabelle evaluates proofs? I feel like I'm having trouble understanding how keywords affect the state of the proof, and it reminds me of learning to program again, when I didn't know what for and continue meant. I barely understand the distinction between have and show, and I keep getting words mixed up like how then means from this, hence means from this have, and thus means from this show, particularly since thus and hence have similar meanings to me in real speech.

Mathias Fleury (May 02 2025 at 04:38):

proof is short for proof standard where it default to apply something. With the - it applies nothing

Mathias Fleury (May 02 2025 at 04:39):

Sebastian Davidson said:

For the last one, I thought that moreover was meant for using the same context as the last thing you said, so you wouldn't have to restate the assumption "A ∧B" and then ultimately was to combine them. Since that seems not to be the case, how should you use it?

It exactly like you said but the context is not shared. Sharing context does not make too much sense anyway since have "A" and "B" exists

Mathias Fleury (May 02 2025 at 04:42):

Sebastian Davidson said:

Also, any tips on remembering what keywords do, and connecting it to how Isabelle evaluates proofs? I feel like I'm having trouble understanding how keywords affect the state of the proof, and it reminds me of learning to program again, when I didn't know what for and continue meant. I barely understand the distinction between have and show, and I keep getting words mixed up like how then means from this, hence means from this have, and thus means from this show, particularly since thus and hence have similar meanings to me in real speech.

Like programming you get used to it. My suggestion is to always start with a working sorry-ed proof. So:

proof
   show "B ∧ A"
     sorry
qed

this should work without errors. If it does not, you get the structure wrong. Once you get that, you only have to add have and also/finally/ultimately/from/...

Mathias Fleury (May 02 2025 at 04:43):

Also always go with the assumes / shows syntax unless the lemma is so trivial that you go apply style.

Last updated: May 31 2025 at 04:25 UTC