1

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ているかどうかに関連していることが判明しました。ZQ

しかし、ここで aac の書き換えが機能しなかった理由がわかりません。Z不一致の原因は何ですか? また、とで同じように動作させるにはどうすればよいQですか?

4

1 に答える 1

2

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.
于 2016-06-25T07:54:08.570 に答える