4

“你问的问题似乎很主观，很可能会被关闭。”

嗯，我知道，但还是觉得值得在这里问。

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

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.

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

4

1 回答 1

3

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

〜P ...

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

H : P x
=========
 错误的

然后它尝试应用可以证明为 False 的定理。不幸的是，它只尝试应用不需要猜测实例的定理（可以与策略一起使用的定理适用并且不需要“with”扩展）。因此，auto 永远不会使用具有“forall a, P a -> False”形式的语句的定理，因为 apply 会抱怨它确实知道如何实例化 a。

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

您烦人的示例有效，因为在某些时候主要公式的目标是“〜P x”，因此主要符号不是，并且 auto 在其表中针对该主要符号具有引理 notP。

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

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

假设 my_le_n : forall x, my_le x x。

假设 my_le_S : forall xy, my_le xy -> 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”和其他类似情况。

于 2013-01-11T09:00:51.420 回答