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.を交換する場合、エラーが発生した。

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を見ることができるように、それは左側と右側との間の接続を表現するために==を使用しています。有理数は、標準ライブラリ内で整数と正の数の対として定義される。

1/2 = 2/4であるから、均等論の比較のための他の方法が必要である（eqの表記である=以外）。 、表記だから、

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

で

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

有理数の場合、あなたはこのような何かにあなたの例を書き直しが必要になることがあります：このような理由からSTDLIBはQeqを定義

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.