Stream: new members

Topic: cases on mutually recursive types

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?

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

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

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.

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

Jonathan Coates (Aug 16 2019 at 19:07):

Ahh, that's perfect. Thank you!

Last updated: May 18 2021 at 15:14 UTC