假设通过应用战术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 calls to ... last call failed.
最佳答案
您可以使用try
战术,如下所示:
T; try by apply L.
这将执行以下操作。首先,它应用
T
。然后,在每个子目标上,应用策略by apply L
。如果战术成功,那就好。否则,如果失败,try
将不执行任何操作。