证明自动化

Question

假设采用战术有子目标清单T：

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

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

我的问题是，我们是否可以T根据的应用结果进行测序，而结果L只剩下一个子目标A'？

我尝试T;apply L.没有成功，因为排序似乎需要所有分支/子目标都经过证明。

我还通过使用by T;apply L.SSReflect 尝试了受控自动化，这是本文的建议。不幸的是，Coq也陷入困境，并报告Ltac calls to ... last call failed.

Answer 1

您可以使用try战术，如下所示：

T; try by apply L.

这将执行以下操作。首先，它适用T。然后，在每个子目标上，应用策略by apply L。如果战术成功，那就好。否则，如果失败，try则不执行任何操作。