Theorem Proving in Lean 4 の内容をカバーする

# Codex による概観 • Lean by Example は Lean 4 の資料なので、TPIL4 と比較しました。結論から言うと、章題レベルではかなりカバーしていますが、TPIL4 を置き換えるほど網羅的ではありません。TPIL4 は Lean 4.26.0 前提の 12 章構成で、依存型理論、命題と証明、量化子と等号、タクティク、帰納型、再帰、構造体、型クラス、conv、公理と計算までを順に扱っています。(lean-lang.org (https://lean-lang.org/theorem_proving_in_lean4/index)) Lean by Example 側は booksrc/SUMMARY.md を見る限り、#check / #eval / #print、def / theorem / inductive / structure / class、主要タクティク、型クラス、Prop / Type / Quotient などはかなり 充実しています。むしろ Mathlib のタクティク、属性、オプション、メタプログラミング寄りの記事は TPIL より広いです。 足りない、または薄い内容は主に以下です。 1. 依存型理論の連続した導入 Type、Prop、∀、暗黙引数などの記事はありますが、TPIL 2章のように「単純型理論 → 型を項として扱う → 関数抽象 → 依存関数型 → 宇宙多相」へ一続きで説明する流れは弱いです。TPIL 2章はこの並び を明示しています。 2. 証明項スタイルの基礎 命題論理やタクティクはありますが、fun による証明、theorem と def の違い、show / have / Exists.intro / Eq.subst / congrArg などを「項として証明を構成する」観点で体系的に読むページは不足気味です。TPIL 3-4章はこの部分をかなり丁寧に扱っています。 (lean-lang.org (https://lean-lang.org/theorem_proving_in_lean4/Quantifiers-and-Equality/)) 3. Interacting with Lean の細部 #guard_msgs、属性、オプション、名前空間などはありますが、TPIL 6章にある import、ライブラリ利用、named arguments、自動束縛暗黙引数、implicit lambdas、simple function sugar あたりは独立記事としては薄いです。(lean-lang.org (https://lean-lang.org/theorem_proving_in_lean4/Interacting-with-Lean/)) 4. 方程式コンパイラと高度なパターンマッチ match、termination_by、mutual はありますが、TPIL 8章の「overlapping patterns」「local recursive declarations」「dependent pattern matching」「inaccessible patterns」「match 式のコンパ イル」のまとまった説明は不足しています。ここは大きな差です。 5. conv 変換モード LeanByExample/Tactic/Conv.lean はほぼ外部リンクだけです。TPIL 11章は lhs / rhs / congr / binder 内の rewrite / conv in / tactic => まで扱っているので、Lean by Example 側では明確に未カ バーです。 6. 帰納型の低レベル仕様の一部 inductive、帰納族、再帰子、strict positivity はよく扱えています。ただし TPIL 7章の「axiomatic details」「mutual and nested inductive types」全体を同じ粒度で読むには、ネストした帰納型 や生成される eliminator の説明がもう少し必要です。 7. 公理と計算内容の総合説明 LeanByExample/Declarative/Axiom.lean、LeanByExample/Type/Quotient.lean、LeanByExample/Modifier/Noncomputable.lean は強いです。ただし TPIL 12章の「公理を足すと計算内容がどう変わるか」 という全体像は、現状だと複数記事に分散しています。TPIL 12章は propext、funext、商、選択、公理的排中律を一章でつなげています。 優先して補うなら、まず conv、次に「方程式コンパイラと依存パターンマッチ」、その次に「TPIL 2-4章相当の証明項スタイル入門」を足すのが効果的です。