20.2.1. 模式 A：simp 引理集🔗

不写新 tactic，只收集领域引理标注 @[simp]。

-- [示意] 为测度论收集 simp 引理
attribute [simp] MeasureTheory.Measure.map_apply
attribute [simp] MeasureTheory.Measure.restrict_apply

example (μ : Measure α) (s : Set α) (hs : MeasurableSet s) :
    μ.restrict s s = μ s := by simp [hs]
  -- ▸ simp 自动找到 restrict_apply 完成化简

适用：等式化简，引理方向明确（左→右）。 局限：不能搜索、不能结构分解、不能处理不等式。

20.2.2. 模式 B：aesop 规则集🔗

声明规则集，注册 safe/unsafe 规则，让 aesop 搜索。

-- [示意] 为集合论推理定义规则集
declare_aesop_rule_sets [SetReasoning]

@[aesop safe apply (rule_sets := [SetReasoning])]
theorem inter_subset_left (s t : Set α) : s ∩ t ⊆ s := Set.inter_subset_left

@[aesop unsafe 70% apply (rule_sets := [SetReasoning])]
theorem subset_union_left (s t : Set α) : s ⊆ s ∪ t := Set.subset_union_left

macro "set_reason" : tactic =>
  `(tactic| aesop (rule_sets := [SetReasoning])
                   (config := { maxDepth := 10 }))

适用：多步推理，每步是已知引理的实例化。 局限：搜索空间指数增长；对结构化分解无能为力。

20.2.3. 模式 C：递归分解（positivity 模式）🔗

递归遍历表达式结构，自底向上收集信息。

-- [示意] positivity 的核心递归骨架
partial def analyzeSign (e : Expr) : MetaM SignResult := do
  if let some r ← findHypothesis e then return r    -- ❶ 找假设
  match_expr e with
- HAdd.hAdd _ _ _ _ a b =>
    combineAdd (← analyzeSign a) (← analyzeSign b)  -- ❷ 递归 + 组合
- HMul.hMul _ _ _ _ a b =>
    combineMul (← analyzeSign a) (← analyzeSign b)
- HPow.hPow _ _ _ a n =>
    combinePow (← analyzeSign a) n                   -- ▸ 偶数幂→非负
- _ => throwError "positivity: 无法分析 {e}"

适用：目标可按表达式结构递归分解，组合规则明确。 局限：只能处理预定义的构造子。

20.2.4. 模式 D：完整决策过程🔗

实现完整算法（如 ring、omega），架构三步： ① 解析 Lean Expr → 内部表示；② 运行判定算法；③ 构造证明项。 步骤 ③ 有两条路——反射（编码为可判定数据，用 decide，简单但慢） 和逐步构造（用 mkApp 等拼装，快但实现复杂）。

适用：有完备判定算法。局限：实现成本最高。

20.4.1. 第一步：明确边界🔗

能处理：a + c ≤ b + d（上下文有 a ≤ b 和 c ≤ d）、 嵌套加法（递归）、自反 a ≤ a（le_refl）。 不处理：乘法/减法/除法单调性、需要 linarith 的间接推理。

20.4.2. 第二步：核心递归🔗

-- [示意] mono_add 核心逻辑
partial def proveLE (lhs rhs : Expr) : TacticM Expr := do
  -- ❶ 相等 → le_refl
  if ← isDefEq lhs rhs then
    mkAppM ``le_refl #[lhs]
  -- ❷ 加法 → 拆解两边
  else if let some (a, c) ← matchAdd lhs then
    if let some (b, d) ← matchAdd rhs then
      let hab ← proveLE a b       -- 递归证明 a ≤ b
      let hcd ← proveLE c d       -- 递归证明 c ≤ d
      mkAppM ``add_le_add #[hab, hcd]
    else searchHypothesis lhs rhs
  -- ❸ 回退 → 在上下文中搜索匹配假设
  else searchHypothesis lhs rhs

20.4.3. 第三步：搜索假设与包装🔗

-- [示意] 在上下文中查找 lhs ≤ rhs 的证明
def searchHypothesis (lhs rhs : Expr) : TacticM Expr := do
  for decl in (← getLCtx) do
    if decl.isImplementationDetail then continue
    if let some (_, l, r) ← matchLE (← instantiateMVars decl.type) then
      if (← isDefEq l lhs) && (← isDefEq r rhs) then
        return decl.toExpr
  throwError "mono_add: 找不到 {lhs} ≤ {rhs} 的证明"
  -- ▸ 错误信息具体——告诉用户缺什么假设

-- [示意] 注册为 tactic
elab "mono_add" : tactic => withMainContext do
  let target ← getMainTarget
  match_expr target with
- LE.le _ _ lhs rhs =>
    closeMainGoal `mono_add (← proveLE lhs rhs)
- _ => throwError "mono_add: 目标不是 _ ≤ _ 形式"

20.4.4. 第四步：测试🔗

-- [示意] 正例
example (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by mono_add
  -- ▸ 拆解加法，匹配 h1 和 h2

example (h1 : a ≤ b) (h2 : c ≤ d) (h3 : e ≤ f) :
    a + c + e ≤ b + d + f := by mono_add
  -- ▸ 递归拆解两层加法

example : a + c ≤ a + c := by mono_add
  -- ▸ le_refl 处理

-- [示意] 反例（应当失败并给出明确错误）
example (h1 : a ≤ b) : a * c ≤ b * c := by mono_add
  -- ✗ "mono_add: 找不到 a * c ≤ b * c 的证明"

20.5.1. 三层错误信息🔗

层次 1（必须）：说明失败位置
  "mono_add: 找不到 a ≤ b 的证明"

层次 2（推荐）：给出修复建议
  "mono_add: 找不到 a ≤ b 的证明，尝试在上下文中添加此假设"

层次 3（理想）：展示推理过程
  "mono_add: 分析 a + c ≤ b + d
     ├─ a ≤ b: 失败——上下文中未找到
     └─ c ≤ d: ✓ 已找到 (hcd : c ≤ d)"

用 trace 实现层次 3：

-- [示意] 用 trace 输出推理链
trace[mono_add] "分析 {lhs} ≤ {rhs}"
-- 用户用 set_option trace.mono_add true 查看

20.7.1. 让用户添加规则🔗

好的领域 tactic 允许用户扩展，不需要改源码：

-- [示意] 方式 1：attribute 注册（模式 A/B）
initialize monoAddExt : SimpExtension ←
  registerSimpAttr `mono_add_lemma "Lemmas for mono_add"

@[mono_add_lemma]
theorem sub_le_sub_right (h : a ≤ b) (c : ℕ) : a - c ≤ b - c := ...

-- [示意] 方式 2：插件系统（模式 C）
@[positivity MyFunc]
def evalMyFunc : PositivityExt where
  eval {u α} _zα _pα (e : Q($α)) := do
    return .nonneg (← proveMyFuncNonneg e)

-- [示意] 方式 3：规则集（模式 B）
@[aesop safe apply (rule_sets := [SetReasoning])]
theorem my_new_set_lemma : ... := ...

模式 A/B 用 attribute 或规则集（零代价）； 模式 C/D 需要设计插件接口（需要定义返回类型和协议）。

20.7.2. 索引而不是线性搜索🔗

当引理集增长到数百条时，线性遍历成为瓶颈。 用 DiscrTree（discrimination tree）做索引：

-- [示意]
-- ✗ 线性搜索——O(n) 遍历
def findLemma (target : Expr) (lemmas : Array Expr) : MetaM (Option Expr) := do
  for l in lemmas do
    if ← isDefEq (← inferType l) target then return some l
  return none

-- ✓ DiscrTree——O(log n) 查找
def findLemma' (target : Expr) (tree : DiscrTree Expr) : MetaM (Array Expr) :=
  tree.getMatch target

simp、aesop、fun_prop 都使用 DiscrTree。 经验法则：引理超过 20 条就用 DiscrTree。

20.8.1. 失败 1：规则集污染🔗

-- [示意]
@[aesop safe apply (rule_sets := [MyDomain])]
theorem exists_of_ne_empty (h : s ≠ ∅) : ∃ x, x ∈ s := ...
  -- ✗ 几乎匹配所有 ∃ 目标，导致搜索爆炸

修复：宽泛引理标 unsafe，或提高匹配精确度。

20.8.2. 失败 2：递归不终止🔗

-- [示意]
partial def analyze (e : Expr) : MetaM Result := do
  match_expr e with
- f a => analyze a：_ => analyze e     -- ✗ 对同一个表达式无限递归！

修复：每个分支要么返回结果，要么对严格更小的子表达式递归。

20.8.3. 失败 3：错误信息丢失🔗

-- [示意]
-- ✗ 吞掉原始错误
try doSomething
catch _ => throwError "myTactic failed"

-- ✓ 保留上下文
try doSomething
catch e => throwError "myTactic: 分析 {expr} 时失败：{e.toMessageData}"

20.8.4. 失败 4：忽略 universe 多态🔗

-- [示意]
def myLemma := @add_le_add Nat ...
  -- ✗ 硬编码 Nat，对 ℝ 等类型失败
  -- ✓ 修复：用 mkAppM 而非 mkApp，自动处理 universe 统一

20.11.1. 练习 1（热身）：simp 引理集🔗

-- [可运行]
-- 为以下场景找到正确的 simp 引理，使 `simp [...]` 一步完成。
example (s t : Finset ℕ) : (s ∪ t).card ≤ s.card + t.card := by
  sorry -- 用 simp + 哪条引理？

example (s : Finset ℕ) : (s ∩ s) = s := by
  sorry -- 用 simp + 哪条引理？

20.11.2. 练习 2（热身）：aesop 规则集🔗

-- [示意]
-- 为以下推理链设计 aesop 规则集。
-- 回答：哪些引理标 safe？哪些标 unsafe？优先级如何？
--
-- 推理链：h : x ∈ s, h2 : s ⊆ t  ⊢  x ∈ t ∪ u
--   步骤 1：由 h2 h 得 x ∈ t
--   步骤 2：由 mem_union_left 得 x ∈ t ∪ u

20.11.3. 练习 3（debug）：修复错误信息🔗

-- [示意]
-- 以下 tactic 失败时用户看不到有用信息，找出问题并修复。
elab "bad_tactic" : tactic => do
  let target ← getMainTarget
  try
    let proof ← someFancyProof target
    closeMainGoal `bad_tactic proof
  catch _ =>
    throwError "bad_tactic failed"
-- 问题：____________
-- 修复：____________

20.11.4. 练习 4（综合）：设计 nontrivial_by tactic🔗

-- 设计（不需要完整实现，写设计文档即可）：
-- 自动证明 Nontrivial α，即类型 α 至少有两个不同元素。
--
-- 回答：
-- 1. 属于哪种模式？（A/B/C/D）
-- 2. 核心策略？（搜索假设？分解类型结构？）
-- 3. 需要哪些引理？
-- 4. 失败时报什么错误？
-- 5. 用户如何为自定义类型扩展？