Destruct multiple disjunctions

Stream: Is there code for X?

[Adam Topaz]

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.

[Adam Topaz]

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

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

[Shing Tak Lam]

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

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Floris van Doorn]

Another way to do this:

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

[Adam Topaz]

That's a nice trick!

[Mario Carneiro]

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