2023年度春・数理解析・計算機数学 III (同 概論I)

レポート課題

• レポート課題 提出期限 2022年8月2日(水) (7月12日修正)

時間

水曜日 1・2限

教室

多元 409

講義予定

• シラバス
• 注意：毎回の課題の提出はTACTのメッセージで行って下さい

第1回 4月12日

Coq/SSReflectの論理

• 講義メモ スクリプト
• 資料 EmacsでCoqを使う
• 設定ファイル coq.emacs (.emacs にコピーす る)
• ProofGeneral PG-master.zip (Safariで ダウンロードする)

第2回 4月19日

述語論理とSSReflectのタクティック

• 講義メモ (4/25修正)

第3回 4月26日

再帰的な定義と帰納法

• 講義メモ

第4回 5月11日

帰納的な定義と型付け

• 講義メモ
• スクリプト

第5回 5月17日

Mathcomp, 自己反映と数論の証明

• 講義メモ
• ssrbool_doc.pdf, ssrnat_doc.pdf (R. Affeldt の SSReflect Tutorial より)
• スクリプト

第6回 5月24日

単一化と自動化

• 講義メモ
• スクリプト

第7回 5月31日

プログラムの証明

• 講義メモ
• スクリプト

第8回 6月7日

Mathcompでのプログラム証明

• 講義メモ
• スクリプト

第9回 6月14日

数学:自然数・実数・総和

• 講義メモ
• コード: ssrcoq8a.v ssrcoq9.v
• bigop_doc.pdf (R. Affeldt の SSReflect Tutorial より)

第10回 6月21日

線形代数

• 講義メモ
• コード: ssrcoq9a.v ssrcoq10.v

6月28日

休講

第11回 7月5日

コンパイラ

• 講義メモ
• コード: ssrcoq10a.v ssrcoq11.v

第12回 7月12日

λ計算の簡約器

• 講義メモ
• コード: ssrcoq11a.v ssrcoq12.v

第13回 7月19日

単一化の証明

• 講義メモ
• コード: ssrcoq12a.v ssrcoq13.v

第14回 7月26日

単一化の証明 (完全性)

• 講義メモ
• コード: ssrcoq14.v

Coq/MathComp/SSReflect

• Coq platform 2022.09.1 / Coq 8.16 のダウンロード
  • Windows
  • MacOS / Arm
  • MacOS / Intel
• CoqIDEが文字化けをしたらVSCodeを使いましょう
  • WindowsのVScodeでCoqを使う（初心者向け）

Coq に関する情報源

Coq@INRIA

開発元 (英語)

Coq Platform

最新版のダウンロード

Programs and Proofs

Ilya Sergey の講義ノート (英語)

MathComp@Github

MathCompの開発元 (英語)

SSReflect チュートリアル

Reynald AffeldtによるCoqのチュートリアル (日本語あり)

Proof Café

名古屋におけるCoqや関数型言語の情報

プログラミングCoq

IIJのCoqチュートリアル（日本語）