手动证明每一步的好处是透明可控，坏处是重复劳动积累。Aesop（Automated Extensible Search for Obvious Proofs）是 Lean 4 / Mathlib4 的声明式自动化框架：用户注册规则集，Aesop 在目标上做有界搜索，自动完成"显而易见但手写繁琐"的证明。本篇覆盖 Aesop 的规则注册、优先级系统、safe/unsafe/norm 三类规则、自定义规则集，以及与 Coq 的 auto/eauto 的设计差异。

Aesop 的基本用法

1
2
3
4
5
6
7
8
import Aesop

-- 标记引理为 Aesop 规则
@[aesop safe]
theorem and_comm_aesop : ∀ (p q : Prop), p ∧ q → q ∧ p :=
  fun _ _ ⟨hp, hq⟩ => ⟨hq, hp⟩

example (h : A ∧ B) : B ∧ A := by aesop

@[aesop safe] 把 and_comm_aesop 注册为安全规则。aesop tactic 在遇到形如 _ ∧ _ 的目标时会尝试应用它。

不加任何属性时，aesop 仍然能证明一些基本命题——Mathlib4 已经为常见结构注册了大量默认规则。

规则分类：safe / unsafe / norm

Aesop 的规则分为三类，搜索策略对它们的处理方式不同：

norm 规则：标准化规则，在搜索开始前和每次规则应用后自动执行。类似 Coq 的 simpl 或 simp，用于把目标化简到标准形式。simp 本身就是 Aesop 的默认 norm 规则之一。

1
2
@[aesop norm]
theorem add_zero_norm (n : Nat) : n + 0 = n := Nat.add_zero n

safe 规则：确定性规则，应用后不会产生错误分支。Aesop 遇到 safe 规则匹配时直接应用，不创建搜索分支。典型例子：And.intro（当两个子目标都能继续推进时）。

1
2
3
4
@[aesop safe [constructors, cases]]
structure MyPair (α β : Type) where
  fst : α
  snd : β

[constructors] 注册该类型的所有构造子为 introduction 规则；[cases] 注册该类型的 cases 规则。

unsafe 规则：可能失败的规则，应用时创建搜索分支。如果当前分支失败，Aesop 会回溯并尝试其他分支。unsafe 规则需要指定成功率百分比：

1
2
3
4
5
@[aesop unsafe 50%]
theorem or_inl_unsafe (h : A) : A ∨ B := Or.inl h

@[aesop unsafe 50%]
theorem or_inr_unsafe (h : B) : A ∨ B := Or.inr h

50% 表示 Aesop 估计该规则在匹配时有一半概率导向正确方向。百分比影响搜索优先级：高百分比的 unsafe 规则优先尝试。

优先级系统

Aesop 的搜索基于最佳优先搜索（best-first search），优先级决定节点展开顺序：

  • norm 规则：总是执行，优先级无意义（它们不创建搜索分支）
  • safe 规则：按注册顺序执行，全部执行完毕后才进入 unsafe 搜索
  • unsafe 规则：百分比高的优先展开
1
2
3
4
5
6
-- 80% 的规则比 20% 的规则优先尝试
@[aesop unsafe 80%]
theorem high_priority_rule ...

@[aesop unsafe 20%]
theorem low_priority_rule ...

还可以用 priority 参数精细控制 norm 和 safe 规则的执行顺序：

1
2
3
4
5
@[aesop norm (priority := 100)]  -- 高优先级 norm，先执行
theorem norm_first ...

@[aesop norm (priority := 1)]    -- 低优先级 norm，后执行
theorem norm_last ...

规则构建器

Aesop 支持多种规则构建器（rule builder），指定规则如何从定理生成搜索动作：

构建器 含义
apply 对目标执行 apply thm（默认）
constructors 对归纳类型注册其构造子为 introduction 规则
cases 对归纳类型注册 cases 拆解规则
simp 把引理加入 simp 的引理集
unfold 展开定义
tactic 执行自定义 tactic
forward 从假设前向推导新假设（类似 Coq 的 eauto 的 eapply） 
1
2
3
4
5
6
7
8
9
-- 注册为 forward 规则：如果上下文有 h : A ∧ B，自动推导出 A 和 B
@[aesop safe forward]
theorem and_left (h : A ∧ B) : A := h.1

-- 注册自定义 tactic 为 Aesop 规则
@[aesop norm tactic]
def my_norm_tactic : Aesop.RuleTac := fun input => do
  -- 在每个目标上执行 simp only [Nat.add_zero]
  ...

自定义规则集

大型项目中把所有规则注册到默认规则集会导致搜索空间爆炸。Aesop 支持命名规则集：

1
2
3
4
5
6
7
8
9
10
-- 声明规则集
declare_aesop_rule_sets [MyProject.Algebra]

-- 向特定规则集注册规则
@[aesop safe (rule_sets := [MyProject.Algebra])]
theorem my_algebra_lemma ...

-- 使用特定规则集
example : ... := by
  aesop (rule_sets := [MyProject.Algebra])

Mathlib4 使用这种模式为不同数学领域维护独立的规则集（Mathlib.Aesop.Sets 中有 Continuous、Measurable 等）。

aesop (rule_sets := [A, B]) 表示搜索时同时启用规则集 A 和 B 中的规则，加上默认规则集。aesop (rule_sets := [A, -default]) 可以排除默认规则集。

搜索配置

Aesop 的搜索行为可通过参数调整：

1
2
3
4
5
-- 增加搜索深度（默认 maxDepth = 5）
example : ... := by aesop (config := { maxRuleApplications := 200 })

-- 只使用 safe 规则（不做 unsafe 搜索）
example : ... := by aesop (config := { enableSimp := true, strategy := .safe })

常用配置项：

参数 默认值 含义
maxRuleApplications 200 最多应用规则次数
enableSimp true 是否在 norm 阶段运行 simp
strategy .bestFirst 搜索策略
terminal false 是否要求 aesop 完全关闭目标

与 Coq auto/eauto 的对比

Coq 的 auto 和 eauto 是经典的 Prolog 风格搜索：

维度 Coq auto/eauto Lean Aesop
搜索策略 深度优先，固定深度界 最佳优先，多指标排序
规则注册 Hint Resolve/Constructors/Unfold @[aesop safe/unsafe/norm]
失败语义 回溯；auto 不 unfold，eauto 尝试存在量词 safe 不回溯，unsafe 回溯
规则集 Create HintDb，显式选用 declare_aesop_rule_sets
标准化 无内建 norm 阶段（需手动 simpl / cbn） norm 规则自动执行
优先级模型 按 cost（整数） 按百分比 + priority

设计哲学差异：Coq 的 auto 设计为"尝试 N 步深度内能用的所有规则"，规则越多越慢但结果稳定；Aesop 设计为"先标准化，再按估计成功率排序搜索"，倾向快速找到高概率路径。

在实际使用中，Aesop 的 norm 阶段对应 Coq 中 auto 之前手动调用 simpl; intros 的习惯——Aesop 自动化了这个前处理步骤。

调试 Aesop

当 aesop 失败时，诊断方法：

1
2
3
4
5
6
7
-- 显示搜索树
set_option trace.aesop true in
example : ... := by aesop

-- 显示应用了哪些规则
set_option trace.aesop.ruleSet true in
example : ... := by aesop

trace.aesop 输出完整的搜索树，包括每个节点尝试了哪些规则、失败原因。常见失败模式：

  • 需要的引理没有注册为 Aesop 规则：@[aesop safe] 加上即可
  • 搜索深度不够：增加 maxRuleApplications
  • 目标类型需要先做 unfold 才能匹配规则：注册 unfold 或 norm 规则
  • unsafe 规则的百分比设置不当，导致正确路径排序靠后

aesop? 与证明搜索透明化

1
2
3
-- aesop? 成功后显示具体证明脚本
example (h : A ∧ B) : B ∧ A := by aesop?
-- 输出类似：exact ⟨h.2, h.1⟩  或  exact And.intro h.2 h.1

aesop? 找到证明后把对应的 term-mode 或 tactic 序列输出到 InfoView，用户可以替换 aesop 为具体脚本。这在两种场景下有价值：CI 中避免 aesop 搜索时间波动、以及需要人类可读证明的形式化文档。

term-mode 对照

Aesop 证明的内容最终都是 term-mode 证明项。对于简单命题：

1
2
3
4
5
-- aesop 找到的证明：
example (h : A ∧ B) : B ∧ A := by aesop

-- 等价 term-mode：
example (h : A ∧ B) : B ∧ A := ⟨h.2, h.1⟩

Aesop 的价值不在于证明单个命题，而在于批量处理数十个"结构相似但手写繁琐"的子目标——在大型形式化项目中这类目标占比极高。

练习

练习 1（基础）：为以下类型注册 Aesop 规则（constructors + cases），然后用 aesop 证明 MyTriple.mk a b c 的各分量可提取：

1
2
3
4
structure MyTriple (α β γ : Type) where
  first  : α
  second : β
  third  : γ

练习 2（进阶）：创建自定义规则集 MyLogic，注册 Or.inl、Or.inr、And.intro 为 unsafe 规则（百分比自行选择），然后用 aesop (rule_sets := [MyLogic]) 证明 (A ∧ B) → (B ∨ A)。

练习 3（挑战）：注册一个 forward 类型的 safe 规则，使得当上下文中有 h : List α 且 h ≠ [] 时，Aesop 自动推导出 ∃ x xs, h = x :: xs。提示：使用 List.exists_cons_of_ne_nil（或等价引理）作为 forward 规则。

参考资料