type-inference - 为什么我不能定义以下 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

为什么 Coq 不自己推断 A 的类型？如何让它推断出 A 的类型？

Answer 1

您需要将 A 声明为隐含的，以便让 Coq 为您推断它。有几种方法可以做到这一点:

1. 将以下声明添加到您的文件中:Set Implicit Arguments.。这将导致 Coq 为 Cons 的 A 等参数打开自动推断，允许您编写 Cons 0 zeros。

2. 仅为 Cons 打开隐式参数，而不影响文件的其余部分:

   Arguments Cons {A} _ _.
   

   此声明将 A 标记为隐式并将其他两个参数保留为显式。

3. 在 stream 的定义中将 A 标记为隐式:

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

   不过，我个人不建议这样做，因为它也会将 A 标记为 stream 的隐式。

您可以在 reference manual 中找到有关隐式参数的更多信息