Ltac call to "cofix" failed. Error: All methods must construct elements in coinductive types

Question

Require Import Streams.

CoFixpoint map {X Y : Type} (f : X -> Y) (s : Stream X) : Stream Y :=
  Cons (f (hd s)) (map f (tl s)).

CoFixpoint interleave {X : Type} (s : Stream X * Stream X) : Stream X := Cons (hd (fst s)) (Cons (hd (snd s)) (interleave (tl (fst s), tl (snd s)))).

Lemma map_interleave : forall {X Y : Type} (f : X -> Y) (s1 s2 : Stream X), map f (interleave (s1, s2)) = interleave (map f s1, map f s2).
Proof.
  Fail cofix. (* error *)
Abort.

Output:

Ltac call to "cofix" failed.
Error: All methods must construct elements in coinductive types.

I'm not sure what this means - both map and interleave are straightforward corecursive functions building values of coinductive types. What's the problem?

Answer 1

The problem stems from the fact that = notation stands for eq, which is an inductive type, not a coinductive one.

Instead, you can show that the streams map f (interleave (s1, s2)) and interleave (map f s1, map f s2) are extensionally equal. Here is an excerpt from the Coq reference manual (§1.3.3)

In order to prove the extensionally equality of two streams s1 and s2 we have to construct an infinite proof of equality, that is, an infinite object of type EqSt s1 s2.

After changing eq to EqSt we can prove the lemma:

Lemma map_interleave : forall {X Y : Type} (f : X -> Y) (s1 s2 : Stream X),
  EqSt (map f (interleave (s1, s2))) (interleave (map f s1, map f s2)).
Proof.
  cofix.
  intros X Y f s1 s2.
  do 2 (apply eqst; [reflexivity |]).
  case s1 as [h1 s1], s2 as [h2 s2].
  change (tl (tl (map f (interleave (Cons h1 s1, Cons h2 s2))))) with
         (map f (interleave (s1, s2))).
  change (tl (tl (interleave (map f (Cons h1 s1), map f (Cons h2 s2))))) with
         (interleave (map f s1, map f s2)).
  apply map_interleave.
Qed.

By the way, many tricks dealing with coinductive datatypes can be found in this CPDT chapter.