réécriture fonctionne pour nombre entier mais pas pour rationnel pour Coq aac_tactics

Question

Je testais Coq réécriture tactiques modulo associativité et commutativité (aac_tactics). L'exemple suivant fonctionne pour entier (Z), mais génère une erreur lorsque les entiers sont remplacés par rationnels (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. 

Lors du remplacement Require Import ZArith. avec Require Import QArith. etc., il y a une erreur:

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

à aac_rewrite H.

Il y avait un problème d'incohérence semblable entre Z et Q, qui se est avéré être lié si l'étendue Z/Q est ouverte.

Mais je ne comprends pas pourquoi la réécriture d'aac n'a pas fonctionné ici. Quelle est la cause de l'incohérence, et comment peut-on le faire se comporter de la même manière pour Z et Q?

Answer 1

La bibliothèque AAC_tactics a besoin de théorèmes qui expriment l'associativité, la commutativité et ainsi de suite. Prenons Qplus_assoc qui exprime la loi d'associativité pour les nombres rationnels.

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

Comme vous pouvez le voir Qplus_assoc ne pas utiliser =, il utilise == pour exprimer le lien entre le côté gauche et le côté droit. Les rationnels sont définis dans la bibliothèque standard sous forme de paires d'entiers et de nombres positifs:

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

Comme, par ex. 1/2 = 2/4, nous avons besoin d'une autre façon de comparer les rationnels pour l'égalité (autre que = qui est la notation pour eq). Pour cette raison, le stdlib définit Qeq:

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

avec la notation

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

Ainsi, en cas de nombres rationnels vous pouvez réécrire votre exemple à quelque chose comme ceci:

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.