Stream: metaprogramming / tactics

Topic: Allowing focussing on multiple goals in case

Yury G. Kudryashov (Dec 18 2020 at 18:45):

tactic#rcases allows multiple targets

Yury G. Kudryashov (Dec 18 2020 at 18:45):

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

Eric Wieser (Dec 18 2020 at 19:05):

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

Eric Wieser (Dec 18 2020 at 19:08):

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 (Dec 18 2020 at 19:16):

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 (Dec 18 2020 at 19:16):

the example is too minimal to reflect this

Mario Carneiro (Dec 18 2020 at 19:17):

Yury means this:

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


Eric Wieser (Dec 18 2020 at 19:31):

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

Eric Wieser (Dec 18 2020 at 19:32):

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 (Dec 18 2020 at 19:33):

Can rcases give me hi and hj for that case?

Mario Carneiro (Dec 18 2020 at 19:53):

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

Eric Wieser (Dec 18 2020 at 20:44):

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 (Dec 18 2020 at 20:45):

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

Eric Wieser (Dec 18 2020 at 20:45):

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

Eric Wieser (Jan 27 2021 at 09:54):

Some more discussion in #general

Last updated: May 09 2021 at 23:10 UTC