Lean 策略编程指南

3. 从零编写 rw🔗

本章从头实现一个简化版 rw，依次回答四个问题：rw 在证明项层面做了什么； 如何实现基本版本；怎样控制归一化；以及如何通过合一重写带量词的等式。

3.1. rw 在证明项层面做了什么🔗

先看一个使用 rw 的证明。第一次重写两个 f a，第二次重写两个 f b。

[可运行]

theorem rw_example (a b : Nat) (f : Nat → Nat) (p : Nat → Prop) (h_eq : ∀ x : Nat, f x = x) (h_finish : p (a + b + a + b)) : p (f a + f b + f a + f b) := a:Natb:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + b + a + b)⊢ p (f a + f b + f a + f b) a:Natb:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + b + a + b)⊢ p (a + f b + a + f b) -- 重写两处 `f a` a:Natb:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + b + a + b)⊢ p (a + b + a + b) -- 重写两处 `f b` All goals completed! 🐙 -- 打印它的证明项 theorem rw_example : ∀ (a b : Nat) (f : Nat → Nat) (p : Nat → Prop), (∀ (x : Nat), f x = x) → p (a + b + a + b) → p (f a + f b + f a + f b) := fun a b f p h_eq h_finish ↦ Eq.mpr (id (congrArg (fun _a ↦ p (_a + f b + _a + f b)) (h_eq a))) (Eq.mpr (id (congrArg (fun _a ↦ p (a + _a + a + _a)) (h_eq b))) h_finish)#print rw_example

打印结果应与下面的证明项相近。

[可运行]

example : ∀ (a b : Nat) (f : Nat → Nat) (p : Nat → Prop), (∀ (x : Nat), f x = x) → p (a + b + a + b) → p (f a + f b + f a + f b) := fun a b f p h_eq h_finish => Eq.mpr ( congrArg (fun X => p (X + f b + X + f b)) (h_eq a : f a = a) : p (f a + f b + f a + f b) = p (a + f b + a + f b) ) (Eq.mpr ( congrArg (fun X => p (a + X + a + X)) (h_eq b : f b = b) : p (a + f b + a + f b) = p (a + b + a + b) ) h_finish) -- 每次重写主要使用以下两个定理： congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂#check congrArg -- 深入子项 Eq.mpr.{u} {α β : Sort u} (h : α = β) (b : β) : α#check Eq.mpr -- 沿等式搬运证明

从 rw 使用的定理可以看出，它先实例化假设 h_eq，再用一次 congrArg 替换目标中的全部匹配项。

3.1.1. 插曲：id 的作用🔗

实际打印的证明里还可能出现恒等函数 id。它用于类型调整：当两个类型定义相等时， id 可以改变其值呈现出的类型。在元编程层面，这是由下面的函数加入证明项的。

[可运行]

Lean.Meta.mkExpectedPropHint (proof expectedProp : Expr) : Expr#check mkExpectedPropHint

3.2. 实现基本的 rw🔗

3.2.1. 抽象变量🔗

基本版本只用一个不带量词的等式重写项。设要在 e := ... A ... A ... 中用 A = B 重写。第一步要找出 e 中所有 A， 构造映射 fun X => ... X ... X ...。

这个过程叫作抽象。先定位 e 中所有 A，再把它们换成对应的绑定变量（bvar）。 bvar 以索引指向绑定子；索引从最内层绑定子向最外层计数。为确定该使用哪个索引， 递归时要携带 offset。

[可运行]

/-- （教程函数）简化版 `kabstract`。 -/ def myAbstract (e a : Expr) (offset : Nat := 0) : MetaM Expr := do if !e.hasLooseBVars then -- 不能重写包含由 `e` 内部绑定之变量的子项 if (← isDefEq e a) then -- 检查 `a` 是否已经位于根部 return mkBVar offset -- 换成绑定变量 -- 否则继续递归 match e with -- 按住 Ctrl 点击 `e.update...` 可查看定义 | .app f x => return e.updateApp! (← myAbstract f a offset) (← myAbstract x a offset) | .mdata _ b => return e.updateMData! (← myAbstract b a offset) -- `b` 是主体 | .proj _ _ b => return e.updateProj! (← myAbstract b a offset) | .letE _ t v b _ => return e.updateLetE! (← myAbstract t a offset) -- 进入绑定子，增大偏移量 (← myAbstract v a offset) (← myAbstract b a (offset + 1)) | .lam _ d b _ => return e.updateLambdaE! (← myAbstract d a offset) (← myAbstract b a (offset + 1)) | .forallE _ d b _ => return e.updateForallE! (← myAbstract d a offset) (← myAbstract b a (offset + 1)) | e => return e -- Lean 的实现稍复杂一些，但仍然易读。 Lean.Meta.kabstract (e p : Expr) (occs : Occurrences := Occurrences.all) : MetaM Expr#check kabstract -- 区别是 `kabstract` 可以选择应用重写的位置。 def myAbstractAt (pos : Nat) (e a : Expr) := kabstract e a (.pos [pos])

下面直接比较两个抽象函数，并观察如何选择位置。日志中的 #0 表示一个在打印项中 没有绑定子的 bvar。这个特定片段用 run_tacq 读取示例的局部上下文，其写法受 当前 InlineLean/SubVerso 的文档代码块处理限制，因此以下作为源码节选展示；完整 示例同时位于已编译的 Book.Support.CustomRw 支持模块中。

[源码节选·非精译]

open Book.Support.CustomRw

example (a b : Nat) (h : (2 * a + b + 1) = (2 * b + a + 1)) : True := by
  run_tacq
    let e1 ← myAbstract h.ty a
    let e2 ← kabstract h.ty a
    -- `kabstract` 与 `myAbstract` 做同一件事。
    logInfo m!"e1: {e1}\ne2: {e2}"
    -- 再看怎样为 `kabstract` 选择位置。
    logInfo m!"pos1: {← myAbstractAt 1 h.ty a}"
    logInfo m!"pos2: {← myAbstractAt 2 h.ty a}"
  trivial

练习。 不使用 kabstract，从零重新实现 myAbstractAt。你能看懂 kabstract 如何用状态单子完成位置计数吗？

现在可以构造 lambda 映射了。

[可运行]

open Book.Support.CustomRw /-- （教程函数）运行 `kabstract` 的简化实现，再用 lambda 包住结果。 -/ def abstractToMapping (e a : Expr) : MetaM Expr := do -- 确保此前所有元变量赋值都已应用到 `e`。 -- 这是递归遍历项所必需的；`isDefEq` 不需要，所以 `a` 不必如此处理。 let e ← instantiateMVars e let body ← myAbstract e a -- 把 `a` 换成 `bvar` return mkLambda `X -- 变量名；因为使用 `bvar`，不必担心名称冲突 BinderInfo.default -- 也可以是 `implicit` 等，例如花括号形式 (← inferType a) -- 变量的类型 body

用一个包含多种构造、而且故意复用 X 这个名字的表达式测试它。这个特定片段中 run_tacq 访问局部假设的写法受当前 InlineLean/SubVerso 限制，下面保留为非精译 源码节选；完整示例同时在支持模块中参与真实编译。

[源码节选·非精译]

open Book.Support.CustomRw

example (A : Nat) (h : -- 一个包含多种构造的复杂表达式
    ∀ (y : Nat), (y = A) →
    let z := A + y
    y + A = (fun (X : Nat) => X + A - y) z -- 同名也无妨
  ) : True := by
  -- `run_tacq` 类似 `run_tac`，但能直接访问上下文。
  -- 它不适合编写策略，却很适合测试。
  run_tacq
    logInfo m!"Before: {h.ty}" -- Qq 类型（编译期）
    let f ← abstractToMapping h.ty A
    logInfo m!"After: {f}"
  trivial

3.2.2. 分解等式🔗

下一步从等式证明中取出宇宙层级、类型和等式两端。

[可运行]

/-- （教程函数）`decomposeEq` 接受等式证明 `pf : a = b`，其中 `(a b : α : Sort u)`，返回 `(u, α, a, b)`。 -/ def decomposeEq (pf : Expr) : MetaM (Level × Expr × Expr × Expr) := do let t ← inferType pf -- `whnf` 有助于把 `Eq` 暴露在根部：它会去掉元数据、实例化元变量、展开定义等。 let t ← whnf t match t with | .app (.app (.app (.const ``Eq [u]) α) a) b => return (u, α, a, b) | _ => throwError "given term {pf} : {t} is not a proof of equality" -- 也可以用 `Expr.app3? ``Eq` 或 `matchEq?`，但后者不给出宇宙层级。 Lean.Expr.app3? (e : Expr) (fName : Name) : Option (Expr × Expr × Expr)#check Expr.app3?

3.2.3. 构造证明项🔗

proveRwImp 接受项 t := ... A ... 和等式 eq : A = B，返回 ... B ... → ... A ... 的证明。

[可运行]

open Book.Support.CustomRw /-- （教程函数）接受项 `t := ... A ...` 和等式 `eq : A = B`， 返回 `... B ... → ... A ...` 的证明。 -/ def proveRwImp (eq t : Expr) : MetaM Expr := do let (u, α, a, b) ← decomposeEq eq -- 找出抽象函数。 let f ← abstractToMapping t a logInfo m!"lhs := {a}, rhs := {b}\nabstr := {f}" -- 同时探测 `t` 的 Sort 层级；它通常是 Prop。 let tt ← inferType t let v := (← inferType tt).sortLevel! let rw_eq := mkApp6 -- 构造 `@congrArg.{u,v} α tt a b f eq : f a = f b` (mkConst ``congrArg [u, v]) α tt a b f eq logInfo m!"rw_eq := {rw_eq}" -- 已知 `f a = t`（定义相等）。下面用著名的 beta 归约计算 `f b`。 let fb := f.beta #[b] -- 语义上也可写成 `f.app b`，但那样得到的目标不够美观。 -- 可取消下一行的注释并比较差异： -- let fb := f.app b if !tt.isSort then -- 为什么要构造蕴含，`t` 就必须是 Sort？ throwError m!"Cannot convert equality between {tt} to an implication" -- 最后构造蕴含。`Eq.mpr` 的宇宙参数就是 `t` 与 `fb` 所在 Sort 的 -- 层级 `tt.sortLevel!`，这里不需要也不应做“减一”。 return mkApp3 (mkConst ``Eq.mpr [tt.sortLevel!]) t fb rw_eq congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂#check congrArg Eq.mpr.{u} {α β : Sort u} (h : α = β) (b : β) : α#check Eq.mpr

下面测试 proveRwImp，并在 run_tacq 脚本中完成目标重写。变量 t 展示了一个 可试验的非命题项；把它传给 proveRwImp 即可触发上面的诊断。这个特定片段对局部 策略上下文的用法受当前 InlineLean/SubVerso 限制，故展示源码而不在文档块中精译； 完整示例同时由支持模块编译验证。

[源码节选·非精译]

open Book.Support.CustomRw

example (a b : Nat) (h : a = b) : 2 * a + b = 2 * b + a := by
  run_tacq goal =>
    let t := q($a + 5 - $a)
    -- 若想观察非命题项的行为，可把上一项传给 `proveRwImp`。
    let imp ← proveRwImp h goal.ty
    let imp_t ← inferType imp
    -- 检验 `proveRwImp` 的结果。
    logInfo m!"imp : {imp_t}"
    -- 完成目标重写。
    let mt := imp_t.bindingDomain!
    logInfo m!"Build mvar of type {mt}"
    let m ← mkFreshExprSyntheticOpaqueMVar mt
    goal.mvarId!.assign (mkApp imp m)
    replaceMainGoal [m.mvarId!]
  -- 检查主目标确实已经重写成功。
  rfl

3.3. 归一化选项🔗

上述 rw 代码在两处执行归一化：分解等式时调用 whnf，以及用 isDefEq 判断是否抽象。完全归一化并非总是理想选择。下面看它可能造成什么结果。这个特定 局部上下文实验受当前 InlineLean/SubVerso 的文档代码块处理限制，以非精译源码 节选展示；完整示例仍由支持模块编译。

[源码节选·非精译]

def myAdd (a b : Nat) : Nat := a + b
def myEq (a b : Nat) : Prop := (a = b)

example (a b c : Nat) (h : myEq (myAdd a b) (myAdd b c))
    (h2 : a + b = c) : True := by
  run_tacq
    let htn ← whnf h.ty
    logInfo m!"{h.ty}\n→ {htn}" -- `whnf` 拆开 `myEq`
    let (u, α, lhs, rhs) ← Book.Support.CustomRw.decomposeEq h
    logInfo m!"lhs := {lhs}, rhs := {rhs}" -- 因而 `decomposeEq` 能拆分等式
    -- 这是个不错的特性。

    -- `isDefEq` 同样会展开定义。
    logInfo m!"({h.ty}) ?= ({htn}) : {← isDefEq h.ty htn}"
    -- 因而 `myAbstract` 也能捕获这种出现。
    logInfo m!"Abstracting ({lhs}) in ({h2.ty}):\n{← Book.Support.CustomRw.abstractToMapping h2.ty lhs}"
    -- 这相当让人困惑：`a + b = c` 中明明看不到 `(myAdd a b)`。
  trivial

两种情况下的归一化都由 Meta.Config 控制。

[可运行]

Lean.Meta.Config : Type#check Meta.Config

按住 Ctrl 点击该类型可以查看全部选项及其说明。值得留意的选项很多，例如 beta、 zeta 和 zetaDelta。又如，要避免把 1 + 3 与 4 认作相同，需要设置 offsetCnstrs := false。这里集中讨论透明度，也就是是否展开定义。

[可运行]

Lean.Meta.Config.transparency (self : Meta.Config) : TransparencyMode#check Meta.Config.transparency -- 最常用的选项如下。 Lean.Meta.TransparencyMode.default : TransparencyMode#check TransparencyMode.default Lean.Meta.TransparencyMode.reducible : TransparencyMode#check TransparencyMode.reducible -- 阻止展开上面的定义

下面设置 reducible 透明度。配置存放在 Reader 单子中，因此只读；不能替外部代码 修改配置，但可以让局部代码在修改后的配置下运行。这个特定 run_tacq 片段访问 局部假设的写法受当前 InlineLean/SubVerso 限制，故作为非精译源码节选；完整示例 同时在支持模块中编译。

[源码节选·非精译]

open Book.Support.CustomRw

#check withConfig
#check withTransparency

example (a b : Nat) (h1 : a = b) (h2 : myEq a b) : True := by
  run_tacq
    logInfo m!"isDefEq default: {← isDefEq h1.ty h2.ty}"
    -- 改变一般上下文的局部作用域。
    withConfig (fun cfg => { cfg with transparency := .reducible }) do
      -- 这里运行的一切都使用 reducible 透明度。
      logInfo m!"isDefEq reducible1: {← isDefEq h1.ty h2.ty}"
    -- 单独设置透明度有一个快捷方式。
    withTransparency .reducible do
      logInfo m!"isDefEq reducible2: {← isDefEq h1.ty h2.ty}"
    -- 将 `lhs` 与表达式匹配时应当这样做。

    -- `whnf` 也一样。
    logInfo m!"whnf default: {← whnf h2.ty}"
    withTransparency .reducible do
      logInfo m!"whnf reducible1: {← whnf h2.ty}"
    -- `whnfR` 是上一写法的快捷方式。
    logInfo m!"whnf reducible2: {← whnfR h2.ty}"
  trivial

3.4. 合一：重写带量词的等式🔗

现在要支持带量词的等式。例如已有规则 ∀ a b : Nat, p a + b = a + q b，希望用它把 p 1 + 2 重写为 1 + q 2。 核心做法是先把带量词的变量换成元变量，得到 p ?a + ?b = ?a + q ?b。这里右端的函数是 q；不能误写成调换 p 参数的式子。 此时左端除元变量外，在结构上与 p 1 + 2 相同，接下来只需找出元变量的取值。

3.4.1. 合一🔗

实际上，寻找元变量取值会自动发生。

[可运行]

example (unused variable `p` Note: This linter can be disabled with `set_option linter.unusedVariables false`p : Nat → Nat) : True := p:Nat → Nat⊢ True matching p 1 + 2 with p ?a + ?b → ?a + p ?bmatched p 1 + 2 with p 1 + 2 → 1 + p 2If match succeeded, the mvars are now assigned: a = 1, b = 2As a string, we still see the metavariables: a = ?_uniq.10971, b = ?_uniq.10972Unless we instantiate: a2 = OfNat.ofNat.{0} Nat 1 (instOfNatNat 1), b2 = OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)p:Nat → Nat⊢ True All goals completed! 🐙

可见，isDefEq 不只是无副作用的检查；它可以给元变量赋值，从而修改证明状态。 除了模基本归约检查相等外，它还尝试寻找满足等式的变量赋值。如果存在，就在证明状态中 执行赋值并返回 true；若返回 false，则证明状态没有改变。

3.4.2. 控制可赋值的元变量🔗

元变量能否被 isDefEq 自动赋值，取决于两个因素。第一个是元变量种类。

[可运行]

mSO1 = mSO2: falsemNat1 = mSyn1: truemNat2 = mSyn2: true?mSyn1 = ?mSyn1, ?mSyn2 = ?mSyn2mSyn1 = mSyn2: true?mSyn2 = ?mSyn2run_meta let mNat1 ← mkFreshExprMVarQ q(Nat) .natural `mNat1 let mNat2 ← mkFreshExprMVarQ q(Nat) .natural `mNat2 let mSyn1 ← mkFreshExprMVarQ q(Nat) .synthetic `mSyn1 let mSyn2 ← mkFreshExprMVarQ q(Nat) .synthetic `mSyn2 -- 相比 synthetic 元变量，natural 元变量优先被赋值。 logInfo m!"mNat1 = mSyn1: {← isDefEq mNat1 mSyn1}" logInfo m!"mNat2 = mSyn2: {← isDefEq mNat2 mSyn2}" logInfo m!"{mNat1} = {mSyn1}, {mNat2} = {mSyn2}" -- 但有需要时，synthetic 也可以被赋值。 logInfo m!"mSyn1 = mSyn2: {← isDefEq mSyn1 mSyn2}" logInfo m!"{mSyn1} = {mSyn2}" -- syntheticOpaque 则不行。 let mSO1 ← mkFreshExprMVarQ q(Nat) .syntheticOpaque `mSO1 let mSO2 ← mkFreshExprMVarQ q(Nat) .syntheticOpaque `mSO2 logInfo m!"mSO1 = mSO2: {← isDefEq mSO1 mSO2}"

我们还经常希望无论种类如何，都禁止给先前创建的元变量赋值。进入新的 MetavarContext.depth 即可做到。

[可运行]

Lean.Meta.withNewMCtxDepth.{u_1} {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (k : n α) (allowLevelAssignments : Bool := false) : n α#check withNewMCtxDepth ?mNat1 = ?mNat1mNat1 = mNat2: falsemSyn = mNat1: truerun_meta let mNat1 ← mkFreshExprMVarQ q(Nat) .natural `mNat1 let mNat2 ← mkFreshExprMVarQ q(Nat) .natural `mNat2 -- 通常优先给 natural 元变量赋值；进入新层级就能阻止它。 withNewMCtxDepth do logInfo m!"mNat1 = mNat2: {← isDefEq mNat1 mNat2}" -- 现在不能给它们赋值 let mSyn ← mkFreshExprMVarQ q(Nat) .synthetic `mSyn -- 但新建的 synthetic 元变量可以被赋成它们。 logInfo m!"mSyn = mNat1: {← isDefEq mSyn mNat1}" logInfo m!"{mSyn} = {mNat1}"

3.4.3. 带量词的 rw🔗

myAbstract 使用了 isDefEq，因此带量词等式的重写为何会匹配它的第一个实例， 现在并不意外。合一在首次可能时就发生；此后 f a 便不能再与 f b 合一。

最后，把量词变成元变量以补完实现。完成这件事的函数是 forallMetaTelescope。 这个特定脚本通过 run_tacq 操作局部目标的写法受当前 InlineLean/SubVerso 限制， 下面以非精译源码节选保留；完整示例及其复用的重写实现都在支持模块中编译。

[源码节选·非精译]

open Book.Support.CustomRw

#check forallMetaTelescope

-- 重写带量词的等式。
example (a b : Nat) (f : Nat → Nat) (p : Nat → Prop)
    (h_eq : ∀ x : Nat, f x = x) (h_finish : p (a + b + a + b)) :
    p (f a + f b + f a + f b) := by
  run_tacq goal =>
    let imp ← withNewMCtxDepth do
      let (mvars, _, eq) ← forallMetaTelescope h_eq.ty -- 把量词变成元变量
      let pf_eq := mkAppN h_eq mvars -- 构造证明项
      logInfo m!"before: {pf_eq} : {eq}"
      -- 使用与前面相同的重写代码。
      let imp ← withTransparency .reducible <| proveRwImp pf_eq goal.ty
      logInfo m!"after: {pf_eq} : {eq}"
      -- 退出 MCtx 上下文前必须实例化变量。
      instantiateMVars imp
    let imp_t ← inferType imp
    logInfo m!"imp_t2 := {imp_t}"
    let mt := imp_t.bindingDomain!
    let m ← mkFreshExprSyntheticOpaqueMVar mt
    goal.mvarId!.assign (mkApp imp m)
    replaceMainGoal [m.mvarId!]
  -- 已成功把 `f a` 重写为 `a`。
  rw [h_eq b] -- 第二步直接使用普通的 `rw`。
  trivial

练习：实现完整的 my_rw 策略。 下列模板故意调用尚未实现的 my_rw。fail_if_success 把预期的精译失败隔离起来，所以书可以构建， 又不会把未完成练习冒充成实现。完成练习时，应删掉语法占位和两层 fail_if_success，实现 my_rw，并恢复原题中的三行证明。

[练习·故意错误]

-- 这里只声明语法，不提供策略精译器：`my_rw` 仍未实现。 syntax "my_rw " term : tactic example (a b : Nat) (f : Nat → Nat) (p : Nat → Prop) (h_eq : ∀ x : Nat, f x = x) (h_finish : p (a + b + a + b)) : p (f a + f b + f a + f b) := a:Natb:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + b + a + b)⊢ p (f a + f b + f a + f b) fail_if_success a:Natb:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + b + a + b)⊢ p (f a + f b + f a + f b) -- 原题：`my_rw h_eq` fail_if_success a:Natb:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + b + a + b)⊢ p (f a + f b + f a + f b) -- 原题：`my_rw h_eq` All goals completed! 🐙 -- 原题：`exact h_finish`