Stream: Beginner Questions

Topic: Naming facts in an Isar proof usable in subgoals

Chengsong Tan (Feb 09 2024 at 04:03):

Hi,

I am trying to prove a large conjunction from a large conjunction, and being able to name each conjunct would allow solvers to pick from them individually, greatly helping the scalability. Here's a MWE demonstrating the ideal proof structure I want:

lemma mwe: "⟦a = 1+1 ∧ b = 2+1 ∧ c = 3+1 ⟧ ⟹ a + b = 5 ∧ b+c = 7 ∧ c+a = 6"
(is "?asmps ⟹ ?concls")
proof (intro conjI)
  have a2: "a = 2" sorry
    have b3: "b = 3" sorry
    have c4: "c = 4" sorry
  show "a+b = 5"
    using a2 b3 by simp
next
  show "b+c = 7"
    using b3 c4 by simp
  show "c+a = 6"
    using c4 a2
qed

The idea is that facts like a2 b3 and c4 should be globally visible in the entire proof so that each subgoal can freely choose to pick facts they need. However using the proof method (intro conjI) they are only visible to the first subgoal. Of course I can replicate the have a2 ... bits in every subproof, but I wonder if there's a more efficient way to achieve the desired effect.

Doing something like

lemma mwe: "⟦a = 1+1 ∧ b = 2+1 ∧ c = 3+1 ⟧ ⟹ a + b = 5 ∧ b+c = 7 ∧ c+a = 6"
(is "?asmps ⟹ ?concls")
  have a2: "a = 2" sorry
    have b3: "b = 3" sorry
    have c4: "c = 4" sorry
proof (intro conjI)

also gives me error.

Best wishes,
Chengsong

Maximilian Schäffeler (Feb 09 2024 at 09:11):

You can just remove the 'next' in this proof.

Last updated: Apr 28 2024 at 12:28 UTC