21.1.1. 四步模式🔗

几乎所有反射 tactic 都遵循同一套模式：

❶ 定义语法（syntax）：  用归纳类型表示表达式
❷ 定义语义（semantics）：语法 → 实际数学对象（解释函数）
❸ 范式化（normalization）：把语法化简为范式
❹ 正确性引理（soundness）：范式化保持语义

使用时：把 Lean 表达式 quote 为语法对象 → 范式化 → 用 decide 验证范式 → 用正确性引理得到原始命题的证明。

21.3.1. ❶ 语法 + ❷ 语义🔗

-- [示意]
inductive IExpr
- lit (n : ℤ)          -- 字面量：var (i : ℕ)          -- 第 i 个变量
- lit (n : ℤ)          -- 字面量：add (a b : IExpr)
- lit (n : ℤ)          -- 字面量：mul (a b : IExpr)
- lit (n : ℤ)          -- 字面量：neg (a : IExpr)

abbrev IEnv := ℕ → ℤ    -- 环境：变量赋值

def IExpr.denote (env : IEnv) : IExpr → ℤ
- .lit n     => n：.var i     => env i
- .lit n     => n：.add a b   => a.denote env + b.denote env
- .lit n     => n：.mul a b   => a.denote env * b.denote env
- .lit n     => n：.neg a     => -(a.denote env)

21.3.2. ❸ 范式化🔗

选 Horner 形式（a * x + b 的递归表示）作为范式：

-- [示意] Horner Normal Form
inductive HNF
- const (n : ℤ)                        -- 常数：horner (p : HNF) (i : ℕ) (q : HNF)  -- p * x_i + q

def IExpr.toHNF : IExpr → HNF := ...     -- ❶ 转换算法
def HNF.denote (env : IEnv) : HNF → ℤ := ... -- ❷ 范式的语义
instance : DecidableEq HNF := ...        -- ❸ 结构相等，可判定

• ❶ 转换算法把 IExpr 递归化为 Horner 范式，合并同类项。

• ❸ DecidableEq 使得 decide 可以比较两个范式。

21.3.3. ❹ 正确性引理🔗

-- [示意] 核心：范式化保持语义
theorem toHNF_sound (e : IExpr) (env : IEnv) :
    e.toHNF.denote env = e.denote env := by
  induction e with                       -- 对语法结构归纳
- lit n => simp [IExpr.toHNF, HNF.denote, IExpr.denote]：add a b iha ihb =>
    simp [*, IExpr.toHNF, HNF.denote, IExpr.denote]; ring
- mul a b iha ihb =>
    simp [*, IExpr.toHNF, HNF.denote, IExpr.denote]; ring
- _ => simp [*, IExpr.toHNF, HNF.denote, IExpr.denote]; ring

-- 推论：范式相等 → 语义相等（tactic 实际使用的引理）
theorem eq_of_toHNF_eq (e1 e2 : IExpr) (env : IEnv)
    (h : e1.toHNF = e2.toHNF) :
    e1.denote env = e2.denote env := by
  have := toHNF_sound e1 env
  have := toHNF_sound e2 env
  rw [h] at *; linarith

正确性引理只需证明一次——之后每个等式判定都是纯计算。

21.3.4. 组装 tactic🔗

-- [示意] MetaM 端的工作极少
elab "int_ring" : tactic => do
  let goal ← getMainTarget
  -- 1. 解析目标 e1 = e2
  -- 2. quote: 把 e1, e2 反射为 IExpr 值
  -- 3. 构造 e1.toHNF = e2.toHNF 的 decide 证明
  -- 4. 用 eq_of_toHNF_eq 得到原始等式的证明
  sorry -- 完整实现需要 quote 机制，见 §20.4

纯反射方案在 MetaM 中几乎不做计算，所有验证交给内核。 实现简单但性能受限——见 §20.6。

21.5.1. Decidable 的角色🔗

-- [示意] Decidable 的定义
inductive Decidable (p : Prop) where
- isTrue  (h : p)     -- p 成立，附带证明：isFalse (h : ¬p)    -- p 不成立，附带反证

-- decide 的工作原理：
-- 1. 找到 Decidable p 的实例
-- 2. 内核对该实例做 whnf 归约
-- 3. 归约到 isTrue h → h 就是证明；归约到 isFalse _ → 失败

反射的本质是把不一定可判定的问题转化为可判定的问题： 原始目标 e1.denote env = e2.denote env 可能不可判定， 但反射后的 e1.toHNF = e2.toHNF（结构相等）一定是 DecidableEq。 正确性引理桥接两者。

21.5.2. decide vs native_decide🔗

-- [示意]
example : (3 + 4 : ℕ) = 7 := by decide
  -- ▸ 内核归约 3 + 4 得到 7，然后 rfl——慢但可信度最高

example : (10 ^ 20 + 1 : ℕ) ≠ 10 ^ 20 := by native_decide
  -- ▸ 编译为原生代码执行——快但信任编译器

• 执行方式 —— decide：内核归约（解释执行） —— native_decide：编译为原生代码

• 速度 —— decide：慢 —— native_decide：快（几个数量级）

• 可信度 —— decide：最高（内核检查每一步） —— native_decide：较低（信任编译器）

• 适用规模 —— decide：小实例（< 1000 步） —— native_decide：大实例

• Mathlib 接受度 —— decide：总是接受 —— native_decide：谨慎使用

经验法则：先试 decide；超时则换 native_decide。

21.6.1. 纯反射🔗

Lean Expr → quote → 内部表示 → 范式化（内核计算）→ decide

优点：实现简单——MetaM 端只做 quote，验证全在内核中。 缺点：内核要执行范式化算法——对大表达式极慢。

21.6.2. 逐步构造🔗

Lean Expr → 解析 → MetaM 中运行算法 → 逐步用 mkApp 构造证明项

优点：MetaM 中的计算是编译后的代码，速度快。 缺点：每一步变换都要构造对应的证明项，实现复杂。

21.6.3. 混合方案（实际选择）🔗

真实 tactic 通常混合两种方案——在 MetaM 中做范式化（快）， 用反射验证范式等价（简单）：

-- [示意] ring 的实际策略（简化版）
-- ❶ MetaM 中范式化为 Horner 形式（编译后的代码，快）
-- ❷ 反射验证：范式 = 原始表达式（正确性引理 + rfl）
-- ❸ MetaM 中比较两个范式（结构相等）
-- ❹ Eq.trans 串联：lhs = norm = rhs

norm_num（第十章）也遵循这个模式：在 MetaM 中做数值计算， 用反射验证结果。对素性测试等复杂运算， 把 Nat.Prime 37 转化为可计算的判定函数。

• 实现难度 —— 纯反射：低 —— 逐步构造：高 —— 混合：中

• 性能 —— 纯反射：慢（内核计算） —— 逐步构造：快 —— 混合：快

• 可信度 —— 纯反射：高 —— 逐步构造：中（依赖实现） —— 混合：高

• 典型代表 —— 纯反射：教学示例 —— 逐步构造：— —— 混合：ring、norm_num

设计建议：原型阶段用纯反射（快速验证算法正确性）， 性能不足时迁移到混合方案。

21.7.1. 失败 1：Decidable 实例缺失🔗

-- [示意]
-- ✗ 函数外延性不可判定
example : (fun x : ℕ => x + 1) = (fun x => 1 + x) := by decide
  -- 错误：failed to synthesize Decidable instance
  -- ✓ 修复：用 funext 和 omega

decide 只能处理有 Decidable 实例的命题。

21.7.2. 失败 2：内核计算超时🔗

-- [示意]
-- ✗ decide 在大实例上超时
example : (List.range 10000).length = 10000 := by decide
  -- 内核展开 10000 次 List.cons → 超时
  -- ✓ 修复 1：native_decide
  -- ✓ 修复 2：simp [List.length_range]（引理推理优于暴力计算）

优先选择引理推理而非暴力计算。

21.7.3. 失败 3：quote 不完整🔗

-- [示意]
-- ✗ quote 无法识别 max 函数，把 max a b 当作不透明变量
-- 结果：max a b + 0 和 max a b 的范式不同
-- ✓ 修复：扩展 quote 识别 max，或先 simp 消除 + 0

遇到"应该能证但不能证"，首先检查 quote 是否识别了所有构造。

21.7.4. 失败 4：native_decide 的信任问题🔗

-- [示意]
-- native_decide 的证明不被内核检查计算过程
-- 如果编译器有 bug，可能产生错误的证明
-- ✓ 建议：开发阶段用 native_decide 加速，最终验证用 decide

native_decide 的可信基础包括 Lean 编译器， 比纯 decide（只信任内核）多一层信任。Mathlib 对其使用有严格限制。

21.7.5. 失败 5：范式化不完备🔗

-- [示意]
-- ✗ 范式化不处理除法：(a * b) / b 和 a 的范式不同
-- ✓ 这不是 bug——范式化的运算集合是有限的
-- ▸ 设计时明确边界：范式化能处理什么运算？

21.10.1. 练习 1（基础 · §20.2 复习）：识别四步模式🔗

标出以下代码中哪些部分对应 ❶语法、❷语义、❸范式化、❹正确性：

-- [示意]
inductive PExpr                    -- (?)
- var (i : Nat)：add (a b : PExpr)

def PExpr.eval (env : Nat → ℕ) : PExpr → ℕ     -- (?)
- .var i => env i：.add a b => a.eval env + b.eval env

def PExpr.sort : PExpr → PExpr := ...            -- (?)

theorem sort_sound (e : PExpr) (env : Nat → ℕ) : -- (?)
    (e.sort).eval env = e.eval env := ...

21.10.2. 练习 2（设计）：选择反射 vs 逐步构造🔗

对以下场景，判断应用纯反射、逐步构造还是混合方案，说明理由：

(a) 验证 8-bit 位运算等式（如 x &&& (x ||| y) = x）
    变量最多 3 个，结果空间 2^24 = 16M。

(b) 验证 ℝ 上的多项式恒等式，变量最多 20 个。

(c) 验证有限群的元素阶，群的阶 ≤ 100。

提示：(a) 穷举可行但边界——native_decide 可能需要； (b) 穷举不可行，必须范式化；(c) 穷举可行，纯 decide 可能够用。

21.10.3. 练习 3（进阶）：设计正确性引理🔗

为"列表排序等价性"反射设计正确性引理的陈述（不需要证明）：

-- [示意] 判定两个列表是否是同一个 multiset
-- 语法：List ℕ
-- 范式化：排序
-- 判定：排序后结构相等
-- 请写出 sort_perm_sound 的类型签名：
-- theorem sort_perm_sound : ???

提示：List.sort l₁ = List.sort l₂ → l₁ ~ l₂（~ 是 List.Perm）。