如何使用加交换律和结合律重新排列 Coq 中的术语？

Question

我有一个关于如何在 Coq 中重新排列术语的一般性问题。例如，如果我们有一个术语 m + p + n + p，人类可以快速将这些术语重新排列为 m + n + p + p（隐式使用 plus_comm 和 plus_assoc）。我们如何在 Coq 中有效地做到这一点？

举个（愚蠢的）例子，

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？

我尝试使用 rewrite plus_comm at 2，但出现错误 Nothing to rewrite. 只需使用 rewrite plus_comm 即可将 LHS 更改为 p + m + n + p。

也欢迎任何关于有效重写的建议。

谢谢。

Answer 1

在这种特殊情况下（整数的线性算术），您可以只使用 omega 策略：

Require Import Omega.

Theorem plus_comm_test: forall n m p: nat,
  m + p + (n + p) = m + n + 2 * p.
Proof. intros; omega. Qed.

但是，有些情况下 omega 是不够的。在那些情况下，标准的 rewrite 策略不是很方便。 Ssreflect 库带有它自己版本的 rewrite 策略，它更适合重写目标子项等任务。例如：

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat.

Theorem plus_comm_test: forall n m p: nat,
  m + p + (n + p) = m + n + 2 * p.
Proof.
move=> n m p.
by rewrite -addnA [p + _]addnC -[_ + p]addnA addnn -mul2n addnA.
Qed.

方括号中的注释，例如 [p + _]，提供了帮助 rewrite 策略找出行动位置的模式。 addn* 引理和朋友是 Ssreflect 自己版本的自然数标准算术结果。

Answer 2

正如 Arthur 所说，有时 omega 是不够的，但我有时会用它来完成像这样的简单步骤。

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 在没有一点帮助的情况下无法触及的函数内部的东西...

Answer 3

ring 策略能够证明这些重排的相等性。

使用你的例子：

Require Import ZArith.
Open Scope Z_scope.

(* Both "ring" and "omega" can prove this. *)
Theorem plus_comm_test : forall n m p : Z,
  m + p + (n + p) = m + n + 2 * p.
Proof.
  intros.
  ring.
Qed.

ring 适用于整数，但我认为它不适用于自然数。

但是，ring可以证明一些omega不能证明的身份。（docs 说，"Multiplication is handled by omega but only goals where at least one of the two multiplicands of products is a constant are solvable. This is the restriction meant by "Presburger 算术。”）

例如：

(* "ring" can prove this but "omega" cannot. *)
Theorem rearrange_test : forall a b c : Z,
  a * (b + c) = c*a + b*a.
Proof.
  intros.
  ring.
Qed.

如何使用加交换律和结合律重新排列 Coq 中的术语？

how to rearrange terms in Coq using plus communtativity and associativity?

coq

coq-tactic