[Coq] Coq Advent Calender : unfold (10 of 25)

　Coq でよく使われる tactic の10番目は unfold です。unfold は関数定義を展開します。
　unfold だけで使う場合も有りますが、fold と組み合わせて使う事もあります。fold は展開された関数を元に戻します。unfold して、simpl とか rewrite とかして、また fold して戻すと式が良い具合に変形されている場合があります。ここではそういう例を見てみましょう。

　まず、sum n := 1 + 2 + ... + nという関数を定義します。

Coq < Fixpoint sum n :=     
Coq <   match n with
Coq <   | O => O
Coq <   | S n' => S n' + sum n'
Coq <   end.
sum is recursively defined (decreasing on 1st argument)

　次に、sum n = 1/2 * n * (n + 1) であることを証明したいのですが、割り算が入ると面倒ですから、次の定理を証明する事にします。今回は環に関する自動証明器の ring を使いたいのでArithとRingをImportしておきます。
　nに関する帰納法で、n=0の場合はさらっと証明を流すことにします。

Coq < Require Import Arith Ring.                          

Coq < Lemma Sample_of_unfold : forall n, 2 * sum n = n * (n + 1).
1 subgoal
  
  ============================
   forall n : nat, 2 * sum n = n * (n + 1)

Sample_of_unfold < induction n.
2 subgoals
  
  ============================
   2 * sum 0 = 0 * (0 + 1)

subgoal 2 is:
 2 * sum (S n) = S n * (S n + 1)

Sample_of_unfold < reflexivity.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * sum (S n) = S n * (S n + 1)

　ここで、sum を unfold して、fold すると式が少し変形されます。

Sample_of_unfold < unfold sum.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 *
   (S n +
    (fix sum (n0 : nat) : nat :=
       match n0 with
       | 0 => 0
       | S n' => S n' + sum n'
       end) n) = S n * (S n + 1)

Sample_of_unfold < fold sum.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * (S n + sum n) = S n * (S n + 1)

　ここでreplaceを使ってちょっと左辺を書き換えます。書き換えて良い証明はsubgoal 2と後回しです。

Sample_of_unfold < replace (2 * (S n + sum n)) with (2 * S n + 2 * sum n).
2 subgoals
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * S n + 2 * sum n = S n * (S n + 1)

subgoal 2 is:
 2 * S n + 2 * sum n = 2 * (S n + sum n)

　ここでIHnを用いて書き換えて式変形を ring で自動証明します。後回しにしたものもringで一発です。

Sample_of_unfold < rewrite IHn.
2 subgoals
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * S n + n * (n + 1) = S n * (S n + 1)

subgoal 2 is:
 2 * S n + 2 * sum n = 2 * (S n + sum n)

Sample_of_unfold < ring.
1 subgoal
  
  n : nat
  IHn : 2 * sum n = n * (n + 1)
  ============================
   2 * S n + 2 * sum n = 2 * (S n + sum n)

Sample_of_unfold < ring.
Proof completed.

Sample_of_unfold < Qed.