coq - 有效使用 Coq 提示数据库的最佳实践

Question

“你问的问题似乎很主观，很可能会结束。”

好吧，我知道这一点，但仍然值得在这里提问。

我多次被告知我应该使用提示数据库和自动，因为它是有史以来最好的东西，诸如此类。但是，有几次我尝试使用它时，我对琐碎的细节感到非常恼火。这是不断发生的一件事。

Section Annoying.

Variable T : Type.
Variable P : T -> Prop.

Axiom notP : forall x, ~ P x.
Hint Resolve notP.

Goal forall (x : T), P x -> False.
intros x.
auto. (* nothing... *)
replace (P x -> False) with (~ P x) by reflexivity.
(* fold not. does not work, don't know why either but that is not the point here... *)
auto.
Qed.

End Annoying.

因此，我的问题是:人们如何使用提示数据库而不会遇到这样的麻烦。是否有有效的提示数据库的经验法则？

Answer 1

auto 通过将未修改的定理应用于目标来工作。它通过对其形状的句法观察来寻找要应用的定理。所以你的定理 notP 只适用于形式的目标

〜P ...

P x -> False 形式的目标在语法上不是这种形式。事实上，自动策略的工作方式如下:首先尽可能多地使用介绍，然后尝试应用定理。所以你的目标转化为

高:P x
==========
错误的

然后它尝试应用可以证明 False 的定理。不幸的是，它只尝试应用不需要猜测实例化的定理(可以与策略一起使用的定理 apply 并且不需要“with”扩展)。所以一个带有形式陈述的定理
“forall a, P a -> False”永远不会被 auto 使用，因为 apply 会提示它确实知道如何实例化 a。

因此，汽车的良好候选证明是您可以仅通过使用介绍和应用来完成的证明，没有展开或应用的实例......没有将定理手动应用于参数，并且在每一步，最右边的公式(在箭头的末尾)定理使用谓词作为出现在目标结论中的谓词。

你烦人的例子是有效的，因为在某些时候，主公式的目标是“~P x”，所以主符号不是，并且 auto 在它的表中包含这个主符号的引理 notP 。

这是一个运行良好的示例:

变量 my_le : nat -> nat -> Prop。

假设 my_le_n : forall x, my_le x x。

假设 my_le_S : forall x y, my_le x y -> my_le x (S y)。

提示解决 my_le_n my_le_S。

多多引理:my_le 10 14。
证明。
汽车。
Qed。

在 Hint 命令之后，auto 的表中有两个词条“my_le_n”和“my_le_S”，当目标主符号是 my_le 时使用。在查看“my_le 10 14”时，它依次尝试这两个引理。第一个失败，但第二个应用并产生一个新目标“my_le 10 13”，这可以重复多次，直到自动设法应用“my_le_n”。所以 auto 探索了一个可能性树，其中分支来自这样一个事实，即可能有几个适用于给定目标的定理。此外，分支的长度限制为 5，因此 my_le 10 15 不会被 auto 解决。您可以通过给 auto 一个数字参数来更改分支的长度。所以“auto 20”将解决“my_le 10 15”和其他类似的情况。