automation - 打样自动化

Question

假设通过应用策略 T 获得子目标列表:

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

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

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

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

我还尝试使用 SSReflect 的 by T;apply L. 进行控制自动化，这由 post 建议。 。不幸的是，Coq 也被卡住了，并报告 Ltac 调用...上次调用失败。

Answer 1

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

T; try by apply L.

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