Jak zaimportować bibliotekę: Coq.Arith.PeanoNat in Coq?

Question

Potrzebuję użyć części standardowej biblioteki o nazwie Coq.Arith.PeanoNat (https://coq.inria.fr/library/Coq.Arith.PeanoNat.html).

Próbowałem importować całą bibliotekę Arith lub tylko ten moduł, ale nie mogę jej użyć w żaden sposób.

Każda inna biblioteka, którą wypróbowałem, działa dobrze. Kiedy robię Require Import Bool., kompiluję i mogę go używać poprawnie. Po Print Bool. mogę przyjrzeć się wszystkimi funkcjami wewnątrz w następnym formacie:

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

Kiedy wykonać jedną Require Import Arith.PeanoNat. lub Require Import Arith. otrzymuję ten jako natychmiastowe wyjście:

[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 

Kiedy pytam Coq Print Arith.PeanoNat wyprowadza: Module Arith := Struct End, wydaje się pusty. Kiedy próbuję użyć czegokolwiek z biblioteki, na przykład le_le pod porównaniami boolowskimi, otrzymuję standard Error: leb_le not a defined object. Mam zaktualizowany Coq i biblioteki i nie mam pojęcia, co może się tu dziać. Doceniam twój wkład w naprawianie tego problemu z biblioteką.

Answer 1

Kiedy próbuję Print Arith.PeanoNat, wyjście jest nieco inaczej: mam Module PeanoNat := Struct Module Nat End a następnie mimo leb_le nie jest w zakresie, Nat.leb_le jest.

(W razie potrzeby używam 8.5beta2).

Answer 2

Jeśli się nie mylę, kluczem do wczytania pliku jest Require. Import ma do czynienia z zarządzaniem przestrzeniami nazw. Często są używane razem, tak jak w Require Import PeanoNat., ale naprawdę robią dwie różne rzeczy.

Kiedy Coq plików (DirName/FileName.vo) są ładowane z Require, to tak jakby zawartość FileName.vo jest owinięty w Module DirName.FileName ... End. Everyting zdefiniowana w pliku jest wtedy dostępny z DirName.FileName.Name.

Plik może sam masz moduły M wewnątrz niego, i dostać się do M „s zawartości, trzeba wpisać DirName.FileName.ModuleName.Name1 itp

Import jest używany, aby uzyskać wszystkie definicje aż do najwyższego poziomu. Wykonując Import DirName.FileName.ModuleName, moduł Name1 jest teraz importowany do najwyższego poziomu i można go przywoływać bez długiej ścieżki.

W powyższym przykładzie plik Arith/PeanoNat.vo definiuje moduł Nat. Właściwie to wszystko definiuje. Więc jeśli zrobisz Require Import Arith.PeanoNat, otrzymasz PeanoNat.Nat na najwyższym poziomie. A następnie Import PeanoNat.Nat przyniesie Nat na najwyższym poziomie. Zauważ, że nie możesz wykonać Require Import PeanoNat.Nat, ponieważ nie jest to plik .vo.

Coq może czasami znaleźć plik .vo bez konieczności podawania całej ścieżki, więc można również wykonać Require Import PeanoNat., a coq znajdzie plik.Jeśli zastanawiasz się, gdzie znaleźć to, zrób Locate PeanoNat.

Coq < Require Import PeanoNat. 

Coq < Locate PeanoNat. 
Module Coq.Arith.PeanoNat 

Innym Nat dostępny jest również z innego miejsca niż 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 

Więc, nie Import bibliotekę, ty Require to. Używasz Import, aby nie używać pełnej nazwy ścieżki. Mam nadzieję, że pomoże to w debugowaniu tego, co się dzieje.