Ltac вызов "Cofix" не удалось. Ошибка: все методы должны конструировать элементы в коиндуктивных типах

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 функциями построения значений коиндуктивных типов. В чем проблема?

Answer 1

Проблема связана с тем, что = обозначение расшифровывается как eq, который является индуктивным типом, а не коиндуктивным.

Вместо этого вы можете показать, что потоки map f (interleave (s1, s2)) а также interleave (map f s1, map f s2) экстенсивно равны. Вот выдержка из справочного руководства Coq ( §1.3.3)

Чтобы доказать экстенсивно равенство двух потоков s1 а также s2 мы должны построить бесконечное доказательство равенства, то есть бесконечный объект типа 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.

Между прочим, в этой главе CPDT можно найти много приемов, касающихся коиндуктивных типов данных.