L'appel Ltac à "cofix" a échoué. Erreur: Toutes les méthodes doivent construire des éléments dans les types 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. 

Sortie:

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

Je ne sais pas ce que cela signifie - à la fois map et interleave sont des valeurs de construction simples fonctions corecursive de types CoInductive. Quel est le problème?

Answer 1

Le problème provient du fait que = notation signifie eq, qui est un type inductif, pas un CoInductive. Au lieu de cela, vous pouvez montrer que les flux map f (interleave (s1, s2)) et interleave (map f s1, map f s2) sont égaux en extension. Voici un extrait du manuel de référence 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 .

Après avoir changé eq-EqSt nous pouvons prouver le lemme:

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. 

Par ailleurs, de nombreuses astuces traitant de types de données CoInductive peuvent être trouvés au this chapitre CPDT.