How to import a library: Coq.Arith.PeanoNat in Coq?

Question

I need to use part of the standard Coq.Arith.PeanoNat library ( https://coq.inria.fr/library/Coq.Arith.PeanoNat.html ).

I tried either to import the whole Arith library, or just this module, but I can not use it anyway.

Every other library I tried works fine. When I do Require Import Bool. I am compiling and I can use it correctly. On the Print Bool. I can take a look at all the functions inside the following format:

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

When I do either Require Import Arith.PeanoNat. or Require Import Arith. I get this as an immediate output:

 [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 

When I ask Coq Print Arith.PeanoNat , it outputs: Module Arith := Struct End , it seems empty. When I try to use something from the library, for example le_le in Boolean comparisons, I get the standard Error: leb_le not a defined object. , I updated Coq and libraries, and I have no idea what could happen here. I would appreciate your input in fixing this library issue.

Answer 1

If I'm not mistaken, Require is the keyword to download the file. Import is associated with namespace management. Often they are used together, as in Require Import PeanoNat. but they really do two different things.

When coq files ( DirName/FileName.vo ) are loaded using Require , it looks like the contents of FileName.vo wrapped in Module DirName.FileName ... End. After that, each access specified in the file is t28>.

The file itself can have M modules inside it, and to access the contents of M you need to enter DirName.FileName.ModuleName.Name1 , etc.

Import used to define all definitions to the top level. By executing Import DirName.FileName.ModuleName , the Import DirName.FileName.ModuleName module Name1 now imported to the top level and can be referenced without a long path.

In the above example, the Arith/PeanoNat.vo defines the Nat module. Actually, that’s all that he defines. So, if you do Require Import Arith.PeanoNat , you get PeanoNat.Nat at the top level. And then Import PeanoNat.Nat will bring Nat to the top level. Please note that you cannot do Require Import PeanoNat.Nat because it is not a .vo file.

Coq can sometimes find a .vo file without having to specify the entire path, so you can also do Require Import PeanoNat. , and coq will find the file. If you're curious where he found it, make a Locate PeanoNat.

 Coq < Require Import PeanoNat. Coq < Locate PeanoNat. Module Coq.Arith.PeanoNat 

Another Nat also available from a place other than 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 

So, you are not an Import library, you are Require it. You use Import to not use the full path name. Hope this helps you debug what's happening.

Answer 2

When I try to Print Arith.PeanoNat , the output is a little different: I get Module PeanoNat := Struct Module Nat End , and then even if leb_le not in scope, Nat.leb_le is.

(I am running 8.5beta2 in case this is relevant).