# 自动化 tactic

> omega/decide/norm_num/ring/linarith/aesop/grind 各自的适用范围与失败时的替代方案。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/automation
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

自动化 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：线性算术的主力

```lean
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 omega
```

**`omega` 是日常用得最多的自动化**。它处理：

- `Nat` 与 `Int` 上的线性算术
- 加减、乘以**常数**、整除/取余（有限支持）
- `<`、`≤`、`=`、`≠`
- 上下文里的假设自动使用

它**特别擅长 `Nat` 减法**——[那个截断行为](https://daiw.org/manual/lean4/types-terms)手工推理很痛苦，`omega` 内建了正确处理。

<Callout type="warn">
  **`omega` 不处理**：变量相乘（`x * y`）、指数、除法（非常数除数）、实数。

  遇到 `x * y` 这类非线性项，`omega` 会直接失败。改用 `nlinarith` 或手工推导。
</Callout>

## ring：环恒等式

```lean
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 ring
```

**`ring` 证明的是「两边化成标准形后相同」的恒等式**——不涉及不等式，也不用假设。

`ring_nf` 是它的规范化版本，把表达式化成标准形但不要求闭合目标：

```lean
example (a b : Nat) (h : (a + b) ^ 2 = 0) : a ^ 2 + 2 * a * b + b ^ 2 = 0 := by
  ring_nf at h ⊢
  exact h
```

`ring` 失败时先问：**这真的是环恒等式吗？** 涉及减法时注意 `Nat` 不是环（没有加法逆元）——`Nat` 上的 `ring` 能力受限，转 `Int` 往往更顺。

## linarith：线性不等式

```lean
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` 会用上下文里的所有线性假设做线性组合。可以显式补充：

```lean
example (x : ℝ) (h : x ^ 2 ≥ 0) : x ^ 2 + 1 > 0 := by linarith
```

`nlinarith` 加了一些非线性预处理（平方非负等），能力更强但不保证：

```lean
example (x : ℝ) : x ^ 2 + 1 > 0 := by nlinarith [sq_nonneg x]
```

方括号里可以给提示项——**`nlinarith` 失败时补充关键的中间事实往往能救**。

## decide：实际计算

```lean
example : 2 + 2 = 4 := by decide
example : (7 : Nat) ∣ 21 := by decide
example : ∀ n < 5, n * n < 25 := by decide
```

**`decide` 真的在算**。它要求命题有 [`Decidable` 实例](https://daiw.org/manual/lean4/typeclasses)。

<Callout type="warn">
  **`decide` 对大数会爆。** 它在**内核里**做完整计算，`decide` 一个涉及大数的命题可能跑几分钟然后栈溢出。

  经验：只对小的、具体的命题用。含变量的通用命题（`∀ n : Nat, ...`）通常不可判定，`decide` 直接失败。

  `native_decide` 用编译后的原生代码计算，快很多——但它**把编译器加进了可信基**（TCB），Mathlib 不接受用它的证明。
</Callout>

## norm_num：数值规范化

```lean
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：通用搜索

```lean
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by aesop
example (xs : List α) : xs ++ [] = xs := by aesop
```

**`aesop`（Automated Extensible Search for Obvious Proofs）是通用证明搜索**：组合 `simp`、逻辑规则、库引理，做最佳优先搜索。

它可以被扩展：

```lean
@[aesop safe apply]
theorem my_rule : ... := ...
```

`safe`（一定不会让证明变难）与 `unsafe`（可能走错路，带概率）是两类规则。

**`aesop` 适合「看起来显然但要几步」的目标**。它失败时通常说明目标需要真正的数学内容，不是机械推理。

## grind：新一代自动化

Lean 较新版本引入的 `grind` tactic，目标是**统一多种自动化**——它整合了同余闭包、线性算术、简化器与实例搜索。

```lean
example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by grind
```

<Callout type="info">
  `grind` 仍在快速演进（官方参考手册为它单列了一章）。它的定位是「先试试这个」——覆盖面比单个专用 tactic 广。

  但**专用 tactic 在其领域内仍然更可靠**：线性算术用 `omega`、环恒等式用 `ring`。`grind` 适合不确定该用哪个时的第一次尝试。

  由于它较新，用前请确认你的 Lean 版本支持，并留意行为可能随版本变化。
</Callout>

## `exact?` / `apply?` / `rw?`：搜库

```lean
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：

```lean
example (a b : Nat) : a + b = b + a := by hint
```

## 选择流程

```text
目标是具体数字的算术？        → norm_num
目标是 Nat/Int 线性算术？      → omega
目标是环恒等式（无不等式）？    → ring
目标是线性不等式？             → linarith
目标含非线性不等式？           → nlinarith [提示项]
目标是可判定的小命题？          → decide
目标是纯逻辑组合？             → tauto / aesop
不确定？                       → grind，或 exact? 搜库
以上都不行                     → 手工分解：have / calc / 找引理
```

## 自动化失败之后

<Callout type="warn">
  **自动化失败不代表命题错了，但值得先检查命题对不对。**

  1. **验证命题本身**：用 `#eval` 在具体值上试（若可计算），或找反例。
  2. **看清目标**：Infoview 里目标可能不是你以为的形式。
  3. **手工分解**：用 `have` 拆成小步，看卡在哪一步。
  4. **搜库**：`exact?` / Loogle / Moogle（见[下一章](https://daiw.org/manual/lean4/mathlib)）。
  5. **补提示**：`nlinarith [sq_nonneg x]` 这类显式提示常常能救。
</Callout>

一个典型的「分解到自动化能吃下」的例子：

```lean
example (a b : ℕ) (h : a ≥ b) : (a - b) + b = a := by
  omega          -- 直接能过

example (x : ℝ) (hx : 0 < x) : x / x = 1 := by
  field_simp     -- 分式要用专门的
```

## 性能注意

```lean
set_option maxHeartbeats 400000 in
theorem slow_one : ... := by aesop
```

自动化 tactic 有**超时限制**（heartbeats）。复杂目标超时会报 `(deterministic) timeout`。

调大限制是权宜之计——**更好的做法是把证明拆小**。单个 tactic 需要几十万 heartbeats 通常意味着该手工引导了。

下一篇：[Mathlib](https://daiw.org/manual/lean4/mathlib)。