The Coq mailing list

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

Hi Agnishom,

> but that does not seem to work. The definition intuitively seems to make
> sense. Also, if we unroll the definition of MonJustBefore, it appears
> (to me) that the recursive call is guarded within the mNext constructor
> in MonDelayWith. How do I make Coq believe this?

mNext is not a constructor, it's a projection (a destructor). That's why 
this definition is not guarded. It is productive, but the guardedness 
checker is too restrictive for one to encode a proof of that fact. You 
have to rewrite the definition altogether to make it guarded.

Your second attempt is basically correct. It's a small mistake: you 
wrote a period after the type instead of ":=". That's why you then enter 
proof mode. That period separates the CoFixpoint command from the 
following record "{| ... |}", which seems to get recognized as a tactic 
that does nothing.

    (* You wrote *)
    CoFixpoint MonSometime {A: Type} (mon: Monitor A) : Monitor A.
    (* but it should be *)
    CoFixpoint MonSometime {A: Type} (mon: Monitor A) : Monitor A :=

Your initial attempt is actually a common example of the limitations of 
the "guardedness" criterion. Other implementations of coinductive types 
based one sized types or clocked type theory make it possible to 
formalize the first definition directly.

Regards,
Li-yao