Coq on Coq, type mismatch

Question

전 (coinductive) 유형을 시험해 보았고 자연수와 벡터 (유형에서 크기가 같은 목록)의 동시 유도 버전을 정의하기로 결정했습니다. 나는 그들과 같은 그래서 무한한 수의 정의 :

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. 

을