| 日時 | 火曜日2限(10:30〜12:00) |
| 場所 | 総合研究7号館情報1講義室 |
| 担当教員: | 五十嵐 淳 |
| オフィスアワー: | 月曜日 17:00〜18:00 (総合研究7号館224) |
| (その他の時間は要アポイントメント) | |
| 担当TA: | 西川 剛史 |
数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 | |
|---|---|---|---|---|---|
| 1 | 10/2 | 導入, Basics.v | スライド0, スライド1 | Coq 環境の構築，テキストのダウンロードと Preface.v, Basics.v の予習 | |
| 2 | 10/9 | Basics.v, Induction.v | スライド2 学生実験２のgitについての資料, GitHub での宿題提出 | 演習問題(締切 10/16 10:30: Basics.v の nandb, andb3, factorial, ltb, plus_id_exercise, zero_nbeq_plus_1) (締切 10/23 10:30: Induction.v の basic_induction, double_plus, eqb_refl) | |
| 3 | 10/16 | 単純型付ラムダ計算 | 配布資料1 | ||
| 4 | 10/23 | 単純型付ラムダ計算(つづき) | |||
| 5 | 10/30 | Lists.v | スライド3 | 演習問題(締切 11/13 10:30: Lists.v の snd_fst_is_swap, list_funs, list_exercises, eqblist, hd_error) | |
| 6 | 11/6 | Poly.v | スライド4 | 演習問題(締切 11/20 10:30: Poly.v の poly_exercises, split, flat_map, currying) | |
| 7 | 11/13 | 多相ラムダ計算 System F, Tactics.v | 配布資料2, スライド5 | ||
| 8 | 11/20 | Tactics.v | 演習問題(締切 12/4 10:30: Tactics.v の apply_exercises1, injection_ex3, discriminate_ex3, plus_n_n_injective, eqb_true, destruct_eqn_practice) | ||
| 9 | 11/27 | Logic.v | スライド6 | 演習問題(締切 12/11 10:30: Logic.v の and_assoc, contrapositive, not_both_true_and_false, or_distributes_over_and, dist_exists_or, In_app_iff, eqb_neq) | |
| 10 | 12/4 | 教室での演習 | 問題集 | ||
| 11 | 12/11 | 自然演繹と Coq | 配布資料3 | ||
| 12 | 12/18 | IndProp.v | スライド7 | 演習問題(締切 1/8 10:30: IndProp.v の ev_double, inversion_practice, ev_sum, le_exercises の一部 (le_trans と O_le_n と le_plus_l) | |
| 13 | 12/25 | (休講) | |||
| 14 | 1/8 | カリーハワード同型対応，ProofObjects.v | 配布資料４, スライド8 | ||
| 15 | 1/29 | 教室での演習 | |||
| 期末試験 | ? |
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) |