The Coq mailing list

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

I have the following definitions:

CoInductive Monitor (A: Type) : Type := {
  mNext: A -> bool * (Monitor A);
}.

CoFixpoint MonOr {A: Type} (mon1 mon2: Monitor A) : Monitor A :=
  {|
    mNext (a : A) :=
      let (b1, mon1) := (mNext mon1 a) in
      let (b2, mon2) := (mNext mon2 a)
      in (b1 || b2, MonOr mon1 mon2)
  |}.

CoFixpoint MonDelayWith {A: Type} (init : bool) (mon : Monitor A) : Monitor A :=
  {|
    mNext (a : A) :=
      let (b1, mon1) := (mNext mon a) in
      (init,  MonDelayWith b1 mon1)
  |}.

Definition MonJustBefore {A: Type} : Monitor A -> Monitor A :=
  MonDelayWith false.

Now, I want to define:

CoFixpoint MonSometime {A: Type} (mon : Monitor A) : Monitor A :=
  MonOr mon (MonJustBefore (MonSometime mon)).

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?

Another way to define the same thing would be:

CoFixpoint MonTrue (A: Type) : Monitor A := {|
  mNext (a: A) := (true, MonTrue A)
|}.

CoFixpoint MonSometime {A: Type} (mon: Monitor A) : Monitor A.
{|
  mNext (a : A) :=
    let (b1, mon') := (mNext mon a) in
    if b1 then (true, MonTrue) else (false, MonSometime mon')
|}.

But for some reason, this generates some proof obligation. Why is that?

And I cannot seem to be able to discharge it:

CoFixpoint MonAlways {A: Type} (mon: Monitor A) : Monitor A.
{|
  mNext (a : A) :=
    let (b1, mon') := (mNext mon a) in
    if (~b1) then (false, MonFalse) else (true, MonAlways mon')
|}. exact mon. Defined.

Any suggestions about the above would be appreciated.

--Agnishom