Stream: Coq users

Topic: Mutual coinduction


view this post on Zulip maxv (Jul 19 2023 at 08:08):

It appears that when types are mutually corecursive, the syntactic well-foundedness check is overly strict. For example, Coq rejects the following piece of code:

CoInductive Stream (A : Type) : Type :=
  | Cons (a : A) (t : Stream A) : Stream A.
CoInductive InfinitaryTree : Type :=
  | Head (st : Stream InfinitaryTree) : InfinitaryTree.

CoFixpoint a : Stream InfinitaryTree :=
  Cons _ (Head a) a.

saying

Recursive call on a non-recursive argument of constructor
"Head a".

I would expect this to be fine, because both corecursive calls are guarded by coinductive constructors. For induction, I know that Program Fixpoint allows you to do "semantic" termination checking in favor of syntactic termination checking. Is there anything equivalent for cofixpoints? Or, how would you deal with this issue?

view this post on Zulip Kenji Maillard (Jul 19 2023 at 12:21):

The corecursive call to a in Head a is not considered guarded because Cons is not co-recursive in its first argument.
You can make the corecursivity of InfinitaryTree explicit in that case and get a syntactically guarded definition:

CoFixpoint a := Cons _ (cofix b := Head (cofix str := Cons _ b str)) a.

Last updated: Jun 22 2024 at 16:02 UTC