10 December, 2010

[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.

No comments: