Coqの入門記事を書く会 (3)
このペースだと、なかなかCoqの一番面白いところ（とわたしが思うところ）に行き着かないので、今回は全力ですっ飛ばして、必要な細かい話を全部片付けちゃおうと思います。次回が面白くなるはずです。今回は、主に、自然数やリストにまつわる証明の巻。
自然数とリスト: Inductive (3.1)
前回、andやorなどの命題が"Inductive"で作られてることをご紹介しました。Coqでは、命題だけでなく、自然数やリストなどなど、普通のデータ型も、Inductiveで定義します。
例えば自然数は Coq.Init.Datatypes.nat
Inductive nat : Set := | O : nat | S : nat -> nat.
こう。O (大文字のオーです) は、0 (ゼロです) を表します。S n は「n の一つ後ろの数」を表します。S (S (S O))) は 3。（ただし、実際に大量に S を並べるのは大変なので、Coq のコードでは 100 や 200 と普通に書けば勝手に処理系がS S ... (S O)と解釈してくれます。実体は S S S ... なので、10000 とか大きい定数を書くと結構大変なことになりますが…）
リストは Coq.Lists.List.list:
Variable A : Type. Inductive list : Type := | nil : list | cons : A -> list -> list. Infix "::" := cons (at level 60, right associativity) : list_scope.
nil で空リストを作るか、cons で、リストに要素を一個足すか、どちらかの方法でリストは作れるし、その方法で作れるものだけがリストです。
さてさて、では早速、この辺りが登場する証明をやってみましょう。まずは簡単なものから。「x が 0 じゃない自然数なら、x+x は x より大きい」。
Require Import Arith Omega. Lemma double_is_big: forall (x:nat), x <> 0 -> x < x+x. Proof. intros.
1行目の Require Import ですが、Arith と Omega という二つの「ライブラリ」をこれから使います、とCoqさんに伝えています。どちらもCoqの標準ライブラリで、Arithには自然数に関する基本的な定理が大量に証明されて入っています。自然数の証明をする場合、とりあえずRequire Importしておくと良いと思います。Omegaについては後で。
さて、続きは…色々なやり方があります。ここで紹介するのはあくまで一例ですので、皆様もっと綺麗な証明を探してみて下さい。
仮定の所に x: nat とあります。仮定にInductiveなものがあわられたら、destructして分解してみる。これはandやorでなくても、命題じゃない、自然数のようなデータ型でも使えます。
destruct x.
natには二つコンストラクタがあったので、ゴールが2つに分かれます。Oで作ったnatの場合（つまりx=0の場合）と、Sで作ったnatの場合です、0の方は、こんな風になります。
H: 0 <> 0 -------------- 0 < 0 + 0
0 < 0+0 って成り立ってないので証明できなさそうな気がしますが、これは、仮定の方がおかしいのです。"H: 0<>0 ならば"…といわれても、そんなことはあり得ません！ということを証明したら、全体を証明したことになります。
そういえば説明し忘れましたが、x <> y は "~(x=y)" のシンタックスシュガーです。x=yではない。
unfold not in H.
すると "H: 0=0 -> False" に変わることで確認できます（注：確認だけなので、これはやってもやらなくても以下の証明には変化ありません）。unfold 〜 in で、ゴールの中だけではなく仮定の中もunfoldできます。
「仮定に成り立たない命題が入ってるぞ」ということをCoqに伝えるのは、contradictionというtacticです。
contradiction H.
- contradiction H.
- 仮定 H: A1->A2->...->An->False があったら、ゴールを、A1とA2と...とAnのn個のゴールに変える
今回の例は "0=0 -> False" なんて仮定は成り立ちませんよ！とcontradictionしたので、証明すべき命題は 0=0 です。
reflexivity.
そりゃ当たり前に = ですよね、とCoqさんに伝えます。イコールに関するtacticは以下の4種類です。
自然数とリスト: rewriteなど (3.2)
x=0の場合は終わったので、残ったゴールはこれです。
------------------------- S x < S x + S x
これを証明するには…なにか、このくらいはさっきImportしたArith標準ライブラリで証明されていないでしょうか。CoqIDEでは
SearchAbout (_ < _ + _).
と打ち込むか、F2キーを押して (_ < _ + _) を検索すると…
「(_ < _ + _) という形のゴールに apply できそうなライブラリ定理の一覧」が表示できます。便利です。
表示された一覧の中に、わたしが見た限りでは直接使えそうなものはなかったのですが、近い物がありました。
plus_lt_compat_l : forall n m p: nat, n<m -> p+n < p+m
これ。p+n < p+m というのは S x < S x + S x の形にはなっていませんが、これを使えば "S x + 0 < S x + S x" なら証明できそう。"S x" と "S x + 0" は等しいので、これが示せれば十分ですよね。
十分ではありません。まず「"S x" と "S x + 0" は等しい」から証明してあげないとCoqさんは納得してくれません。納得させます。
assert (S x = S x + 0).
初回にやった assert (X:=t) というtacticは、tという証明を書いて、その型の命題を仮定に追加するものでした。今回の assert (命題) は、「(命題)が成り立つので仮定に足してくれ！証明は今からやる！」とCoqさんに伝えるものです。
assertすると、メインの証明はいったん脇に置いておいて、assertされた命題の証明モードに入ります。ゼロを足しても値は等しい、というのは流石に標準の定理にあって、SearchAbout (_ = _ + 0). するとすぐ見つかりますので、それをapplyすれば証明完了。
apply plus_n_O.
証明が１行で書ける場合は
assert (S x = S x + 0) by apply plus_n_O.
と assert 〜 by でまとめて書いちゃうこともできます。
- assert P.
- メインの証明のことは一端忘れて、P を証明するモードに入る。終わったら、メインの証明のなかで P を仮定として使えるようになる
- assert P by tac.
- Pの証明が1行で書ける場合。Pを仮定に追加。
- cut P.
- assertと順番が逆になったもの。ゴールが "P->今のゴール" に変わる。ただし、それが終わった後にPの証明をしないといけない。
assertで脇道にそれましたが、無事に仮定が増えて、こうなっているはずです。
H0: S x = S x + 0 ------------------------- S x < S x + S x
ここで、「"S x" は "S x + 0" に等しいとわかっているんだから、ゴールにある "S x" は "S x + 0" に書き換えてよ！」とCoqさんに伝えるtacticが、rewrite。
rewrite H0 at 1.
"at 1" は"１個目の" S xを書き換えてね、の意味です。これを指定しないとゴールが(S x + 0) < (S x + 0) + (S x + 0) に全部変わってしまって困ります。"at 1" なら
------------------------- S x + 0 < S x + S x
狙い通りにこの形になってくれるので、使いたかったライブラリ定理 plus_lt_compat_l : forall n m p: nat, n
apply plus_lt_compat_l.
ゴールが 0 < S x に変わりますが、SearchAbout (0 < S _). で、ピッタリの定理が見つかります。
apply lt_O_Sn. Qed.
まとめ。
- rewrite H (at p1 p2 ....)
- e1 = e2 の形の仮定 H があるときに、ゴールの中のe1をe2に書き換え。at ... があるときは、指定した番号のe1のみを書き換え。
- rewrite <-H.
- e1 = e2 の仮定 H を使って、逆向きに、e2をe1に書き換え
- rewrite (<-)H in H1.
- ゴールじゃなくて別の仮定H1の中を書き換え
- replace e1 with e2.
- まず、e1=e2を証明するモードに入る。証明できたらゴールの中のe1をe2に書き換え。
- replace e1 with e2 by tac.
- tac 1行でe1=e2を証明。さらに、ゴールの中のe1をe2に書き換え。
自然数とリスト: 自動証明 (3.3)
Coqさんは非常に賢いので、実は、今回くらいの証明は自動でやってくれます。
Proof. intros. omega. Qed.
omega はプレスバーガー算術という美味しそうな名前の理論の簡易全自動ソルバーで、整数に関する等式や不等式のかなりの部分を自動的に証明してくれます。
- omega
- 整数/自然数の、足し算引き算や定数倍に関する、等式や不等式を自動証明。変数と変数の掛け算があると使えない。
- ring
- 足し算引き算掛け算に関する等式を、単に式を整理することで自動証明。不等式は使えない。
- field
- 足し算引き算掛け算割り算に関する等式を、単に式を整理することで自動証明。不等式は使えない。
- fourier
- 実数に関する線形不等式の自動証明
自然数とリスト: 帰納法 (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)でやります。
自然数とリスト: 帰納法の色々 (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.
あとはさっきと同様。
自然数とリスト: exists (3.6)
ここまで forall, ->, and, or, not のCoqでの使い方を見ました。Wikipediaの一階述語論理のページなどを見てみると、もう一種類、この手の論理結合子があります。∃（存在する）。Coq では、exists と書きます。
Theorem even_or_odd: forall (n:nat), exists m, (n=2*m \/ n=2*m+1). Proof. induction n.
「どんな自然数 n に対しても、自然数 m が存在して、(n=2*m \/ n=2*m+1) を満たす」。こういう「これこれこういう値が存在します」という主張の定理を書くために使います。
証明してみましょう。帰納法でやります。induction n。
0の場合とそれ以外の場合にゴールが分かれますが、まずは0の方から。nを0に置き換えた
------------------------------- exists m:nat, 0=2*m \/ 0=2*m+1
これを証明しないといけません。どうしましょう。existの正体を見てみると Coq.Init.Logic.ex:
(* Remark: exists x, Q denotes ex (fun x => Q) ... *) Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P.
これも Inductive な命題です。exists x, P を証明するための公理は「"具体的な値 x" と "P x の証明" があれば、ex P が証明できる」という ex_intro。要するに、「Pであるようなxが存在する」を証明するには、具体的にそのxの値を人間が思いついて、Coqさんに教えてあげないといけません。
今回の場合、0=2*m \/ 0=2*m+1 を満たすような m は… m=0 とすれば成り立ってますね。これを Coq に教える tactic は、命題の記述と同じなのでちょっとややこしいですが、exists です。
exists 0.
これで、ゴールが 0=2*0 \/ 0=2*0+1 に変わります。あとは簡単。
left. simpl. reflexivity.
exists 0. の代わりに、Inductiveなゴールの証明の仕方の基本通り、"apply コンストラクタ" で書くこともできます: apply (ex_intro _ 0). が、やや面倒なのでexists tacticを使うのがよいと思います。
帰納法のもう一つのケースはこちら。
n : nat IHn : exists m : nat, n = 2 * m \/ n = 2 * m + 1 -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
今度は仮定の方にもexistsが出てきますが、Inductiveなものが仮定にでききたらdestruct IHn. こう変わります。
n : nat x : nat H : n = 2 * x \/ n = 2 * x + 1 -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
「ほにゃららな自然数 m が存在する」という仮定を、「自然数 x がある」「x はほにゃららを満たす」と分解してくれます。
仮定 H がまだ \/ の形なのでさらに分解 destruct H. すると、ゴールが２つに分裂して、１つめはこう。
H : n = 2 * x -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
さて、n=2*x という仮定の下で、m をどうすれば S n = 2 * m \/ S n = 2 * m + 1 が成り立つようにできるか。ここはうんうん唸って考えましょう。m=x とすれば、∨の右側が成り立ちます。
exists x. right. omega.
もう一つのゴールは
H : n = 2 * x + 1 -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
こうですが、今度は、m=x+1 とすると、左が成り立ちます。
exists (x+1). left. omega. Qed.
まとめ。
- exists e.
- exists x, P という形のゴールを示すときに、x=e とすれば示せますよ！と具体的な値をCoqさんに教える方向で証明する。
たぶん、Coqを使った証明で一番直接的に難しいのは、exists の証明です。これを証明するには、具体的にどの値を当てはめれば成り立つのか、完全に人間が考えてあげないといけません。今回だと、こっちの場合はm=xで行ける、こっちだとm=x+1…と言った具合に。数学の教科書などでは「十分大きな x を取れば P x が成り立つから exists x, P x」のような言い方をしたりしますが、こういう時でも、十分大きい x とは具体的にいくつなのか、100なのか65536なのか無量大数なのか、中身が実際に証明できる大きさを明確に書く必要があります。
などは、直感的には対して難しくない定理なはずなんですが、この難しさのせいで結構な難問になってるように思います。
適度な練習問題としては、さきほども紹介しましたが、
などなど。
Setバージョン
前回、A∨B には、よく似た意味の {A}+{B} というものがある、という紹介をしました。違いは、前者が Prop で後者が Set なことですが、証明の仕方はだいたい同じです。exists x, P にも同じ関係の {x | P} という Set バージョンがあります（Coq.Init.Specif.sig）。
などに登場します。この問題の
Definition tails {A:Set} (ys: list A) : {xss | all_suffixes xss ys}.は、だいたい
Theorem tails: forall (A:Set) (ys: list A), exists xss, all_suffixes xss ys.
と同じ意味です。証明も全く同じく、exists と destruct でできます。違いは、{_}+{_} の場合と同じく、「ゴールがSetのときはPropをdestructできない」という制約のみ。この制約の意味するところについては、次回ご紹介したいと思います。
自然数とリスト: まとめ (3.7)
駆け足でいろいろ紹介しました。
- SearchAbout でライブラリを検索
- 自然数やリストはInductiveなデータ
- = に関する証明 reflexivity, symmetry, transitivity, discriminate
- = を使った書き換え rewrite, replace
- 計算をすすめる simpl, cbv, ...
- 自動証明 omega, ring, field, ring_simplify, field_simplify
- 帰納法 induction
- intro しすぎにご用心。generalize
- 整礎帰納法
- exists
当初の予定では3回くらいにわけるつもりだったんですが、めんどくさくなったので一気に書いてしまうことにしました。駆け足すぎてよくわからなくなってしまってると思いますが、他の入門記事やチュートリアルなどと併用してください（いい加減になってきた…）。ではでは。
追伸
そういえば、このシリーズでは intros や destruct では自分で仮定に名前をつけることはせずに、Coqの自動生成にまかせちゃっているんですが、これって、コーディングスタイルとしては良くないのかもしれません。ということにさっき気づきました。H0 やら H1 やらではよく分からないですよね。本当は、ちゃんと名前をつけて intros 等した方がいいと思います！
