共同感應，類型不匹配

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. 

它的所有工作，除了我給了一個無限covector

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

解決此問題的標準方法在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.