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?
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.