[Coq] Coq Advent Calender : induction (13 of 25)

　Coq でよく使われる tactic の13番目は induction です。

　Coq は帰納的な型を定義すると、その型に対する帰納法を自動で定義してくれます。例えば

Inductive nat : Set :=  
  O : nat 
| S : nat -> nat

という自然数natに対して、

forall P : nat -> Prop, 
  P 0 -> 
  (forall n : nat, P n -> P (S n)) -> 
  forall n : nat, P n

というnat_indを定義してくれます。これを使って、自然数nについての帰納法の証明の時に、

• n=0 の場合のゴール
  
• nの時成り立つという仮定IHnと、S nの場合のゴール
  

を作ってくれます。同様にリストであれば、nilとconsの場合などです。

　今までにも何度か induction を使った証明を示してきましたが、今回も簡単な例を。

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

plus_comm < induction n.
2 subgoals
  
  ============================
   forall m : nat, 0 + m = m + 0

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < intro m.
2 subgoals
  
  m : nat
  ============================
   0 + m = m + 0

subgoal 2 is:
 forall m : nat, S n + m = m + S n

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

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < erewrite <- plus_n_O.
2 subgoals
  
  m : nat
  ============================
   m = m

subgoal 2 is:
 forall m : nat, S n + m = m + S n

plus_comm < reflexivity.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  ============================
   forall m : nat, S n + m = m + S n

plus_comm < intro m.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S n + m = m + S n

plus_comm < simpl.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S (n + m) = m + S n

plus_comm < erewrite <- plus_n_Sm.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S (n + m) = S (m + n)

plus_comm < erewrite IHn.
1 subgoal
  
  n : nat
  IHn : forall m : nat, n + m = m + n
  m : nat
  ============================
   S (m + n) = S (m + n)

plus_comm < reflexivity.
Proof completed.

plus_comm < Qed.