Induction over mutually inductive predicates

Stream: lean4

[Jannis Limperg]

A student of mine is currently struggling with induction over mutually inductive predicates (in Prop) because

• induction doesn't support mutual inductive types;
• mutual recursion is implemented via well-founded recursion, but inductive predicates don't have (and can't have) a useful SizeOf instance.

As far as I can tell, he has the following options, none of which are particularly pleasing:

• Recurse over the data rather than the predicates.
• Put the predicates into Type.
• Use the recursor directly.
• Give up on mutual types and define the union of the predicates as a single inductive predicate, essentially doing the elaborator's job by hand.

Is there a more idiomatic way?

[Mario Carneiro]

Nope, this is currently not really supported. The best option for now is just using the recursor directly

[Mario Carneiro]

Probably using an inductive family is the path of least resistance

[Jannis Limperg]

Okay, thanks!