1

我正在测试 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.用etc替换Require Import QArith.的时候报错：

错误：策略失败：未找到模数 AC 的匹配发生。

在aac_rewrite H.

Z和之间也存在类似的不一致问题Q，这与Z/Q范围是否开放有关。

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

4

1 回答 1

2

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.
于 2016-06-25T07:54:08.570 回答