cases by match arms

Stream: new members

[Henning Dieterichs]

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]

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]

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

[Reid Barton]

Sort of a beefed-up split_ifs, I guess?

[Henning Dieterichs]

I guess match is rarely used for math anyway?

[Henning Dieterichs]

exact
Reid Barton said:

Sort of a beefed-up split_ifs, I guess?

, :wink: