Named deferred goals

Stream: Is there code for X?

[Stuart Presnell]

Is there a way to defer the current subgoal and assign a name to it, and then later switch to work on that named goal (in a similar way to tactic#case)?

[Stuart Presnell]

For example, this might be used to make proofs in calc mode more readable, by separating the step-by-step part of the proof from the proving-the-steps part.

[Stuart Presnell]

So you could write something like

calc a = b : by defer step1
...    = c : by defer step2
...    = d : by defer step3

and then close the goals "step1", "step2", "step3" separately.

[Mario Carneiro]

you can use rotate to move a goal to the end, but that only works within a single begin/end block

[Mario Carneiro]

the way I would write something like that is:

begin
  calc a = b : _
  ...    = c : _
  ...    = d : _,
  { ... },
  { ... },
  { ... },
end

[Stuart Presnell]

Ah, I didn't know you could do that (although I now see that it's noted explicitly in the documentation https://leanprover-community.github.io/extras/calc.html)

[Eric Rodriguez]

I remember in the lean4 stream there was an attempt to make a tactic like swap n but it was basically a focus block for the nth goal; did that end up happening? Is it worth backporting it to Lean3?

[Eric Wieser]

Isn't that just work_on_goal?

[Eric Wieser]

I feel like the real request here is to name the underscores, which lean4 supports natively

[Stuart Presnell]

How do you write that in lean4?

[Eric Wieser]

I was under the impression it was ?foo in place of _