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

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

お知らせ

2026年度ページ立ち上げ(2026.9.14)

講義内容

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

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

回数	date	内容(予定)
1	10/6	導入, Basics.v
2	10/13	休講
3	10/20	Basics.v, Induction.v
4	10/27	単純型付ラムダ計算
5	11/10	単純型付ラムダ計算(つづき)
6	11/17	Lists.v
7	11/26	Poly.v
8	12/1	多相ラムダ計算 System F
9	12/8	演習
10	12/15	Tactics.v
11	12/22	Logic.v
12	1/5	自然演繹とRocq
13	1/12	IndProp.v
14	1/19	カリーハワード同型対応，ProofObjects.v
補	1/20(？)	演習
期末試験	?

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

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

FAQ

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

Proof General, RocqIDE の操作

機能	Proof General	RocqIDE (メニュー操作)
一歩読み進める(Rocqにテキストの内容を送信)	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年版です．内容の食い違いについては教科書の記述を優先します．)
Rocq: 公式サイト
ProofGeneral: emacs から Rocq を操作するためのソフトウェア．
Company-coq: ProofGeneral の拡張集． forall と打つと ∀ で表示されたりするのでうれしい．自動補完などもできる．
coquille: vim から Coq を操作するためのソフトウェア．(使ったことありません．動作報告求む．)
Coqoon: Eclipse から Coq を操作するためのプラグイン．(使ったことありません．動作報告求む．)
vscoq: Visual Studio Code から Coq を操作するためのプラグイン．(使ったことありません．動作報告求む．)

五十嵐淳