ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発

はじめに

第1章 ゼロから始めるLean言語入門
　1.1 Leanの特徴
　1.2 Leanによるプログラミングの例

第2章 Leanによる初めての証明
　2.1 環境構築
　2.2 自然数を定義して1 + 1 = 2を証明する

第3章 Leanにおける論理
　3.1 命題論理
　3.2 証明を楽にするコツ
　3.3 述語論理
　3.4 排中律と直観主義論理
　3.5 選択原理
　3.6 カリー・ハワード同型対応
　3.7 依存型

第4章 帰納法で、足し算の性質を証明する
　4.1 型クラスで見やすく綺麗に
　4.2 帰納法で0 + n = nを証明する
　4.3 等式変形による単純化を自動化する
　4.4 足し算の交換法則と結合法則を解放する
　4.5 帰納法を改善する

第5章 分配法則を証明し、マクロで再利用可能にする
　5.1 掛け算を定義して交換法則、結合法則、分配法則を示す
　5.2 分配法則を再利用可能にする

第6章 自然数の順序と、計算を利用する証明
　6.1 a + b = a + c → b = cを証明する
　6.2 順序を定義する
　6.3 狭義順序を定義する
　6.4 記法の展開を楽にする
　6.5 足し算が順序を保つことを示す
　6.6 a ≤ b → b ≤ a → a = bを示す
　6.7 順序関係を決定可能にする

第7章 同値関係で割って整数を作る
　7.1 同値関係
　7.2 商とQuotient
　7.3 整数を作る

第8章 Mathlibを使って整数の性質を証明する
　8.1 Mathlibのインポート方法
　8.2 代数系について
　8.3 整数が足し算に関してアーベル群であることを利用する
　8.4 整数は環
　8.5 整数は前順序
　8.6 整数は半順序
　8.7 整数は足し算に関して可換な順序群
　8.8 整数の順序関係は決定可能
　8.9 整数は全順序
　8.10 整数は順序環

第9章 grindタクティク
　9.1 grindタクティクの使い方
　9.2 MyNat再訪

おわりに
付録A 練習問題の解答
索引