Lean 4 自动化内幕
本书深入讲解 Lean 4 的自动化(tactic)系统内幕:元编程模型、表达式操作、tactic 实现原理,以及 Mathlib 中各种自动化工具的工作机制。
本书假设你已有基本的 Lean 4 使用经验,了解 theorem、by、simp 等基础语法。
本书校验版本:Lean 4 v4.30.0-rc1,Mathlib 同期主线(2026 年 4 月)。
Contents
- 1. 环境与运行约定
- 2. Lean 4 元编程模型
- 3. Expr:Lean 4 的内部表示
- 4. 编写你的第一个 Tactic
- 5. 目标管理
- 6. Type Class Synthesis
- 7. simp——化简的瑞士军刀
-
8. ring 和
ring_nf:代数范式化 - 9. omega:Presburger 算术决策过程
- 10. linarith、nlinarith 与 polyrith
-
11.
norm_num:数值计算框架 - 12. aesop:可配置的启发式搜索
- 13. grind:E-matching 与 Congruence Closure
-
14. decide 与
native_decide:有限计算判定 - 15. positivity:符号非负性推理
-
16.
fun_prop:函数性质的自动证明 - 17. gcongr:广义合同性
-
18.
field_simp:分式化简 - 19. pushneg、contrapose、bycontra
- 20. 设计你自己的领域自动化
- 21. 反射证明模式
- 22. 性能工程
- 23. 对接外部工具
- 24. 从证明模式到自动化:方法论
- 25. 迈向分析自动化
- 26. 附录 A:Metaprogramming API 速查表