Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Allowing focussing on multiple goals in `case`


view this post on Zulip Yury G. Kudryashov (Dec 18 2020 at 18:45):

tactic#rcases allows multiple targets

view this post on Zulip Yury G. Kudryashov (Dec 18 2020 at 18:45):

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

view this post on Zulip Eric Wieser (Dec 18 2020 at 19:05):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:16):

the example is too minimal to reflect this

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 18 2020 at 19:33):

Can rcases give me hi and hj for that case?

view this post on Zulip Mario Carneiro (Dec 18 2020 at 19:53):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 18 2020 at 20:45):

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

view this post on Zulip Eric Wieser (Dec 18 2020 at 20:45):

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

view this post on Zulip Eric Wieser (Jan 27 2021 at 09:54):

Some more discussion in #general


Last updated: May 09 2021 at 23:10 UTC