| 日時 | 火曜日2限(10:30〜12:00) |
| 場所 | 総合研究４号館共通３ |
| 担当教員: | 五十嵐 淳 |
| オフィスアワー: | 水曜日 18:00〜19:00 (総合研究7号館224) |
| (その他の時間は要アポイントメント) | |
| 担当TA: | 四十坊 純也 |
数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 | |
|---|---|---|---|---|---|
| 1 | 10/4 | 導入, Basics.v | スライド0, スライド1 | Coq 環境の構築，テキストのダウンロード | |
| 2 | 10/11 | Basics.v, Induction.v | スライド2 学生実験２のgitについての資料, GitHub での宿題提出 | 演習問題(締切 10/18 10:30: Basics.v の nandb, andb3, factorial, ltb, plus_id_exercise, zero_nbeq_plus_1) (締切 10/25 10:30: Induction.v の basic_induction, double_plus, eqb_refl, add_comm_informal) | |
| 3 | 10/18 | 単純型付ラムダ計算 | 配布資料1(改訂版) | ||
| 4 | 10/25 | 単純型付ラムダ計算(つづき) | |||
| 5 | 11/1 | Lists.v | スライド3 | 演習問題(締切 11/15 10:30: Lists.v の snd_fst_is_swap, list_funs, list_exercises, eqblist, hd_error) | |
| 6 | 11/8 | Poly.v | スライド4 | 演習問題(締切 11/22 10:30: Poly.v の poly_exercises, split, flat_map, currying) | |
| 7 | 11/15 | 多相ラムダ計算 System F | 配布資料2(改訂版) 問題集 | ||
| 8 | 11/29 | Tactics.v | スライド5 | 演習問題(締切 12/12 10:30: Tactics.v の apply_exercises1, injection_ex3, discriminate_ex3, eqb_true, destruct_eqn_practice) | |
| 9 | 12/6 | 演習 | (範囲: 問題集1〜3節) | ||
| 10 | 12/13 | Logic.v | スライド6 | 演習問題(締切 1/10 10:30: Logic.v の and_assoc, contrapositive, not_both_true_and_false, or_distributes_over_and, dist_exists_or, In_app_iff, logical_connectives) | |
| 11 | 12/20 | 自然演繹と Coq | 配布資料3 | ||
| 12 | 12/27 | 演習 | (範囲: 問題集全部) | ||
| 13 | 1/17 | IndProp.v | スライド7 | 演習問題(締切 1/24 10:30: IndProp.v の ev_double, inversion_practice, ev_sum, le_and_lt_facts の一部 (le_trans と O_le_n と le_plus_l) | |
| 14 | 1/24 | カリーハワード同型対応，ProofObjects.v | 配布資料４, スライド8 | ||
| 期末試験 | ? |
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 を省略して解答を行った場合，演習上・採点時の不都合はありますでしょうか？
Coqtop died badly. Resetting. というメッセージがでてうまく動作しません．
Require Export .... で 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) |