Goal state in goal chaining

Stream: general

[Yaël Dillies]

I suspect one of the reasons people use ; so little is that you basically go blind with respect to the goals. Would it be possible to show all focused goals with their respective states simultaneously?

example (p q r : Prop) (h : r) : (p → r) ∧ (q → r) :=
begin
  split;
  { intro, -- currently shows one goal with the cursor here
-- 1 goal
-- p q r : Prop
-- h : r
-- ᾰ : p
-- ⊢ r
-- I want it to show
-- 2 goals
-- p q r : Prop
-- h : r
-- ᾰ : p
-- ⊢ r
-- p q r : Prop
-- h : r
-- ᾰ : q
-- ⊢ r
    exact h }
end

[Sebastian Ullrich]

You might be happy to hear that Lean 4 does this image.png

[Patrick Massot]

Another reason is that ; very often lead to obfuscated proofs if there is more than one tactic after it.

[Yaël Dillies]

Oooh, very nice Sebastian! Consider my point moot.

[Yaël Dillies]

Patrick Massot said:

Another reason is that ; very often lead to obfuscated proofs if there is more than one tactic after it.

But why is it obfuscating? I claim this is precisely because you can hardly inspect the goal. If you have split, { tac1, tac2, tac3 }, { tac1, tac2, tac3 }, then replacing it with split; { tac1, tac2, tac3 } doesn't obfuscate anything. I would even claim it makes the proof more readable.

[Yaël Dillies]

Of course, a side effect would be that people will start trying to parallel-golf, which indeed could obfuscate stuff. But that's a question of what people will do with the tools we hand them, rather than the tools themselves.

[Kevin Buzzard]

I almost always avoid the semicolon when teaching in Lean 3 for the sole reason that I think the students will find it confusing. The only times I've used it in my class so far are split; assumption and split;linarith, i.e. split; close both goals; for such arguments you don't need to see the tactic state.

[Henrik Böving]

It's made a little more explicit that its different from , in Lean 4 by both not having a comma and having <;> instead of just the regular ; so maybe that helps?

[Eric Wieser]

I've sometimes seen proofs like split; simp; nonsense and lean happily ignores the nonsense - which is another mark against using ;

[Bryan Gin-ge Chen]

I'm a bit late to the conversation, but lean#201 tracks this in (community) Lean 3. (As Yaël said, this is probably moot as we'll probably move to Lean 4 before this issue is tackled).