Переписать работает для целого числа, но не для рациональных для 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 ZArith. с Require Import QArith. и т.д., есть ошибка:

Ошибка: Тактическая ошибка: Не найдено совпадений по модулю AC.

в 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 не использует =, оно использует == чтобы выразить связь между левой стороной и правой стороной. Рациональные числа определены в стандартной библиотеке как пары целых и положительных чисел:

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

Так как, например, 1/2 = 2/4, нам нужен какой-то другой способ сравнения рациональных чисел для равенства (кроме = что обозначение для eq). По этой причине stdlib определяет 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.