工学部専門科目「計算と論理」

日時	火曜日2限(10:30～12:00)
場所	総合研究７号館情報１
担当教員:	五十嵐淳
オフィスアワー:	火曜日 17:00～18:00 (総合研究7号館224)
	(その他の時間は要アポイントメント)
担当TA:	村瀬唯斗(通信情報システム専攻Ｄ２)

お知らせ

2024年度ページ立ち上げ(2024.9.26)

講義内容

数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．

講義スケジュールと配布資料

回数	date	内容(予定)	資料	宿題
1	10/1	導入, Basics.v	スライド0, スライド1	Coq 環境の構築，テキストのダウンロード
2	10/8	Basics.v, Induction.v
3	10/22	単純型付ラムダ計算
4	10/29	単純型付ラムダ計算(つづき)
5	11/5	Lists.v
6	11/12	Poly.v
7	11/19	多相ラムダ計算 System F
8	11/26	演習	(範囲: 問題集1～3節)
9	12/3	Tactics.v
10	12/10	Logic.v
11	12/17	自然演繹と Coq
12	12/24	IndProp.v
13	1/7	カリーハワード同型対応，ProofObjects.v
14	1/14	演習	(範囲: 問題集全部)
期末試験	?

自習の進め方(宿題について)

教科書の該当する章のファイルを Proof General (もしくは CoqIDE) で読み込む．
Coq への読み込みコマンドを使いながら教科書を読み進める．
練習問題の指示に従ってファイルを書き換える(解答を埋める)．
- (* FILL IN HERE *) Admitted. の行を消して，証明を書く． (最初の方の問題について書くべき「証明」は決まっている．)
- わからない問題については，Admitted. を残しておく．(証明途中で詰まった場合でも，全部消さずに，最後に Admitted. を書いておく．)
Coq に読み込ませてみて，背景が青(緑)になれば無事に Coq のチェックに通った，ということ．ただし， Proof General, CoqIDE は Qed. の打ち忘れ(よくある!)を関知してくれないので，make XXXX.vo (XXXX.v をチェックするなら)を実行するか CoqIDE で Compile → Compile Buffer を実行して再確認してください．

FAQ

Proofgeneral だと通る証明なのに，make など coqc を通すとエラーになります．
主な理由はふたつあります．
1. Proofgeneral と coqc では字句解析のやり方がちょっと違っています．Proofgeneral はピリオドまでをひと区切りとしますが，coq はピリオドの後の文字もピリオドとつなげたひとつのトークンとする場合があります．ピリオドの後に空白を入れると直ることが多いです．
2. どこかの Proof. を Qed. や Admitted. で閉じ忘れている可能性があります．
Windows の CoqIDE で Compile buffer をしても成功・失敗がよくわかりません．
Windows の CoqIDE には，compile buffer が失敗しても何もメッセージを返さない，というバグがあるらしいです．(長い間放置されているバグ報告)
Mac に Coq をインストールしようと思い INRIA から coqide-8.X.Y.dmg をダウンロード・マウントして，起動してみましたが，「…は壊れているため開けません．ディスクイメージを取り出す必要があります」などと言われてしまいます．どうしたらよいでしょう．
Mac OS のセキュリティ設定の問題で，ダウンロードしたファイルを実行しようとした時に表示されるようです．「システム環境設定」の「セキュリティとプライバシー」を起動し，「一般」タブのところにある［ダウンロードしたアプリケーションの実行許可］欄で［すべてのアプリケーションを許可］を選択してから実行してみてください．
Require Export .... でエラーが出ます．
Error: Compiled library XXXXX.vo makes inconsistent assumptions over library Coq.Init.Notations というエラーが出る場合，ここで読み込もうとしているファイルを再コンパイルして .vo ファイルを作り直してください．それでも発生するようなら，再コンパイルした時の coqc と， Proofgeneral/CoqIDE から呼んでいる coqc のバージョン違いの可能性があります．(特に，brew, opam, INRIA からダウンロードした Coq が混在している場合は要注意です．CoqIDE の人はメニューで Compile → Make を使うのがよさそうです．Proofgeneral の場合，メニューから Coq → Auto Compilation → Compile Before Require にチェックを入れておくと吉です．) あと，The file /Users/admin/Desktop/Coq/XXXXX.vo contains library Top.XXXXX and not library XXXXX の場合，配布した Makefile が壊れている可能性があります．配布した教科書に含まれている Makefile で上書きしてください．
Compute や Check コマンドなどを .v ファイルに書くと警告 ``Warning: query commands should not be inserted in scripts.'' が出るのですが．(CoqIDE の場合…かな？)
無視してください :-) これらのコマンドは，証明をしている最中に式の計算をしたり型を調べるためのもので，直接証明に貢献していないという意味で無駄な記述なので，そういう警告が出ることになっています．
simpl を省略して解答を行った場合，演習上・採点時の不都合はありますでしょうか？
採点時には基本ないです．演習上，ということであれば，式が複雑なまま考えないといけないので，あんまり我慢する意味はないかな，と思います．
CoqIDE で Coqtop died badly. Resetting. というメッセージがでてうまく動作しません．
Require Export .... で CoqIDE がハングします．
CoqIDE は日本語を含むパス(上位を含めたフォルダ名)がうまく扱えないようなので，Coq のインストールパス，教科書のファイルのパスに日本語が含まれないようにしてみてください．それでもだめなら我々に連絡を!

Proof General, CoqIDE の操作

機能	Proof General	CoqIDE (メニュー操作)
一歩読み進める(Coq にテキストの内容を送信)	C-c C-n	Navigation → Forward
一歩戻る (undo)	C-c C-u	Navigation → Backward
カーソル位置まで進む(戻る)	C-c RET	Navigation → Go to
ファイル末尾まで読み込む	C-c C-b	Navigation → End
証明すべき命題(ゴール)を表示	C-c C-p
既になされた証明・定義を表示	C-c C-t
SearchAbout	C-c C-a C-a	Queries → SearchAbout (F2)

リソース

教科書

Benjamin C. Pierce 他著 Software Foundations シリーズ第1巻 Logical Foundations (この本家版は時おりバージョンアップがあるので使わないでください．)

参考書

ボランティアによる教科書の和訳版(元になった版は2011年版です．内容の食い違いについては教科書の記述を優先します．)

Coq: INRIA の公式サイト

ProofGeneral

emacs から Coq を操作するためのソフトウェア．

Company-Coq

ProofGeneral の拡張集． forall と打つと ∀ で表示されたりするのでうれしい．自動補完などもできる．

coquille

vim から Coq を操作するためのソフトウェア．(使ったことありません．動作報告求む．)

Coqoon

Eclipse から Coq を操作するためのプラグイン．(使ったことありません．動作報告求む．)

vscoq

Visual Studio Code から Coq を操作するためのプラグイン．(使ったことありません．動作報告求む．)

五十嵐淳