3

我在用:

$ 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

4

1 回答 1

4

您需要声明A为隐式以要求 Coq 为您推断它。有几种方法可以做到:

  1. 将以下声明添加到您的文件中:Set Implicit Arguments.. 这将导致 Coq 为诸如 for 之类的参数打开自动推理ACons从而允许您编写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

您可以在参考手册中找到有关隐式参数的更多信息

于 2015-05-04T16:53:47.250 回答