我有一个证明，它在两种情况下得出结论，如下所示:
+ rewrite H. apply lemma1.
+ apply lemma1.
虽然这相对简单，但我想将其合并为一个策略。我想做的英语是，“尝试重写，如果失败，什么也不做，尝试应用lemma1。
所以一个相关的问题是“什么都不做的策略是什么？”
这是我的尝试之一:
try (rewrite H || nil); apply lemma1.
我不知道如何弄清楚Ltac中的“空战术”是什么，也不知道如何找出它的名字。
这是另一个，我在其中“分发”lemma1。
do 2 try (rewrite H; apply lemma1 || apply lemma1).
这也没有证明第二种情况。
最佳答案
我认为在这种情况下您不需要“不执行任何操作”策略，因为当给予 try 的策略失败时，try 不执行任何操作。如果我没看错的话，你只想尝试重写 H;应用引理1. 就是这样。因此，它将尝试重写 H，在成功的情况下，它将应用引理 1。否则，当重写失败时，它只会应用引理1。因此，它在任何情况下都适用 lemma1。
关于coq - 如何在 Ltac 中尝试某种策略，但如果失败则继续，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/69859421/