定理証明言語『LEAN』
以前の記事で述べたプラトンの三段論法を改めて記します。
- ソクラテスは人間である
- 人間はすべからく死ぬ
- ソクラテスは死ぬ
今回はこれをプログラムによって証明したいと思います。
証明器『Glaceon』の説明
まずは下記の証明エリアをご覧ください。
※実際の証明はこの記事の次の項目で行います！
下の証明器はGlaceonと読んでいて、ふれぁがLEANを使って作ったものです。
それぞれのエリアはそれぞれ下記の役割を持っています。
- 証明器の左エリア ： 実際に証明を書く場所
- 証明器の右エリア ： 現在の証明状況を表示
- 証明器の右エリア下部： 問題の証明完了表示
証明器右下は “Solved!” か “not solved yet…” のいづれかになっていれば、解けたかどうかの判定がLEANによって行われた状態です。もしどちらでもなく、 “checking…” の表示となっていれば現在判定中であることを知らせます。その場合はしばらくお待ち下さい。
証明を行う際は右エリアを見ながら左エリアの中で証明を書いていくことなります。
証明記述エリア
左エリアの中を少し説明しましょう。
左エリアの中は点線で上部と下部に分かれていて、このうち上部は使用できる命題などの世界を管理しているので、特に絶対に触らないでください。
variables Socrates human is_mortal : Type
------------------------------------------------------
(...)※webの技術力がなくて物理的に書き換えない出来ないように出来ませんでした。。
“theorem” のワード以降が命題（または定理、補題）の主張となります。
/-- La Mort de Socrate -/
theorem La_Mort_de_Socrate
(Socrates_is_Human : Socrates -> human)
(Human_is_Mortal : human -> is_mortal)
: Socrates -> is_mortalそして “begin” と “end” で囲まれた部分が、実際に証明を記述する部分となります。この範囲より外を書き換えるのはルール違反です。
:= begin
-- この中に証明を書いてください
sorry,
end基本的に “begin” と “end” で囲まれた範囲は、デフォルトでsorryが最初から書かれています。
これは、証明が完了していない状況でエラーを一時的に回避するための特殊コマンドです。エラーは証明の完了・未完了とは別であって、エラーはいかなるときでも必ず回避しなければなりません。エラー状態では必ず証明未完了の判定となります。
今後、”sorry” コマンドは証明の記述中に最もお世話になると思います。
適当な意味のない文字を証明記述エリアに書き込んでみてください。Glaceonが証明を理解出来ずにエラーが出てしまう場合は証明記述エリアでエラーが発生している箇所が示されるはずです。
※証明に用いるためのコマンド（=tacticsと呼ばれる）はたくさん存在します。今後、この豊富なtacticsを用いて様々な数学の定理を証明していくことになるでしょう。
最後に現在の証明状況表示エリアの表示確認を行ってみましょう。
証明記述内の “– この中に証明を書いてください” にテキストカーソルを合わせてみてください。カーソルを合わせると右の表示エリアに以下のような表示がされるはずです。
[現在の証明状況]
------------------------------------------------------
Socrates human is_mortal : Type,
Socrates_is_Human : Socrates → human,
Human_is_Mortal : human → is_mortal
⊢ Socrates → is_mortal詳細は後ほど述べますが、記号 “⊢” の段が証明すべき主張で、それより上の段に書かれているものが、現在手元に存在している仮定になります。
この場合、証明状況は以下のように還元されます：
[ 仮定 ]
- Socrates、human、is_mortal（型として宣言）
- Socrates_is_Human（命題）
- Human_is_mortal（命題）
[ 主張 ]
- Socrates → is_mortal（命題）
この証明状況を言葉で言い換えると、「ソクラテスは人間」、「人間ならば死ぬ運命」の仮定から、「ソクラテスは死ぬ運命」の命題を証明せよということです。
Glaceonを利用した実際の証明の記述については続きの記事で述べたいと思います！
(No liked Yet)