使用库中证明的结果 (Coq)
Use results proven in a library (Coq)
如何使用在给定库中证明的结果?例如,我想使用库 BinInt
中的 Lemma peano_ind
。我在 CoqIDE 中这样写:
Require Import BinInt.
Check peano_ind.
并得到一个“在当前目录中找不到引用 peano_ind
环境。”错误。我也无法在证明期间将其与 apply
一起使用。
但是,它应该在那里,因为 Locate Library BinInt.
我看到 Coq 可以找到文件 BinInt.vo,当我打开文件 BinInt.v 我可以看到 Lemma peano_ind
.
我在 Debian 9.0 + CoqIDE 8.5pl2 和 Windows 10 + CoqIDE 8.6 上都遇到了这个问题。
所有这些都是因为我想对整数进行归纳。一个不同的解决方案也很好,但我仍然对我缺乏使用一些以前证明的结果的能力感到沮丧。
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
。
如何使用在给定库中证明的结果?例如,我想使用库 BinInt
中的 Lemma peano_ind
。我在 CoqIDE 中这样写:
Require Import BinInt.
Check peano_ind.
并得到一个“在当前目录中找不到引用 peano_ind
环境。”错误。我也无法在证明期间将其与 apply
一起使用。
但是,它应该在那里,因为 Locate Library BinInt.
我看到 Coq 可以找到文件 BinInt.vo,当我打开文件 BinInt.v 我可以看到 Lemma peano_ind
.
我在 Debian 9.0 + CoqIDE 8.5pl2 和 Windows 10 + CoqIDE 8.6 上都遇到了这个问题。
所有这些都是因为我想对整数进行归纳。一个不同的解决方案也很好,但我仍然对我缺乏使用一些以前证明的结果的能力感到沮丧。
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
。