정수는 재 작성하지만 Coq aac_tactics는 합계가 아닙니다.

Question

Coq 다시 쓰기 전술 계수 법과 결합력 (aac_tactics)을 테스트하고있었습니다. 다음 예제에서는 정수 (Z)에 대해 작동하지만 정수가 이터 리 (Q)로 바뀌면 오류가 발생합니다.

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

관련이있는 것으로 밝혀졌다 Z 및 Q 간의 불일치 유사한 문제가 있었다

aac_rewrite H.에서 :

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. 등으로 대체 오류가 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.