## Stream: new members

### Topic: cases by match arms

#### Henning Dieterichs (Dec 21 2020 at 12:09):

I have a match that branches over two inductive types. However, there are way fewer arms than cases due to _. Is there a nice way to do cases on the arms rather than the match-inputs?

Here is an (artificial) example:

inductive Category
| foo
| bar
| baz

def cat (n: nat): Category := if n < 5 then Category.foo else Category.bar

def foo (n: nat) := match cat n, cat (n + 1) with
| Category.foo, _ := n + 1
| Category.bar, Category.bar := n + 2
| Category.bar, _ := n + 3
| Category.baz, _ := n + 4
end

example (n: nat): foo n > n :=
begin
unfold foo, -- goal: foo._match_1 n (cat n) (cat (n + 1)) > n
sorry,
end


There are 16 cases with cases cat n; cases cat (n+1);. However, I would like to only consider the four cases of the match. Each match arm case should provide hypotheses which describe all cases when that match arm is selected. (I think it would be reasonable to do this kind of casing automatically when unfolding a definition that uses pattern matching)

#### Henning Dieterichs (Dec 21 2020 at 12:18):

Maybe a tactic unfold_match is what I'm looking for. It would be nice if it would consider nested matches too.
In my actual scenario, I have this:

def Gdt.mark_inactive_leaves : Gdt → Env → Ant bool
| (Gdt.grd (Grd.xgrd grd) tr) env :=
match xgrd_eval grd env with
| none := tr.mark_all_leaves_inactive
| some env' := tr.mark_inactive_leaves env'
end
| ...


My goal G is like this:

G[  (Gdt.grd (Grd.xgrd gdt_grd) gdt_tr).mark_inactive_leaves env   ]


It would be nice if I could do unfold_match Gdt.mark_inactive_leaves which would solve the goal and create two new ones:

h:  xgrd_eval grd env = none
G[ tr.mark_all_leaves_inactive  ]


and

h:  xgrd_eval grd env = some env'
G[ tr.mark_inactive_leaves env'  ]


Does such a tactic exist?

#### Mario Carneiro (Dec 21 2020 at 18:49):

I recall someone working on this back in june, but I don't know if we got a PR out of it

#### Reid Barton (Dec 21 2020 at 18:51):

Sort of a beefed-up split_ifs, I guess?

#### Henning Dieterichs (Dec 21 2020 at 18:52):

I guess match is rarely used for math anyway?

#### Henning Dieterichs (Dec 21 2020 at 18:53):

exact
Reid Barton said:

Sort of a beefed-up split_ifs, I guess?

, :wink:

Last updated: May 08 2021 at 05:14 UTC