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.
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:
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:
And then, in the detours of the check of guards for fixpoints on both
J, I realized that
rtree.ml is not any more able to show that expressions such as:
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: Dec 05 2023 at 12:01 UTC