初心者の目から見たCoq/SSReflect/MathComp
What is this 記事?
この記事はeeic （東京大学工学部電気電子・電子情報工学科） Advent Calendar 2018 その2 18日目に参加しています．
真面目で面白い事が書きたくなったので, Coqの記事を書いてみた
ゴリゴリの情報科学っぽいことを初心者がやってみたよノートなので対象者は限られるかもしれないが, eeicにも興味を持ちそうな人はいるはず
少し変わった世界に触れ, 敷居を低く感じてもらったら嬉しい
はじめに
この記事はほぼこの本[1]の内容を参考にしています.
Coqは証明支援システムの一つである[2]. と言われても何のことだか分からない. OCaml（eeicB4夏の神授業たるプログラミング言語で習う奴）で実装された, 記号論理学ツールだと思って頂ければ多分問題ない.
教養時代に記号論理学を取った人なら少しピンとくるであろう, 矛盾なら全て成り立つとか, 命題だの否定だのを導入したり除去したりする, アレだ. プログラミング言語の範疇には多分入る…と思うが,
そう, どうせ学科の人はverilogだのsqlだの, なんかプログラミング言語ではないらしい何かの概念の概要を知っている人が多いので, プログラミング言語である時点で, ゆるふわで, メジャーで, 受け入れ易くて然るべきだ.
SSReflectはCoqの拡張機能, MathCompはそのライブラリ, と言う立ち位置らしいが, 正直まだピンと来ていない. この記事では, 命題や導入・除去っぽいものを書いてるのがSSReflect+MathCompの文法で, それを正しいとIDE上で解釈している部分がCoqの仕事みたいなふわっとした理解で多分良い.
ちなみに, 真面目な呼び方をすると命題やその証明を書き綴ることは「形式化」, それが正しいと機械に判別させることは「検証」と呼ぶ.
どこがeeicっぽいんですか
計算論
B4夏プログラミング言語
が好きな人は雰囲気がもろ同じだし.
で少しだけ三段論法をフニャフニャするプログラムみたいなのを学ぶのでその関連知識みたいな所がある. また, 入り口は記号論理学めいているが突き詰めると確率や情報理論の定理も形式化出来る（通信路符号化定理もあるよ）ので,
- 情報通信理論
は間違いなく関係あるし, ワンチャン統計的機械学習やアルゴリズムも関連する. これは間違いなくeeic, 完全にeeic.
証明てw何がすごいんですか？
ソフトウェアのコードも要するに大量の計算で, 正しさが証明されるべきであり, 証明されたものは安全である（雑理解）. 故にVerificationという, ソフトウェアの安全性に関わる分野に利用されるし, 元々, 私はセキュリティ系の興味でCoqの存在を知った. ブロックチェーン辺りの安全性の検査の為に流行ったりしてるらしい.
CoqでTLS/SSLを実装したら安全性のキモみたいな部分が分かってOpenSSLの脆弱性を発見できた[3]みたいな, 訳の分からない世界だって存在する.
もうちょっとパンピーのロマンに近付けて話題を持っていくと, 2018年現在もコンピュータの力でしか解けない事で有名な四色定理がある. あまりにも証明が複雑で長いので, Coqでチェックされる事で, まあこの証明は正しいんじゃないかということになっている [4].
（むしろロマンの破壊者では？）
そういえば, Advent Calendarのページには思いっきり「画像処理っぽい何か」と研究の何かを書く予定だったらしき記述があるが, 四色定理の証明は画像を処理しているので, ギリギリ予定通りと言ったところか.
インストール
Mac
恐らくMacに対する環境構築が一番引っかかりやすいし, 私もMacでやったので, そうでない人はこれ[5]で多分出来るので出来てくれ（不親切）. CoqIDEという環境も加えてインストールする. やり方は複数あるがopamというOCamlのパッケージマネージャを使うのが恐らく丸い.
brew install opam
にある奴をopam install coqide.8.7.0 ではなくopam install coqideで行う方法で入れた.
環境はmacOS10.14.1である.
使ってみる
左の窓がスクリプトエリア, 右上の窓がゴールエリア, 右下の窓がレスポンスエリアだ. 基本的にスクリプトエリアに証明を書き, デバッガのように一行ずつ読み込んで行けば, ゴールエリアに, 何が仮定なのか（横線の上部分）, 何がまだ証明されていないのか（下部分）が映るという構造だ.
読み込み方は矢印のクリックで行う, ほぼ直感通りに動くし, やり直しも容易で夢のよう.
文法の解説が結構つらい事に薄々気付き, もう紹介出来ればいいやみたいな雑な気持ちになったので概要だけ説明する.
Hypothesisが仮定でTheoremが証明したいものみたいなのは雰囲気で理解してもらい, ProofからQedまでが証明の記述だという事も雰囲気で理解してもらう. X, Y:Propは, XとYという名前の命題がありますよ程度の意味.
move: というのはタクティクスと呼ばれる手続きで, ここでは「仮定Xと証明したいものYがあった時, Yを(XならばY)に遷移させる」手続きだ. Xが仮定なら, (XならばY)を証明するだけでYは証明されるので正当な手続きだ. よって今画面にはX->Yが証明したいものとして映っている.
次にby という行を読み込ませるが, by はターミネータと呼ばれる処理で, 「証明したいもの」「自明じゃん乙w」って言って削除してくれる. よく見たらX->Yは仮定にあるので, 自明, という解釈だ. これで「証明したいもの」は無くなるので証明は完了する.
やや難しい奴
Coqはデフォルトは直観主義論理らしいので, 排中律を仮定しないと古典論理として動かない. 記号論理学を取った人は, 直観主義論理に加える仮定として, 背理法, 排中律, 二重否定除去は同じ意味を持つ, みたいな綺麗なことをやったと思う.
その「同じ意味」であることを確認する為に, その中のごく一部であるが「直観主義で排中律が仮定されたら二重否定除去も出来る」を証明させる（正確には人間が証明手続きを書きゴールエリアの反応で確かめる）とこうなる.
プラスマイナス記号はただのインデントで意味はない.
move=>hoge は証明したいものがX->Yとかの場合にXにhogeという命題名を付けた上で仮定側に持っていく操作.
move\ hugaは, 仮定hugaがあり, 証明したいものがX->Yの時に, 証明したいものを(huga /\ X) -> Yに変える操作.
case:A\/B は, A\/Bが証明済みである時に, 証明したいものがXならばA->XとB->X両方証明すればいいじゃん的な変形をする操作である. これ以上の説明が苦しくなってきたので雰囲気だけ分かる落書きを貼る.
こんな感じで証明の正しさが分かるらしい. 多分人間より頭のいいことをやっている.
最後に
不完全性定理の証明[6] コピペしてポチポチするだけで記述が変形して証明が進み, 何も分からないけど幸せになれる.
四色定理の証明[7] gitで証明が手に入る時代. ただし複数ファイルのコンパイルが必要で面倒（やり方を調べ中で私にもチョットワカラナイ）.
テキトーな理解を晒しているのであまりスゴイ人に見つかりたくないので技術系なのにqiitaではなく自分のブログに書きました.
とはいえ, 仮にヤベーこと言ってたら是非ともボコボコにして出来れば色々御教授願えればありがたい.
