22.4.1. profiler：整体耗时🔗

-- [可运行] 开启 profiler
set_option profiler true in
theorem my_thm : ∀ n : ℕ, n + 0 = n := by
  intro n; simp
-- ▸ 输出形如：
-- elaboration of my_thm took 12.3ms
-- typecheck of my_thm took 0.8ms

第一步永远是 profiler——先定位是哪个声明慢，再深入分析。

22.4.2. trace：细粒度追踪🔗

-- [示意] 追踪 simp 的每一步重写
set_option trace.Meta.Tactic.simp.rewrite true in
theorem ex2 : 0 + n = n := by simp
-- ▸ [Meta.Tactic.simp.rewrite] Nat.zero_add:1000, 0 + n ==> n

-- [示意] 追踪 type class synthesis
set_option trace.Meta.synthInstance true in
-- ▸ 显示 typeclass 搜索树，包括尝试和回溯

-- [示意] 追踪 unification
set_option trace.Meta.isDefEq true in
-- ▸ 显示每次 definitional equality 检查

常用 trace 选项速查：

• trace.Meta.Tactic.simp.rewrite：simp 应用了哪些引理

• trace.Meta.Tactic.simp.discharge：simp 的 discharge 尝试

• trace.Meta.synthInstance：typeclass synthesis 过程

• trace.Meta.isDefEq：unification 过程（输出极大，慎用）

• trace.profiler.threshold：只显示超过阈值的步骤

二分定位：profiler → 哪个 theorem 慢 → 逐行 sorry → 哪行 tactic 慢 → trace 深入。

22.5.1. 全局 simp vs simp only🔗

-- [示意] ❌ 全局 simp——加载所有 @[simp] 引理
simp
-- ▸ Mathlib 环境下 @[simp] 引理有数千条
-- ▸ 复杂度 ≈ O(子表达式数 × 引理数 × 重写轮数)

-- [示意] ✅ simp only——只用必要的引理
simp only [Nat.add_zero, Nat.mul_one]
-- ▸ 引理集从数千条缩减到 2 条

22.5.2. simp? 工作流🔗

-- [示意] 开发时的最佳实践
-- ❶ 先用 simp 探索（开发阶段）
-- ❷ 用 simp? 获取实际使用的引理列表
-- ❸ 替换为 simp only [...]（提交前）

example : 0 + n + 0 = n := by
  simp?
  -- ▸ 建议: simp only [Nat.zero_add, Nat.add_zero]

22.5.3. 其他 simp 调优🔗

-- [示意] 关闭 discharge（simp 不尝试放电侧条件）
simp (config := { decide := false })

-- ❌ @[simp] 同时标记 a = b 和 b = a → 无限循环
-- ✓ @[simp] 引理应保证重写方向一致（左边"更复杂"）

22.7.1. 高阶 unification🔗

-- [示意] ❌ 让 Lean 推断太多类型参数
exact some_very_polymorphic_lemma
-- ▸ 最坏情况下 unification 是不可判定的

-- [示意] ✅ 显式提供关键类型参数
exact @some_lemma ℝ _ _ a b
-- ▸ @ 关闭隐式参数，_ 让 Lean 推断简单的 typeclass 参数

22.7.2. typeclass synthesis 爆炸🔗

-- [示意]
-- 深层实例链：Ring ℝ → AddCommMonoid ℝ → AddMonoid ℝ → ...
-- ▸ 搜索树可能指数级增长

-- ✅ 策略 1：提供局部实例
have inst : Ring ℝ := inferInstance
-- ▸ 后续 tactic 直接用 inst，不再搜索

-- ✅ 策略 2：控制搜索深度
set_option synthInstance.maxSize 256 in  -- 默认 128

coercion 链：ℕ → ℤ → ℚ → ℝ 的隐式转换触发多层 synthesis。 用 (↑n : ℝ) 显式标注最终类型，或在证明开头 push_cast。

22.9.1. 缓存与避免重复🔗

-- [示意] ❌ 重复调用
let t1 ← goal.getType
doSomething t1
let t2 ← goal.getType        -- 浪费

-- [示意] ✅ 缓存
let target ← goal.getType
doSomething target
doSomethingElse target

22.9.2. 避免不必要的 whnf🔗

-- [示意] ❌ whnf 可能展开大量定义
let t ← whnf (← goal.getType)
-- ▸ whnf 递归展开直到头部是构造子——代价可能很高

-- [示意] ✅ 用 matchApp? 等结构化匹配代替
let target ← goal.getType
if let some (f, args) ← matchApp? target then ...
-- ▸ 只检查头部函数，不做深层展开

22.9.3. 控制 isDefEq🔗

-- [示意] isDefEq 是 MetaM 中最昂贵的操作之一
-- ❌ 盲目尝试
for lemma in lemmas do
  if ← isDefEq lemmaConcl target then return lemma

-- ✅ 廉价预筛选 + 精确匹配
for lemma in lemmas do
  if quickCheck lemma target then       -- 头符号匹配
    if ← isDefEq lemmaConcl target then return lemma

注意：isDefEq 有副作用——它会给 metavariable 赋值。 即使最终不用该引理，赋值已经发生。 用 withoutModifyingState 隔离探索性调用。

22.11.1. 证明项膨胀🔗

-- [示意] simp 生成的证明项可能非常大
-- 每一步重写记录：应用的引理、类型参数实例化、局部变量
-- 100 步重写可能生成数万个 Expr 节点
-- decide 更严重：证明项包含完整的归约过程

缓解策略：

• native_decide 生成更紧凑的证明项（不记录归约过程）

• 拆分大证明为多个中间引理（每段 simp 链较短）

• 用引理推理代替暴力计算（simp [List.length_range] 优于 decide）

证明项大小影响 .olean 文件大小， 进而影响所有下游文件的加载时间。

22.11.2. 增量编译与文件组织🔗

-- [示意] ❌ 粗粒度 import
import Mathlib               -- 加载整个 Mathlib

-- [示意] ✅ 细粒度 import
import Mathlib.Tactic.Ring   -- 只加载需要的模块
import Mathlib.Data.Nat.Basic

文件依赖图：
        A.lean
       / \
      B    C        ← B 和 C 可以并行编译
       \ /
        D.lean      ← D 必须等 B 和 C 都编译完

优化原则：减少文件间依赖；把慢定义和快定义分开文件； 用 lake build +A +B 并行编译无依赖模块。

Mathlib 在 CI 中对每个 PR 测量编译时间差异， 显著增加编译时间的 PR 需要优化后再合并。

22.12.1. 原始版本（慢）🔗

-- [示意]
set_option maxHeartbeats 800000 in  -- 需要 4 倍预算
theorem slow_example (a b c : ℕ) :
    (a + b) * c + 0 = c * a + c * b := by
  simp [Nat.add_mul, Nat.mul_comm, Nat.add_comm, Nat.add_zero]
  ring

22.12.2. 诊断过程🔗

-- [示意]
-- ❶ profiler → simp 占 90% 时间
-- ❷ trace.simp → Nat.mul_comm 导致循环（a*b → b*a → a*b）
-- ❸ 分析 → 只需 Nat.add_zero 消除 + 0，剩下交给 ring

22.12.3. 优化版本（快）🔗

-- [示意] 不需要额外 heartbeats
theorem fast_example (a b c : ℕ) :
    (a + b) * c + 0 = c * a + c * b := by
  simp only [Nat.add_zero]   -- 只消除 + 0
  ring                        -- ring 处理交换律和分配律

heartbeats 从 ~600000 降到 ~5000（100x 改善）。

优化检查清单：

□ profiler 定位瓶颈（simp？unification？typeclass？）
□ simp 瓶颈 → simp? → simp only
□ unification 瓶颈 → 添加类型标注
□ typeclass 瓶颈 → 缓存实例或限制搜索
□ decide 瓶颈 → native_decide 或引理推理
□ 优化后 heartbeats ≤ 200000？

22.13.1. 失败 1：maxHeartbeats 军备竞赛🔗

-- [示意]
-- ❌ 每次超时就加 maxHeartbeats
set_option maxHeartbeats 400000 in   -- 第一次
set_option maxHeartbeats 800000 in   -- Lean 升级后又超时
set_option maxHeartbeats 1600000 in  -- 加了一条引理又超时
-- ✓ 正确做法：优化证明本身

22.13.2. 失败 2：trace 输出导致 IDE 卡死🔗

-- [示意]
-- ❌ 在大文件上开 trace.Meta.isDefEq → 输出几十万行
-- ✓ 先用 sorry 缩小范围，只对单个 tactic 开 trace

22.13.3. 失败 3：#reduce 代替 #eval🔗

-- [示意]
#reduce (List.range 1000).length  -- ❌ 极慢：内核归约
#eval (List.range 1000).length    -- ✓ 瞬间：编译后执行

22.13.4. 失败 4：无数据支撑的优化🔗

-- [示意]
-- ❌ "simp 可能慢，我全换成 simp only"
-- ❌ "加类型标注总没错"
-- ▸ 没有数据支撑的优化可能无效，还降低可读性
-- ✓ 先 profiler，再 trace，最后优化——data-driven

22.14.1. 练习 1（诊断）：读 profiler 输出🔗

以下 profiler 输出说明了什么？应该优先优化什么？

elaboration of slow_lemma took 3.2s
  tactic execution took 2.8s
    simp took 2.6s
  typecheck took 0.3s

提示：simp 占 81%——应优化 simp（simp? → simp only）。 typecheck 0.3s 也较高——可能是证明项过大，但优先处理 simp。

22.14.2. 练习 2（设计）：分析性能权衡🔗

对以下场景，分析瓶颈在哪个阶段（elaboration / tactic / typecheck）， 并建议优化方向：

(a) 用 decide 证明 100 以内所有素数的 Goldbach 猜想

(b) 在深层 typeclass 层级上使用 15 步 simp 链

(c) 自定义 tactic 在 MetaM 中对 200 个候选引理逐一尝试 isDefEq

提示： (a) tactic（decide 穷举）+ typecheck（证明项大）→ native_decide 或拆引理。 (b) elaboration（typeclass）+ tactic（simp）→ 缓存实例，simp only。 (c) tactic（isDefEq 昂贵）→ 头符号预筛选，withoutModifyingState 隔离。