The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Gil,

Just allowing `fix` in `cofix` would be unsound (see 
https://github.com/coq/coq/issues/4261). But maybe fix could be treated 
similarly to cofix for the purposes of guardedness checking, in addition 
to its decreasing argument requirement?

One workaround is to replace the inductive type with a non-recursive 
encoding, list X = { n : nat & fin n -> X }.

Li-yao

On 2023-03-02 2:02 AM, Chung-Kil Hur wrote:
> 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