coq - 使用库 (Coq) 中证明的结果

Question

如何使用给定库中经过验证的结果？例如，我想使用库 BinInt 中的 Lemma peano_ind。我在 CoqIDE 中写的:

Require Import BinInt.
Check peano_ind.

并得到一个“在当前中找不到引用peano_ind”环境。”错误。我也无法在证明过程中将它与 apply 一起使用。

但是，它应该在那里，因为使用 Locate Library BinInt. 我看到 Coq 可以找到文件 BinInt.vo，当我打开文件 BinInt.v 时，我可以看到 引理peano_ind。

我在 Debian 9.0 + CoqIDE 8.5pl2 和 Windows 10 + CoqIDE 8.6 上都遇到了这个问题。

<小时/>

所有这些都是因为我想对整数进行归纳。对此有一个不同的解决方案也很好，但我仍然对无法使用一些先前经过验证的结果感到沮丧。

Answer 1

BinInt 库在不同子模块中针对不同类型具有多个 peano_ind 定义之一。您可以使用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。