Zulip Chat Archive

Stream: Is there code for X?

Topic: Destruct multiple disjunctions


view this post on Zulip Adam Topaz (Oct 08 2020 at 15:49):

Suppose I have a number of disjunctions (or some other inductive type) are hypotheses in my context. Is there a tactic that will case split on all of them and give the appropriate number of subgoals? Is there some rcases magic that will do this?

Here is a silly example:

import tactic

variables (p1 p2 q1 q2 c11 c12 c21 c22 : Prop)
  (h11 : p1  q1  c11)
  (h12 : p1  q2  c12)
  (h21 : p2  q1  c21)
  (h22 : p2  q2  c22)

include h11 h12 h21 h22

example : p1  p2  q1  q2  c11  c12  c21  c22 :=
begin
  intros h1 h2,
  cases h1,
  { cases h2,
    { left, finish [h11] },
    { right, left, finish [h12] }},
  { cases h2,
    { right, right, left, finish [h21] },
    { right, right, right, finish [h22] }},
end

I would be much happier if I didn't have to write cases h2 twice.

view this post on Zulip Adam Topaz (Oct 08 2020 at 15:52):

It would be nice if, in this case, I could write something along the lines of

  rcases [h1,h2] with [h1|h1,h2|h2],

view this post on Zulip Shing Tak Lam (Oct 08 2020 at 16:01):

example : p1  p2  q1  q2  c11  c12  c21  c22 :=
begin
  rintros (h1 | h1) (h2 | h2),
  -- 4 goals here
  all_goals {finish}
end

view this post on Zulip Adam Topaz (Oct 08 2020 at 16:01):

okay, sure that works for this example. But my actual assumptions are a bit more complicated than this.

view this post on Zulip Reid Barton (Oct 08 2020 at 16:02):

rcases h1 with h1 | h1; rcases h2 with h2 | h2,

view this post on Zulip Adam Topaz (Oct 08 2020 at 16:03):

Yeah that's exactly what I'm looking for. Didn't think of using ; thanks!

view this post on Zulip Floris van Doorn (Oct 08 2020 at 21:40):

Another way to do this:

obtain hp1|hp2, hq1|hq12 : _  _ := h1, h2⟩,

view this post on Zulip Adam Topaz (Oct 08 2020 at 21:43):

That's a nice trick!

view this post on Zulip Mario Carneiro (Oct 11 2020 at 07:15):

This is now supported as of #4569:

example : p1  p2  q1  q2  c11  c12  c21  c22 :=
begin
  intros h1 h2,
  rcases e1, e2 with h1 | h1, h2 | h2⟩,
end
example : p1  p2  q1  q2  c11  c12  c21  c22 :=
begin
  intros h1 h2,
  obtain h1 | h1, h2 | h2 := e1, e2⟩,
end

in addition to the already supported rintros (h1 | h1) (h2 | h2), form that was mentioned


Last updated: May 07 2021 at 21:10 UTC