The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Hi Coq-Club,

I just realized that Coq's guardedness checking basically rejects *every* corecursive function for mixed inductive coinductive types.

I wonder whether there is a way around, or why Coq does not support it.

To be more specific, here is an example.

==================

Variant rtreeF X :=
| node (n: nat) (chl: list X).

CoInductive rtree : Type := rtgo
{ rtobs : rtreeF rtree }.

CoFixpoint rtfix {X} (coalg: X -> rtreeF X) (x: X) : rtree :=
  match coalg x with
  | node n chl => rtgo (node n
    ((fix itr xs := match xs with
                   | nil => nil
                   | cons x xs' => cons (rtfix coalg x) (itr xs')
                   end) chl))
  end.

========================

The function `rtfix` defines the unique function from X to rtree, given a coalgebra from X to streamF X.

I think this corecursive function must be accepted in order to use the mixed inductive-coinductive type `rtree`.

However, it seems that there is no way to accept the above `rtfix` function.

Thanks!

Gil