mututal instances and autogeneration

Stream: general

[Brian Milnes]

I have a mutual inductive definition for a PL semantics: a rather natural way to do this. It works well, but the definitions (which I'm moving from Coq) are rather complicated and so I have some test code. #eval and printing things fails because writing instances of the has_repr type class has failed due to it not taking a mutual keyword also. Am I missing a keyword to make these? It would also be very nice if we had a command that just generated these, perhaps represent?

[Eric Wieser]

Can you give a #mwe?

[Jannis Limperg]

Don't use mutual inductives in Lean. They work only very superficially; the problems you're seeing are only the tip of the iceberg. For instance, termination checking with mutual inductives is unreliable as far as I recall and Lean doesn't generate good induction principles for them.

(For what it's worth, I'm not sold on the utility of mutual inductives even in languages where they work, like Agda. In my experience, if you mutualise a central inductive type, you also have to mutualise basically every definition, which gets old quickly.)

[Alcides Fonseca]

What is the alternative? I have the same issue as Brian.

[Jannis Limperg]

Ideally, I think, reformulate your syntax so that it isn't mutually inductive any more. This may come at the cost of additional boilerplate, e.g. duplicated constructors, but I find that less painful.

If there is no acceptable formulation without mutual inductives, I guess you'll have to bite the bullet. I would then try to prove a custom induction principle and define any functions/proofs in terms of that. You might want to do the translation into a non-mutual inductive type yourself rather than letting Lean do it, since then you can at least see clearly what's going on. But I don't have experience with this in Lean, so take my opinions with a big grain of salt.