[Coq] Coq Advent Calender : specialize (23 of 25)

　Coq でよく使われる tactic の23番目は specialize です。

　公理とかライブラリにある定理とか証明済み補題とかに特定の引数を適用した物を仮定に使いたい事があります。forall n, P n. みたいな補題Lのnに特定の値 n0 を代入した P n0 が仮定にあると良いなぁ、とか。
　勿論、assert(H:P n0)とかcut (P n0)とか書いても良いのですが、specialize (L n0). と書けば cut (P n0)してapply (L n0) するのと同じになり、証明が短く判りやすくなります。

replaceの説明の時と同じ定理を、replaceを使わず、specializeとrewriteを使って証明してみます。証明の前提と成る公理は replace の回を参照して下さい。

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

inv_r < intros.
1 subgoal
  
  a : G
  ============================
   a * inv a = 1

inv_r < specialize (id_l (a * inv a)).
1 subgoal
  
  a : G
  ============================
   1 * (a * inv a) = a * inv a -> a * inv a = 1

specializeすると、公理 id_l に (a * inv a) を適用した物が得られますので、intro して書き換えて消去します。あとは同様に。

inv_r < intro H; rewrite <- H; clear H.
1 subgoal
  
  a : G
  ============================
   1 * (a * inv a) = 1

inv_r < specialize (inv_l (inv a)); intro H; rewrite <- H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * inv a * (a * inv a) = inv (inv a) * inv a

inv_r < specialize (assoc (inv (inv a)) (inv a) (a * inv a)); intro H; rewrite H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * (inv a * (a * inv a)) = inv (inv a) * inv a

inv_r < specialize (assoc (inv a) a (inv a)); intro H; rewrite <- H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * (inv a * a * inv a) = inv (inv a) * inv a

inv_r < specialize (inv_l a); intro H; rewrite H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * (1 * inv a) = inv (inv a) * inv a

inv_r < specialize (id_l (inv a)); intro H; rewrite H; clear H.
1 subgoal
  
  a : G
  ============================
   inv (inv a) * inv a = inv (inv a) * inv a

inv_r < reflexivity.
Proof completed.

inv_r < Qed.