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.

输出：

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

我不确定这是什么意思 - map 和 interleave 都是简单的核心递归函数，构建余归类型的值。有什么问题？

Answer 1

问题是因为=符号代表eq，它是一种归纳类型，不是一种归纳类型。

相反，您可以证明流 map f (interleave (s1, s2)) 和 interleave (map f s1, map f s2) 在外延上是相等的。这是 Coq 参考手册的摘录 (§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.

将eq改成EqSt后可以证明引理：

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.

顺便说一下，在 this CPDT 章节中可以找到许多处理余归数据类型的技巧。

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

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

coq

coq-tactic

coinduction