# Need help to define CoFixpoint

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 )
``````  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.
``````

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.