Allowing focussing on multiple goals in `case`

Stream: metaprogramming / tactics

[Yury G. Kudryashov]

tactic#rcases allows multiple targets

[Yury G. Kudryashov]

You can do rcases ⟨a, b⟩ with ...

[Eric Wieser]

I don't follow, how would you write the above with rcases?

[Eric Wieser]

Perhaps my title was unclear - I'm not talking about cases matching on multiple objects, but on case being able to focus on multiple goals.

[Mario Carneiro]

I think it would be nice to have work_on_goals and not just work_on_goal for this, but usually you can phrase such proofs with ; to pick out the goals just by having the tactic fail when it's not applicable

[Mario Carneiro]

the example is too minimal to reflect this

[Mario Carneiro]

Yury means this:

example (α β : Type*) (i j : α ⊕ β) : ℕ :=
begin
  rcases ⟨i, j⟩ with ⟨i|i, j|j⟩,
  exacts [1, 2, 2, 1]
end

[Eric Wieser]

I thought about work_on_goals too, although I wasn't sure where to insert unsolved goals back into the goals list

[Eric Wieser]

Which is a problem, because it makes

work_on_goals [0, 3] {},
work_on_goals [1, 2] {},

behave poorly if the tactic blocks change the number of goals

[Eric Wieser]

Can rcases give me hi and hj for that case?

[Mario Carneiro]

I think you should try not to write tactic scripts like this

[Eric Wieser]

Can you suggest an alternative for these lines?

https://github.com/leanprover-community/mathlib/blob/f942f91ff4ae9f080f520d8093a0448cec334bf0/src/linear_algebra/alternating.lean#L546-L563

[Eric Wieser]

I mean, I guess I could just expand all four cases and deal with the duplication

[Eric Wieser]

But if I were doing this on paper, I'd want to group the similar goals

[Eric Wieser]

Some more discussion in #general