cases on mutually recursive types

Stream: new members

[Jonathan Coates]

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]

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]

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

[Jonathan Coates]

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]

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]

Ahh, that's perfect. Thank you!