重写适用于整数但不适用于 Coq10=]

Question

我正在测试 Coq 重写策略模结合性和交换性 (aac_tactics)。以下示例适用于整数 (Z)，但在将整数替换为有理数 (Q) 时会生成错误。

Require Import ZArith. 
Import Instances.Z.

Goal (forall x:Z, x + (-x) = 0) 
 -> forall a b c:Z, a + b + c + (-(c+a)) = b.
intros H ? ? ?. 
aac_rewrite H.

将Require Import ZArith.替换为Require Import QArith.等时出现错误：

Error: Tactic failure: No matching occurence modulo AC found.

在 aac_rewrite H.

在Z和Q之间也出现了类似的不一致问题，结果证明与Z/Q范围是否打开有关。

但我不明白为什么 aac 重写在这里不起作用。不一致的原因是什么，如何使 Z 和 Q 的行为相同？

Answer 1

AAC_tactics 库需要表达结合性、交换性等的定理。让我们以Qplus_assoc为例，它表达了有理数的结合律。

Qplus_assoc
     : forall x y z : Q, x + (y + z) == x + y + z

如你所见，Qplus_assoc并没有使用=，而是使用==来表达左手边和右手边的联系。有理数在标准库中定义为整数对和正数：

Record Q : Set := Qmake {Qnum : Z; Qden : positive}.

因为，例如1/2 = 2/4，我们需要一些其他方法来比较相等的有理数（= 除外，它是 eq 的表示法）。为此，stdlib 定义了 Qeq:

Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.

带符号

Infix "==" := Qeq (at level 70, no associativity) : Q_scope.

因此，对于有理数，您可能希望将示例重写为如下内容：

Require Import Coq.QArith.QArith.
Require Import AAC_tactics.AAC.
Require AAC_tactics.Instances.
Import AAC_tactics.Instances.Q.

Open Scope Q_scope.

Goal (forall x, x + (-x) == 0) -> 
     forall a b c, a + b + c + (-(c+a)) == b.
  intros H ? ? ?.
  aac_rewrite H.
  Search (0 + ?x == ?x).
  apply Qplus_0_l.
Qed.

重写适用于整数但不适用于 Coq10=]

rewrite works for integer but not for rationals for Coq aac_tactics

coq

coq-tactic

coq-plugin