[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.