The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>]

Milad Niqui 
<milad AT cs.kun.nl>
 wrote:
> Dear All,
> 
>   I am trying to define a cofixpoint on an impredicative type.
> 
> ---------------------------------------------------------------------------
> CoInductive T :Set :=  c0 : (A:Set)A->T.
> 
> 
> Definition Zero_T := (c0 nat O).
> 
> 
> CoFixpoint omega:T ->T:= [t:T]Cases t of
>                                (c0 A x) => (c0 T (omega Zero_T))
>                            end.
> 
> (*
> Error: Recursive definition of G is ill-formed.
> In environment
> G :
> T ->T
> Not allowed recursive call in a non-recursive argument of constructor
> *)
> 
> ----------------------------------------------------------------------------
> 
> Intuitively the definition of omega is productive, it just generates the 
> infinite application of constructor c0.

Hi Milad,

I am not an expert of coinductive types, but it seems to me that the
coinductive type you defined is not recursive, i.e. c0 does not take a
term of type T as an argument. The fact that the parameter A could be T
itself is (probably) not captured by the type system.


Are you sure that the type you meant was not the following:

CoInductive T [A:Set] :Set := c0 : (T A)->(T A).

In this case you can define:

CoFixpoint omega:(T nat) ->(T nat) := 
 [t:(T nat)]Cases t of
   (c0 x) => (c0 nat (omega t))
 end.


Cheers,

Pierre