| 日時 | 火曜日2限(10:30〜12:00) |
| 場所 | 総合研究7号館情報1講義室 |
| 担当教員: | 五十嵐 淳 (igarashi) |
| オフィスアワー: | 月曜日 17:00〜18:00 (総合研究7号館224) |
| (その他の時間は要アポイントメント) | |
| 担当TA: | 福田 陽介 |
数理論理学の基礎と，数理論理学を用いた計算機プログラムの検証について講述する．また，講義を補完するため，証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う．
| 回数 | date | 内容(予定) | 資料 | 宿題 |
|---|---|---|---|---|
| 1 | 10/3 | 導入, Basics.v | スライド0, スライド1 | テキスト Preface.v, Basics.v の予習，Coq 環境の構築，課題提出システム登録 |
| 2 | 10/10 | Basics.v, Induction.v | スライド2 | 演習問題(締切 10/17 10:30: Basics.v の nandb, andb3, factorial, blt_nat, plus_id_exercise, andb_true_elim2) |
| 3 | 10/17 | Induction.v(つづき), 単純型付ラムダ計算 | 配布資料1 | 演習問題(締切 10/31 10:30: Induction.v の basic_induction, double_plus, beq_nat_refl) |
| 4 | 10/24 | 単純型付ラムダ計算(つづき) | ||
| 5 | 10/31 | Lists.v | スライド3 | 演習問題(締切 11/14 10:30: Lists.v の snd_fst_is_swap, list_funs, list_exercises, beq_natlist, hd_error) |
| 6 | 11/7 | Poly.v | スライド4 | 演習問題(締切 11/21 10:30: Poly.v の poly_exercises, split, flat_map, currying) |
| 7 | 11/14 | System F, Tactics.v | 配布資料2, スライド5 | |
| 8 | 11/21 | Tactics.v, Logic.v | スライド6 | 演習問題(締切 12/5 10:30: Tactics.v の apply_exercises1, inversion_ex3, inversion_ex6, plus_n_n_injective, beq_nat_true, destruct_eqn_practice) |
| 9 | 11/28 | 教室での演習 | 問題集 | |
| 10 | 12/5 | Logic.v | 演習問題(締切 12/26 10:30: Logic.v の and_assoc, or_distributes_over_and, contrapositive, not_both_true_and_false, dist_exists_or, in_app_iff, beq_nat_false_iff) | |
| 11 | 12/12 | 自然演繹と Coq | 配布資料3 | |
| 12 | 12/19 | (休講) | ||
| 13 | 12/26 | IndProp.v | スライド7 | 演習問題(締切 1/19 10:30: IndProp.v の ev_double, inversion_practice, ev_sum, le_exercises の一部 (le_trans と O_le_n と le_plus_l), leb_iff |
| 14 | 1/9 | 教室での演習 | ||
| 15 | 1/30 | カリーハワード同型対応，ProofObjects.v | 配布資料４, スライド8 | |
| 期末試験 | 2/6 |
Error: No focused proof (No proof-editing in progress).のようにエラーになること(証明中ではないこと)を確認してください． その他の原因として，
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) |