The Coq mailing list

[Milad Niqui <milad AT cs.kun.nl>]

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.
Moreover, the definition of omega seems to be guarded (the recursive 
occurence of omega in second branch is guarded by constructor c0 and by 
nothing else);
and the error I get does not complain about unguardedness, rather about 
the position of the recursive call.
I know that allowing recursion on impredicative polymorphic types leads 
to terms that are structurally smaller than themselves, and this is bad 
for well-foundedness. But what is the problem in the case of coinductive 
types? Here we don't need the computation tree to be well-founded and 
guardedness can be checked syntacticaly, So why doesn't Coq accept this 
term?

Thanks in advance for any remark,

--
Milad Niqui

Computing Science Department,                tel:+31 24 365 2610
University of Nijmegen,                      fax:+31 24 365 2525
P.O.B. 9010,                                 email: 
milad AT cs.kun.nl
6500 GL Nijmegen,                            http://www.cs.kun.nl/~milad
The Netherlands.