16 December, 2010

[Coq] Coq Advent Calender : ring (16 of 25)

 Coq でよく使われる tactic の16番目は ring です。

 ring は可換な半環 ( 演算 +, * があって、それぞれ単位元 0, 1 があって、それぞれ交換則と結合則が成り立って、分配法則があってな数学的構造)での計算を行ってくれます。基本的には多項式の掛け算を展開し、標準形に直して比較するようなことをします。
 使用するにはRequire Import Ring.が必要です。

 下記で色々試してみましたが、適宜 rewrite, replace なども併用しないとうまくいきませんでした。


Coq < Require Import ZArith Ring.

Coq < Open Scope Z_scope.

Coq < Lemma Sample_of_ring : forall a b:Z, a + b = 7 -> a * b = 12 -> a^2 + b^2 = 25.
1 subgoal

============================
forall a b : Z, a + b = 7 -> a * b = 12 -> a ^ 2 + b ^ 2 = 25

Sample_of_ring < intros a b H1 H2.
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
a ^ 2 + b ^ 2 = 25

Sample_of_ring < replace (a^2 + b^2) with ((a+b)^2 - 2*a*b) by ring.
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
(a + b) ^ 2 - 2 * a * b = 25

Sample_of_ring < rewrite H1.
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
7 ^ 2 - 2 * a * b = 25

Sample_of_ring < replace (2*a*b) with (2*12) by ring [H2].
1 subgoal

a : Z
b : Z
H1 : a + b = 7
H2 : a * b = 12
============================
7 ^ 2 - 2 * 12 = 25

Sample_of_ring < reflexivity.
Proof completed.

Sample_of_ring < Qed.

No comments: