The Coq mailing list

[David Monniaux <David.Monniaux AT imag.fr>]

It is well-known that a function nat -> X can be also seen as an
infinite sequence, that is, the element of a coinductive type

Variable X : Type.
CoInductive infinite_seq :=
  | Step : X -> infinite_seq -> infinite_seq.

The idea is as follows: since nat ~ (unit + nat), then (nat -> X) ~ (X *
(nat -> X)).
Now if we model nat -> X by infinite_seq X, this yields
(infinite_seq X) ~ X * infinite_seq

Let us now try to generalize this to binary constructors, like with a
datatype Bin with A as leaf and C as binary constructor.
Bin ~ (unit + Bin*Bin), then (Bin -> X) ~ (unit * ((Bin*Bin)->X)) ~
(unit * (Bin->(Bin->X))) by currying.

This yields
(foo X) ~ X * (foo (foo X))

Thus the declaration:

CoInductive foo (X : Type) :=
  | Moo : X -> (foo (foo X)) -> foo X.

But then I get:

Error: Non strictly positive occurrence of "foo" in
 "X -> foo (foo X) -> foo X".

Isn't this check a bit too strict? My remembrances on the positivity
check in (co)inductive datatypes is hazy, but I don't see how this
construction could create inconsistencies.


-- David Monniaux Directeur de recherche au CNRS, laboratoire VERIMAG
http://www-verimag.imag.fr/~monniaux/