coq - 选择子项重写的惯用方法

Question

假设我们有一个形式的结论: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

虽然这个公式确实说明了我想要做什么，
对于比“a b c ...”更复杂的公式，它变得非常冗长。

Answer 1

rewrite <- lemma预计 lemma是一个等式，即类型为 something1 = something2 形式的项.与大多数其他策略一样，您也可以向它传递一个返回等式的函数，即类型为 forall param1 … 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).

您不需要提供所有参数，只需确定要应用引理的位置即可。例如，这里指定 d 就足够了作为第二个论点。您可以通过完全保留第三个参数并指定通配符 _ 来实现此目的。作为第一个参数。

rewrite <- (plus_assoc _ d).

有时会有相同的子项，而您只想重写其中之一。在这种情况下，您不能使用 rewrite战术一族。一种方法是使用 replace使用更大的术语，您可以选择要更改的内容或事件 assert替换整个目标。另一种方法是使用 set策略，它允许您为特定出现的子术语命名，然后依靠该名称来识别特定子术语，最后调用 subst完成后删除名称。

另一种方法是忘记应用哪个引理，只需指定您想要如何更改目标，例如 assert或普通 replace … with …. .然后让自动化战术如 congruence , omega , solve [firstorder]等找到使证明工作的参数。使用这种方法，您必须写下目标的大部分内容，但可以节省指定引理。哪种方法最有效取决于您在大证明上的位置，以及在开发过程中什么趋于稳定，什么不是。