假设我们有以下形式的结论：a + b + c + d + e。
我们还有一个引理：plus_assoc : forall n m p : nat, n + (m + p) = n + m + p。
将术语任意“插入一对括号”的惯用方法是什么？也就是说，如果有多个可用位置，我们如何轻松地选择重写位置。
我最终要做的事情如下：
replace (a + b + c + d + e)
with (a + b + c + (d + e))
by now rewrite <- ?plus_assoc
尽管此公式确实说明了我要执行的操作，但是对于比“ ab c ...”更复杂的公式而言，它变得非常漫长。
rewrite <- lemma期望lemma是一个等式，即类型为 形式的项something1 = something2。与大多数其他策略一样，您也可以向它传递一个返回等式的函数，即类型为 形式的术语forall param1 \xe2\x80\xa6 paramN, something1 = something2，在这种情况下，Coq 将寻找一个可以将引理应用于参数的位置，以形成一个目标的子项。Coq 的算法是确定性的，但让它选择并不是特别有用，除非执行重复重写，最终耗尽所有可能性。这里 Coq 恰好选择了你想要的目标rewrite <- plus_assoc，但我认为这只是一个例子，你追求的是通用技术。
您可以通过向引理提供更多参数来更好地控制在何处执行重写，以获得更具体的等式。例如，如果您想指定(((a + b) + c) + d) + e应该变成((a + b) + c) + (d + e)，即关联引理应该应用于参数(a + b) + c，d并且e，你可以写
rewrite <- (plus_assoc ((a + b) + c) d e).\n您不需要提供所有参数，只需提供足以查明要应用引理的位置即可。例如，在这里，指定d为第二个参数就足够了。您可以通过完全保留第三个参数并指定通配符来做到这一点_为第一个参数来完成此操作。
rewrite <- (plus_assoc _ d).\n有时会有相同的子术语，而您只想重写其中之一。在这种情况下，你不能rewrite单独使用这一系列策略。一种方法是使用replace更大的术语，您可以选择要更改的内容或事件assert来替换整个目标。另一种方法是使用策略set，它允许您为特定出现的子术语命名，然后依靠该名称来识别特定的子术语，最后调用subst在完成后调用以删除该名称。
另一种方法是忘记要应用哪些引理，而只指定您想要如何使用类似assert或 的普通内容来更改目标replace \xe2\x80\xa6\xc2\xa0with \xe2\x80\xa6.。然后让自动化策略如congruence，，omegasolve [firstorder]等自动化策略找到使证明有效的参数。使用这种方法，您确实必须写下目标的大部分内容，但可以节省指定引理的时间。哪种方法最有效取决于您在大证明中的位置以及在开发过程中什么趋于稳定，什么不稳定。