Coq on Coinduction、タイプミスマッチ

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. 

を