为什么我无法定义以下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