11.2.1. Result 类型🔗

插件的返回类型 NormNum.Result 有三个构造子。 下面是简化后的核心形状，省略了部分字段；完整定义见 Mathlib.Tactic.NormNum.Core：

inductive Result where
- isNat (inst : Expr) (lit : Expr) (proof : Expr)
    -- 表达式 = Nat.cast lit，proof : e = Nat.cast lit
- isNegNat (inst : Expr) (lit : Expr) (proof : Expr)
    -- 表达式 = -Nat.cast lit
- isBool (val : Bool) (proof : Expr)
    -- 命题为 True/False

isNat 和 isNegNat 把任意数值表达式规范化为自然数字面量或其负值， 附带一个证明该等式的 proof。isBool 用于布尔判定（如素性）。

11.2.2. 插件注册🔗

用 @[norm_num <pattern>] attribute 注册插件：

-- pattern 指定该插件能处理的 head symbol
@[norm_num Nat.Prime _]
def evalPrime : NormNumExt where
  eval {u α} (e : Expr) : SimpM (Option Result) := do
    -- e 是待规范化的表达式
    -- 返回 some result 表示成功，none 表示该插件不处理
    ...

norm_num 收到一个目标时的分派流程：

1. 提取目标表达式的 head symbol

2. 在注册表中查找匹配的插件

3. 依次尝试匹配的插件，直到某个返回 some

4. 用返回的 Result 构造最终证明

11.2.3. 内置插件清单🔗

• 插件：evalAdd —— 处理的 head symbol：HAdd.hAdd —— 示例：2 + 3 = 5

• 插件：evalMul —— 处理的 head symbol：HMul.hMul —— 示例：6 * 7 = 42

• 插件：evalPow —— 处理的 head symbol：HPow.hPow —— 示例：2 ^ 10 = 1024

• 插件：evalDiv —— 处理的 head symbol：HDiv.hDiv —— 示例：(10 : ℚ) / 3

• 插件：evalMod —— 处理的 head symbol：HMod.hMod —— 示例：17 % 5 = 2

• 插件：evalPrime —— 处理的 head symbol：Nat.Prime —— 示例：Nat.Prime 127

• 插件：evalGcd —— 处理的 head symbol：Nat.gcd —— 示例：Nat.gcd 12 8 = 4

• 插件：evalDvd —— 处理的 head symbol：Dvd.dvd —— 示例：(3 : ℤ) ∣ 12

• 插件：evalLe —— 处理的 head symbol：LE.le —— 示例：(2 : ℝ) ≤ 3

• 插件：evalLt —— 处理的 head symbol：LT.lt —— 示例：(1 : ℚ) < 2

11.3.1. 加法示例🔗

证明 37 + 45 = 82：

-- meta 层：Lean 原生 Nat 加法，瞬间得到 82
-- object 层：构造如下证明项
-- norm_num 不是直接 rfl——它把大数拆成 kernel 容易验证的步骤

-- 内部大致流程：
-- 1. 37 和 45 都已是 Nat literal，无需进一步规范化
-- 2. meta 层计算 37 + 45 = 82
-- 3. 构造 proof : 37 + 45 = 82
--    利用 Nat literal 的 kernel reduction 特性
--    kernel 验证 isNatLit 37 + isNatLit 45 →β isNatLit 82 ✓

11.3.2. 素性示例🔗

证明 Nat.Prime 127：

-- meta 层：
-- 1. 检查 127 > 1
-- 2. 试除 2, 3, 5, 7, 11（≤ √127 ≈ 11.3）
-- 3. 确认无因子

-- object 层：
-- 构造 minFac 证书：minFac 127 = 127
-- 这比让 kernel 枚举所有可能的因子快得多
-- kernel 只需验证证书的正确性，不需要自己搜索

11.3.3. 与 kernel computation 的对比🔗

• 计算位置 —— norm_num：meta 层（elaborator） —— decide / native_decide：kernel / 编译器

• 输出 —— norm_num：证明项（证书） —— decide / native_decide：rfl : decide p = true

• 大数性能 —— norm_num：优秀 —— decide / native_decide：可能超时

• 可信基 —— norm_num：kernel 验证证书 —— decide / native_decide：信任 kernel reduction / native code

• 可扩展性 —— norm_num：插件系统 —— decide / native_decide：需要 Decidable 实例

11.4.1. 插件的结构🔗

一个 norm_num 插件只需做三件事：模式匹配、meta 层计算、构造证明。 下面用伪代码展示骨架——不涉及 Qq 等元编程细节：

@[norm_num MyFunc _]            -- ❶ 注册：声明处理哪个 head symbol
def evalMyFunc : NormNumExt where
  eval (e : Expr) := do
    -- ❷ 模式匹配：提取 MyFunc 的参数
    let arg ← 从 e 中提取参数，失败则 return none

    -- ❸ meta 层计算：用 Lean 原生函数得到结果
    let result := myFuncImpl arg

    -- ❹ 构造证明：给 kernel 一个可验证的证书
    let proof ← 构造 "MyFunc arg = result" 的证明项
    return some (.isNat ... result proof)

关键设计规则：当插件无法处理当前表达式时，返回 none 而非抛出

failure。none 让 norm_num 继续尝试其他插件；failure 会中断

整个 pipeline，导致本可由其他插件处理的目标也一起失败。

完整的可编译示例（为 Nat.fib 编写插件）留作练习 10.4； 它需要用到 NormNumExt、Qq quoted expression 和 proof construction， 属于进阶元编程内容。

11.4.2. 插件开发要点🔗

模式匹配要精确：@[norm_num Nat.fib _] 中的 pattern 决定何时触发。 写错 pattern 会导致插件永远不被调用，且无任何报错。

证明构造是难点：meta 层计算很容易，但构造让 kernel 接受的证明项需要 对 Lean 的类型系统和 kernel reduction 规则有深入理解。 常用策略：

• 小范围：直接用 mkDecideProof，让 kernel reduce

• 大范围：构造分步证书（如素性的 minFac 证书）

• 通用：用 Qq quoted expression 确保类型安全

11.5.1. 作为 simp 的 discharger🔗

simp 在化简条件引理时可以调用 norm_num 来 discharge 数值侧条件：

-- 引理 div_add_mod 有侧条件 b ≠ 0
-- simp 在应用该引理时需要证明 3 ≠ 0
-- norm_num 作为 discharger 自动处理
example (n : ℤ) : n % 3 + 3 * (n / 3) = n := by
  simp [Int.emod_add_ediv]
  -- simp 内部：需要 (3 : ℤ) ≠ 0 → norm_num discharge ✓

11.5.2. 管线组合🔗

常见的组合模式：

-- 模式 1：simp 化简结构，norm_num 收尾数值
example : (2 : ℝ) * 3 + 1 = 7 := by
  norm_num
  -- norm_num 单独即可，不需要 simp

-- 模式 2：simp 展开定义后 norm_num 计算
example : Nat.factorial 5 = 120 := by
  simp [Nat.factorial]
  -- 展开 factorial 定义
  norm_num
  -- 计算具体值

-- 模式 3：norm_num 作为 simp extension
-- 在 simp set 中启用 norm_num
example : (2 : ℝ) + 3 ≠ 6 := by
  simp (config := { decide := false }) only []
  norm_num

11.6.1. 含变量的表达式🔗

-- ✗ norm_num 无法处理含自由变量的表达式
example (x : ℝ) : x + 0 = x := by
  norm_num  -- 失败！x 不是具体数值
  -- 应使用：simp 或 ring

norm_num 只处理完全具体的数值表达式。 一旦出现自由变量，它会返回 none，tactic 报错。

11.6.2. 缺少插件🔗

-- ✗ 没有处理 Nat.sqrt 的内置插件
-- example : Nat.sqrt 49 = 7 := by norm_num  -- 失败

-- 解法 1：展开定义后用其他 tactic
example : Nat.sqrt 49 = 7 := by native_decide

-- 解法 2：编写自定义插件（见 10.4 节）

当 norm_num 失败时，检查目标的 head symbol 是否有对应插件。 set_option trace.Meta.NormNum true 可以查看插件分派过程。

11.6.3. 类型不匹配🔗

-- ✗ 默认数值类型是 Nat，Nat 上没有减法负数
-- example : 3 - 5 = -2 := by norm_num
-- 类型错误：Nat 上 3 - 5 = 0（截断减法）

-- ✓ 指定整数类型
example : (3 : ℤ) - 5 = -2 := by norm_num

norm_num 对类型敏感。确保数值表达式在正确的类型上工作。

11.6.4. 诊断工具🔗

-- 查看 norm_num 的插件分派和执行过程
set_option trace.Meta.NormNum true in
example : (2 : ℝ) + 3 = 5 := by norm_num