Ubuntu で『ソフトウェアの基礎』を読む
この記事は Ubuntu 14.04 上に Proof General と Coq をインストールし、Emacs から『ソフトウェアの基礎』を読む（実行する）ためのメモです。日本語の解説記事が見つからなかったので書きました。なお、筆者は Coq や Proof General に関して素人なので、誤りなどがありましたらご指摘いただけると幸いです。
Proof General と Coq のインストール
Emacs はインストールしてあるものとします。Proof General と Coq は以下の apt コマンドでインストールできます。
sudo apt install proofgeneral coq補足: apt-get install ではなく apt install となっているのは誤りではありません。Ubuntu 14.04 から「aptコマンド」が使えるようになりました。詳細はこの記事をご参照ください。(2014/09/03 追記)
注意: 2014年8月31日現在、apt でインストールした Proof General のバージョンは 4.3pre130510 です。開発版は 4.3pre131011 のようですが、この記事では無視します。一方、インストールした Coq は 8.4pl3 ですが、最新版は 8.4pl4 です。8.4pl3 には重大なバグがあり、8.4pl4 で修正されたそうですが、近日中に 8.5 がリリースされる予定 (pdf) ということもあり、この記事では面倒を避けて古いものをそのまま使います。最新版を使いたいという方は以下の記事などをご参照ください。
『ソフトウェアの基礎』のソースをダウンロードして解凍
有志による日本語訳はこちらの「ソース」からダウンロードできますが、最終更新日が2011年6月とやや古いので、原文の方を以下のリンクからダウンロードします。なお、原文のバージョンは現時点で 3.1 (July 2014) です。
ダウンロードしてきたファイルを適当に解凍します。
tar zxvf sf.tar.gzテキストを読んで実行
それでは、動作確認のために解答したフォルダの中の Basics.v を Emacs で開きます。
光栄にも将軍が我々を歓迎してくれました。閣下のご尊顔を拝していると、Basics.v のバッファに自動で切り替わります。自動で移動しない場合は手動でバッファを切り替えてください。なお、環境によっては Proof General のツールバーが表示されているはずです。
ふむふむと読んでいって Exercise 1 まで進めたとします。おんどりの導くままに正解と思うコードを入力し、そのコードの下あたりにカーソルを移動させたら、おもむろに C-c C-return を押します（つまり Ctrl を押したまま c を押し、次に Ctrl を押したまま Enter を押す）。
すると、カーソルより上の画面の背景の色が変わり、上図のように画面が3分割されます。一番下の画面 *response* に nandb is defined と表示されていればとりあえずOKです。文法などに誤りがある場合は *response* にエラーメッセージが表示されますので、コードを修正しましょう。
次に、自分で定義した nandb が正しいか確かめましょう。Exercise 1 の下に Example と (* FILL IN HERE *) Admitted. からはじまる文が並んでいます。本文に従って (* FILL IN HERE *) Admitted. を Proof. reflexivity. Qed. に書き換えたら、それらの行の下付近にカーソルを移動させて、再度 C-c C-return を押します。
自分で定義した nandb が正しければ背景の色が変わり、*response* には何も表示されません（あるいは test_nandb4 is defined などと表示されます）。nandb に誤りがあれば、エラーが出力されます。例えば以下のような:
Toplevel input, characters 0-11:
Error: Impossible to unify "true" with "nandb false false".
どうやら Example test_nandb2 でエラーが起きたようです。このテストが通るように nandb を書き直したら、再度 C-c C-return を押して正しさを確認しましょう。
まとめ
以上のように、『ソフトウェアの基礎』を読んで実行するときは、実行したい行にカーソルを移動させて C-c C-return を押せば大体やりたいことが実現できます。Check や Eval のある行も C-c C-return でOKです。
Proof General には他にも便利な機能がありますので、公式ページのドキュメントなどをご参照ください。よく使うキーバインドはこちらのページにまとまっています。
補足: Basics の中間付近からステップ実行が必須になります。ツールバーを利用してもよいですが、キーボードから操作できた方がなにかと便利ですので、1ステップ進む C-c C-n と1ステップ戻る C-c C-u をぜひ活用しましょう。また、Proof General の機能である Electric Terminator がオンになっていると、ピリオドを入力した際にその部分まで自動的に評価してくれます。機能のオン・オフは C-c . と押すことで切り替えられます。(2014/09/03 追記)
