如何使用加交流性和关联性重新排列Coq中的术语？ [英] how to rearrange terms in Coq using plus communtativity and associativity?

问题描述

我对如何在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中的术语？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！