使用"Arguments"命令时Coq"Error:No focused proof"

Question

我正在阅读软件基础书.在关于多态的章节中,有一节关于"隐式参数".在本节中,有一行:

Arguments nil {X}.

当我尝试在Poly.v文件上运行Coq (该章节的源代码,在此tarball中可用)时,它停在上面的行,给我错误:

Error: No focused proof (No proof-editing in progress).

我已将Poly.v文件缩减为这些内容,这仍然会给出相同的错误:

Inductive list (X:Type) : Type :=
  | nil : list X.

Arguments nil {X}.

我在Coq参考手册中找到的关于此错误的唯一内容是

当人们试图在校对编辑模式之外使用校对编辑命令时,Coq会引发错误消息:没有聚焦证据.

我认为"证明编辑模式"是指使用策略证明定理的上下文.我不认为它是在那种模式,也不是Coq,因为它说"没有正在进行的校对编辑".这是有道理的.

该错误声称这Arguments是一个"证明编辑命令",虽然它没有在其文档中说明,并且在证明处理章节中Arguments没有提到.

这让我觉得Coq错误地将其Arguments视为校对编辑命令,但我不知道为什么.

我认为这对我的设置而不是Poly.v文件本身来说是错误的,因为它是Software Foundations一书的一部分.我正在使用CoqIDE,作为Coq 8.3pl4的一部分,与Ubuntu 12.04一起发布.

Answer 1

这是您正在使用的coq版本的问题.当前版本的Software Foundations仅与coq 8.4兼容.如果您想在不升级coq的情况下继续,相关命令的旧版本是:

Implicit Arguments nil [[X]].

您可以在此处找到与您的coq版本兼容的poly.v的完整副本:

玩得开心!