自然数とリスト: 帰納法の色々 (3.5)
Coqでの帰納法の仕組みについて、ちょっとだけ。CoqIDE に
Inductive nat := | O : nat | S : nat -> nat.
と打ち込んで nat を再定義してみてください。
nat is defined nat_rect is defined nat_ind is defined nat_rec is defined
こう右下に表示されると思います。実は、nat を定義すると同時に、裏でひっそりと3つの公理がCoqによって自動で定義されているのです。これが帰納法の正体です。
Print nat_ind.
こんな命題です。
nat_ind =
fun P : nat -> Prop => nat_rect P
: forall P : nat -> Prop,
P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
- 自然数に関するどんな命題 P : nat -> Prop も、
- 0 で成り立つ P O 証明
- n で成り立 P n てば、S n でも成り立つ P (S n) という証明
- の二つがあるなら forall n : nat, P n すべての n で成り立つ
と書いてあります。まさに帰納法です。induction n. という tactic は、基本的には、実は apply nat_ind. しているだけだったりします（実際はゴールに n が複数あるときの扱いなど、induction n の方が便利になるように工夫が入っていますけど）。
Require Import List. Print list_ind.
すると list の帰納法も見られます。
False_ind
and や or など再帰的じゃないInductiveにも、一応機械的に帰納法の公理が定義されているのですが、あんまり使い道はありません。唯一使えるのが False のために自動定義される False_ind で
Print False_ind. False_ind = 略 : forall P : Prop, False -> P
どんな命題 P も、「False が成り立っているなどというあり得ない事態であれば、成り立つ」。これを使うと apply False_ind. で、どんなゴールも False に変えられます。仮定がそもそもおかしいときに「仮定がそもそもおかしいぞ」とCoqさんに伝えるのに使います。apply False_ind してから普通にFalseを証明してしまえばよし。さきほど紹介した condtraction H. があれば普通は用が足りますが、仮定にそのまま１個でバシッと矛盾しているものを作るのが難しいときには、「Falseを証明する」方が楽だったりします。
カリーハワード
さて、カリーハワード対応の時間です。「帰納法」とは、プログラミングで言うと、何にあたるのでしょうか。
list_ind =
fun (A : Type) (P : list A -> Prop) => list_rect P
: forall (A : Type) (P : list A -> Prop),
P nil ->
(forall (a : A) (l : list A), P l -> P (a :: l)) ->
forall l : list A, P l答えは、foldr です。Haskell には"依存型"がないので、"P nil" や "P l" の部分が全部同じ型 b になって簡単化してますが、やっていることは同じで
- nil の場合の結果
- cons x xs の場合、x と "xs を foldr して結果" から計算結果を求めて返す関数
の二つから、任意のリストを受け取ってリスト全体を計算して返す関数を作るのがfoldrであります。
整礎帰納法
「数学的帰納法」って、こうじゃなかったけ？と記憶されている方もいらっしゃるかもしれません。
- nより小さい全ての数で成り立つなら、nでも成り立つ
が言えれば、「全てのnで成り立つ」と言える。
これは 整礎帰納法 と呼ばれる証明方法で、普通の帰納法よりさらに強力なテクニックです。Sqrt 2 @ Anarchy Proof などではたぶんこれが使いたくなると思います。
Coqでは自然数に関する整礎帰納法はCoq.Arith.Wf_natというモジュールで定義されていて、
Requirt Import Wf_nat.
Print lt_wf_ind.
lt_wf_ind =
中略
: forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
(forall m : nat, m < n0 -> P m) -> P n0) ->
P nこうです。読んで字のごとしです。使うには直接
apply lt_wf_ind.
するか、induction 〜 using という tactic を使います。帰納法っぽいtacticを使いやすくapplyしてくれるものです。
induction n using lt_wf_ind.
ある条件を満たす順序関係があれば、自然数以外でも整礎帰納法は使えます。詳しくは Coq.Init.Wf。
introしすぎにご用心
さっきの例題を、ちょっとだけ形をいじって
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 m: nat), m = 2 * sum n -> m = n*(n+1). Proof.
こうしたものを考えます。
intros. induction n.
こうすると、n=0 の場合まではなんとかなる（rewrite H. simpl. reflexivity.）のですが、S n の場合が
H : m = 2 * sum (S n) IHn : m = 2 * sum n -> m = n * (n + 1) --------------------------------------- m = S n * (S n + 1)
帰納法の仮定 IHn が、何かちょっと困った形になってしまいます。これは、全部 intros してから induction すると、「intros で仮定に押し上げて m を固定してしまった状態で帰納法を回す」ことになってしまうせい。正しくは
forall (m:nat), m=2*sum n -> m = n*(n+1)
というように、m がforallされた命題が、全てのnで成り立つことを証明しないとうまくいきません。
ということで、intros ではなく、intro で n だけ剥がしてから induction しましょう。（実は induction tactic は便利に作られていて、なにもintroせずにinduction nと書いたら自動で n まででintroを止めてinducitonを始めてくれるので、それでも可です。）
Proof. intro n. induction n. (以下は練習問題)
「forall や -> を見たらとりあえず intros 」という方針をこれまで推奨してきましたが、induction を使う前に限っては、必要最小限の intro で 止めておく方がうまくいくことが多いようです。
実は、もっといじわるなバージョンも考えられます。
Theorem Sum_of_nat: forall (m n: nat), m = 2 * sum n -> m = n*(n+1). Proof.
今度は、m の方が n より先にあるため、n だけを intro しようとしても無理で、intros m n. のように、必ず m も仮定に引っ張り上げてしまいます。こういう時には、仕方なく intros してから、"generalize" という tactic で、仮定を forall に戻します。
intros m n. generalize m. induction n.
あとはさっきと同様。
