假设通过应用战术T拥有子目标列表:

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


并且假设我们知道引理L可用于证明AA'',但不能证明A'

我的问题是,我们是否可以对T进行排序,并给出L的应用结果,而我只剩下一个子目标A'

我尝试T;apply L.失败,因为排序似乎需要证明所有分支/子目标。

我还尝试通过使用SSReflect中的by T;apply L.来控制受控的自动化,此post建议这样做。不幸的是,Coq也陷入困境,并报告Ltac calls to ... last call failed.

最佳答案

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

T; try by apply L.


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

10-07 16:19
查看更多