Is mutual inductive type definition essential in coq core language?

Question

I'm studying Coq's core language and I found that mutual inductive type definition is in it. https://coq.inria.fr/refman/language/core/inductive.html#theory-of-inductive-definitions

Before I read the material, I had supposed that Coq translates mutual definitions in Gallina into nonmutual ones in its core language, since it allows the core language to be smaller. But it wasn't and then I started to wonder why.

For instance, even and odd can be defined mutually as follows.

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
| odd_S : forall n, even n -> odd (S n).

However, one can write another definition without with keyword.

Inductive even_or_odd: (is_even: bool) -> nat -> Prop :=
    | even_O : even true 0
    | even_S : forall n, even false n -> even true (S n)
    | odd_S : forall n, even true n -> even false (S n).

Definition even := even_or_odd true.
Definition odd := even_or_odd false.

I agree that the former looks better than the latter. However, What I wonder is if it is always possible to rewrite any mutually defined inductive type in a nonmutual way. If then, Coq does not necessarily include the mutual definition syntax in its core language.

Does the mutual definition allow more expressions to be defined? Is there any mutually defined type that can't be translated to a nonmutual one?

Or there isn't, but my concern about minimal core language is not a big deal?

Also, I am so sure that mutual fixpoints always can be translated to nonmutual ones. It looks much more clear to me compared to the case of inductive definition. Am I right?

Answer 1

It is always possible, as you noted, to translate a mutual inductive family into a non-mutual family, in much the same way as you described.

A couple of difficulties though:

1. If your mutual inductives are not parametrized, say you have

Inductive Foo := foo : Bar -> Foo
with Bar := bar : Foo -> Bar

(with some constants if you want to make the types non-empty)

Then you have 2 non-dependent types, for which induction, recursion and pattern matching are rather straightforward. But the translation you suggest involve creating a FooBar : bool -> Type which now needs dependent pattern matching everywhere. It's not impossible to cope with this as well, but it makes the elaborator quite a bit more involved.

2. Even worse are mutual inductives with different parameters: Imagine now

Inductive Foo : nat -> Type := ...
with Bar : bool -> Type := ...

Now we need to define a type FooBar : forall b : bool, I b -> Type where I true = nat and I false = nat. I'll let you imagine the case of multiple, possibly dependent parameters.

All these complications add up to a system that is quite complicated: I think it's a reasonable decision to add special support in the core to handle mutually inductive families, and it's the decision the Coq developers have made.

The Lean developers originally made a different decision, see here for instance.

However my understanding is that the complexities outlined above, along with the difficulty of hiding all this to the user, has made them re-think their position (I believe, but at the moment I can't find the reference of how things are in Lean 4).