Need help to define CoFixpoint

Using Coq
1

We have a cofixpoint mplus and going to define cofixpoint bind which just calls mplus in one of the match cases. But Coq complains that definition of bind is ill-formed.

We tried:

  1. To look cofixpoint analogue of fixpoint’s struct trik but no luck
  2. To inline mplus into bind but it introduce other nested recursive calls, and a new definition is still ill-formed.
  3. to look at paco tutorial but we still are not sure that it is a right way to go (and it looks complicated :slight_smile: )
  CoInductive stream (A: Type): Type :=
  | Cons : A -> stream A -> stream A
  | Delay : stream A -> stream A
  | Nil : stream A.

  Definition from_fun z := Delay z.

  Definition force_lazy {A: Type} (s: stream A) :=
    match s with
    | Nil _ => Nil _
    | Delay _ s => Delay _ s
    | Cons _ h tl => Cons _ h tl
    end.

  Definition force {A: Type} (x: stream A) :=
    match x with
    | Delay _ zz => force_lazy zz
    | xs => xs end.

  (* append two streams with interleaving *)
  CoFixpoint mplus {A: Type} (xs ys: stream A) :=
    match xs with
    | Nil _ => force ys
    | Cons _ x xs => Cons _ x (from_fun A (mplus (force ys) xs))
    | Delay _ _ => from_fun _ (mplus (force ys) xs)
    end.

  CoFixpoint bind {A: Type} (s: stream A) (f: A -> stream A) : stream A :=
    match s with
    | Nil _ => Nil _
    | Cons _ x tl =>
        mplus (force_lazy (f x))
          (from_fun _ (bind (force tl) f))
    | Delay _ zz => from_fun _ (bind (force_lazy zz) f)
    end.
2

Have you tried using TLC’s fixed point combinator? (requires classical logic)

See e.g., the “filter on stream” example.
Documentation in my ITP’10 paper: http://www.chargueraud.org/research/2010/fix/fix.pdf
Don’t hesitate to ask if you need further help.