Skorzystaj z wyników sprawdzonych w bibliotece (Coq)

Question

Jak korzystać z wyników sprawdzonych w danej bibliotece? Na przykład chcę użyć Lemma peano_ind z biblioteki BinInt. Piszę to w CoqIDE:

Require Import BinInt. 
Check peano_ind. 

i dostać "The peano_ind referencyjny nie został znaleziony w bieżącym środowiska." błąd. Nie jestem również w stanie go używać z apply podczas proofa.

Jednak powinien tam być, ponieważ dzięki Locate Library BinInt. widzę, że Coq może znaleźć plik BinInt.vo, a kiedy otworzę plik BinInt.v, widzę Lemma peano_ind.

Mam dokładnie ten problem zarówno na Debian 9.0 + CoqIDE 8.5pl2, jak i na Windows 10 + CoqIDE 8.6.

---

Wszystko to dlatego, że chciałem wykonać indukcję nad liczbami całkowitymi. Inne rozwiązanie byłoby również miłe, ale nadal jestem sfrustrowany moim brakiem możliwości wykorzystania wcześniej sprawdzonych wyników.

Answer 1

Biblioteka BinInt ma jedną z różnych definicjipeano_ind w różnych submodułach dla różnych typów. Znajdziesz je przy użyciu Locate peano_ind:

Constant Coq.NArith.BinNat.N.peano_ind 
    (shorter name to refer to it in current context is BinNat.N.peano_ind) 
Constant Coq.PArith.BinPos.Pos.peano_ind 
    (shorter name to refer to it in current context is Pos.peano_ind) 
Constant Coq.ZArith.BinInt.Z.peano_ind 
    (shorter name to refer to it in current context is Z.peano_ind) 

Następnie można użyć tych kwalifikowanych nazw, na przykład:

Check Z.peano_ind. 
Z.peano_ind 
    : forall P : Z -> Prop, 
     P 0%Z -> 
     (forall x : Z, P x -> P (Z.succ x)) -> 
     (forall x : Z, P x -> P (Z.pred x)) -> forall z : Z, P z 

Można również Import Z w celu umożliwienia korzystania z nazwy peano_ind bez zastrzeżeń.