コンピュータと協働して数学する!
定理証明支援系Coq/SSReflect/MathComp,待望の入門書.
◆定理証明支援系とは?
数学の定理証明を支援するソフトウェアのこと.数学の高度化に伴い,従来の「紙と鉛筆」では証明の構成・検証がますます困難になるなか, Coqをはじめとする定理証明支援系が開発されてきました.こうしたシステムには,証明の正しさを保証する機能のほか,証明をコンピュータが扱える形に翻訳する「数学の形式化」の作業を効率化する仕組みが備えられています.実際Coqは「四色定理」や「ケプラー予想」といった歴史的な大問題を解くのにも利用され,話題をよびました.
◆日本語初のチュートリアル
本書は, Coqとその拡張言語SSReflect/MathCompの初となる解説書です.定理証明支援系の研究利用と普及を手がけてきた著者らが,開発環境のインストール手順から基本的な操作,代表的な命令・ライブラリの使い方までを案内します.集合論,代数学,確率・統計,そして情報理論の簡単な定理を題材に, Coq/SSReflect/MathCompの使い方を易しく例示.本書をひととおり読みこなせば,幅広い分野の定理を形式化する力が自然と身につくはずです.
◆まずは触ってみよう!
数学者を目指す方は「大規模証明時代の必須ツール」として,プログラマの方であれば「ソフトウェア検証などの応用を見据えた基礎トレーニング」として, Coq/SSReflect/MathCompに触れてみてはいかがでしょうか.コンピュータと手を携えて定理をつくっていく――その新感覚の面白さに,きっと魅了されることでしょう.
◆電子版が発行されました
◆詳細は、森北出版Webサイトにて
第1章 Coq/SSReflect/MathCompとは
1.1 はじめに
1.2 型理論とカリー-ハワード同型対応
1.3 Coq/SSRe ect/MathCompのインストール・設定・環境(Microsoft Windows 上バイナリ版)
1.4 Coq/SSReflect/MathCompのライブラリ
第2章 使ってみよう
2.1 画面の構成要素
2.2 モーダスポネンスの形式化
2.3 ヒルベルトの公理Sの形式化
2.4 自然数と和の形式化
2.5 論理式の形式化
第3章 命令
3.1 タクティク,タクティカル,コマンド,クエリー
3.2 タクティクmove=>, move:, move: =>, move
3.3 タクティクapply, apply=>, apply:, apply: =>, apply
3.4 タクティクcase, case:, case=>, case=&: gt;, case=> [ | ], case
3.5 タクティクelim, elim:, elim=>, elim=&: gt;, elim=> [ | ]
3.6 タクティクrewrite
3.7 ビュー機能:タクティクmove/, apply/, case
3.8 タクティクhave, suff, wlog
3.9 コマンドDenition, Lemma, Theorem, Corollary, Fact, Proposition, Remark, Proof, Qed, Fixpoint
3.10 クエリーCompute―計算結果を表示する
3.11 クエリーCheck, About, Print, Search, Locate
3.12 コマンドAbort, Admitted
3.13 スクリプトの管理と整理―コマンドVariable(s), Hypothesis, Axiom
3.14 コマンドInductive
3.15 コマンドRecord, Canonical
3.16 Coqのタクティクsplit, left, right, exists
第4章 MathCompライブラリの基本ファイル
4.1 ssrbool.v―bool型のためのライブラリ
4.2 eqtype.v―eqType型のためのライブラリ
4.3 ssrnat.v―SSRe ect向けnat型のライブラリ
4.4 seq.v―リスト, seq型のライブラリ
4.5 fintype.v―有限型のライブラリ
4.6 bigop.v―総和,総乗等のライブラリ
第5章 集合の形式化
5.1 集合,部分集合
5.2 包含関係と等号
5.3 集合上の演算
5.4 集合間の写像
5.5 fintypeを用いた有限集合の形式化
5.6 ライブラリfinset
第6章 代数学の形式化
6.1 テーマ1:整数がその加法で可換群になること
6.2 テーマ2:有限群とラグランジュの定理
第7章 確率論と情報理論の形式化
7.1 確率論と情報理論のライブラリInfotheoのインストール
7.2 確率論―分布,期待値,分散
7.3 情報理論―情報エントロピー,二元エントロピー関数
7.4 おまけ:自作ファイルのコンパイル
あとがき
索引
