# Can you always replace mutually recursive references with parameters?

This is a follow up to a question someone else previously posted: Expressivity of mutual/nested inductives vs. regular inductives.

Adopting Agda-ish notation, the basic strategy is to turn your bunch of mutually defined inductive types into a single inductively defined universe, indexed over its collection of sorts...

...

BEFORE

mutual
data Even : Set where
zero : Even
suco : Odd -> Even

data Odd  : Set where
suce : Even -> Odd


AFTER

data Sort : Set where
even odd : Sort

data Stuff : Sort -> Set where
zero : Stuff even
suco : Stuff odd -> Stuff even
suce : Stuff even -> Stuff odd

Even = Stuff even
Odd  = Stuff odd


However, Twitter user @JulesJacobs5 offers a different approach:

In Coq you can sometimes parameterize one inductive with some T, and then use the parameterized one in the definition of the other one ...

For example, using the even-odd example, we could take this mutually-defined example:

Inductive odd : Set := suce (e : even)
with even : Set := zero | suco (o : odd).


...and turn it into this non-mutual version:

Inductive make_odd (even_placeholder : Set) : Set :=
| suce (e : even_placeholder)
.

Inductive even : Set :=
| zero
| suco (o : make_odd even)
.

Definition odd := make_odd even.


My question: Can we take any mutually-defined inductive type, and "de-mutualize" it via this "Replace all mutual references with a parameter" technique?

If not, what is an example where this technique would fail? A concrete code example would be appreciated.

EDIT: I'm not interested in whether such a "de-mutualizing" technique would make proofs more or less tedious. I'm purely interested in whether or not this particular technique can always be applied.

• This produces nested inductives though, which imo is worse than mutual inductives in both theory and application.
– Trebor
Aug 15, 2023 at 10:56
• @Trebor Do you think nested inductives are always worse, or only in certain contexts? I agree that in the above example, the mutual definition is nicer than the nested version. However, compare Ind tree := node : (list tree) -> tree to Mutual[tree,tlist] := node : tlist -> tree | tnil : tlist | tcons : tree -> tlist -> tlist. I'd argue that the first (nested) encoding is better than the second (mutual) encoding, since you can reuse all of list's functions and theorems, without having to reimplement them for tlist. Aug 16, 2023 at 5:25
• It is indeed the first thought that you can reuse functions, but turns out you can't in some of the cases! It poses difficulties for termination checking. Coq already had a rule to deal with this, it works well but doesn't cover more advanced cases. For other theorem proves that doesn't have the rule it's worse.
– Trebor
Aug 16, 2023 at 6:45