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

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在 bool 比较下，我得到标准 Error: leb_le not a defined object.我已经更新了 Coq 和库，但我不知道这里会发生什么。感谢您在解决此库问题方面的意见。

Answer 1

如果我没记错的话，Require是加载文件的关键字。 Import与管理 namespace 有关。它们经常一起使用，如 Require Import PeanoNat. ，但他们确实在做两件不同的事情。

当使用 DirName/FileName.vo 加载 coq 文件 ( Require ) ，就好像FileName.vo的内容包裹在 Module DirName.FileName 中... End.然后使用 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不必使用完整路径名。我希望这可以帮助您调试正在发生的事情。