rw 按从左到右的顺序匹配第一个符合的子项并替换，simp 则对所有可匹配位置做化简。两者在精度上处于两个极端：一个只打第一枪，一个全部扫射。实际证明中经常需要介于两者之间的操作——精确指定重写位置。Lean 4 提供了 conv 和 calc 两套工具：conv 在目标的语法树上导航到具体子表达式再执行重写，calc 把一串等式或不等式推导组织成可读的链式结构。

本篇的前置知识是 rw、simp 的基本用法（见第 04 篇：核心 tactic 精讲和第 05 篇：simp 与 norm_num）。所有代码在 Lean 4 v4.12.0 + Mathlib4 下通过 lake build 验证。

conv 的基本结构

conv 开启一个子目标编辑会话。在这个会话内，当前目标被视为一棵语法树，通过导航组合子定位到具体子表达式后再执行操作。

最简单的例子：目标是 ⊢ 0 + n = n，想用 Nat.zero_add 重写左侧。在更复杂的情况下等号两侧可能都包含相同的子项，此时需要限定重写范围。

1 2	`example (n : ℕ) : 0 + n = n := by conv_lhs => rw [Nat.zero_add]`

conv_lhs 是 conv => lhs 的简写，把焦点锁定在等式左侧。执行 rw [Nat.zero_add] 后，左侧的 0 + n 被替换为 n，目标变成 ⊢ n = n，随后 rfl 自动关闭。

等价的完整写法：

1 2	`example (n : ℕ) : 0 + n = n := by conv => lhs; rw [Nat.zero_add]`

分号 ; 在 conv 模式中表示"先执行前一个导航，再在结果上执行后续操作"。

导航组合子

conv 提供了一组组合子，用于在目标的语法树上移动焦点。

lhs 与 rhs

对任何二元关系 a R b（包括 =、≤、<、∣ 等），lhs 把焦点移到 a，rhs 移到 b。

1
2
3

example (a b : ℕ) (h : a = b) : a + 1 = b + 1 := by
  conv_lhs => rw [h]
  -- 目标变为 ⊢ b + 1 = b + 1

进入 conv_lhs 后，InfoView 展示的目标形式略有不同：

1	`\| ⊢ a + 1`

竖线 | 标记当前焦点位置。执行 rw [h] 后变为 | ⊢ b + 1。退出 conv 后回到正常目标 ⊢ b + 1 = b + 1。

arg：定位函数参数

arg 1 和 arg 2 分别定位到函数应用的第一个和第二个显式参数。对于 f a b，arg 1 指向 a，arg 2 指向 b。

1 2	`example (n : ℕ) : Nat.succ (0 + n) = Nat.succ n := by conv_lhs => arg 1; rw [Nat.zero_add]`

arg 1 把焦点从 Nat.succ (0 + n) 移到 0 + n。

ext：进入绑定器

对包含 ∀、fun、∃ 等绑定器的表达式，ext x 引入绑定变量 x 并把焦点移到绑定体内部。

1 2	`example : (fun x : ℕ => 0 + x) = (fun x => x) := by conv_lhs => ext x; rw [Nat.zero_add]`

在 conv 外部也可以用函数外延性 ext x 直接拆：

-- tactic-mode 不用 conv
example : (fun x : ℕ => 0 + x) = (fun x => x) := by
  ext x
  exact Nat.zero_add x

两种写法效果相同，区别在于 conv 版本把 ext 和 rw 组合在同一个子目标编辑会话里，适合更复杂的导航场景。

enter：复合导航路径

enter 接受一个导航指令列表，相当于把多个导航步骤串联。列表中的数字 n 等价于 arg n。

1
2
3

example (f : ℕ → ℕ) (a b : ℕ) (h : a = b) :
    f (a + 1) + 2 = f (b + 1) + 2 := by
  conv_lhs => enter [1, 1, 1]; rw [h]

导航路径 [1, 1, 1]：第一个 1 进入加法第一个参数 f (a + 1)，第二个 1 进入 f 的参数 a + 1，第三个 1 进入 a + 1 的第一个参数 a。rw [h] 在这个位置把 a 替换为 b。

enter 在深层嵌套时比连写多个 arg 更紧凑。

conv 内部操作

定位到目标子表达式后，可以在 conv 块内执行多种 tactic：

操作	作用
`rw [h]`	对焦点位置做重写
`simp [lemmas]`	对焦点位置做化简
`ring`	对焦点位置做环等式判定
`norm_num`	对焦点位置做数值规范化
`change expr`	把焦点处的表达式替换为定义等价的 `expr`

change 在 conv 中特别有用。普通模式下 change 替换整个目标，但在 conv 中只替换焦点处的子表达式：

example (n : ℕ) : n + 0 = n := by
  conv_lhs => rhs; change 0
  -- 焦点处的 0 保持不变（已经是 0），这里只是演示 change 的粒度
  simp

conv at：操作假设

conv at h => ... 把 conv 的焦点从目标切换到假设 h。导航组合子和内部操作完全相同。

example (n m : ℕ) (h : 0 + n = m) : n = m := by
  conv at h => lhs; rw [Nat.zero_add]
  -- h 变为 h : n = m
  exact h

这个模式在需要"整理假设"后再引用时很常见。rw [...] at h 也能做到，但当假设的结构较深、需要只改某一处时，conv at h 的精度更高。

多重出现的精确控制

当同一子项在目标中多次出现时，conv 的价值最为突出。目标 ⊢ f a + f a = b + f a，如果只想改写第一个 f a（有引理 h : f a = b）：

1
2
3

example (f : ℕ → ℕ) (a b : ℕ) (h : f a = b) :
    f a + f a = b + f a := by
  conv_lhs => lhs; rw [h]

lhs 定位到加法的第一个参数 f a，rw [h] 只对这个位置生效。

rw 自身有 (config := { occs := .pos [1] }) 语法指定重写第几次出现，但 conv 的导航方式更直观，不依赖出现序号的计数——特别是当目标结构改变导致出现序号也变化时，conv 的路径更稳定。

calc 链式推导

calc 把一系列等式或不等式步骤组织成线性推导链。每一步给出关系和证明，Lean 通过传递性自动连接。

基本语法：

1
2
3

example (a b c : ℕ) (hab : a = b) (hbc : b = c) : a = c := by
  calc a = b := hab
    _ = c := hbc

每行 _ R expr := proof 中，_ 代表前一行的右端。proof 可以是 term 也可以是 by tactic_block。

涉及算术的例子：

example (n : ℕ) : (n + 1) * (n + 1) = n * n + 2 * n + 1 := by
  calc (n + 1) * (n + 1)
      = n * n + n + (n + 1) := by ring
    _ = n * n + 2 * n + 1 := by ring

这个例子直接用 ring 一步就能解决。calc 的价值在于复杂推导的可读性——把一个不明显的等式分解为若干"每步都显然"的小步骤，在涉及手动引理引用（而非纯算术）的场景下尤其有用。

InfoView 中的 calc

在 InfoView 中逐步执行 calc 时，光标停在哪一行，InfoView 就显示那一步需要证明的关系。第一行展示：

1	`⊢ (n + 1) * (n + 1) = n * n + n + (n + 1)`

第二行展示：

1	`⊢ n * n + n + (n + 1) = n * n + 2 * n + 1`

这种逐步查看机制在调试长推导链时非常有效——定位到出错的那一步，单独修复它的证明。

calc 与混合关系

calc 不限于等式。只要两个相邻步骤的关系有 Trans 实例，就可以混合使用。Mathlib 为常见的序关系注册了大量 Trans 实例：

import Mathlib.Tactic

example (a b c d : ℕ) (hab : a ≤ b) (hbc : b < c) (hcd : c ≤ d) :
    a < d := by
  calc a ≤ b := hab
    _ < c := hbc
    _ ≤ d := hcd

传递性链 ≤ → < → ≤ 最终得到 <。这种混合推导在分析类证明中非常常见。

#check @Trans.trans 可以查看 Trans 类型类的签名。#print instances Trans 可以列出当前环境中注册的所有 Trans 实例，了解哪些关系组合是合法的。

conv 与 calc 的结合

calc 中每一步的证明可以使用任意 tactic，包括 conv。两者结合解决的典型场景是：推导链中某一步需要对子表达式做精确重写。

example (f g : ℕ → ℕ) (n : ℕ) (hfg : ∀ x, f x = g x)
    (hg : g n + g n = 2 * g n) :
    f n + f n = 2 * g n := by
  calc f n + f n
      = g n + f n := by conv_lhs => lhs; rw [hfg]
    _ = g n + g n := by conv_lhs => rhs; rw [hfg]
    _ = 2 * g n := hg

第一步只重写加法左侧的 f n，第二步只重写右侧，第三步直接引用假设。calc 给出推导的宏观脉络，conv 处理每一步内部的精确定位。

term-mode 对照

calc 有对应的 term-mode 写法。等式链等价于连续的 Eq.trans：

-- tactic-mode
example (a b c : ℕ) (hab : a = b) (hbc : b = c) : a = c := by
  calc a = b := hab
    _ = c := hbc

-- term-mode
example (a b c : ℕ) (hab : a = b) (hbc : b = c) : a = c :=
  Eq.trans hab hbc

两步的等式链等价于一次 Eq.trans，三步等价于嵌套的 Eq.trans (Eq.trans hab hbc) hcd。步数越多，term-mode 的嵌套越深，可读性下降明显。calc 的线性排列在三步以上时几乎总是更好的选择。

conv 没有 term-mode 等价物。在证明项层面，精确重写对应的是手动构造包含 congrArg / congrFun 的 term，复杂度远超 conv 的导航语法。conv 属于"只在 tactic-mode 下可用"的工具。

用 #print 查看 conv 证明的底层证明项：

theorem conv_demo (n : ℕ) : 0 + n = n := by
  conv_lhs => rw [Nat.zero_add]

#print conv_demo
-- 输出的证明项包含 eq_self_iff_true 或类似的等式重写构造

#print axioms conv_demo 确认这个证明没有引入额外公理——只依赖 propext、Quot.sound 等 Lean 的标准公理。

实战经验

conv 的调试

在 conv 块内，光标停在不同导航指令之后时，InfoView 会实时显示当前焦点。利用这一点可以"逐步导航"——先写一个 arg 1，看 InfoView 里焦点是不是预期的子表达式，再决定下一步往哪走。

example (a b : ℕ) : a + (0 + b) = a + b := by
  conv_lhs =>
    arg 2
    -- 光标停在这里时 InfoView 显示 | ⊢ 0 + b
    rw [Nat.zero_add]

conv、simp only 与 rw 的选择

经验法则：

目标中只有一个需要重写的位置 → conv 定位后 rw
目标中多处需要同一引理重写 → simp only [lemma]
目标中多处出现同一子项但只想改其中几个 → conv 逐个定位

calc 的步骤粒度

calc 的步骤应该"每步都能被一个 tactic 一击解决"。如果某一步需要复杂的多行 tactic 证明，说明步骤拆得不够细。反过来，如果连续几步都用 rfl 就能关闭，说明步骤太细，可以合并。

给读者的练习

练习 1（基础）：用 conv 证明以下等式，只重写等号左侧的第二个 f a：

-- 给定 h : f a = b，证明：
example (f : ℕ → ℕ) (a b : ℕ) (h : f a = b) :
    f a + f a + f a = f a + b + f a := by
  sorry

提示：conv_lhs 进入后用 lhs 和 rhs 定位到加法的正确分支，然后用 arg 继续深入。

练习 2（中等）：用 calc 证明以下不等式链：

import Mathlib.Tactic

example (a b : ℕ) (h : a ≤ b) : a ≤ b + 1 := by
  sorry

提示：搭一个两步的 calc，用 h 和 Nat.le_succ 或 le_of_lt / Nat.lt_succ_of_le 组合。

练习 3（进阶）：结合 conv 和 calc 证明：

1
2
3

example (f : ℕ → ℕ) (n : ℕ) (h1 : f 0 = 1) (h2 : ∀ m, f m + f m = 2 * f m) :
    f 0 + f 0 = 2 := by
  sorry

提示：用 calc 搭链 f 0 + f 0 = 2 * f 0 = 2 * 1 = 2，在某一步内用 conv 精确替换 f 0 为 1。

本篇覆盖了 Lean 4 中精确控制重写位置的两个核心工具。conv 的导航组合子（lhs/rhs/arg/ext/enter）提供了在语法树上的移动能力，calc 的链式结构提供了复杂推导的可读性骨架。两者结合，能处理大多数"直接 rw 或 simp 不够用"的场景。下一篇将讨论自定义 tactic 与宏（第 08 篇），深入 macro/elab/syntax 三件套。