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:

4. 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: Oct 08 2024 at 15:02 UTC