前回の Coq はいきなり難しすぎました。forall とか、数学やってる人には常識なのかも知れないけど一介のプログラマには高度すぎます。ikegami さんに単純な例 http://www.youtube.com/watch?v=f9XOdpmeJ0o を教えてもらったんだけど同じじゃつまらないのでちょっと変えてやってみます。
- 風が吹く -> 桶屋が儲かる
- 風が吹く
- 以上の二つが成り立つ時、「桶屋が儲かる」が成り立つ。
矢印 -> は、条件と結果を現す記号です。「としたら」とか、「ならば」のように読みます。ここで一体何を証明しようとしているのか確認するのは大切だと思うので強調しますが、ここでは「風が吹く -> 桶屋が儲かる」こと自体を証明しようとしているわけではありません。もしも「風が吹く -> 桶屋が儲かる」と「風が吹く」の二つが正しいとしたら、「桶屋が儲かる」も正しいと言う事、つまり、
- (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる
が証明する式です。
Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Section 風桶の証明 (* 一応スコープを作って中を区切ります。*). Coq < Variable 風が吹く 桶屋が儲かる : Prop (* 必要な二つの要素を宣言。*). 風が吹く is assumed 桶屋が儲かる is assumed Coq < Theorem 風桶 : (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる (* これから証明モードに入ります。 === の上に今知ってる仮定、下に証明したい式(ゴール)が表示されます。 いわば上にあるのが持ち物で、下にあるのが今からやっつける敵と考える事も出来ます。 仮定のうち、: の右側に書いてある奴が実際使える物です。 最初に定義した要素が二つ上に表示されていますが、これは : の左側なので証明には使えません。*). 1 subgoal 風が吹く : Prop 桶屋が儲かる : Prop ============================ (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる 風桶 < intro (* intro という命令を使うと、ゴールにある -> が分解されて頭の部分が仮定に加わります。 いわば敵を分解して持ち物に加えるわけです。 この結果「風が吹く -> 桶屋が儲かる」という仮定を使えるようになります。*). 1 subgoal 風が吹く : Prop 桶屋が儲かる : Prop H : 風が吹く -> 桶屋が儲かる ============================ 風が吹く -> 桶屋が儲かる 風桶 < intro (* もう一度 intro を使うと、 さらに「風が吹く」という仮定を使えるようになります *). 1 subgoal 風が吹く : Prop 桶屋が儲かる : Prop H : 風が吹く -> 桶屋が儲かる H0 : 風が吹く ============================ 桶屋が儲かる 風桶 < apply H (* apply を使うと、獲得した仮定を使う事が出来ます。 いわば持ち物を使っていよいよ敵をやっつけるわけです。 この場合、H の「風が吹く -> 桶屋が儲かる」とゴールの「桶屋が儲かる」がマッチします。 論理を逆転して -> の後ろからマッチさせてゆきます。*). 1 subgoal 風が吹く : Prop 桶屋が儲かる : Prop H : 風が吹く -> 桶屋が儲かる H0 : 風が吹く ============================ 風が吹く 風桶 < apply H0 (* 今度のゴールは H0 とぴったりマッチするので、これで証明は終わりです。*). Proof completed. 風桶 < Qed (* Theorem モードを閉じて、最後に戦いの成果を振り返りましょう。*). intro. intro. apply H. apply H0. 風桶 is defined Coq < Print 風桶 (* Coq は命題を型、証明を関数だと考えています。 上の操作は関数を直接作る代わりに、人間に分かりやすい証明の言葉で作ったわけです。 Print を使うと Coq が実際に内部でどんな証明を作ったか分かります *). 風桶 = fun (H : 風が吹く -> 桶屋が儲かる) (H0 : 風が吹く) => H H0 : (風が吹く -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる Coq < End 風桶の証明 (* Section スコープを閉じます。スコープを閉じても「風桶」の定義は残ってますが、 Variable で宣言した「風が吹く」や「桶屋が儲かる」は残らないので、 Print で表示される結果はちょっと変わります *).
参考
以下、蛇足だとは思いますが正式な証明です。
Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Section 風桶の証明. Coq < Variable 風が吹く 土ぼこりが立つ 盲人が増える 三味線が売れる 猫が減る ネズミが増える 箱が齧られる 桶屋が儲かる : Prop. 風が吹く is assumed 土ぼこりが立つ is assumed 盲人が増える is assumed 三味線が売れる is assumed 猫が減る is assumed ネズミが増える is assumed 箱が齧られる is assumed 桶屋が儲かる is assumed Coq < Theorem 風桶 : (風が吹く -> 土ぼこりが立つ) -> (土ぼこりが立つ -> 盲人が増える) -> (盲人が増える -> 三味線が売れる) -> (三味線が売れる -> 猫が減る) -> (猫が減る -> ネズミが増える) -> (ネズミが増える -> 箱が齧られる) -> (箱が齧られる -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる. 1 subgoal 風が吹く : Prop 土ぼこりが立つ : Prop 盲人が増える : Prop 三味線が売れる : Prop 猫が減る : Prop ネズミが増える : Prop 箱が齧られる : Prop 桶屋が儲かる : Prop ============================ (風が吹く -> 土ぼこりが立つ) -> (土ぼこりが立つ -> 盲人が増える) -> (盲人が増える -> 三味線が売れる) -> (三味線が売れる -> 猫が減る) -> (猫が減る -> ネズミが増える) -> (ネズミが増える -> 箱が齧られる) -> (箱が齧られる -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる 風桶 < intros. 1 subgoal 風が吹く : Prop 土ぼこりが立つ : Prop 盲人が増える : Prop 三味線が売れる : Prop 猫が減る : Prop ネズミが増える : Prop 箱が齧られる : Prop 桶屋が儲かる : Prop H : 風が吹く -> 土ぼこりが立つ H0 : 土ぼこりが立つ -> 盲人が増える H1 : 盲人が増える -> 三味線が売れる H2 : 三味線が売れる -> 猫が減る H3 : 猫が減る -> ネズミが増える H4 : ネズミが増える -> 箱が齧られる H5 : 箱が齧られる -> 桶屋が儲かる H6 : 風が吹く ============================ 桶屋が儲かる 風桶 < apply H5. (* 以下 apply H4, apply H3, ... と続くけど省略 *) 風桶 < apply H6. Proof completed. 風桶 < Qed. intros. apply H5. apply H4. apply H3. apply H2. apply H1. apply H0. apply H. apply H6. 風桶 is defined Coq < Print 風桶. 風桶 = fun (H : 風が吹く -> 土ぼこりが立つ) (H0 : 土ぼこりが立つ -> 盲人が増える) (H1 : 盲人が増える -> 三味線が売れる) (H2 : 三味線が売れる -> 猫が減る) (H3 : 猫が減る -> ネズミが増える) (H4 : ネズミが増える -> 箱が齧られる) (H5 : 箱が齧られる -> 桶屋が儲かる) (H6 : 風が吹く) => H5 (H4 (H3 (H2 (H1 (H0 (H H6)))))) : (風が吹く -> 土ぼこりが立つ) -> (土ぼこりが立つ -> 盲人が増える) -> (盲人が増える -> 三味線が売れる) -> (三味線が売れる -> 猫が減る) -> (猫が減る -> ネズミが増える) -> (ネズミが増える -> 箱が齧られる) -> (箱が齧られる -> 桶屋が儲かる) -> 風が吹く -> 桶屋が儲かる Coq < End 風桶の証明.
