coq - Ltac 调用 "cofix"失败。错误 : 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 章节。