The Coq mailing list

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

Hi Li-yao,

Thanks for pointing out the github issue.

Although using a container type is a sensible workaround, it might be better to directly support inductive coinductive types.

After reading the github issue, I thought about a simple improvement to just accept the lifting of a coalgebra f: X -> F X to the corecursive map !f : X -> nu F.

Once the lifting is accepted, in principle one can define any desired corecursive function by lifting an appropriate coalgebra, and then prove that the lifted function satisfies the desired recursive equation (eg, using paco and the axiom saying that bisimulation implies equality).

Now, the simple idea is to make the guardedness checking allow a fixpoint under a (guarding) constructor if the definition of fixpoint does not include any destructor.

It seems that this simple relaxation is sound and also allows the desired lifting of a coalgebra.

For example, in my example of rosetree below, the fixpoint function under the guarding constructor "rtgo" does not include any destructor "rtobs" and thus the lifting function "rtfix" would be accepted.

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

Set Implicit Arguments.

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.

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

I wonder whether this simple improvement has any problem.

Thanks,

Gil

On Thu, Mar 2, 2023 at 9:30 PM Li-yao Xia <lysxia AT gmail.com> wrote:

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