Zulip Chat Archive

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

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

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

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  ]


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):

Reid Barton said:

Sort of a beefed-up split_ifs, I guess?

, :wink:

Last updated: Dec 20 2023 at 11:08 UTC