如何導入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 

當我問勒柯克Print Arith.PeanoNat它輸出：Module Arith := Struct End，它似乎是空的。當我嘗試使用庫中的任何東西時，例如在布爾比較下的le_le，我得到標準Error: leb_le not a defined object.我已經更新了Coq和庫，並且我不知道這裏會發生什麼。我會很感激你在解決這個庫問題上的投入。

Answer 1

當我嘗試Print Arith.PeanoNat時，輸出略有不同：我得到Module PeanoNat := Struct Module Nat End然後即使leb_le不在範圍內，Nat.leb_le是。

（如果相關，我運行8.5beta2）。

Answer 2

如果我沒有弄錯，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不必使用完整的路徑名稱。我希望這可以幫助您調試正在發生的事情。