ライブラリ（Coq）で証明された結果を使用する

Question

特定のライブラリで証明された結果をどのように使用すればよいですか？たとえば、ライブラリBinIntのLemma peano_indを使用したいとします。私はCoqIDEでこれを書く：

Require Import BinInt. 
Check peano_ind. 

と取得「参照peano_indが現在の 環境に見つかりませんでした。」エラー。私はまた証明の間にapplyとそれを使用することができません。 Locate Library BinInt.と私はコックがファイルBinInt.voを見つけることができることがわかり、私は、ファイルを開いたときにBinInt.v私はLemma peano_indを見ることができるので

しかし、それは、そこにする必要があります。

私は、Debian 9.0 + CoqIDE 8.5pl2とWindows 10 + CoqIDE 8.6の両方でこの正確な問題を抱えています。

---

これはすべて整数に対する誘導を行いたいからです。そのための別の解決策もいいかもしれませんが、私は以前に証明されたいくつかの結果を使用する能力が不足していることにまだ不満を抱いています。

Answer 1

BinIntライブラリーは、異なるタイプの異なるサブモジュールに個のpeano_indの定義の1つを持っています。あなたは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) 

は、その後、例えば、これらの修飾名を使用することができます。

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 

ます。またImport Z非修飾名peano_indを使用できるようにすることができます。