bullet to focus subgoals

Stream: new members

[Joachim Breitner]

In Isabelle I am a big fan of named subgoals (I find them more readable and easier to maintain), and in Coq I can at least get close using bullets. In lean I found { … } allows me to focus on a single goal. Is there something like Coq’s bullets in lean?

[Johan Commelin]

Not in Lean 3. We only have { ... } to structure subproofs.

[Johan Commelin]

Well... you can write show your_target, { ... } which adds readability.

[Sebastien Gouezel]

{...} is really the equivalent of the bullets. What you can also do to improve readability is to state the goal you are going to prove, with show. Like

  -- assume you have 3 goals foo, bar and baz,
  show foo,
  { ...,
    ... },
  show bar,
  { ...,
    ... },
  show baz,
  { ...,
    ... }

[Joachim Breitner]

Will show pick a suitable subgoal? Or will that break if some change means the goals are now in different order or maybe some are solved?

[Johan Commelin]

No, it picks the right goal (if it exists)

[Johan Commelin]

If some change means the goal no longer exits, of course the proof will complain.

[Joachim Breitner]

Great, thanks. And I could have just looked that up on https://leanprover.github.io/reference/tactics.html :blushing:

[Eric Wieser]

tactic#case is also handy for named goals produced by cases or induction

[Joachim Breitner]

Ah, this is great, thanks!