Zulip Chat Archive

Stream: general

Topic: Goal state in goal chaining

Yaël Dillies (Jan 21 2022 at 20:33):

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) :=
  { 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 }

Sebastian Ullrich (Jan 21 2022 at 20:37):

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

Patrick Massot (Jan 21 2022 at 20:38):

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

Yaël Dillies (Jan 21 2022 at 20:40):

Oooh, very nice Sebastian! Consider my point moot.

Yaël Dillies (Jan 21 2022 at 20:42):

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 (Jan 21 2022 at 20:43):

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 (Jan 21 2022 at 20:48):

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 (Jan 21 2022 at 20:50):

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 (Jan 21 2022 at 21:19):

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 (Jan 22 2022 at 02:03):

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).

Last updated: Aug 03 2023 at 10:10 UTC