Coinduction на Coq, несоответствие типов

Question

Я пробовал коиндуктивные типы и решил определить коиндуктивные версии натуральных чисел и векторов (списки с их размером в типе). Я определил их и бесконечное число так:

CoInductive conat : Set :=
| cozero : conat
| cosuc : conat -> conat.

CoInductive covec (A : Set) : conat -> Set :=
| conil : covec A cozero
| cocons : forall (n : conat), A -> covec A n -> covec A (cosuc n).           

CoFixpoint infnum : conat := cosuc infnum.

Все это работало, за исключением определения, которое я дал для бесконечного ковектора

CoFixpoint ones : covec nat infnum := cocons 1 ones.

который дал следующее несоответствие типов

Error:
In environment
ones : covec nat infnum
The term "cocons 1 ones" has type "covec nat (cosuc infnum)" while it is expected to have type
 "covec nat infnum".

Я думал, что компилятор примет это определение, поскольку по определению infnum = cosuc infnum. Как я могу заставить компилятор понять, что эти выражения одинаковы?

Answer 1

Стандартный способ решения этой проблемы описан в CPDT Адама Члипалы (см. Главу " Коиндукция").

Definition frob (c : conat) :=
  match c with
  | cozero => cozero
  | cosuc c' => cosuc c'
  end.

Lemma frob_eq (c : conat) : c = frob c.
Proof. now destruct c. Qed.

Вы можете использовать приведенные выше определения следующим образом:

CoFixpoint ones : covec nat infnum.
Proof. rewrite frob_eq; exact (cocons 1 ones). Defined.

или, возможно, немного более читабельным образом:

Require Import Coq.Program.Tactics.

Program CoFixpoint ones : covec nat infnum := cocons 1 ones.
Next Obligation. now rewrite frob_eq. Qed.