Zulip Chat Archive

Stream: new members

Topic: cases by match arms


view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 21 2020 at 18:51):

Sort of a beefed-up split_ifs, I guess?

view this post on Zulip Henning Dieterichs (Dec 21 2020 at 18:52):

I guess match is rarely used for math anyway?

view this post on Zulip 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