[Coq] Coq Advent Calender : simpl (9 of 25)

　Coq でよく使われる tactic の９つ目は simpl です。simpl はβι簡約(beta, iota)をして式を簡単にします。βι簡約が何かについては「言語ゲーム」の記事が判りやすいです。β簡約は関数適用で、ι簡約だと再帰的に関数が適用される、と考えると良いです。

　予め、足し算の定義を示しておきます。plus を含んだ式を simpl すると、一つ目の変数 n について再帰的にパターンマッチして式を変形してくれます。

Coq < Print plus.
plus = 
fix plus (n m : nat) : nat := match n with
                              | 0 => m
                              | S p => S (plus p m)
                              end
     : nat -> nat -> nat

Argument scopes are [nat_scope nat_scope]

　では足し算を使った simpl の使用例です。

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

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

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

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

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

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

simpl を使うと左辺の0 + mがnに簡約されますが、右辺は変化がありません。ここは別途証明しておいた（というか標準ライブラリにはいっている）定理のplus_n_Oを使って書き換える事にします。

Sample_of_simpl < Check plus_n_O.         
plus_n_O
     : forall n : nat, n = n + 0

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

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

Sample_of_simpl < reflexivity.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S n + m = m + S n

帰納法の後半も simpl を使い、別の補題plus_n_Smを使います。

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

Sample_of_simpl < Check plus_n_Sm.
plus_n_Sm
     : forall n m : nat, S (n + m) = n + S m

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

Sample_of_simpl < erewrite IHn.
1 subgoal
  
  n : nat
  m : nat
  IHn : n + m = m + n
  ============================
   S (m + n) = S (m + n)

Sample_of_simpl < reflexivity.
Proof completed.

Sample_of_simpl < Qed.