如何导入库:Coq.Arith.PeanoNat在Coq中？

Question

我需要使用名为Coq.Arith.PeanoNat(https://coq.inria.fr/library/Coq.Arith.PeanoNat.html)的标准库部分.

我已经尝试导入整个Arith库或只是导入这个模块,但我不能以任何方式使用它.

我试过的其他每个图书馆工作得很好.我什么时候Require Import Bool.编译,我可以正确使用它.当Print Bool.我可以看看所有在接下来的格式里面的功能:

Module
Bool
:= Struct
Definition...
.
.
.
End

当我做任何一个Require Import Arith.PeanoNat.或Require Import Arith.我得到这个立即输出:

[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
<W> Grammar extension: in [tactic:simple_tactic], some rule has been     masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked

当我问Coq Print Arith.PeanoNat它输出:时Module Arith := Struct End,它似乎是空的.当我尝试使用库中的任何东西时,例如le_le在布尔比较下,我得到标准Error: leb_le not a defined object.我更新了Coq和库,我不知道这里可能会发生什么.我很感激您在修复此库问题方面的意见.

Answer 1

如果我没有弄错,Require是加载文件的关键字. Import与管理名称空间有关.通常他们一起使用Require Import PeanoNat.,但他们真的做了两件事.

当COQ文件(DirName/FileName.vo)被加载Require,这是因为如果内容FileName.vo被包裹在Module DirName.FileName... End.在文件中定义Everyting与随后访问DirName.FileName.Name.

文件本身可以有模块M,要获取M内容,必须输入DirName.FileName.ModuleName.Name1等.

Import用于将所有定义提升到最高级别.通过执行Import DirName.FileName.ModuleName该模块Name1现在可以导入到顶层,并且可以在没有长路径的情况下进行引用.

在上面的示例中,该文件Arith/PeanoNat.vo定义了模块Nat.实际上,这就是它所定义的全部内容.所以,如果你这样做, Require Import Arith.PeanoNat你就PeanoNat.Nat达到顶级水平.然后Import PeanoNat.Nat将带到Nat顶级.请注意,您不能这样做,Require Import PeanoNat.Nat因为它不是.vo文件.

Coq有时可以找到一个.vo文件,而不必指定整个路径,所以你也可以这样做Require Import PeanoNat.,coq会找到该文件.如果你想知道它在哪里找到它,那就做吧Locate PeanoNat.

Coq < Require Import PeanoNat.

Coq < Locate PeanoNat.
Module Coq.Arith.PeanoNat

另一个Nat也可以从另一个地方获得PeanoNat.

Coq < Require Import Nat.
Warning: Notation _ + _ was already used in scope nat_scope
Warning: Notation _ * _ was already used in scope nat_scope
Warning: Notation _ - _ was already used in scope nat_scope

Coq < Locate Nat.
Module Coq.Init.Nat

所以,你不是Import一个图书馆Require.您使用Import不必使用完整路径名.我希望这可以帮助您调试正在发生的事情.

Answer 2

当我尝试时Print Arith.PeanoNat，输出略有不同：我得到Module PeanoNat := Struct Module Nat End，然后即使leb_le不在范围内，Nat.leb_le也是。

8.5beta2（如果相关的话我会跑）。