Coq 上的共归纳，类型不匹配答案

【问题标题】：Coinduction on Coq, type mismatchCoq 上的共归纳，类型不匹配
【发布时间】：2018-03-26 03:24:30
【问题描述】：

我一直在尝试协导类型，并决定定义自然数和向量的协导版本（列表及其类型中的大小）。我将它们和无限数定义为：

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。如何让编译器理解这些表达式是相同的？

【问题讨论】：

标签： coq proof dependent-type coinduction corecursion

【解决方案1】：

解决此问题的标准方法在 Adam Chlipala 的 CPDT 中有所描述（参见 Coinduction 章节）。

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.

【讨论】：