4. 从零编写 simp🔗

本章从证明项层面解释 simp，然后逐步实现一个小型简化器。内容依次是：simp 究竟构造什么证明项、补隐式参数、自定义结果类型、基本递归简化、trace 调试、进入绑定器，以及收集带标签的引理。为避免混淆，下文把每段程序明确标为可运行、示意、练习模板、故意错误或源码节选；完整可编译实现位于 Book/Support/CustomSimp.lean。

4.1. 1. `simp` 在证明项层面做什么🔗

simp 不像 rw 那样把全部相等改写一次完成。它递归进入表达式；合并两个都发生了变化的分支时，使用 congr 以及 congrArg、congrFun 一类同余定理。

[可运行]

congr.{u, v} {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂#check congr
congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂#check congrArg
congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a#check congrFun

考虑下列证明。simp only [h_eq] 会在三个位置改写 f；紧随其后的 #print 保留了原教程“观察生成证明项”的教学步骤。这两项也以 CustomSimpSupport.simpProofTermExample 及其 #print 在支持模块中编译。

[可运行]

theorem simp_example (a b c : Nat) (f : Nat → Nat) (p : Nat → Prop)
    (h_eq : ∀ x : Nat, f x = x)
    (h_finish : p (a + c + b + c + a + c)) :
    p (f a + c + f b + c + f a + c) := bya:Natb:Natc:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + c + b + c + a + c)⊢ p (f a + c + f b + c + f a + c)
  simp only [h_eq]a:Natb:Natc:Natf:Nat → Natp:Nat → Proph_eq:∀ (x : Nat), f x = xh_finish:p (a + c + b + c + a + c)⊢ p (a + c + b + c + a + c)
  exact h_finishAll goals completed! 🐙

theorem simp_example : ∀ (a b c : Nat) (f : Nat → Nat) (p : Nat → Prop),
  (∀ (x : Nat), f x = x) → p (a + c + b + c + a + c) → p (f a + c + f b + c + f a + c) :=
fun a b c f p h_eq h_finish ↦
  Eq.mpr
    (id
      (congrArg p
        (congrFun'
          (congrArg HAdd.hAdd
            (congr
              (congrArg HAdd.hAdd
                (congrFun'
                  (congrArg HAdd.hAdd
                    (congr (congrArg HAdd.hAdd (congrFun' (congrArg HAdd.hAdd ((fun x ↦ h_eq x) a)) c))
                      ((fun x ↦ h_eq x) b)))
                  c))
              ((fun x ↦ h_eq x) a)))
          c)))
    h_finish#print simp_example

整理后的完整证明项如下。表达式是逐层建成的；h_eq a 在证明项里出现两次，因为两个位置分别改写，这一点也与一次多处替换的 rw 不同。InlineLean 对这种包含占位函数 (·) 和密集类型 ascription 的长项高亮有限，故标为源码节选；同一项在 Book/Support/CustomSimp.lean 中并非注释，而是由 Lean 完整检查。

[源码节选；支持模块已编译]

/-
example (a b c : Nat) (f : Nat → Nat) (p : Nat → Prop)
    (h_eq : ∀ x : Nat, f x = x)
    (h_finish : p (a + c + b + c + a + c)) :
    p (f a + c + f b + c + f a + c) :=
  Eq.mpr
  (congrArg (fun X => p (X + c))
    (congr
      (congrArg (fun X => (X + c + ·))
        (congr
          (congrArg
            (fun X => (X + c + ·)) (h_eq a : f a = a)
            : (f a + c + ·) = (a + c + ·))
          (h_eq b : f b = b)
          : f a + c + f b = a + c + b)
        : (f a + c + f b + c + ·) = (a + c + b + c + ·))
      (h_eq a : f a = a)
      : f a + c + f b + c + f a = a + c + b + c + a)
    : p (f a + c + f b + c + f a + c) =
      p (a + c + b + c + a + c))
  h_finish
-/
unexpected end of input

递归同余并不比 rw 无条件地更一般。尤其是依赖类型中，同一个索引同时决定项的类型时，局部同余步骤可能无法保持类型正确；rw 能一次运输所有相关位置。这个限制不是说所有依赖改写都失败，而是本章这种逐子项合并的同余算法没有一般的 dependent congruence 支持。

[可运行]

example (a b : Nat) (h_eq : a = b) (p : ∀ n : Nat, Fin n → Prop)
    (h : ∀ y : Fin b, p b y) : ∀ x : Fin a, p a x := bya:Natb:Nath_eq:a = bp:(n : Nat) → Fin n → Proph:∀ (y : Fin b), p b y⊢ ∀ (x : Fin a), p a x
  try simp only [h_eq]a:Natb:Nath_eq:a = bp:(n : Nat) → Fin n → Proph:∀ (y : Fin b), p b y⊢ ∀ (x : Fin a), p a x
  rw [h_eq]a:Natb:Nath_eq:a = bp:(n : Nat) → Fin n → Proph:∀ (y : Fin b), p b y⊢ ∀ (y : Fin b), p b y
  exact hAll goals completed! 🐙

4.2. 2. 补齐隐式参数🔗

手写 congrArg 和 Eq.mpr 时，显式填写宇宙层级与隐式参数很繁琐。以下四种方式都能构造 Eq.trans pf1 pf2：低层 mkApp6 要提供全部参数；Qq 准引号携带静态类型标注； mkAppM 在 MetaM 执行时推断隐式参数；常见操作还常有 mkEqTrans 这样的专用函数。

[源码节选；支持模块已编译] 下面保留完整 example、普通项与四种元构造，并在 Book/Support/CustomSimp.lean 中逐一用 isDefEq 验证结果，不以日志输出冒充测试。

/-
example (a b c : Nat) (pf1 : a = b) (pf2 : b = c) : True := by
  have pf3 : a = c := Eq.trans pf1 pf2
  have pf3' := @Eq.trans.{1} Nat a b c pf1 pf2
  run_tacq
    let lowlev :=
      mkApp6 (mkConst ``Eq.trans [1]) (mkConst ``Nat) a b c pf1 pf2
    logInfo m!"lowlev = {lowlev}"
    let pfQ : Q($a = $c) := q(Eq.trans $pf1 $pf2)
    logInfo m!"pfq = {pfQ}"
    let pfAppM ← mkAppM ``Eq.trans #[pf1, pf2]
    logInfo m!"pfAppM = {pfAppM}"
    let pfEqT ← mkEqTrans pf1 pf2
    logInfo m!"pfEqT = {pfEqT}"
  trivial
-/
unexpected end of input

准确地说，Qq 利用元程序在 Lean elaboration 时已经获得的类型索引来检查准引号；但准引号所表示的 Expr 仍在元程序运行时被构造。mkAppM 则在元程序执行于 MetaM 时，查询当前环境和元变量上下文并推断参数。不能简单把二者说成“Qq 只在编译期运行、 mkAppM 只在运行期运行”。

[可运行]

CustomSimpSupport.buildTransQ {u : Level} {α : Q(Sort u)} {a b c : Q(«$α»)} (pf1 : Q(«$a» = «$b»))
  (pf2 : Q(«$b» = «$c»)) : Q(«$a» = «$c»)#check CustomSimpSupport.buildTransQ
CustomSimpSupport.buildTransM (pf1 pf2 : Expr) : MetaM Expr#check CustomSimpSupport.buildTransM

buildTransM 必须处在 MetaM，这样才有足够上下文推断表达式类型和隐式参数。 buildTransQ 本身不需要 MetaM，但其 u α a b c 类型索引虽由调用者隐式传入，仍是正确构造结果的关键。本章后面采用 mkAppM；Qq 也完全可用，只是标注管理更细碎。

4.2.1. 练习：构造算术表达式🔗

定义 myCalculation，接收两个 Nat、Int 或 Rat 表达式 a b，构造 a + b * a，并自动推断类型及相应类型类实例。可以尝试专用函数、mkAppM 和 Qq。编辑文件中部时，可暂放 #exit 阻止 Lean 重编译后文，完成后务必删除。

[练习模板] 复制下面整个 harness；可先走 mkAppM 路径，也可把调用切换到 myCalcQ2。支持模块保留同名 Qq 占位路径及三种数系的完整检查。

/-
def myCalculation (a b : Expr) : MetaM Expr := do
  return a

-- 预备占位；Qq 解法需要把签名改成合适的 Q(...)。
def myCalcQ2 (a : Expr) (b : Expr) : Expr := a

example (a b : Nat) (c d : Int) (e f : Rat) : True := by
  run_tacq
    let ab ← myCalculation a b
    -- let ab := myCalcQ2 a b
    let cd ← myCalculation c d
    -- let cd := myCalcQ2 c d
    let ef ← myCalculation e f
    -- let ef := myCalcQ2 e f
    logInfo m!"ab := {ab}, cd := {cd}, ef := {ef}"
    unless ← isDefEq ab q($a + $b * $a) do
      throwError "ab := {ab} != a+b*a"
    unless ← isDefEq cd q($c + $d * $c) do
      throwError "cd := {cd} != c+d*c"
    unless ← isDefEq ef q($e + $f * $e) do
      throwError "ef := {ef} != e+f*e"
  trivial
-/
unexpected end of input

Qq 提示：它能推断实例，但不能把实例直接写成隐式的 [Q(HAdd $α $α $α)]。先将 Q(HAdd $α $α $α) 作为显式参数，并在调用处插入 q(inferInstance)；乘法同理。进一步可用一个由 exact 策略填充的默认参数，把实例推断推迟到合适阶段。

[负测试；支持模块已编译] 占位实现只返回 a。支持模块不是把失败藏进注释，而用 fail_if_success 实际执行上述断言，并同时验证 myCalcQ2 占位也不能通过。

CustomSimpSupport.myCalculationPlaceholder (a _b : Expr) : MetaM Expr#check CustomSimpSupport.myCalculationPlaceholder
CustomSimpSupport.myCalcQ2 (a _b : Expr) : Expr#check CustomSimpSupport.myCalcQ2

[可运行] 参考实现用 HMul.hMul 与 HAdd.hAdd，支持模块已对三种数系执行同一组 isDefEq 检查。

CustomSimpSupport.myCalculation (a b : Expr) : MetaM Expr#check CustomSimpSupport.myCalculation

4.3. 3. 自定义 `SimpResult`🔗

简化 a 的输出是同类型的新表达式 expr，以及证明 pf : a = expr。如果没有发生简化，令 pf? = none，避免制造无用的 rfl；需要完整证明时再补。库中的 Simp.Result 与带 Qq 标注的 Simp.ResultQ 采用相近设计。

[可运行]

CustomSimpSupport.SimpResult : Type#check CustomSimpSupport.SimpResult
Lean.Meta.Simp.Result : Type#check Simp.Result
Lean.Meta.Simp.ResultQ {u : Level} {α : Q(Sort u)} (_e : Q(«$α»)) : Type#check Simp.ResultQ

empty 建立空结果；getProof 在必要时用 Eq.refl；trans 用 Eq.trans 串接结果。

[源码节选]

/-
def SimpResult.empty (e : Expr) : SimpResult := { expr := e, pf? := none }

def SimpResult.getProof (r : SimpResult) : MetaM Expr :=
  match r.pf? with
  | some pf => pure pf
  | none => mkAppM ``Eq.refl #[r.expr]

def SimpResult.trans (r1 r2 : SimpResult) : MetaM SimpResult := do
  match r1.pf?, r2.pf? with
  | none, _ => return r2
  | some pf1, none => return { expr := r2.expr, pf? := some pf1 }
  | some pf1, some pf2 =>
    return { expr := r2.expr, pf? := some (← mkAppM ``Eq.trans #[pf1, pf2]) }
-/
unexpected end of input

应用节点要组合函数结果 f = g 与参数结果 a = b。都不变则为空；只改参数用 congrArg；只改函数用 congrFun；两边都改用 congr。库中对应辅助函数是 mkCongr、mkCongrArg、mkCongrFun。

[可运行]

CustomSimpSupport.SimpResult.app (rf rArg : SimpResult) : MetaM SimpResult#check CustomSimpSupport.SimpResult.app
Lean.Meta.mkCongr (h₁ h₂ : Expr) : MetaM Expr#check mkCongr
Lean.Meta.mkCongrArg (f h : Expr) : MetaM Expr#check mkCongrArg
Lean.Meta.mkCongrFun (h a : Expr) : MetaM Expr#check mkCongrFun

4.4. 4. 基本 `simp` 实现🔗

算法分成两层。simProcBasic rules a 的作用域严格限于 a 的根：它按顺序寻找可匹配的（也可带全称量词的）等式规则，至多做一次根部改写，不查看 a 的子表达式，也不负责反复归约。递归函数 simpRec0 才访问应用树各处、调用根部过程，并在成功后重复。

[源码节选]

/-
def simProcBasic (rules : List Expr) (a : Expr) : MetaM SimpResult :=
  withNewMCtxDepth do
    for rule in rules do
      let eq ← whnf (← inferType rule)
      let (mvars, _, eq) ← forallMetaTelescope eq
      let some (_, ar, br) := eq.app3? ``Eq
        | throwError "Not an equality: {rule} : {eq}"
      if ← withTransparency .reducible (isDefEq a ar) then
        let br ← instantiateMVars br
        let pf := mkAppN rule (← mvars.mapM instantiateMVars)
        return { expr := br, pf? := some pf }
    return .empty a
-/
unexpected end of input

withNewMCtxDepth 隔离匹配产生的元变量；forallMetaTelescope 把量词实例化为元变量； isDefEq 在 reducible 透明度下匹配左端；成功后实例化右端与证明。

[源码节选] run_tacq 局部上下文测试在支持模块中编译。

/-
let e := q($f ($a + $b))
let res ← simProcBasic [h] e
logInfo m!"Simplify ({e}) to: {res.expr}"
logInfo m!"Proof term: {res.pf?}"
-/
unexpected end of input

[源码节选]

/-
partial def simpRec0 (simProc : Expr → MetaM SimpResult) (a : Expr) := do
  let an ← whnfR a
  let res ← match an with
    | .app f arg => (← simpRec0 simProc f).app (← simpRec0 simProc arg)
    | _ => pure (.empty an)
  let resProc ← simProc res.expr
  if resProc.pf?.isNone then return res
  let res ← res.trans resProc
  res.trans (← simpRec0 simProc res.expr)
-/
unexpected end of input

这里声明 partial，因为规则可能循环，Lean 无法证明终止。第二个测试把 h_test : 2 * f a = f b * 3 的类型递归化简，并检查结果确为 2 * a = b * 3，同时确认生成了可推断类型的证明项。

[源码节选；支持模块已编译]

/-
example (a b : Nat) (f : Nat → Nat) (h : ∀ x, f x = x)
    (h_test : 2 * f a = f b * 3) : True := by
  run_tacq
    let res ← simpRec0 (simProcBasic [h]) h_test.ty
    logInfo m!"Simplify ({h_test.ty}) to: {res.expr}"
    logInfo m!"Proof term: {res.pf?}"
    unless ← isDefEq res.expr q(2 * $a = $b * 3) do
      throwError "unexpected recursive result"
  trivial
-/
unexpected end of input

[可运行]

CustomSimpSupport.simProcBasic (rules : List Expr) (a : Expr) : MetaM SimpResult#check CustomSimpSupport.simProcBasic
CustomSimpSupport.simpRec0 (simProc : Expr → MetaM SimpResult) (a : Expr) : MetaM SimpResult#check CustomSimpSupport.simpRec0

4.4.1. 借用库的 `simp` 基础设施🔗

库的设计同样模块化，并有更多功能。可以保留自定义 simProcBasic，却把递归交给 Simp.main；库实现还能进入绑定器。将自定义结果转为 Simp.Step 时，无变化返回 continue，有变化返回 visit；done、visit、continue 还能控制后续访问与重复。

[源码节选；支持模块已编译] 此块依赖 run_tacq goal => 的 goal 上下文；这里保留从上下文、simproc、methods、Simp.main 到应用结果及完成目标的完整组合。支持模块执行的是同一示例，并检查“无进展”分支。

/-
example (a b c : Nat) (p : Nat → Nat → Prop)
    (h₁ : a = b) (h₂ : b = c) (finish : ∀ x, p x c → p x c) :
    (∀ x, p x a → p x a) := by
  run_tacq goal =>
    let ctx : Simp.Context ← Simp.mkContext
    let method : Simp.Simproc := fun e : Expr => do
      let res ← simProcBasic [h₁, h₂] e
      if res.pf?.isNone then return Simp.Step.continue
      else return Simp.Step.visit { expr := res.expr, proof? := res.pf? }
    let methods : Simp.Methods := { pre := method }
    let (res, _stats) ← Simp.main goal.ty ctx (methods := methods)
    logInfo m!"Simplify ({goal.ty}) to: {res.expr}"
    logInfo m!"Proof term: {res.proof?}"
    let mvarIdNew ← applySimpResultToTarget goal.mvarId! goal.ty res
    if mvarIdNew == goal.mvarId! then throwError "simp made no progress"
    replaceMainGoal [mvarIdNew]
  exact finish
-/
unexpected end of input

[可运行]

Lean.Meta.Simp.Simproc : Type#check Simp.Simproc
Lean.Meta.Simp.main (e : Expr) (ctx : Simp.Context) (stats : Simp.Stats := { }) (methods : Simp.Methods := { }) :
  MetaM (Simp.Result × Simp.Stats)#check Simp.main
Lean.Meta.applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result) : MetaM MVarId#check applySimpResultToTarget

4.5. 5. 用 trace 调试🔗

logInfo 适合基本调试，但隐藏输出时要删代码，消息多时也会混乱。Lean 的 trace 系统允许按类别开关；例如 whnf 内部可能产生 trace.Meta.whnf。可以用 withOptions 临时设置，也可注册自己的类别并调用 trace[WhateverName]。

[源码节选；支持模块已编译] run_meta 与 trace 宏的命令上下文可能受 InlineLean 限制；支持模块真实执行以下基础示例，并产生 Meta.whnf、WhateverName 与 MyTrace 输出。

/-
run_meta
  let e1 : Q(Nat) := q(let x := 3; x^2)
  let e2 ← withOptions (fun opt => opt.setBool `trace.Meta.whnf true) do
    whnf e1
  logInfo m!"logInfo e2: {e2}"

run_meta
  withOptions (fun opt => opt.setBool `trace.WhateverName true) do
    trace[WhateverName] m!"Hello trace"

set_option trace.MyTrace true in
run_meta
  trace[MyTrace] m!"Hello trace"
-/
unexpected end of input

通常使用 set_option。trace 类必须在导入文件中注册；本项目在 TutorialAux/Init.lean 注册 MyTrace。可局部打开，也可全局打开后再关闭。

[示意]

/-
set_option trace.MyTrace true in
run_meta
  trace[MyTrace] m!"Hello trace"

set_option trace.MyTrace true
set_option trace.MyTrace false
-/
unexpected end of input

4.5.1. 树状 trace🔗

withTraceNode、withTraceNode'、withTraceNodeBefore 可把消息组成树。教程包装 withTraceNodeBefore'，让调用者直接给字符串或表达式，不必手写返回消息的函数。

[可运行]

Lean.withTraceNode {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadRef m] [AddMessageContext m]
  [MonadOptions m] {ε : Type} [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToTraceResult ε α]
  (cls : Name) (msg : Except ε α → m MessageData) (k : m α) (collapsed : Bool := true) (tag : String := "") : m α#check withTraceNode
Lean.withTraceNode' {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadRef m] [AddMessageContext m]
  [MonadOptions m] [MonadAlwaysExcept Exception m] [MonadLiftT BaseIO m] (cls : Name) (k : m (α × MessageData))
  (collapsed : Bool := true) (tag : String := "") : m α#check withTraceNode'
Lean.withTraceNodeBefore {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] {ε : Type} [MonadRef m]
  [AddMessageContext m] [MonadOptions m] [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
  [ExceptToTraceResult ε α] (cls : Name) (msg : Unit → m MessageData) (k : m α) (collapsed : Bool := true)
  (tag : String := "") : m α#check withTraceNodeBefore
CustomSimpSupport.withTraceNodeBefore' {α μ : Type} {m : Type → Type} [Monad m] [MonadTrace m] {ε : Type} [MonadRef m]
  [AddMessageContext m] [MonadOptions m] [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
  [ExceptToTraceResult ε α] [ToMessageData μ] (cls : Name) (msg : μ) (k : m α) (collapsed : Bool := true)
  (tag : String := "") : m α#check CustomSimpSupport.withTraceNodeBefore'

withTraceNodeBefore 在开始时计算节点消息，在结束时根据结果计算图标。Option、Bool 已有默认结果解释；自定义类型可实现 ExceptToTraceResult。本章对 SimpResult 的约定是：有证明为成功（✅），无证明为失败（❌），抛异常为错误（💥）。

[源码节选]

/-
instance : ExceptToTraceResult Exception SimpResult where
  toTraceResult x := match x.map SimpResult.pf? with
    | .ok (some _) => .success
    | .ok none => .failure
    | .error _ => .error
-/
unexpected end of input

树状示例先输出 Start，在 Pack 1 中建立子节点并得到 40，最后输出可选结果。可把 pure (some a) 换成 none 或 throwError "Crashed" 来观察不同图标。另一个 Pack 2 示例记录 expr := 2 和 pf : 1 + 1 = 2。两段均在支持模块真实执行；构建日志会显示嵌套树，而不只是检查辅助函数名称。

[源码节选；支持模块已编译]

/-
set_option trace.MyTrace true in
run_meta
  trace[MyTrace] "Start"
  let res? : Option Nat
      ← withTraceNodeBefore' `MyTrace "Pack 1" do
    trace[MyTrace] "Start inside"
    let a : Nat ← withTraceNode' `MyTrace do
      trace[MyTrace] "Double inside"
      pure (40, m!"obtaining 40")
    trace[MyTrace] "Subresult {a}"
    pure (some a)
  trace[MyTrace] "Result is {res?}"

set_option trace.MyTrace true in
run_meta
  let _res : SimpResult
      ← withTraceNodeBefore' `MyTrace "Pack 2" do
    let expr := q(2)
    let pf : Q(1 + 1 = 2) := q(rfl)
    trace[MyTrace] "expr := {expr}"
    trace[MyTrace] "pf := {pf}"
    pure ⟨expr, some pf⟩
-/
unexpected end of input

SimpResult.trace 只记录非空结果，并把证明项放在标记为 (proof term) 的子节点中。

[源码节选；定义在支持模块中编译]

/-
def SimpResult.trace (res : SimpResult) : MetaM Unit := do
  match res.pf? with
  | some pf =>
    trace[MyTrace] "=> {res.expr}"
    withTraceNode' `MyTrace do
      trace[MyTrace] pf
      pure ((), "(proof term)")
  | _ => pure ()
-/
unexpected end of input

4.6. 6. 在绑定器内部实现 `simp`🔗

库的 simp 可进入 ∀ x, p x a → p x a，证明项使用 implies_congr 与 forall_congr。原教程在这里再次用 #print 观察绑定器下的证明项；支持模块以 CustomSimpSupport.simpProofTermExample2 编译同一定理及打印命令。

[可运行]

theorem simp_example2 (a b c : Nat) (p : Nat → Nat → Prop)
    (h₁ : a = b) (h₂ : b = c)
    (finish : ∀ x, p x c → p x c) :
    ∀ x, p x a → p x a := bya:Natb:Natc:Natp:Nat → Nat → Proph₁:a = bh₂:b = cfinish:∀ (x : Nat), p x c → p x c⊢ ∀ (x : Nat), p x a → p x a
  simp only [h₁, h₂]a:Natb:Natc:Natp:Nat → Nat → Proph₁:a = bh₂:b = cfinish:∀ (x : Nat), p x c → p x c⊢ ∀ (x : Nat), p x c → p x c
  exact finishAll goals completed! 🐙

theorem simp_example2 : ∀ (a b c : Nat) (p : Nat → Nat → Prop),
  a = b → b = c → (∀ (x : Nat), p x c → p x c) → ∀ (x : Nat), p x a → p x a :=
fun a b c p h₁ h₂ finish ↦
  Eq.mpr (id (forall_congr fun x ↦ implies_congr (congrArg (p x) (Eq.trans h₁ h₂)) (congrArg (p x) (Eq.trans h₁ h₂))))
    finish#print simp_example2

我们为自定义结果补上 implies_congr 与 forall_congr 两个组合器。

[可运行]

implies_congr.{u, v} {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)#check implies_congr
forall_congr.{u} {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), p a = q a) : (∀ (a : α), p a) = ∀ (a : α), q a#check forall_congr
CustomSimpSupport.SimpResult.impl (r1 r2 : SimpResult) : MetaM SimpResult#check CustomSimpSupport.SimpResult.impl
CustomSimpSupport.SimpResult.forallResult (fv : Expr) (r : SimpResult) : MetaM SimpResult#check CustomSimpSupport.SimpResult.forallResult

impl 从 a = b、c = d 构造 (a → c) = (b → d)；forallResult 接收自由变量 fv 下的点态证明 p fv = q fv，先用 mkLambdaFVars 绑定证明，再调用 forall_congr 得到 (∀ x, p x) = (∀ x, q x)。可参考库函数 mkImpCongr 和 mkForallCongr。

[源码节选]

/-
| .forallE _name t body _bi =>
  if !body.hasLooseBVars then
    let rt ← simpRec simProc t
    let rBody ← simpRec simProc body
    rt.impl rBody
  else if !(← isProp an) then
    pure (.empty an)
  else
    forallBoundedTelescope an (some 1) fun fvars body => do
      let res ← simpRec simProc body
      res.forallResult fvars[0]!
-/
unexpected end of input

这里必须强调限制：非依赖 forallE 实际表示蕴含，可用 implies_congr；依赖分支只有整个全称式是 Prop 时才用 forall_congr。这不是一般 dependent congruence：对产生 Type 的依赖函数类型不做改写。forallBoundedTelescope ... (some 1) 只展开一层，把裸 Expr 中的 bound variable 换成局部上下文里的 free variable。

mySimpGoal 读取主目标，在上下文中调用 simpRec。若无进展则保留诊断字符串 "mySimpGoal made no progress"；成功时建立新目标 res.expr，并用 Eq.mpr 把它的证明运输回旧目标。

[可运行]

example (a b c : Nat) (p : Nat → Nat → Prop)
    (h₁ : a = b) (h₂ : b = c) (finish : ∀ x, p x c → p x c) :
    ∀ x, p x a → p x a := bya:Natb:Natc:Natp:Nat → Nat → Proph₁:a = bh₂:b = cfinish:∀ (x : Nat), p x c → p x c⊢ ∀ (x : Nat), p x a → p x a
  run_tacq CustomSimpSupport.mySimpGoal (CustomSimpSupport.simProcBasic [h₁, h₂])a:Natb:Natc:Natp:Nat → Nat → Proph₁:a = bh₂:b = cfinish:∀ (x : Nat), p x c → p x c⊢ ∀ (x : Nat), p x c → p x c
  exact finishAll goals completed! 🐙

4.6.1. 练习：存在量词🔗

当前实现专门识别 forallE，没有给存在量词提供结构化同余分支。扩展 simpRec，使它显式、稳健地处理 ∃ x, p x a，而不是偶然依赖 Exists 的应用编码。

[练习模板] 下面是可复制的完整 harness。先补 simpRec 的存在量词分支，再移除 fail_if_success 和末尾的标准 simpa 回退；届时内部两行应直接完成目标。

/-
example (a b : Nat) (p : Nat → Nat → Prop)
    (h : a = b) (finish : ∃ x, p x b) :
    (∃ x, p x a) := by
  fail_if_success
    run_tacq mySimpGoal (simProcBasic [h])
    exact finish
  simpa only [h] using finish
-/
unexpected end of input

[负测试；支持模块已编译] 当前 forall_congr 分支不会自动覆盖存在量词。支持模块原样执行 run_tacq mySimpGoal ...; exact finish，并由 Lean 的 fail_if_success 确认它确实失败；回退证明只用于让整个测试定理可编译，不把预期失败注释掉。

4.7. 7. 收集带标签的引理🔗

标准 simp 不要求每次列出全部规则，而会读取 @[simp]。这里定义 my_tag。初始化分两步：registerSimpleScopedEnvExtension 建立 myExt，保存带标签定理的名称与类型； registerBuiltinAttribute 注册属性并在添加时写入扩展。初始化定义必须先在一个被导入模块中完成，之后才能给本章定理加属性。实际文件是 TutorialAux/Tag.lean； TutorialAux/Init.lean 导入它并另行注册 MyTrace。这修正了原文提到但仓库中缺失的 TutorialAux/Tag.lean 引用。

[源码节选]

/-
initialize myExt :
    SimpleScopedEnvExtension (Expr × Expr) (Array (Expr × Expr)) ←
  registerSimpleScopedEnvExtension {
    addEntry := fun arr et => arr.push et
    initial := #[]
  }

initialize registerBuiltinAttribute {
  name := `my_tag
  descr := "a custom tag"
  add := fun name _stx _kind ↦ MetaM.run' do
    let e : Expr := mkConst name
    let t ← inferType e
    myExt.add (e, t)
}
-/
unexpected end of input

这里有一处重要的 monad 边界：BuiltinAttribute.add 的 hook 运行在 CoreM，而 inferType 需要 MetaM，所以 MetaM.run' do 明确把 hook 从 CoreM 带入一个新的 MetaM 上下文。这个教学版 hook 没有检查合法性：它不确认被标记声明是否真是定理、其类型是否为等式、改写方向是否合理，也不处理 universe 参数；错误可能直到登记时的 inferType 或稍后 simProcTag 解构 Eq 时才出现。生产属性应在 add 中尽早验证并给出定位清楚的诊断。

支持模块给结合律反向、a + a = 2 * a 等定理直接加 @[my_tag]，也展示先定义再用 attribute [my_tag] 添加。读取 myExt.getState (← getEnv) 即可遍历 (e, t)。

[可运行]

myExt : SimpleScopedEnvExtension (Expr × Expr) (Array (Expr × Expr))#check myExt
CustomSimpSupport.add_assoc_rev (a b c : Nat) : a + (b + c) = a + b + c#check CustomSimpSupport.add_assoc_rev
CustomSimpSupport.two_mul_rev (a : Nat) : a + a = 2 * a#check CustomSimpSupport.two_mul_rev
CustomSimpSupport.simProcTag (expr : Expr) : MetaM SimpResult#check CustomSimpSupport.simProcTag

simProcTag 与 simProcBasic 的主要区别是规则来自环境扩展。每次尝试时用 forallMetaTelescope t 新建量词元变量，以 mkAppN e mvars 构造证明，再匹配等式左端；成功后实例化右端和证明。

[可运行]

example (a : Nat) (p : Nat → Prop) (h : p (4 * a + 2 * a + a)) :
    p ((a + a + a) + a + (a + a + a)) := bya:Natp:Nat → Proph:p (4 * a + 2 * a + a)⊢ p (a + a + a + a + (a + a + a))
  run_tac CustomSimpSupport.mySimpGoal CustomSimpSupport.simProcTaga:Natp:Nat → Proph:p (4 * a + 2 * a + a)⊢ p (4 * a + 2 * a + a)
  exact hAll goals completed! 🐙

4.7.1. 练习：宇宙层级🔗

当前属性注册时用 mkConst name，因此明确只接受没有宇宙参数的定理。请修改 TutorialAux/Tag.lean 与 simProcTag，使规则能在每次应用时取得新鲜宇宙元变量。可查看 getConstInfo 与 mkFreshLevelMVarsFor。存储的 (Expr × Expr) 未必是理想格式；元变量必须在尝试应用定理时创建，不能在初始化时创建，否则多个位置会错误共享实例化。

[练习模板] 下面保留可复制的完整目标：辅助检查、要登记的多态定理，以及登记成功后应通过的最终 harness 都在内。

/-
#check getConstInfo
#check mkFreshLevelMVarsFor
-- 可把扩展条目改存 Name，并在 simProcTag 每次尝试时建立新鲜 universe metavariables。

#check eq_self
attribute [my_tag] eq_self

example (a : Nat) : a + a = 2 * a := by
  run_tac mySimpGoal simProcTag
  exact True.intro
-/
unexpected end of input

[负测试；支持模块已编译] 精确的 attribute 诊断可能随 Lean 版本改变，因此支持模块验证更稳定的根因：像当前 hook 一样，以 mkConst 构造 eq_self 时不给 universe level，再调用 inferType，并用 fail_if_success 要求该 MetaM 动作失败。也就是说，“当前实现拒绝多态规则”是执行过的测试，不是注释或哨兵。

CustomSimpSupport.testCurrentTagHookOnEqSelf : MetaM Unit#check CustomSimpSupport.testCurrentTagHookOnEqSelf

修完后应删除这个负测试或将其反转为成功测试，再取消上面 attribute [my_tag] eq_self 与最终 example 的隔离。元变量必须在尝试应用定理时创建，不能在初始化时创建，否则多个改写位置会错误共享实例化。

4. 从零编写 simp🔗

4.1. 1. simp 在证明项层面做什么🔗

4.2. 2. 补齐隐式参数🔗

4.2.1. 练习：构造算术表达式🔗

4.3. 3. 自定义 SimpResult🔗

4.4. 4. 基本 simp 实现🔗

4.4.1. 借用库的 simp 基础设施🔗

4.5. 5. 用 trace 调试🔗

4.5.1. 树状 trace🔗

4.6. 6. 在绑定器内部实现 simp🔗

4.6.1. 练习：存在量词🔗

4.7. 7. 收集带标签的引理🔗

4.7.1. 练习：宇宙层级🔗

4.1. 1. `simp` 在证明项层面做什么🔗

4.3. 3. 自定义 `SimpResult`🔗

4.4. 4. 基本 `simp` 实现🔗

4.4.1. 借用库的 `simp` 基础设施🔗

4.6. 6. 在绑定器内部实现 `simp`🔗