自动化 tactic
omega/decide/norm_num/ring/linarith/aesop/grind 各自的适用范围与失败时的替代方案。
自动化 tactic 能省下大量机械劳动，但每个都有明确的适用范围。用错工具是新手卡住的主因——知道该用哪个，比知道有哪些更重要。
速查表
| tactic | 解决什么 | 来源 |
|---|---|---|
rfl | 定义展开后相同 | 核心 |
decide | 可判定的具体命题（实际计算） | 核心 |
omega | 线性算术（Nat/Int 的 + - * 常数、< ≤ =） | 核心 |
simp | 用 simp 引理集重写 | 核心 |
norm_num | 数值计算与规范化 | Mathlib |
ring | 交换环恒等式 | Mathlib |
field_simp | 分式化简 | Mathlib |
linarith | 线性不等式（含有理系数） | Mathlib |
nlinarith | 非线性不等式（有限能力） | Mathlib |
positivity | 证明表达式为正/非负 | Mathlib |
aesop | 通用搜索（逻辑 + simp + 规则集） | Mathlib |
grind | 新一代通用自动化 | 核心（较新） |
exact? / apply? | 搜索库里的定理 | 核心 |
omega：线性算术的主力
example (a b : Nat) (h1 : a ≤ b) (h2 : b ≤ 10) : a ≤ 10 := by omega
example (n : Nat) (h : n > 0) : n - 1 + 1 = n := by omega
example (x y : Int) (h : 2 * x + 3 * y = 7) (h2 : x = 2) : y = 1 := by omegaomega 是日常用得最多的自动化。它处理：
Nat与Int上的线性算术- 加减、乘以常数、整除/取余（有限支持）
<、≤、=、≠- 上下文里的假设自动使用
它特别擅长 Nat 减法——那个截断行为手工推理很痛苦，omega 内建了正确处理。
omega 不处理：变量相乘（x * y）、指数、除法（非常数除数）、实数。
遇到 x * y 这类非线性项，omega 会直接失败。改用 nlinarith 或手工推导。
ring：环恒等式
example (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by ring
example (x y : Int) : (x - y) * (x + y) = x ^ 2 - y ^ 2 := by ringring 证明的是「两边化成标准形后相同」的恒等式——不涉及不等式，也不用假设。
ring_nf 是它的规范化版本，把表达式化成标准形但不要求闭合目标：
example (a b : Nat) (h : (a + b) ^ 2 = 0) : a ^ 2 + 2 * a * b + b ^ 2 = 0 := by
ring_nf at h ⊢
exact hring 失败时先问：这真的是环恒等式吗？ 涉及减法时注意 Nat 不是环（没有加法逆元）——Nat 上的 ring 能力受限，转 Int 往往更顺。
linarith：线性不等式
example (x y : ℚ) (h1 : x ≤ 3) (h2 : y ≤ 2) : x + y ≤ 5 := by linarith
example (a b c : ℝ) (h1 : a < b) (h2 : b < c) : a < c := by linarith比 omega 更通用（支持有序域、有理系数），但只处理线性。
linarith 会用上下文里的所有线性假设做线性组合。可以显式补充：
example (x : ℝ) (h : x ^ 2 ≥ 0) : x ^ 2 + 1 > 0 := by linarithnlinarith 加了一些非线性预处理（平方非负等），能力更强但不保证：
example (x : ℝ) : x ^ 2 + 1 > 0 := by nlinarith [sq_nonneg x]方括号里可以给提示项——nlinarith 失败时补充关键的中间事实往往能救。
decide：实际计算
example : 2 + 2 = 4 := by decide
example : (7 : Nat) ∣ 21 := by decide
example : ∀ n < 5, n * n < 25 := by decidedecide 真的在算。它要求命题有 Decidable 实例。
decide 对大数会爆。 它在内核里做完整计算，decide 一个涉及大数的命题可能跑几分钟然后栈溢出。
经验：只对小的、具体的命题用。含变量的通用命题（∀ n : Nat, ...）通常不可判定，decide 直接失败。
native_decide 用编译后的原生代码计算，快很多——但它把编译器加进了可信基（TCB），Mathlib 不接受用它的证明。
norm_num：数值规范化
example : (37 : ℕ) * 41 = 1517 := by norm_num
example : (2 : ℝ) + 2 < 5 := by norm_num
example : Nat.Prime 101 := by norm_num处理具体数值的算术与比较，比 decide 更聪明（不做暴力计算），且有扩展支持素数、整除等。
具体数字的目标先试 norm_num，它通常比 decide 快得多。
aesop：通用搜索
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by aesop
example (xs : List α) : xs ++ [] = xs := by aesopaesop（Automated Extensible Search for Obvious Proofs）是通用证明搜索：组合 simp、逻辑规则、库引理，做最佳优先搜索。
它可以被扩展：
@[aesop safe apply]
theorem my_rule : ... := ...safe（一定不会让证明变难）与 unsafe（可能走错路，带概率）是两类规则。
aesop 适合「看起来显然但要几步」的目标。它失败时通常说明目标需要真正的数学内容，不是机械推理。
grind：新一代自动化
Lean 较新版本引入的 grind tactic，目标是统一多种自动化——它整合了同余闭包、线性算术、简化器与实例搜索。
example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by grindgrind 仍在快速演进（官方参考手册为它单列了一章）。它的定位是「先试试这个」——覆盖面比单个专用 tactic 广。
但专用 tactic 在其领域内仍然更可靠：线性算术用 omega、环恒等式用 ring。grind 适合不确定该用哪个时的第一次尝试。
由于它较新，用前请确认你的 Lean 版本支持，并留意行为可能随版本变化。
exact? / apply? / rw?：搜库
example (a b : Nat) : a + b = b + a := by exact?
-- Try this: exact Nat.add_comm a b这三个是学 Mathlib 的最佳工具：
| tactic | 找什么 |
|---|---|
exact? | 能直接闭合目标的定理 |
apply? | 能 apply 到目标的定理（留下子目标） |
rw? | 能重写目标的等式 |
它们会搜索整个已 import 的库。搜到后把结果抄进代码——不要留着 exact? 在最终版本里（它每次都要重新搜索，很慢）。
配合 hint（Mathlib）一次试多个 tactic：
example (a b : Nat) : a + b = b + a := by hint选择流程
目标是具体数字的算术？ → norm_num
目标是 Nat/Int 线性算术？ → omega
目标是环恒等式（无不等式）？ → ring
目标是线性不等式？ → linarith
目标含非线性不等式？ → nlinarith [提示项]
目标是可判定的小命题？ → decide
目标是纯逻辑组合？ → tauto / aesop
不确定？ → grind，或 exact? 搜库
以上都不行 → 手工分解：have / calc / 找引理自动化失败之后
自动化失败不代表命题错了，但值得先检查命题对不对。
- 验证命题本身：用
#eval在具体值上试（若可计算），或找反例。 - 看清目标：Infoview 里目标可能不是你以为的形式。
- 手工分解：用
have拆成小步，看卡在哪一步。 - 搜库：
exact?/ Loogle / Moogle（见下一章）。 - 补提示：
nlinarith [sq_nonneg x]这类显式提示常常能救。
一个典型的「分解到自动化能吃下」的例子：
example (a b : ℕ) (h : a ≥ b) : (a - b) + b = a := by
omega -- 直接能过
example (x : ℝ) (hx : 0 < x) : x / x = 1 := by
field_simp -- 分式要用专门的性能注意
set_option maxHeartbeats 400000 in
theorem slow_one : ... := by aesop自动化 tactic 有超时限制（heartbeats）。复杂目标超时会报 (deterministic) timeout。
调大限制是权宜之计——更好的做法是把证明拆小。单个 tactic 需要几十万 heartbeats 通常意味着该手工引导了。
下一篇：Mathlib。