Come importare la libreria: Coq.Arith.PeanoNat in Coq?

Question

È necessario utilizzare la parte della libreria standard denominata Coq.Arith.PeanoNat (https://coq.inria.fr/library/Coq.Arith.PeanoNat.html).

Ho provato a importare l'intera libreria Arith o solo questo modulo, ma non posso usarlo in entrambi i modi.

Ogni altra libreria che ho provato funziona perfettamente. Quando faccio Require Import Bool. compilo e posso usarlo correttamente. Su Print Bool. Posso dare un'occhiata a tutte le funzioni all'interno nel formato seguente:

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

Quando faccio uno Require Import Arith.PeanoNat. o Require Import Arith. ho questa uscita come immediata:

[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 

Quando chiedo Coq Print Arith.PeanoNat emette: Module Arith := Struct End, sembra essere vuoto. Quando provo a utilizzare qualsiasi cosa dalla libreria, ad esempio le_le in confronti booleani, ottengo lo standard Error: leb_le not a defined object. Ho aggiornato Coq e le librerie e non ho idea di cosa potrebbe succedere qui. Apprezzerei il tuo contributo nel risolvere questo problema di libreria.

Answer 1

Quando provo Print Arith.PeanoNat, l'uscita è leggermente diverso: ho Module PeanoNat := Struct Module Nat End e quindi, anche se non è leb_le portata, Nat.leb_le è.

(Corro 8.5beta2 nel caso sia rilevante).

Answer 2

Se non mi sbaglio, Require è la parola chiave per caricare un file. Import ha a che fare con la gestione degli spazi dei nomi. Spesso vengono utilizzati insieme, come in Require Import PeanoNat., ma in realtà stanno facendo due cose diverse.

Quando coq file (DirName/FileName.vo) sono caricati con Require, è come se il contenuto del FileName.vo è avvolto in Module DirName.FileName ... End. Everyting definito nel file viene quindi accede con DirName.FileName.Name.

Il file può avere moduli M all'interno di esso, e raggiungere M 's contenuti, si deve digitare DirName.FileName.ModuleName.Name1 ecc

Import viene utilizzata per ottenere tutte le definizioni fino al livello superiore. Facendo Import DirName.FileName.ModuleName il modulo Name1 viene ora importato al livello più alto e può essere referenziato senza il percorso lungo.

Nell'esempio sopra riportato, il file Arith/PeanoNat.vo definisce il modulo Nat. In realtà, questo è tutto ciò che definisce. Quindi se fai il numero Require Import Arith.PeanoNat ottieni PeanoNat.Nat al livello più alto. E quindi Import PeanoNat.Nat porterà il livello Nat al livello superiore. Notare che non è possibile eseguire Require Import PeanoNat.Nat perché non è il file .vo.

Coq può talvolta trovare un file .vo senza che sia necessario specificare l'intero percorso, quindi è anche possibile eseguire Require Import PeanoNat. e coq troverà il file.Se vi chiedete dove si trovò, fare Locate PeanoNat.

Coq < Require Import PeanoNat. 

Coq < Locate PeanoNat. 
Module Coq.Arith.PeanoNat 

Un altro Nat è disponibile anche da un altro luogo di 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 

Quindi, non lo fai Import una libreria, è Require esso. Si utilizza Import per non dovere utilizzare il nome completo del percorso. Spero che questo ti aiuti a eseguire il debug di ciò che sta accadendo.