问题描述
我对如何在Coq中重新排列术语有一个一般性的问题。例如，如果我们有一个术语 m + p + n + p ，人类可以迅速将这些术语重新排列为 m + n + p + p （隐式使用plus_comm和plus_assoc）。
I have a general question about how to rearrange terms in Coq. For example, if we have a term m + p + n + p, humans can quickly re-arrange the terms to something like m + n + p + p (implicitly using plus_comm and plus_assoc). How do we do this efficiently in Coq?
对于一个（愚蠢的）示例，
For a (silly) example,
Require Import Coq.Arith.Plus.
Require Import Coq.Setoids.Setoid.
Theorem plus_comm_test: forall n m p: nat,
m + p + (n + p) = m + n + 2 * p.
Proof. intros. rewrite plus_assoc. simpl. rewrite <- plus_n_O.
现在，我们有
1 subgoals
...
______________________________________(1/1)
m + p + n + p = m + n + (p + p)
我的问题是：
我如何重写LHS有效地 m + n + p + p ？
How do I rewrite the LHS to m + n + p + p effectively?
我尝试使用重写plus_comm为2 ，但给出错误没什么可重写的。只需使用重写 plus_comm 的更改到 p + m + n + p 的LHS。
I tried to use rewrite plus_comm at 2, but it gives an error Nothing to rewrite. Simply using rewrite plus_comm changes the LHS to p + m + n + p.
也欢迎提供有关有效重写的任何建议。
Any suggestions on effective rewrites are also welcome.
谢谢。
推荐答案
正如亚瑟（Arthur）有时所说的 omega 是不够的，但是有时我会用它来完成简单的步骤。
As Arthur says sometimes omega is not enough, but I sometimes use it for simple steps like this.
Require Import Omega.
Theorem test: forall a b c:nat, a + b + 2 * c = c + b + a + c.
intros.
replace (c + b + a) with (a + b + c) by omega.
replace (a + b + c + c) with (a + b + (c + c)) by omega.
replace (c + c) with (2 * c) by omega.
reflexivity.
Qed.
这是一个愚蠢的例子，因为 omega 本来可以一口气解决所有问题的，但是有时候您想重写 omega 内的函数，如果没有一点帮助的话……
This is a silly example, because omega would have solved it all in one go, but sometimes you want to rewrite things inside functions that omega can't reach into without a little help...
这篇关于如何使用加交流性和关联性重新排列Coq中的术语？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！