证明自动化

Question

假设通过应用策略有一个子目标列表 T:

______________________________________(1/10)
A
______________________________________(2/10)
A'
______________________________________(3/10)
A''

并且假设我们知道引理 L 可以用来证明 A 和 A'' 但不能 A'。

我的问题是，我们能否将 T 与 L 的申请结果进行排序，这样我只剩下一个子目标 A'？

我尝试了 T;apply L. 但没有成功，因为排序似乎需要所有 branches/sub-goals 证明。

我还尝试使用来自 SSReflect 的 by T;apply L. 来控制自动化，这是由建议的。不幸的是，Coq 也卡住了，并报告 Ltac calls to ... last call failed.

Answer 1

你可以使用try战术，像这样：

T; try by apply L.

这会执行以下操作。首先，它适用于 T。然后，在每个子目标上，它应用策略 by apply L。如果策略成功，那很好。否则，如果失败，try 什么都不做。

Answer 2

我会推荐 Arthur 的 T; try by apply L.。但是如果你需要更多的控制，你可以使用

T; [ (* first goal *) now apply L 
   | (* second goal *) now apply L 
   | (* last goal *) idtac ].

Answer 3

Coq 8.6 也有目标选择器，所以如果 T 创建了 4 个子目标，你可以写

T. 1-2,4: apply L.

在除第三个子目标之外的所有子目标中应用 L。

Answer 4

如 Vilhelm 所述，Coq 8.6 具有目标选择器。

您也可以执行 T; only 1,3: apply L.，它的优点是只对策略 T.

生成的子目标进行编号

Proof automation