爲什麼我無法定義以下CoFixpoint？

Question

我使用：

$ coqtop -v 
The Coq Proof Assistant, version 8.4pl5 (February 2015) 
compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1 

予定義的下列CoInductive類型，stream：

$ coqtop 
Welcome to Coq 8.4pl5 (February 2015) 

Coq < CoInductive stream (A : Type) : Type := 
Coq < | Cons : A -> stream A -> stream A. 
stream is defined 

Coq < Check stream. 
stream 
    : Type -> Type 

Coq < Check Cons. 
Cons 
    : forall A : Type, A -> stream A -> stream A 

然後，我試圖定義以下CoFixpoint定義，zeros：

Coq < CoFixpoint zeros : stream nat := Cons 0 zeros. 

然而，我得到了以下錯誤：

Toplevel input, characters 38-39: 
> CoFixpoint zeros : stream nat := Cons 0 zeros. 
>          ^
Error: In environment 
zeros : stream nat 
The term "0" has type "nat" while it is expected to have type 
"Type". 

我想通了，我必須顯式實例變量A：

Coq < CoFixpoint zeros : stream nat := Cons nat 0 zeros. 
zeros is corecursively defined 

爲什麼不勒柯克本身推斷A類型？我如何使其推斷A的類型？

Answer 1

您需要聲明A隱含的要求Coq爲您推斷它。有幾種方法：

1. 將以下聲明添加到您的文件中：Set Implicit Arguments.。這會導致Coq打開A等參數的自動推斷Cons，允許您編寫Cons 0 zeros。

2. 打開只是Cons隱含參數，不影響文件的其餘部分：

   Arguments Cons {A} _ _. 
   

   此聲明標記A爲隱式並保持其他兩個參數爲明確。

3. 馬克A在stream定義爲隱：

   CoInductive stream {A : Type} : Type := 
   | Cons : A -> stream A -> stream A. 
   

   我個人不推薦的，這樣做，因爲這將標誌着A作爲隱含的stream爲好。

您可以找到有關在reference manual