自然数とリスト: 帰納法 (3.4)
別の問題を証明してみましょう。Anarchy Proof から Sum of natural numbers をお借りします。ring を使わないでやってみよう、という問題ですが、気にせずringを使って解いちゃいますので、ネタバレにはなっていないはず…。
Require Import Arith Omega. Fixpoint sum (n: nat) := match n with | O => 0 | S m => n + sum m end. Theorem Sum_of_nat: forall (n: nat), 2 * sum n = n * (n + 1). Proof. intros. destruct n.
まずは、ここまでで解説したtacticを使って挑戦してみます。実はそれではうまくいかないのですが、しばらくおつきあい下さい。
1つめのゴール、n=0の場合の 2*sum 0=0*(0+1)は簡単です。
simpl. reflexivity.
両辺計算すると 0 になるので、0=0 は reflexivity で。simpl は計算できるところは計算して下さい、というtacticです。計算させるtacticはsimplの他にhnf、compute、cbv、lazy、vm_computeなどがありますが詳細はリファレンスなどをご覧下さい。そこそこ適当に計算するのがsimpl、本気でできる限り計算するのがcbv、くらいの感覚で。ringとfieldの性質を使って式を整理する、ring_simplify、field_simplify というのもあります。
もう一つのゴールが問題です。simpl すると…まだごちゃごちゃしているので、さらに ring_simplify すると
simpl. ring_simplify. n:nat ----------------------------------- 2*n + 2*sum n + 2 = n*n + 3*n + 2
こうなります。これは、もし 2*sum n = n*n + n が成り立てば、ゴールの中の 2*sum n を rewrite すれば左辺と右辺が同じになるのですが、それって、今証明しようとしている式ほとんどそのまんまです。堂々巡り。
こういう時に使うのが、数学的帰納法です。Coqでは、Inductiveな物をdestructする代わりに、inductionというtacticで分解します。
Theorem Sum_of_nat: forall (n: nat), 2 * sum n = n * (n + 1). Proof. intros. induction n. (* destruct n の代わりに！ *) simpl. reflexivity. simpl. ring_simplify.
さっきと同じ証明をすると、今度は…
仮定に IHn : 2 * sum n = n * (n+1) という便利な等式が入っています！
rewrite IHn. ring. Qed.
証明完了。
- n=0 で命題（たとえば 2 * sum 0 = 0 * (0 + 1)）が成り立つ
- nで成り立つなら、S n でも（2 * sum (S n) = S n * (S n + 1)）成り立つ
この二つが証明できたなら、その命題はすべての自然数 n で成り立つ！という証明方法です。一方で destruct での証明は
- n=0 で命題（たとえば 0<>0 -> 0<0+0）が成り立つ
- S n でも（0<>S n -> S n < S n + S n）成り立つ
の二つが証明できたら、すべての自然数 n で成り立つ、という証明です。帰納法の方が、"nで成り立つなら" という仮定を使える分、強力なわけですね。
帰納法の考え方は、自然数だけではなく、再帰的に定義された（つまり、S : nat -> nat のようにコンストラクタが作りたいものと同じ型を引数にとる）Inductive すべてに一般化できます。リストの場合
- xs=nil で成り立つ
- xs で成り立つなら、cons x xs でも成り立つ
が言えれば、その命題は全てのリストで成り立つことが証明できます。
ここまでの総まとめの練習問題としては
などいかかでしょうか…と思ったら、まだ exists の説明してないですね。これはあとで。(3.6)でやります。
