Zulip Chat Archive

Stream: new members

Topic: cases on mutually recursive types


view this post on Zulip Jonathan Coates (Aug 16 2019 at 16:40):

Sorry if this is the wrong place to ask this - just wanted to double check a couple of things before flying off to the issue tracker. I've been trying to use the cases tactic on mutually-recursive types, and hit a bit of a wall. Basically, consider the (somewhat absurd) type:

mutual inductive mut, aux
with mut : Type
| mono : mut  mut
| cons : mut  mut  mut
with aux : Type
| nil : aux

I'm trying to use it as follows:

example : mut  aux := begin intro xs, cases xs,
    case mut.mono : x { exact x },
    case mut.cons : x _ { exact x }
end

However, while this looks like it should work, it fails to check - mut.mono and mut.cons are not actually constructors.

Using #print shows that mut.mono is in fact an alias to the actual constructor (@[pattern] def mut.mono : mut → mut := mut._mut_.mono_0). Just wondering - is this expected behaviour, and if so, is there a suitable workaround?

view this post on Zulip Mario Carneiro (Aug 16 2019 at 17:03):

This is expected behavior. cases and induction only currently work on actual inductive types, which limits their usefulness when applied to mutual and nested inductives, which are compiled to simple inductive types. Try using the equation compiler instead, which respects these fake inductives

view this post on Zulip Mario Carneiro (Aug 16 2019 at 17:04):

But the real answer is that nested and mutual inductives are buggy and unstable so we avoid them when possible

view this post on Zulip Jonathan Coates (Aug 16 2019 at 17:11):

Ah that's good to know, thank you!

I was originally using the equation compiler/match expressions, and then found myself rather wanting the constructor hypothesis that cases provides.

view this post on Zulip Mario Carneiro (Aug 16 2019 at 17:31):

you can get the hypothesis by doing the same trick that cases does: use match t, rfl : \forall x : T, x = t -> _ with ...

view this post on Zulip Jonathan Coates (Aug 16 2019 at 19:07):

Ahh, that's perfect. Thank you!


Last updated: May 18 2021 at 15:14 UTC