いざべる!!

定理証明系(関数型言語でプログラムを書くと、そのプログラムについてなんかの性質を証明できるよ!証明が正しいかどうかはコンピュータがチェックしてくれるよ!証明は大変だけど、多少はコンピュータが手伝ってくれるよ!)だと、国内ではCoqとかAgdaとかが流行ってるみたいですけど、天邪鬼な私はIsabelle/HOLで遊ぶよ!

まずはインストールから。Macだよ。

http://www.cl.cam.ac.uk/research/hvg/Isabelle/

ごちゃごちゃ考えずに、上のサイトからダウンロードするのが良い。Isabelle2009-2とかいうアプリケーションを起動すると、Aquamacsが起動するので、\で円マークが入らないように設定する。elispをコピペしたら、なんかバックスラッシュが\になっちゃったので、適当にぐぐってください。これをやらないと、いろいろ入力できなくて発狂します。

これが一番良い方法かは知りません。でもとりあえず動くよ。こないだつくばに行ったときに先生に聞いてみたら、XでEmacs使ってるとか言ってました。

Aquamacsのメニューから「Proof-General→Options→X-Symbol」にチェック入れておく。これで「\<longrightarrow>」とか書いてスペース押すと→になったりする。

Documentationのページの

  • Tutorial on Isabelle/HOL
  • Tutorial on Isar

くらいにざっと目を通しておく。正直に言うとあんまり通してません。

日本語の資料だとIsabelle/HOLを用いた定理証明入門というのがある。

で、練習問題はあなぷるを見る。Coqだからちょっと嫌だけど、がんばる。

http://as305.dyndns.org/aps/problem/view/1

lemma "(P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q"
proof
  assume pq: "P \<longrightarrow> Q"
  from pq have "P \<longrightarrow> Q".
qed

多分これで同じ意味になってるんじゃないだろうか。


二番目のFalsoからいきなり難しそうになったので、諦めました。もう寝る時間だしー。

あと全体的にどの記号をどうやって入力するのかがわかりません。困った。