[Coq] Coq Advent Calender : replace (12 of 25)

Coq でよく使われる tactic の12番目は replace です。

　replace t1 with t2 とすると、t2 = t1 という等式をsubgoalに追加し、t2 = t1 を用いてゴールの書き換えを行います。書き換え規則 t2 = t1 の証明を先送りにすることで本筋の証明の見通しがよくなります。また、simpl, unfold, rewriteを使う場合とかで、「ゴールのこの部分だけ書き換えたいのだが別のところも書き換えられてしまう」と悩む場面もありますが、そういうときは replace でとりあえず部分的に書き換え、あとでその箇所の書き換えを証明すると楽です。

　replace を多用するのは、等式変形を繰り返す場合です。今回はそういう例を。
　下記の様に群 G を定義してみます。

Coq < Axiom G : Set.  (* 群G *)
Coq < Axiom G_dec : forall a b:G, {a=b} + {a <> b}.  (* 単位元や逆元の一意性とかを示す時に必要 *)
Coq < Axiom mult : G -> G -> G.  (* 乗法 *)
Coq < Notation "a * b" := (mult a b).  (* 記号 * で書ける様にする *)
Coq < Axiom assoc : forall a b c:G, (a * b) * c = a * (b * c).  (* 結合則 *)
Coq < Axiom G1 : G.  (* 単位元 *)
Coq < Notation "1" := G1.  (* 記号 1 で書ける様にする *)
Coq < Axiom id_l : forall a:G, 1 * a = a.  (* 左単位元である *)
Coq < Axiom inv : G -> G.  (* 逆元 *)
Coq < Axiom inv_l : forall a:G, (inv a) * a = 1.  (* 左逆元 *)

　では、左逆元は右逆元でもあることを証明してみます。長くなるのでゴールを示すのは要所要所だけです。replaceを使うと、subgoalが増えているのが判ります。

Coq < Theorem inv_r : forall a:G, a * (inv a) = 1.
inv_r < intros.
1 subgoal
  
  a : G
  ============================
   a * inv a = 1

inv_r < replace (a * inv a) with (1 * a * inv a).
2 subgoals
  
  a : G
  ============================
   1 * a * inv a = 1

subgoal 2 is:
 1 * a * inv a = a * inv a

inv_r < replace (1 * a * inv a) with ((inv (inv a) * (inv a)) * a * inv a).
3 subgoals
  
  a : G
  ============================
   inv (inv a) * inv a * a * inv a = 1

subgoal 2 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 3 is:
 1 * a * inv a = a * inv a

inv_r < replace (inv (inv a) * inv a * a * inv a) with (inv (inv a) * (inv a * a) * inv a).
4 subgoals
  
  a : G
  ============================
   inv (inv a) * (inv a * a) * inv a = 1

subgoal 2 is:
 inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a
subgoal 3 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 4 is:
 1 * a * inv a = a * inv a

inv_r < rewrite inv_l.  (* ここからは replace を使わなくても rewrite で簡単に変形出来る *)
inv_r < rewrite assoc.
inv_r < rewrite id_l.
inv_r < rewrite inv_l.
4 subgoals
  
  a : G
  ============================
   1 = 1

subgoal 2 is:
 inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a
subgoal 3 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 4 is:
 1 * a * inv a = a * inv a

inv_r < reflexivity.  (* メインゴールの証明完了。残りは replace の書き換えの証明 *)
3 subgoals
  
  a : G
  ============================
   inv (inv a) * (inv a * a) * inv a = inv (inv a) * inv a * a * inv a

subgoal 2 is:
 inv (inv a) * inv a * a * inv a = 1 * a * inv a
subgoal 3 is:
 1 * a * inv a = a * inv a

inv_r < rewrite <- assoc; reflexivity.
2 subgoals
  
  a : G
  ============================
   inv (inv a) * inv a * a * inv a = 1 * a * inv a

subgoal 2 is:
 1 * a * inv a = a * inv a

inv_r < erewrite inv_l; reflexivity.
1 subgoal
  
  a : G
  ============================
   1 * a * inv a = a * inv a

inv_r < rewrite assoc; rewrite id_l; reflexivity.
Proof completed.

inv_r < Qed.
intros.
replace (a * inv a) with (1 * a * inv a) .
 replace (1 * a * inv a) with (inv (inv a) * inv a * a * inv a) .
  replace (inv (inv a) * inv a * a * inv a) with
   (inv (inv a) * (inv a * a) * inv a) .
   rewrite inv_l in |- *.
   rewrite assoc in |- *.
   rewrite id_l in |- *.
   rewrite inv_l in |- *.
   reflexivity.
   
   rewrite <- assoc in |- *; reflexivity.
   
  erewrite inv_l in |- *; reflexivity.
  
 rewrite assoc in |- *; rewrite id_l in |- *; reflexivity.
 
inv_r is defined

Coq <