The Coq mailing list

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

Hi Colin,

Although a surprising quirk of nested Cofixpoints, this is actually the 
expected behavior.

Quoting CPDT (http://adam.chlipala.net/cpdt/html/Cpdt.Coinductive.html)

> a co-recursive call must be a direct argument to a constructor, 
nested only inside of other constructor calls or fun or match expressions.

To "fun" and "match", add "cofix" (but not "fix"!).

"smap" and "smap2" normalize respectively to terms of the forms:

smap  = (fun A B f => (cofix s := ...))
smap2 = (fun A B => (cofix f s := ...))

Notably, they are not convertible to each other. The arity of each cofix 
is fixed once and for all.

Now unfolding "smap" and "smap2" in the definitions of "incr" and 
"incr2", and beta-reducing...

> CoFixpoint incr (w : wtree) : wtree :=
>    match w with
>    | node n ls => node (S n) (Cons w ((cofix smap_f s := ... incr 
...) ls))
>    end.
>
> (* The following is *rejected* by the guardedness checker, using smap2
> defined with an argument *)
> CoFixpoint incr2 (w : wtree) : wtree :=
>    match w with
>    | node n ls => node (S n) (Cons w ((cofix smap2 f s := ... f ...) 
incr2 ls))
>    end.

Crucially, since "f" is a "fun" parameter of "smap", beta-reduction 
substitutes it with "incr", whereas "f" is a "cofix" parameter of 
"smap2", so "incr2" remains stuck outside.

Now looking at the guardedness condition, "incr" is fine: its recursive 
occurence is nested, successively, in a "match", a "node" (that's at 
least 1 constructor), a "Cons", a "cofix", and another "Cons".

"incr2" however, is nested not *inside* the "cofix", but in one of its 
arguments, which is entirely a different location.

The definition is not guarded according Coq's rules of guardedness.  I 
don't have a formal reference to point to, but at least for "match" and 
"cofix" the right shapes can be illustrated more precisely as follows:

match BAD with
| p => GOOD
end BAD

(cofix f x ... z := GOOD) BAD

There definitely exist alternative guardedness conditions that would 
accept more productive programs, but as those illustrate, the current 
one has the overwhelming advantage of simplicity.

Regards,
Li-yao

On 6/10/19 8:36 PM, Colin Stebbins Gordon wrote:
> I've been working with a structure that is essentially a coinductive data
> type that contains a coinductive collection of itself.  While defining
> cofixpoints on this structure, I kept bumping into a weird behavior where a
> seemingly sensible productive definition would be rejected for my chosen
> coinductive collection, but accepted for the streams in the standard
> library.  Eventually I tracked it down to how the notion of map is
> declared: of two seemingly equivalent ways of defining things, one passes
> the guardedness check, and the other is rejected.
>
> Here's a self-contained definition of (possibly-finite) streams, along with
> two definitions of map:
>
> Set Implicit Arguments.
>
> Section Streams.
> Variable A : Type.
> CoInductive Stream : Type :=
>      Cons : A -> Stream -> Stream
>     | Nil : Stream.
> End Streams.
>
> Section Map.
> Polymorphic Variables A B : Type.
> Polymorphic Variable f : A -> B.
> Polymorphic CoFixpoint smap (s:Stream A) : Stream B :=
>    match s with
>    | Nil _ => Nil _
>    | Cons x xs => Cons (f x) (smap xs)
>    end.
> End Map.
>
> Section Map2.
> Polymorphic Variables A B : Type.
> (*Polymorphic Variable f : A -> B.*)
> (* Notice that now instead of making f a variable, it is not an argument to
> smap(2) *)
> Polymorphic CoFixpoint smap2 (f : A -> B) (s:Stream A) : Stream B :=
>    match s with
>    | Nil _ => Nil _
>    | Cons x xs => Cons (f x) (smap2 f xs)
>    end.
> End Map2.
>
> Unset Implicit Arguments.
>
> The only difference between smap and smap2 is that one is defined with f as
> a section variable, while the other takes it as a parameter.
>
> Now if I define a simplification of what I was working with:
>
> (* A simple coinductive structure with (1) data and (2) a container of
> itself *)
> CoInductive wtree : Set :=
> | node : nat -> Stream wtree -> wtree.
>
> I can try to define two versions of the same cofixpoint, one accepted and
> one rejected:
>
> (* The following is accepted by the guardedness checker, using smap defined
> with a Variable *)
> CoFixpoint incr (w : wtree) : wtree :=
>    match w with
>    | node n ls => node (S n) (Cons w (smap incr ls))
>    end.
>
> (* The following is *rejected* by the guardedness checker, using smap2
> defined with an argument *)
> CoFixpoint incr2 (w : wtree) : wtree :=
>    match w with
>    | node n ls => node (S n) (Cons w (smap2 incr2 ls))
>    end.
>
> The error message I get for incr2 is:
>
> Recursive definition of incr2 is ill-formed.
> In environment
> incr2 : wtree -> wtree
> w : wtree
> n : nat
> ls : Stream wtree
> Unguarded recursive call in
> "cofix smap2 (f : wtree -> wtree) (s : Stream wtree) : Stream wtree :=
>     match s with
>     | Cons x xs => Cons (f x) (smap2 f xs)
>     | Nil _ => Nil wtree
>     end".
> Recursive definition is: "fun w : wtree => match w with
>                                             | node n ls => node (S n) (Cons
> w (smap2 incr2 ls))
>                                             end".
>
> The only difference is the use of the section variable when defining the
> map.  I realize syntactic guardedness checks are brittle by nature, but
> this still surprised me: I would not expect this particular change to
> affect the guardedness check.  Is this by design, a quirk of the current
> implementation (this is 8.9.0), or is there a subtle reason I'm missing
> that one (or both?) should actually be rejected?
>
> Thanks,
> Colin