I hope I didn't ask this question before, does mutual induction as language feature offer any logical power over nested induction ? or is it just for convenience ?

IIRC, mutual induction can be translated into indexed induction. For example, mutually defined `Even`

and `Odd`

can be translated to `Parity : nat -> bool -> Prop`

. I guess this indexed induction is not too far from nested (but otherwise unindexed) induction.

under the right conditions indexed can also be translated to non indexed with an identity type.

nested induction however is probably strictly stronger, but i dont remember where in the literature it is claimed. @Pierre-Marie Pédrot might be able to say more.

Ali Caglayan said:

under the right conditions indexed can also be translated to non indexed with an identity type.

"under the right conditions" = the type is non recursive OR you accept using non recursively uniform parameters in the translation result

Of course this leaves you needing the identity type to bootstrap

BTW do you all mean "nested/mutual inductives" or do you really refer to induction, and if the later is that different from recursion?

nested inductives can be translated to mutual AFAIK, eg `Inductive rose := Rose (_ : list rose)`

becomes `Inductive rose := Rose (_ : list_rose) with list_rose := nil | cons (_:rose) (_:list_rose)`

However translating mutual to single is unclear or maybe impossible when they live in different universes. OTOH I don't know any interesting examples of mutual inductives in different universes.

Last updated: Nov 29 2023 at 21:01 UTC