Ltac呼叫「cofix」失敗。錯誤：所有方法都必須構建coinductive類型

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是直接corecursive功能coinductive類型的建築價值。有什麼問題？

Answer 1

問題從=符號代表eq，它是一個電感型，不一個coinductive一個事實造成的。

相反，您可以顯示流map f (interleave (s1, s2))和interleave (map f s1, map f s2)延伸相等。下面是從勒柯克參考手冊（§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. 

順便說一句，花樣繁多處理coinductive數據類型可以發現在this CPDT章節。