Coqで遊ぶその3: forall について / 色々な証明戦略を試す

forall についての雑文

さて、ここで教科書の Coq in a Hurry に戻ると、私が作った「風が吹く」「桶屋が儲かる」なんかの命題を Variable で定義する代わりに、forall というキーワードを使っています。つまり、

Variable 風が吹く 桶屋が儲かる : Prop.
Theorem 風桶 : (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる

の代わりに

Theorem 風桶 : forall 風が吹く 桶屋が儲かる:Prop, (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる.

とやっても、だいたい同じように証明できるという事です(intro が二つ余分に必要です)。ではそもそも forall とは何でしょうか？ forall とは、universal quantifier (全称記号)といって、「すべての何とか」を表す記号だそうです。しかし、「すべての『風が吹く』」って全く意味が通じませんね。私は小学生の頃この全称記号という物を知って、未だにちゃんと理解できないので、もう直感的な理解は諦めて、使い方だけ覚える事にしました。

forall とは、let みたいな物だと思います。let とは、let x := 1 in x + 1 のように、ある式の中だけで一時的に使える変数を作るものです。forall と let の違いは次の通りです。

forall の一時変数は型だけ指定されている。let の一時変数は型と具体的な値が指定されている。
forall の結果は Prop だけ。let の結果はどんな型でも OK.

ここで脱線しますが、Coq in a Hurry の 5 ページにすごい事が書いてあります。「forall x:A, P x」のように書く命題は、実は関数の型としても考えられるそうです。forall は、沢山の命題を纏めたものだと考える事が出来るので、どれか一つ具体的な値を選ぶと一つの命題が取り出せるからです。実際に forall の式を型だと見なして実験してみます。

Coq < Variable f : (forall x:nat, 0 <= x).
Warning: f is declared as a parameter because it is at a global level
f is assumed

Coq < Check f 1.
f 1
     : 0 <= 1

つまり関数型の記法で書くと、「forall x:A, P x」は「x:A の時 A -> P x」なのです。こ、これって滅茶苦茶すごくないですか？つまり、「値」である x が、「型」である P x の一部になってしまったのです。つまり型もまた値である事を示しています。なんというオブジェクト指向！この話はどんどん掘り下げたいですが、この辺で脱線終わりにします。

色々な証明戦略

もう一度 Coq での証明の手順について纏めます。

Coq の分かる形で命題を式に直す。
Theorem コマンドで証明モードに入る。
既知の事実(前提)は === の上に、未知の事実(ゴール)は下に表示される。
証明モードの目的は、戦略コマンドと前提を使ってゴールを分解して未知の事実を無くす事です。

前回の証明では intro と apply しか使いませんでしたが、マニュアルを見ると山ほどあります。http://alohakun.blog7.fc2.com/blog-entry-276.html に分かりやすい解説があって助かりました。簡単に言うと、-> ~ /\ \/ のそれぞれの要素に「導入」と「除去」という操作があって、ゴールをどんどん小さくして行けば良いです。

導入ゴールを使って前提を追加する操作。
除去前提を使ってゴールを変形する操作。

コマンドの説明。

intro :
- (->導入) ゴールが A -> B の時、A を前提に加えゴールが B だけになる。
  - A -> B は、もしも A だったら。。。という意味なので、どんだけあり得なくても A を前提に出来る。
- (~導入) ゴールが ~A の時、A を前提に加えゴールが False になる。
  - ~A とは、A が成り立たないという意味なので、A を前提に加えるとゴールが成り立たなくなる(?).
- (forall導入) ゴールが forall x : A, Y の時、x : A を前提に加えゴールが Y になる。
  - 全ての x : A は仮定なので、とりあえず前提に出来る。
apply :
- (->除去) ゴールが B の時、前提に A -> B があると、ゴールが A になる。
  - A なら B という事が分かっているので、A を証明出来たら B も証明出来るはず。
- (forall除去) ゴールが P x の時、前提に forall x, P x があるとゴールが証明される。
  - 全ての場合に置いて P x が成り立つから。
split :
- (/\導入) ゴールが A /\ B (A かつ B) の時、A と B それぞれを二つのゴールに分ける。
  - A と B を別々に両方証明出来たら A かつ B も証明出来ると言える。
elim :
- (/\除去) ゴールが X の時、前提に A /\ B があると、ゴールが A -> B -> X になる。
  - A かつ B が分かっているので、A と B の両方を前提に加える事が出来る(後で intro を使ってゴールから前提にもって来る)。
- (\/除去) ゴールが X の時、前提に A \/ B があると、A -> X と B -> X の二つのゴールが出来る。
  - A または B のどちらかが真のとき X が成り立つなら、A -> X と B -> X の両方とも成り立つはず。
- (~除去) ゴールが X の時、前提に ~A があるとゴールが A になる。
  - もしも前提に A があれば、前提に A と ~A の両方存在する事になるので、X が何であっても成り立つ???
left :
- (\/導入左) ゴールが A \/ B の時、ゴールを A にする。
  - ゴールは A の B どちらかなので、A が成り立てば全体が成り立つ。
right :
- (\/導入右) ゴールが A \/ B の時、ゴールを B にする。
  - ゴールは A の B どちらかなので、B が成り立てば全体が成り立つ。

また、以下の便利コマンドもあります。

intros : 出来るだけ沢山 intro する。
destruct : elim; intro. の代わり
Undo : 戻る
Restart : 最初からやり直し

これだけ知っていれば Coq in a Hurry P9 の Exercise 5.6 が全部解けます。慣れれば全然頭を使わずによくも悪くもゲーム感覚で出来ます。気持ちいー！！！こんなに面白いのに、なんでみんなやらないのか謎です。参考までに問題も載せます。

コツ

とりあえず intros でざくっと前提を増やす。
ゴールを減らす(除去)より、導入を増やす(導入: intros や destruct)を先にすると楽

Theorem ex561 : forall A B C : Prop, A/\(B/\C) -> (A/\B)/\C.
Theorem ex562 : forall A B C D : Prop, (A->B)/\(C->D)/\A/\C -> B/\D.
Theorem ex563 : forall A : Prop, ~(A/\~A).
Theorem ex564 : forall A B C : Prop, A\/(B\/C) -> (A\/B)\/C.
Theorem ex565 : forall A : Prop, ~~(A\/~A).
Theorem ex566 : forall A B : Prop, (A\/B)/\~A -> B.
Theorem ex567 : forall A:Set, forall P Q:A->Prop, (forall x, P x)\/(forall y, Q y)->forall x, P x\/Q x.