# tactic 基础

> tactic 是什么、intro/exact/apply/refine 的精确差别、目标管理与 rcases 模式语言。

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

## tactic 是构造项的程序

`by` 之后的每条 tactic，都在**帮你写那个证明项**。

```lean
theorem manual (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

theorem tactical (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq
```

两者产生的**最终项完全相同**。tactic 只是构造过程的自动化——用 `#print tactical` 能看到它生成的项。

理解这点很重要：**tactic 失败不是「证明错了」，是「没能造出那个项」**。

## 目标与上下文

```lean
theorem example_state (a b : Nat) (h : a = b) : b = a := by
  -- a b : Nat        ← 局部上下文
  -- h : a = b
  -- ⊢ b = a          ← 目标
  exact h.symm
```

tactic 做的事只有两类：**改变上下文**（加/改假设）或**改变目标**。

## 核心 tactic

### exact

```lean
theorem use_exact (p : Prop) (hp : p) : p := by exact hp
```

「**目标就是这个项**」。要求类型**完全匹配**（允许定义展开）。

`exact?` 会**搜索库里能直接闭合目标的定理**——非常有用：

```lean
example (a b : Nat) : a + b = b + a := by exact?
-- 提示：exact Nat.add_comm a b
```

### apply

```lean
theorem use_apply (p q : Prop) (hpq : p → q) (hp : p) : q := by
  apply hpq
  exact hp
```

「**用这个定理，缺的参数留作新目标**」。

`apply f` 会把 `f` 的结论与目标匹配，把 `f` 还缺的参数变成新目标。

<Callout type="info">
  **`exact` 与 `apply` 的区别**：

  - `exact h` —— h 必须**完全**是目标。
  - `apply h` —— h 的**结论**是目标，前提变成新目标。

  `exact hpq hp` 与 `apply hpq; exact hp` 等价。`apply` 适合分步推进。
</Callout>

### intro

```lean
theorem use_intro (p q : Prop) : p → q → p := by
  intro hp hq
  exact hp
```

「**把目标里的箭头/量词移到上下文**」。

对应逻辑里的蕴含引入与全称引入——本质是写 `fun`：

```lean
theorem use_intro' (p q : Prop) : p → q → p := fun hp _ => hp
```

`intro` 可以一次引入多个，也可以直接模式匹配：

```lean
example (p q : Prop) : p ∧ q → q := by
  intro ⟨_, hq⟩
  exact hq
```

### refine

```lean
theorem use_refine (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  refine ⟨?_, ?_⟩
  · exact hp
  · exact hq
```

「**给出部分项，用 `?_` 标出待填的洞**」。

`refine` 是 `exact` 与 `apply` 的一般化——你控制项的骨架，把不想现在填的地方留成目标。

命名洞便于引用：

```lean
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  refine ⟨?left, ?right⟩
  case left => exact hp
  case right => exact hq
```

### rfl / trivial / assumption

```lean
example : 2 + 2 = 4 := by rfl              -- 按定义相等
example : True := by trivial               -- 平凡目标
example (p : Prop) (hp : p) : p := by assumption   -- 从上下文里找
```

| tactic | 何时用 |
| --- | --- |
| `rfl` | 两边计算后相同 |
| `trivial` | `True`、`rfl`、`assumption` 的组合尝试 |
| `assumption` | 上下文里已经有一模一样的假设 |

`assumption` 在自动化中常用——不必记住假设叫什么名字。

## 目标管理

### focus dot

```lean
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp        -- 只处理第一个目标
  · exact hq
```

`·`（`\.`）**聚焦当前第一个目标**，块内必须把它完全解决。

**强烈建议总是用 `·`**：不用它的话所有 tactic 作用在「当前所有目标」上，证明会变得难读且脆弱。

### case

```lean
example (n : Nat) : n = n := by
  cases n with
  | zero => rfl
  | succ k => rfl
```

按名字处理分支，比位置更稳健。

### 组合子

```lean
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor <;> assumption
```

| 组合子 | 含义 |
| --- | --- |
| `t1 <;> t2` | 先跑 t1，再对**它产生的所有目标**跑 t2 |
| `t1 ; t2` | 顺序执行（换行等价） |
| `first \| t1 \| t2` | 试 t1，失败就试 t2 |
| `try t` | 试 t，失败也不报错 |
| `repeat t` | 反复跑 t 直到失败 |
| `all_goals t` | 对所有目标跑 t |
| `any_goals t` | 对任意目标跑 t（至少一个成功） |

`<;>` 是最常用的——`constructor <;> assumption` 一行解决对称的分支。

## rcases 模式语言

`rcases` / `obtain` 用一套小语言描述「怎么拆」：

```lean
example (h : (p ∧ q) ∨ (r ∧ s)) : True := by
  rcases h with ⟨hp, hq⟩ | ⟨hr, hs⟩
  · trivial
  · trivial
```

| 模式 | 含义 |
| --- | --- |
| `⟨a, b⟩` | 拆结构体/合取/存在 |
| `a \| b` | 分情况（析取/多构造子） |
| `⟨a, b\|c⟩` | 嵌套 |
| `-` | 丢弃 |
| `rfl` | 若是等式，**直接代入** |
| `_` | 自动命名 |

`rfl` 模式特别有用：

```lean
example (a b : Nat) (h : ∃ c, a = b + c) : b ≤ a := by
  obtain ⟨c, rfl⟩ := h      -- 直接把 a 替换成 b + c
  omega
```

`obtain` 与 `rcases` 基本同义，习惯上 `obtain` 用于「我知道结构」，`rcases` 用于「分情况」。

## 常用辅助

```lean
example (a b : Nat) (h : a = b) : b = a := by
  have h2 : b = a := h.symm      -- 引入中间结论
  exact h2

example (n : Nat) : n + 0 = n := by
  show n + 0 = n                  -- 显式声明目标（可改写成定义等价形式）
  simp
```

| tactic | 作用 |
| --- | --- |
| `have h : T := e` | 加一个已证的中间结论 |
| `suffices h : T by ...` | 「只需证 T」——先用后证 |
| `show T` | 把目标改写成定义等价的形式 |
| `change T` | 同 `show`，更严格 |
| `clear h` | 从上下文删掉 h |
| `rename_i x` | 给自动生成的名字改名 |
| `specialize h a` | 把全称假设特化到具体值 |

`have` 是[结构化证明](https://daiw.org/manual/lean4/structured-proofs)的基础，下面会专门讲。

## 排查 tactic 失败

### 看清当前状态

把光标放在失败的 tactic **之前**，Infoview 显示的就是它面对的状态。**大多数失败是因为状态与你以为的不同**。

### trace 与 sorry

```lean
example (n : Nat) : n + 0 = n := by
  trace_state          -- 打印当前状态
  sorry
```

用 `sorry` 临时闭合，先确认前面的步骤对不对。

### 拆开自动化

```lean
example (a b : Nat) : a + b = b + a := by
  -- simp 失败时，看它到底做了什么
  simp?
```

`simp?` 会显示 `simp` 实际用了哪些引理，可以据此改成显式的 `simp only [...]`。

### 常见错误信息

| 信息 | 含义 |
| --- | --- |
| `unsolved goals` | tactic 跑完了目标还在——信息里会列出剩余目标 |
| `type mismatch` | `exact` 给的项类型不对 |
| `failed to unify` | `apply` 的结论与目标对不上 |
| `no goals` | 目标已经没了还在写 tactic |
| `tactic 'rfl' failed` | 两边计算后不相同 |

<Callout type="warn">
  **`apply` 失败常见于隐式参数推断不出来。** 试试用 `@` 显式给出，或者用 `refine` 手工留洞：

  ```lean
  refine my_thm ?_ ?_      -- 明确留两个洞，避免 apply 的启发式
  ```
</Callout>

## 一个从零构造的证明

```lean
theorem and_or_distrib (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  constructor
  · intro ⟨hp, hqr⟩
    rcases hqr with hq | hr
    · left;  exact ⟨hp, hq⟩
    · right; exact ⟨hp, hr⟩
  · intro h
    rcases h with ⟨hp, hq⟩ | ⟨hp, hr⟩
    · exact ⟨hp, Or.inl hq⟩
    · exact ⟨hp, Or.inr hr⟩
```

**每一步都对应[上一章](https://daiw.org/manual/lean4/logic-connectives)那张引入/消去表**——没有任何需要「灵感」的地方。基础逻辑证明基本都是这样机械推进的。

下一篇：[重写与化简](https://daiw.org/manual/lean4/rewriting)。