ライブラリをインポートする方法：Coq.Arith.PeanoNat in 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 

をPrint Arith.PeanoNat出力：Module Arith := Struct End、それは空のようです。ライブラリから何かを使用しようとすると、たとえばboolean比較の下でle_leという標準が得られます。Error: leb_le not a defined object.私はCoqとライブラリを更新しましたが、ここで何が起こっているのか分かりません。このライブラリの問題を修正していただきありがとうございます。

Answer 1

私がPrint Arith.PeanoNatを試してみると、出力はわずかに異なります：を取得し、leb_leが有効範囲にない場合でもNat.leb_leです。

（該当する場合は8.5beta2）

Answer 2

私が間違っていない場合、Requireはファイルをロードするキーワードです。 Importは名前空間の管理と関係があります。彼らはしばしばRequire Import PeanoNat.のように一緒に使用されますが、実際には2つの異なることをしています。

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をトップレベルに持ち込みます。 .voファイルではないため、Require Import PeanoNat.Natは実行できません。

Coqはパス全体を指定することなく.voファイルを見つけることがあるため、Require Import PeanoNat.も指定でき、coqがファイルを検索します。それはそれを見つけた場所を疑問に思う場合は、Locate PeanoNat.

Coq < Require Import PeanoNat. 

Coq < Locate PeanoNat. 
Module Coq.Arith.PeanoNat 

を行う別のNatあなたRequireは、だから、あなたがいないImportライブラリを行う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を使用します。これが起こっていることをデバッグするのに役立ちます