The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Thank you, Li-Yao!

The second case was a small typo indeed.

In the first case, you correctly pointed out that mNext is not a constructor but a projection. However, is there a way to rewrite the definition of MonDelayWith with the constructor Build_Monitor (which was automatically generated) and let cofix so that MonDelayWith is guarded and my attempted definition of MonJustBefore works?

I had never heard of one sized types or clocked type theory. Thanks for the pointers!

--Agnishom

On Sat, Feb 8, 2020 at 10:59 AM Li-yao Xia <lysxia AT gmail.com> wrote:

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