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:

- (I,J) := μ(X,Y).(F Y, G X)
- I' A := μX.F(A); J := μY.G(μX.F(Y)); I := μX.F(μY.G(μX.F(Y)))
- 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:

- 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

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.)

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: Jun 13 2024 at 04:03 UTC