## Stream: Coq devs & plugin devs

### Topic: Overlap of recursive presentations of mutual inductive types

#### Hugo Herbelin (Aug 30 2023 at 18:25):

I fell on a amusing phenomenon about representing mutual inductive types as, say:

``````Inductive I := C : F J -> I with J := D : G I -> J.
``````

where `F` and `G` are strictly positive functors.

Such types can also be defined by:

``````Inductive I' A := C : F A -> I' A. Inductive J := D : G (I' J) -> J. Definition I := I' J.
``````

or,. symmetrically, with:

``````Inductive J' B := D : G B -> J' B. Inductive I := C : F (J I) -> I. Definition J := J' I.
``````

Abstractly, this can be represented respectively by:

1. (I,J) := μ(X,Y).(F Y, G X)
2. I' A := μX.F(A); J := μY.G(μX.F(Y)); I := μX.F(μY.G(μX.F(Y)))
3. J' B := μY.G(B); I := μX.F(μY.G(X)); J := μY.G(μX.F(μY.G(X)))

Then, the Coq module `rtree.ml` is supposed to be able to compare such recursive expressions by expanding the loops whenever needed and it works well.

However, while working with #17950, trying to recompute the recursive structure of nested/mutual types from scratch, I fell on an extra representation which is:

1. I := μX.F(μY.G(X)); J := μY.G(μX.F(Y))

And then, in the detours of the check of guards for fixpoints on both `I` and `J`, I realized that `rtree.ml` is not any more able to show that expressions such as:

• I := μX.F(μY.G(X))
• and μX.F(μY.G(μX'.F(Y)))

are equivalent...

I believe that equivalence of such recursive trees is completely standard (??) (for instance, this seems related to Fischer-Ladner trees) but I was surprised that we never fell on the problem before.

Should I try to avoid the representation 4. and use 1. instead? Or should I try to improve `rtree.ml` so that it knows how to deal with 4.?

(*) as found in the `mind_recargs` field of the implemetation of coq

#### Hugo Herbelin (Aug 30 2023 at 18:30):

By the way, the mutual cofixpoint example of Burak Ekici on coq-club yesterday works out of the box when we recompute the inductive structure of the types involved. (More precisely, I have two implementations: it works with the implementation based on parametric recursive structure but not with the implementation recomputing the whole inductive structure from scratch, precisely because of the rtree limitation above.)

#### Hugo Herbelin (Oct 25 2023 at 12:36):

I believe that equivalence of such recursive trees is completely standard

FTR, I learnt (from Alexis S.) that the equivalence between the 3 representations is actually Bekić theorem.

Last updated: Dec 05 2023 at 12:01 UTC