rewrite works for integer but not for rationals for Coq aac_tactics

Question

I was testing Coq rewrite tactics modulo associativity and commutativity (aac_tactics). The following example works for integer (Z), but generates an error when integers are replaced by rationals (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.

When replacing Require Import ZArith. with Require Import QArith. etc., there is an error:

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

at aac_rewrite H.

There was a similar inconsistency issue between Z and Q, which turned out to be related to whether the Z/Q scope is open.

But I don't understand why aac rewrite didn't work here. What's the cause of the inconsistency, and how can one make it behave the same for Z and Q?

Answer 1

The AAC_tactics library needs theorems which express associativity, commutativity and so forth. Let's take Qplus_assoc which expresses the associativity law for the rational numbers.

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

As you can see Qplus_assoc doesn't use =, it uses == to express the connection between the left-hand side and the right-hand side. Rationals are defined in the standard library as pairs of integers and positive numbers:

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

Since, e.g. 1/2 = 2/4, we need some other way of comparing the rationals for equality (other than = which is the notation for eq). For this reason the stdlib defines Qeq:

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

with notation

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

So, in case of rational numbers you might want to rewrite your example to something like this:

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.