coq战术-重写工作为整数，但不为coq的有理数aac_tactics

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 QArith.等替换Require Import ZArith.时，报错:

错误:tactical failure: No matching occurrence modulo AC found.

at 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的符号)。因此，标准库定义了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.