共同感应，类型不匹配

2017-10-13 107 views 2 likes

我一直在尝试共同诱导类型，并决定定义自然数和向量的共同诱导版本（与他们的大小类型列表）。我确定他们和无限多的像这样：共同感应，类型不匹配

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。我怎样才能让编译器理解这些表达式是一样的？

来源

2017-10-13 Gabriel Barreto

回答

解决此问题的标准方法在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.

来源

2017-10-14 07:20:52

共同感应，类型不匹配

回答

相关问题