[Coq] Coq Advent Calender : exact (24 of 25)

　Coq でよく使われる tactic の24番目は exact です。

　現在のゴールが、仮定のどれか、あるいは既存の定理にマッチする時に exact H?. とか exact my_theorem. とかするとゴールが証明されます。前者の場合は assumption. で済みますし、exact ではなく apply でもOKなんで、無理に使う必要は無いですが、ゴールと同じ物があったという意図を多少は示せるのかも。

　exact を使って書いてみました。

Coq < Lemma Sample_of_exact : forall n m, n + m = m + n.
1 subgoal
  
  ============================
   forall n m : nat, n + m = m + n

Sample_of_exact < intros.
1 subgoal
  
  n : nat
  m : nat
  ============================
   n + m = m + n

Sample_of_exact < induction n.
2 subgoals
  
  m : nat
  ============================
   0 + m = m + 0

subgoal 2 is:
 S n + m = m + S n

Sample_of_exact < simpl.
2 subgoals
  
  m : nat
  ============================
   m = m + 0

subgoal 2 is:
 S n + m = m + S n

Sample_of_exact < exact (plus_n_O m).
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S n + m = m + S n

Sample_of_exact < simpl.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (n + m) = m + S n

Sample_of_exact < rewrite IHn. 
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (m + n) = m + S n

Sample_of_exact < exact (plus_n_Sm m n).
Proof completed.

Sample_of_exact < Qed.