13.2.1. E-graph 数据结构🔗

grind 内部维护一个 E-graph（equality graph），由两部分组成：

• Union-Find：维护等价类，支持 merge(a, b) 和 find(a)

• Term DAG：记录项的结构，如 f(a) 是 f applied to a

关键不变量：congruence rule——若 find(a₁) = find(b₁)， 则 merge(f(a₁), f(b₁))。每次 merge 后都检查此条件并传播。

13.2.2. 推理示例🔗

-- [示意] 假设: {a = b, g(f(a)) = c}，目标: g(f(b)) = c

Step 1 — 初始化：每个子项各自一个等价类
Step 2 — merge(a, b)
  → congruence: f(a) vs f(b) → merge(f(a), f(b))
    → congruence: g(f(a)) vs g(f(b)) → merge(g(f(a)), g(f(b)))
Step 3 — merge(g(f(a)), c) → find(g(f(b))) = find(c) ✓

复杂度 O(n log n)（n = 项数量），依赖路径压缩 union-find。

13.3.1. @[grind] vs @[simp]🔗

• 属性：@[simp] —— 引理用法：有向重写 lhs → rhs —— 方向性：单向，lhs 必须是"大"的

• 属性：@[grind] —— 引理用法：E-matching pattern trigger —— 方向性：无向，按模式匹配

一条引理可同时标记 @[simp, grind]，各在各的引擎中生效。

13.4.1. 基本调用🔗

13.4.2. 传入临时引理🔗

要点：grind [lemma] 中的引理不需要 @[grind] 标记。

这是控制 E-matching 作用域的推荐方式——避免全局注册带来的爆炸风险。

13.4.3. 配置参数🔗

-- [示意]
set_option grind.maxSteps 20000 in   -- 步数上限
set_option grind.maxEmatch 2000 in   -- E-matching 实例化上限
example : ... := by grind

经验法则：需要 maxSteps > 50000 时，通常意味着目标不适合 grind。

13.6.1. 组合使用🔗

13.7.1. 失败 1：目标不是等式🔗

诊断线索：目标形如 ∃ x, ... 或 P ∨ Q（需要选边）→ grind 无能为力。

13.7.2. 失败 2：定义未展开🔗

核心规则：grind（和 simp 一样）不自动 unfold 用户定义。

要么 @[grind] 注册等式引理，要么手动 unfold，要么 simp [f] 先化简。

13.7.3. 失败 3：E-matching 爆炸🔗

-- [示意] ✗ 宽泛的 trigger 导致组合爆炸
@[grind] theorem bad_trigger : ∀ x y, f x = g y → h x y = 0 := sorry
-- n 个 f 项 × m 个 g 项 → n×m 次实例化 → 超时

诊断：set_option trace.grind.ematch true 看实例化次数——同一引理上百次 = 太宽泛。 修复：移除 @[grind]，改用 grind [specific_instance] 手动传入；或缩窄模式。

13.7.4. 失败 4：需要 case split🔗

-- [可运行] ✗ grind 对 if/match 的 case split 有限
example (h : if b then a = 1 else a = 2) : a = 1 ∨ a = 2 := by
  grind  -- 可能失败
  -- 修复：cases b <;> simp_all

涉及 if/match 分支时，先 split_ifs 或 cases 拆开再让 grind 收尾。

13.7.5. 失败 5：高阶 / dependent types🔗

-- [示意] ✗ E-graph 是一阶数据结构
example (h : ∀ f : Nat → Nat, f 0 = 0) : id 0 = 0 := by
  grind  -- 可能失败：量化变量是函数类型
  -- 修复：exact h id

E-graph 是一阶结构，量化变量本身是函数时 E-matching 可能找不到合适实例。

13.8.1. Trace 选项🔗

-- [示意]
set_option trace.grind true in        -- 全部推理过程
set_option trace.grind.ematch true in  -- 只看 E-matching 实例化
set_option trace.grind.eqc true in     -- 只看等价类合并
set_option trace.grind.split true in   -- 只看 case split
example : ... := by grind

13.8.2. 调试流程🔗

 grind 失败
   │
   ├─ 开 trace.grind true
   │   ├─ E-graph 缺关键项？ → 补引理 grind [lemma] 或 unfold
   │   ├─ 关键等式未合并？   → 检查是否缺中间等式假设
   │   ├─ E-matching 未触发？ → 检查 @[grind] 注册和模式
   │   └─ 实例化爆炸？       → 移除 @[grind]，改手动传入
   │
   └─ 修复后关闭 trace（显著拖慢编译）

技巧：先用 trace.grind.ematch 单独看，输出比 trace.grind 小得多。

13.9.1. 模式 A：长等式链 + 深 congruence🔗

13.9.2. 模式 B：注册领域引理🔗

-- [示意] 为代数结构注册引理
@[grind] theorem mul_comm_ab : ∀ (a b : MyGroup), a * b = b * a := sorry
@[grind] theorem mul_assoc_ab : ∀ (a b c : MyGroup),
    a * b * c = a * (b * c) := sorry

example (a b c : MyGroup) : a * b * c = c * (b * a) := by
  grind  -- ▸ E-matching 实例化交换律和结合律

警告：交换律 + 结合律是 E-matching 爆炸经典诱因，实践中改用 ring/group。

13.9.3. 模式 C：手动拆分 + grind 收尾🔗

手动处理分支逻辑（Or/if/match），每个分支内让 grind 完成等式推理。

13.10.1. 练习 1：基础等式链 ★🔗

-- 用一个 tactic 关闭目标
example (h1 : a = b) (h2 : b = c) (h3 : c = d) : f a = f d := by
  sorry

等式链 + congruence 是 grind 的标准场景。

13.10.2. 练习 2：传入临时引理 ★★🔗

-- 定义引理并传入 grind 使 example 通过
-- theorem my_lemma : ∀ x, f (g x) = x := sorry

example (h : y = g (g a)) : f y = g a := by
  sorry  -- 用 grind [...]

需要 f (g ?x) = ?x。E-matching 实例化 x := g(a) 得 f(g(g(a))) = g(a)， 配合 h 的 congruence 完成。

13.10.3. 练习 3：诊断并修复失败 ★★🔗

-- 以下 grind 调用会失败，解释原因并修复
def double (n : Nat) : Nat := n + n

example : double 3 = 6 := by
  grind  -- 失败！

grind 不展开 double。修复：unfold double; omega 或 simp [double]。 展开后是纯算术 3 + 3 = 6，omega 比 grind 更合适。

13.10.4. 练习 4：控制 E-matching 爆炸 ★★★🔗

-- 以下代码可能导致 grind 超时，分析原因并修复
@[grind] theorem inj_f : ∀ x y, f x = f y → x = y := sorry
@[grind] theorem expand_f : ∀ x, f x = g (h x) := sorry

example (h1 : a = b) (h2 : g (h a) = c) : f b = c := by
  grind  -- 可能超时

inj_f 的 trigger f ?x = f ?y 在 expand_f 引入新 f 项后被反复触发。 修复：移除 inj_f 的 @[grind]，只保留 expand_f：

attribute [-grind] inj_f
example (h1 : a = b) (h2 : g (h a) = c) : f b = c := by
  grind [expand_f]

教训：全局 @[grind] 注册的引理会影响所有 grind 调用点，爆炸风险远高于局部 grind [lemma]。

除非确认引理的 trigger 足够窄，否则优先使用 grind [lemma] 按需传入。

13.10.5. 练习 5：组合 tactic ★★★🔗

-- 用 cases + grind 的组合关闭目标
example (h : (a = b ∧ c = d) ∨ (a = d ∧ c = b))
    : f a c = f b d ∨ f a c = f d b := by
  sorry

cases h 拆 Or，每个分支 obtain ⟨h1, h2⟩ := h 拆 And， 然后 left; grind 或 right; grind。