1

我有一个关于如何在 Coq 中重新排列术语的一般性问题。例如，如果我们有一个 term 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)

我的问题是：

如何m + n + p + p有效地重写 LHS？

我尝试使用rewrite plus_comm at 2，但它给出了一个错误Nothing to rewrite.只需使用重写plus_comm将 LHS 更改为p + m + n + p.

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

谢谢。

4

3 回答 3

2

在这种特殊情况下（整数的线性算术），您可以使用以下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策略确定在哪里行动的模式。引理和朋友是 Ssreflect 自己的addn*自然数标准算术结果版本。

于 2015-10-07T02:48:45.293 回答
1

正如 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在没有一点帮助的情况下是无法触及的……

于 2015-10-07T16:09:57.560 回答
0

该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无法证明的身份。（文档说，“乘法由 omega 处理，但只有乘积的两个被乘数中至少有一个是常数的目标是可解的。这是“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.
于 2019-02-24T05:10:15.290 回答