## Stream: Is there code for X?

### Topic: Destruct multiple disjunctions

#### 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.

#### 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],


#### 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


#### 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.

#### Reid Barton (Oct 08 2020 at 16:02):

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

#### Adam Topaz (Oct 08 2020 at 16:03):

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

#### Floris van Doorn (Oct 08 2020 at 21:40):

Another way to do this:

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


#### Adam Topaz (Oct 08 2020 at 21:43):

That's a nice trick!

#### 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