Aesop¶

Aesop（Automated Extensible Search for Obvious Proofs）是 Lean 4 的一个证明搜索策略。它与 Isabelle 的 auto 大体相似。本质上，Aesop 的工作方式如下：

与 simp 类似，你可以将一组（大量的）定义标记为 @[aesop] 属性，将它们注册为 Aesop 的**规则**。规则可以是任意的策略。我们提供了方便的方式来创建常见类型的规则，例如应用某个引理的规则。
Aesop 接受这些规则，并尝试将它们逐一应用到初始目标上。如果某个规则成功并生成子目标，Aesop 会递归地将规则应用到这些子目标上，构建一个**搜索树**。
搜索树以**最佳优先**的方式被探索。你可以将规则标记为更有可能或不太可能有用。基于这些信息，Aesop 会优先处理搜索树中更有希望的目标，先处理更有希望的目标，再处理不太有希望的目标。
在将任何规则应用到目标之前，目标会被**规范化**，使用一组特殊的（可定制的）规范化规则。一个重要的内置规范化规则会运行 simp_all，因此你的 @[simp] 引理会被 Aesop 考虑。
规则可以被标记为**安全的**，以优化 Aesop 的性能。安全规则会被急切地应用，并且永远不会回溯。例如，Aesop 的内置规则会安全地将目标 P ∧ Q 拆分为 P 和 Q 的目标。拆分后，原始目标 P ∧ Q 永远不会被重新访问。
Aesop 提供了一组内置规则，用于执行逻辑操作（例如对假设 P ∨ Q 进行案例分析）和一些其他直接的推理。
Aesop 使用类似于 simp 和其他 Lean 策略的索引方法。这意味着即使规则集很大，它也应该保持相对较快的速度。
当以 aesop? 调用时，Aesop 会打印一个证明目标的策略脚本，类似于 simp?。这样你可以避免一直运行 Aesop 的性能损失。然而，脚本生成目前并不完全可靠，因此你可能需要调整生成的脚本。

Aesop 适用于两个主要用例：

通用自动化，Aesop 用于处理“简单”目标。通过注册足够多的引理作为 Aesop 规则，你可以将 Aesop 变成一个更强大的 simp。
专用自动化，构建特定的 Aesop 规则集来处理某一类目标。Mathlib 中的策略如 measurability 和 continuity 就是通过 Aesop 实现的。

我偶尔会更新这个 README，因此细节可能会过时。如果你有问题，请创建一个 issue 或在 Lean Zulip 上联系我（Jannis Limperg）。欢迎提交 Pull Request！

还有一篇关于 Aesop 的论文，涵盖了许多这里讨论的主题，有时会更详细。

构建¶

安装了 elan 后，lake build 应该就足够了。

将 Aesop 添加到你的项目¶

要在 Lean 4 项目中使用 Aesop，首先将此包添加为依赖项。在你的 lakefile.lean 中添加：

require aesop from git "https://github.com/leanprover-community/aesop"

你还需要确保你的 lean-toolchain 文件包含与 Aesop 相同的 Lean 4 版本，并且 Aesop 的依赖项（目前只有 std4）的版本匹配。遗憾的是，我们目前不支持版本范围。

现在以下测试文件应该可以编译：

import Aesop

example : α → α :=
  by aesop

快速入门¶

为了让你快速上手，我将通过一系列示例解释 Aesop 的主要概念。下一节将进行更全面、参考风格的讨论。

我们首先定义自己的列表版本（以避免与标准库冲突）和一个 append 函数：

inductive MyList (α : Type _)
  | nil
  | cons (hd : α) (tl : MyList α)

namespace MyList

protected def append : (_ _ : MyList α) → MyList α
  | nil, ys => ys
  | cons x xs, ys => cons x (MyList.append xs ys)

instance : Append (MyList α) :=
  ⟨MyList.append⟩

我们还告诉 simp 展开 append 的应用：

@[simp]
theorem nil_append : nil ++ xs = xs := rfl

@[simp]
theorem cons_append : cons x xs ++ ys = cons x (xs ++ ys) := rfl

当 Aesop 第一次遇到目标时，它会通过运行一组可定制的规范化规则来规范化目标。其中一个规范化规则实际上会运行 simp_all，因此 Aesop 会自动考虑 simp 引理。

现在我们定义 MyList 上的 NonEmpty 谓词：

@[aesop safe [constructors, cases]]
inductive NonEmpty : MyList α → Prop
  | cons : NonEmpty (cons x xs)

在这里，我们看到了第一个真正的 Aesop 功能：我们使用 @[aesop] 属性构建了两个与 NonEmpty 类型相关的 Aesop 规则。这些规则被添加到一个全局规则集中。当 Aesop 搜索证明时，它会系统地应用每个可用的规则，然后递归地搜索由规则生成的子目标的证明，依此类推，构建一个搜索树。当 Aesop 应用一个不生成子目标的规则时，目标就被证明了。

一般来说，规则可以是任意的策略。但由于你可能不想为每个规则编写策略，aesop 属性提供了几个**规则构建器**，用于构建常见类型的规则。在我们的示例中，我们构建了：

一个 constructors 规则。该规则在目标为 NonEmpty _ 时尝试应用 NonEmpty 的每个构造函数。
一个 cases 规则。该规则搜索假设 h : NonEmpty _ 并对它们进行案例分析（类似于 cases 策略）。

上述两个规则都被添加为**安全**规则。当安全规则在证明搜索过程中成功应用于某个目标时，它会被应用，并且该目标永远不会被再次访问。换句话说，搜索不会回溯安全规则。我们稍后会看到**不安全**规则，它们可以回溯。

有了这些规则，我们可以证明一个关于 NonEmpty 和 append 的定理：

@[aesop unsafe 50% apply]
theorem nonEmpty_append₁ {xs : MyList α} ys :
    NonEmpty xs → NonEmpty (xs ++ ys) := by
  aesop

Aesop 在四个步骤中找到这个证明：

一个内置规则引入了假设 h : NonEmpty xs。默认情况下，Aesop 的规则集包含一些处理逻辑连接词 →、∧、∨ 和 ¬ 以及量词 ∀ 和 ∃ 以及其他一些基本类型的直接规则。
NonEmpty 的 cases 规则对 h 进行案例分析。
我们之前添加的 simp 规则 cons_append 展开了 ++ 操作。
NonEmpty 的 constructor 规则应用了 NonEmpty.cons。

如果你想查看 Aesop 如何证明你的目标（或者为什么它没有证明你的目标，或者为什么它花了太长时间来证明你的目标），你可以启用追踪：

set_option trace.aesop true

这会让 Aesop 在搜索证明时打印出它所采取的步骤。你还可以通过启用 trace.aesop.tree 选项查看 Aesop 构建的搜索树。更多追踪选项，输入 set_option trace.aesop 并查看自动补全建议。

如果在上述示例中你调用 aesop?，Aesop 会打印一个证明脚本。在撰写本文时，它看起来像这样：

intro a
obtain @⟨x, xs_1⟩ := a
simp_all only [cons_append]
apply MyList.NonEmpty.cons

经过一些后处理，你可以使用这个脚本来代替 Aesop 调用。这样你可以避免反复让 Aesop 搜索证明的性能损失。目前，证明脚本生成有一些已知的错误，但大多数时候它生成的脚本是可用的。

nonEmpty_append₁ 上的 @[aesop] 属性将此引理作为**不安全**规则添加到默认规则集中。对于这个规则，我们使用了 apply 规则构建器，它生成一个规则，每当目标是 NonEmpty (_ ++ _) 形式时，尝试应用 nonEmpty_append₁。

不安全规则是可以回溯的规则，因此在它们被应用到目标后，Aesop 仍然可以尝试其他规则来解决同一目标。这对于 nonEmpty_append₁ 是有意义的：如果我们有一个目标 NonEmpty (xs ++ ys)，我们可以通过显示 NonEmpty xs（即应用 nonEmpty_append₁）或通过显示 NonEmpty ys 来证明它。如果 nonEmpty_append₁ 被注册为安全规则，我们将总是选择 NonEmpty xs，而永远不会调查 NonEmpty ys。

每个不安全规则都带有一个**成功概率**，这里是 50%。这是对规则成功证明的可能性的一个非常粗略的估计。它用于优先处理目标：初始目标的优先级为 100%，每当我们应用一个不安全规则时，其子目标的优先级是其父目标的优先级乘以应用规则的成功概率。因此，重复应用 nonEmpty_append₁ 会给我们优先级为 50%、25% 等的目标。Aesop 总是首先考虑优先级最高的未解决目标，因此它更喜欢涉及较少且高概率规则的证明尝试。此外，当 Aesop 在多个不安全规则之间进行选择时，它会优先选择成功概率最高的规则。（平局会以确定性的方式打破。）

在添加 nonEmpty_append 后，Aesop 可以证明这个引理的一些推论：

example {α : Type u} {xs : MyList α} ys zs :
    NonEmpty xs → NonEmpty (xs ++ ys ++ zs) := by
  aesop

接下来，我们证明另一个关于 NonEmpty 的简单定理：

theorem nil_not_nonEmpty (xs : MyList α) : xs = nil → ¬ NonEmpty xs := by
  aesop (add 10% cases MyList)

在这里，我们使用了一个 add 子句来添加一个仅在此特定 Aesop 调用中使用的规则。该规则是一个不安全的 cases 规则，用于 MyList。（如你所见，你可以省略 unsafe 关键字，只指定成功概率。）这个规则是危险的：当我们将其应用于假设 xs : MyList α 时，我们会得到 x : α 和 ys : MyList α，因此我们可以再次对 ys 应用 cases 规则，依此类推。因此，我们给这个规则一个非常低的成功概率，以确保 Aesop 尽可能应用其他规则。

以下是一些 Aesop 的规范化阶段特别有用的示例：

@[simp]
theorem append_nil {xs : MyList α} :
    xs ++ nil = xs := by
  induction xs <;> aesop

theorem append_assoc {xs ys zs : MyList α} :
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  induction xs <;> aesop

由于我们之前将 append 的展开引理添加到了全局 simp 集合中，Aesop 可以或多或少地自行证明关于这个函数的定理（尽管实际上 simp_all 已经足够了）。然而，我们仍然需要显式地进行归纳。这是一个有意的设计选择：自动化归纳的技术存在，但它们复杂、有些慢且不完全可靠，因此我们更喜欢手动进行。

更多示例可以在本仓库的 AesopTest 文件夹中找到。特别是，文件 AesopTest/List.lean 包含了从 Lean 3 版本的 mathlib 移植的 200 个基本列表引理的 Aesop 化版本，文件 AesopTest/SeqCalcProver.lean 展示了 Aesop 如何帮助形式化一个简单的序列演算证明器。

参考¶

本节系统地、相当全面地介绍了 Aesop 的操作方式。

规则¶

规则是一个策略加上一些相关的元数据。规则有三种类型：

规范化规则（关键字 norm）必须生成零个或一个子目标。（零意味着规则关闭了目标）。每个规范化规则都与一个整数**惩罚**（默认值为 1）相关联。规范化规则按惩罚顺序应用，惩罚最低的优先。对于惩罚相同的规则，顺序未指定。有关规范化算法的详细信息，请参见下文。

规范化规则也可以是 simp 引理。这些引理使用 simp 构建器构建。它们在规范化过程中通过特殊的 simp 调用使用。

安全规则（关键字 safe）在规范化之后但在任何不安全规则之前应用。当安全规则成功应用于目标时，目标变为**非活动**，意味着不再考虑其他规则。与规范化规则一样，安全规则与惩罚（默认值为 1）相关联，惩罚决定了规则的尝试顺序。

安全规则应该是保可证性的，意味着如果目标是可证的，并且我们对其应用了安全规则，生成的子目标仍然应该是可证的。这是一个不太精确的概念，因为可证性取决于整个 Aesop 规则集。

不安全规则（关键字 unsafe）仅在所有可用的安全规则都失败时才尝试。当不安全规则应用于目标时，目标不会被标记为非活动，因此其他（不安全）规则仍然可以应用于它。这些规则应用被认为是独立的，直到其中一个证明目标（或者直到我们耗尽了所有可用的规则并确定目标在当前规则集下不可证）。

每个不安全规则都有一个介于 0% 和 100% 之间的**成功概率**。这些概率用于确定目标的优先级。初始目标的优先级为 100%，每当我们应用一个不安全规则时，其子目标的优先级是规则父目标的优先级乘以规则的成功概率。安全规则被视为具有 100% 的成功概率。

规则也可以是**多规则**。这些规则向目标添加多个规则应用。例如，注册 Or 类型的构造函数将生成一个多规则，给定目标 A ∨ B，生成一个目标为 A 的规则应用和一个目标为 B 的规则应用。这相当于为每个构造函数注册一个规则，但多规则可以稍微更高效和更自然。

搜索树¶

Aesop 的核心数据结构是一个搜索树。这棵树交替包含两种节点：

目标节点：这些节点存储一个目标，以及与搜索相关的元数据。目标节点的父节点和子节点是规则应用节点。特别是，每个目标节点都有一个介于 0% 和 100% 之间的**优先级**。
规则应用（'rapp'）节点：这些目标存储一个规则（加上元数据）。rapp 节点的父节点和子节点是目标节点。当搜索树包含一个规则为 r、父节点为 p、子节点为 c₁, ..., cₙ 的 rapp 节点时，这意味着规则 r 的策略被应用于 p 的目标，生成了 cᵢ 的子目标。

当一个目标节点有多个子 rapp 节点时，我们有一个选择如何解决目标的选择。这使得这棵树成为一个 AND-OR 树：要证明一个 rapp，必须证明它的所有子目标；要证明一个目标，必须证明它的任何一个子 rapp。

搜索¶

我们从一个包含单个目标节点的搜索树开始。该节点的目标是 Aesop 应该解决的目标。然后我们在一个循环中执行以下步骤，如果 (a) 根目标已被证明；(b) 根目标变得不可证；或 © 达到 Aesop 的某个规则限制（例如，应用规则的总数或搜索深度），则停止。

选择优先级最高的活动目标节点 G。粗略地说，目标节点是活动的，如果它未被证明并且我们尚未对其应用所有可能的规则。
如果 G 的目标尚未被规范化，则规范化它。这意味着我们运行以下规范化循环：
运行惩罚为负的规范化规则（惩罚最低的优先）。如果其中任何一个规则成功，则使用规则生成的目标重新启动规范化循环。
对所有假设和目标运行 simp，使用全局 simp 集合（即标记为 @[simp] 的引理）加上 Aesop 的 simp 规则。
运行惩罚为正的规范化规则（惩罚最低的优先）。如果其中任何一个规则成功，则使用规则生成的目标重新启动规范化循环。

当所有规范化规则都失败时，循环结束。它会破坏性地更新 G 的目标（并可能直接证明它）。 - 如果我们尚未尝试将安全规则应用于 G 的目标，则尝试应用每个安全规则（惩罚最低的优先）。一旦规则成功，将相应的 rapp 和子目标添加到树中，并将 G 标记为非活动。子目标接收与 G 相同的优先级。 - 否则，至少有一个不安全规则尚未在 G 上尝试（否则 G 将是非活动的）。尝试成功概率最高的不安全规则，如果成功，则将相应的 rapp 和子目标添加到树中。子目标接收 G 的优先级乘以应用规则的成功概率。

如果目标的所有可能规则都已应用，并且所有生成的子 rapp 都不可证，则目标**不可证**。如果 rapp 的任何子目标不可证，则 rapp 不可证。

在搜索过程中，目标或 rapp 也可能变得**无关**。这意味着我们不需要再次访问它。非正式地说，目标和 rapp 是无关的，如果它们是搜索树的一个分支的一部分，该分支已经成功证明了其目标，或者永远无法证明其目标。更正式地说：

如果目标的父 rapp 不可证，则目标无关。（这意味着目标的某个兄弟已经不可证，因此我们知道父 rapp 永远不会被证明。）
如果 rapp 的父目标已被证明，则 rapp 无关。（这意味着 rapp 的某个兄弟已经被证明，我们只需要一个证明。）
如果目标或 rapp 的任何祖先是无关的，则目标或 rapp 无关。

规则构建器¶

**规则构建器**是一个元程序，它将一个表达式转换为 Aesop 规则。当你用 @[aesop] 属性标记一个声明时，构建器会应用于声明的常量。当你使用 add 子句时，如 (add <phase> <builder> (<term))，构建器会应用于给定的项，该项可能涉及目标中的假设。然而，某些构建器仅支持全局常量。如果 term 是单个标识符，例如假设的名称，可以省略其周围的括号。

目前可用的构建器有：

apply：生成一个类似于 apply 策略的规则。
forward：当应用于类型为 A₁ → ... Aₙ → B 的项时，生成一个规则，该规则在目标中查找假设 h₁ : A₁, ..., hₙ : Aₙ，如果找到，则添加一个新的假设 fwd : B。例如，考虑引理 even_or_odd：

even_or_odd : ∀ (n : Nat), Even n ∨ Odd n

将其注册为前向规则会将目标

n : Nat
m : Nat
⊢ T

转换为：

n : Nat
hn : Even n ∨ Odd n
m : Nat
hm : Even m ∨ Odd m
⊢ T

前向构建器还可以接受一个**立即名称**列表：

forward (immediate := [n]) even_or_odd

立即名称（此处为 n）指的是 even_or_odd 的参数。当 Aesop 应用带有显式立即名称的前向规则时，它仅将相应的参数与假设匹配。（此处，even_or_odd 只有一个参数，因此没有区别。）

如果没有给出立即名称，Aesop 会认为每个参数都是立即的，除了实例参数和依赖参数（即可以从后续参数的类型推断出的参数）。

如果上下文中已经存在相同类型的假设，前向规则永远不会添加新的假设。 - destruct：类似于 forward，但在规则应用后，清除作为立即参数使用的命题假设（即类型为 Prop 的假设）。这在你想消除假设时很有用。例如，规则

@[aesop norm destruct]
theorem and_elim_right : α ∧ β → α := ...

会将目标

h₁ : (α ∧ β) ∧ γ
h₂ : δ ∧ ε

转换为：

h₁ : α
h₂ : δ

如果假设 h 被用作 destruct 规则的立即参数，而另一个假设 h' 依赖于 h，但 h' 不是同一规则的立即参数，则 h 不会被清除。这是因为我们不能在不清除 h' 的情况下清除 h。 - constructors：当应用于归纳类型或结构 T 时，生成一个规则，该规则尝试将 T 的每个构造函数应用于目标。这是一个多规则，因此如果多个构造函数适用，它们会被并行考虑。如果你使用此构建器构建不安全规则，每个构造函数应用都会收到相同的成功概率；如果这不是你想要的，可以为构造函数添加单独的 apply 规则。 - cases：当应用于归纳类型或结构 T 时，生成一个规则，该规则对上下文中的每个假设 h : T 进行案例分析。该规则会递归到子目标中，因此当应用于具有假设 h₁ : A ∨ B ∨ C 和 h₂ : D ∨ E 的目标时，cases Or 会生成 6 个目标。然而，如果 T 是递归类型（例如 List），我们只对每个假设进行一次案例分析。否则，我们会无限循环。

cases_patterns 选项可用于仅在特定形状的假设上应用规则。例如，规则 cases (cases_patterns := [Fin 0]) Fin 只会对类型为 Fin 0 的假设进行案例分析。模式可以包含下划线，例如 0 ≤ _。可以给出多个模式（用逗号分隔）；当至少有一个模式匹配假设时，规则就会被应用。 - simp：当应用于等式 eq : A₁ → ... Aₙ → x = y 时，将 eq 注册为规范化过程中内置 simp 过程的 simp 引理。因此，此构建器只能构建规范化规则。 - unfold：当应用于定义或 let 假设 f 时，注册 f 以在规范化过程中展开（即替换为其定义）。因此，此构建器只能构建规范化规则。展开在一个单独的 simp 过程中进行。

simp 构建器也可以用于展开定义。区别在于，simp 规则执行智能展开（类似于 simp 策略），而 unfold 规则执行非智能展开（类似于 unfold 策略）。非智能展开会展开函数，即使它们的方程不匹配，因此 unfold 规则会导致循环，因此被禁止。 - tactic：接受一个策略并将其直接转换为规则。当此构建器在 add 子句中使用时，你可以使用例如 (add safe (by norm_num)) 将 norm_num 注册为安全规则。by 块也可以包含多个策略以及对假设的引用。当你在 add 子句中使用 (by ...) 时，Aesop 会自动使用策略构建器，除非你指定了不同的构建器。

当此构建器在 @[aesop] 属性中使用时，标记该属性的声明必须具有类型 TacticM Unit、Aesop.SingleRuleTac 或 Aesop.RuleTac。后者是 Aesop 数据类型，它们将策略与额外的元数据关联起来；使用它们可能会使规则操作更高效。

规则策略不应是“无操作”的：如果规则策略不适用于目标，它应该失败而不是返回未更改的目标。所有无操作规则都会浪费时间；无操作的 norm 规则会使规范化进入无限循环；而无操作的 safe 规则会阻止不安全规则的应用。

规范化规则不能分配元变量（除了目标元变量）或引入新的元变量（除了新的目标元变量）。这可能是一个问题，因为某些 Lean 策略（例如 cases）即使在你不期望的情况下也会这样做。目前没有很好的解决方案。 - default：默认构建器。这是在你注册规则时未指定构建器时使用的构建器，但你也可以显式使用它。根据规则的阶段，默认构建器会尝试不同的构建器，使用第一个有效的构建器。这些构建器是： - 对于 safe 和 unsafe 规则：constructors、tactic、apply。 - 对于 norm 规则：constructors、tactic、simp、apply。

透明选项¶

规则构建器 apply、constructors 和 cases 都有一个 transparency 选项。此选项控制规则执行的透明度。例如，使用构建器 apply (transparency := reducible) 注册规则会使规则的行为类似于策略 with_reducible apply。

然而，即使你更改了规则的透明度，它仍然以 reducible 透明度进行索引（因为我们用于索引的数据结构仅支持 reducible 透明度）。因此，假设你注册了一个透明度为 default 的 apply 规则。进一步假设该规则得出结论 A ∧ B，而你的目标是 T，其中 def T := A ∧ B。由于该规则可以在 default 透明度下展开 T 以发现 A ∧ B，因此该规则可以应用于目标。然而，该规则永远不会被应用，因为索引过程只看到 T，并不认为该规则可能适用。

要覆盖此行为，你可以编写 apply (transparency! := default)（注意感叹号）。这会禁用索引，因此规则会在每个目标上尝试。

规则集¶

规则集通过以下命令声明：

declare_aesop_rule_sets [r₁, ..., rₙ] (default := <bool>)

其中 rᵢ 是任意名称。为了避免冲突，请在你的包的命名空间中选择名称。设置 default := true 会使规则集默认激活。default 子句可以省略，默认为 false。

在规则集中，规则由其名称、构建器和阶段（safe/unsafe/norm）标识。这意味着你可以将相同的声明添加为具有不同构建器或不同阶段的多个规则，但不能添加具有不同优先级或不同构建器选项的规则（如果规则的构建器有选项）。

规则可以出现在多个规则集中，但在这种情况下，你应该确保它们具有相同的优先级并使用相同的构建器选项。否则，Aesop 会认为这些规则相同并任意选择一个。

开箱即用，Aesop 使用默认规则集 builtin 和 default。builtin 集包含处理各种构造的内置规则（见下文）。default 集包含由 Aesop 用户添加的规则，而没有指定规则集。

`@[aesop]` 属性¶

可以通过用 @[aesop] 属性注释声明来将其添加到规则集中。与其他属性一样，你可以使用 @[local aesop] 仅在当前部分或命名空间内添加规则，并使用 @[scoped aesop] 仅在当前命名空间打开时添加规则。

单一规则¶

在大多数情况下，你会希望为声明添加一个规则。语法如下：

@[aesop <phase>? <priority>? <builder>? <builder_option>* <rule_sets>?]

其中：

<phase> 是 safe、norm 或 unsafe。除非满足以下条件，否则不能省略。
<priority> 是：
对于 simp 规则，是一个自然数。这用作生成的 simp 引理的优先级，因此注册优先级为 n 的 simp 规则大致等同于属性 @[simp n]。如果省略，则默认为 Lean 的默认 simp 优先级。
对于 safe 和 norm 规则（除了 simp 规则），是一个整数惩罚。如果省略，则默认为 1。
对于 unsafe 规则，是一个介于 0% 和 100% 之间的百分比。不能省略。在给出百分比时，可以省略 unsafe 阶段说明。
对于 unfold 规则，可以给出惩罚，但目前被忽略。
<builder> 是上述构建器之一。如果未指定构建器，则使用给定阶段的默认构建器。

当使用 simp 构建器时，可以省略 norm 阶段，因为此构建器只能生成规范化规则。

<builder_option>* 是零个或多个构建器选项的列表。有关不同构建器的选项，请参见上文。
<rule_sets> 是一个子句，形式为：

(rule_sets := [r₁, ..., rₙ])

其中 rᵢ 是声明的规则集。（括号是必需的。）规则仅添加到指定的规则集。如果省略此子句，则默认为 (rule_sets := [default])。

多个规则¶

有时为单个声明添加多个规则是有用的，例如为同一归纳类型添加 cases 和 constructors 规则。在这种情况下，你可以编写例如：

@[aesop unsafe [constructors 75%, cases 90%]]
inductive T ...

@[aesop apply [safe (rule_sets := [A]), 70% (rule_sets := [B])]]
def foo ...

@[aesop [80% apply, safe 5 forward (immediate := x)]]
def bar (x : T) ...

在第一个示例中，为 T 注册了两个不安全规则，一个成功概率为 75%，另一个为 90%。

在第二个示例中，为 foo 注册了两个规则。两者都使用 apply 构建器。第一个是默认惩罚的 safe 规则，添加到规则集 A。第二个是成功概率为 70% 的 unsafe 规则，添加到规则集 B。

在第三个示例中，为 bar 注册了两个规则：一个成功概率为 80% 的 unsafe 规则，使用 apply 构建器；一个惩罚为 5 的 safe 规则，使用 forward 构建器。

一般来说，@[aesop] 属性的语法是：

attr      ::= @[aesop <rule_expr>]
            | @[aesop [<rule_expr,+>]]

rule_expr ::= feature
            | feature <rule_expr>
            | feature [<rule_expr,+>]

其中 feature 是一个阶段、优先级、构建器或 rule_sets 子句。此语法生成一个或多个特征树，每个树的每个分支指定一个规则。（分支是特征列表。）

添加外部规则¶

你可以使用 attribute 命令为之前声明的常量添加规则，无论是在你自己的开发中还是在导入的包中：

attribute [aesop norm unfold] List.all -- List.all 来自 Init

你也可以使用 add_aesop_rules 命令：

add_aesop_rules safe [(by linarith), Nat.add_comm 0]

如你所见，此命令可用于添加策略和复合项。使用 local add_aesop_rules 和 scoped add_aesop_rules 以获得与 @[local aesop] 和 @[scoped aesop] 等效的效果。

删除规则¶

有两种删除规则的方法。通常只需删除 @[aesop] 属性即可：

attribute [-aesop] foo

这将从所有规则集中删除与声明 foo 关联的所有规则。然而，这种删除不是持久的，因此规则会在文件末尾重新出现。这是 Lean 属性系统的一个基本限制：一旦声明被标记为属性，就无法永久取消标记。

如果你只想删除某些规则，可以使用 erase_aesop_rules 命令：

erase_aesop_rules [safe apply foo, bar (rule_sets := [A])]

这将删除：

所有使用 apply 构建器的 foo 安全规则（但不包括其他，例如不安全规则或 forward 规则）；
规则集 A 中所有 bar 的规则。

一般来说，语法是：

erase_aesop_rules [<rule_expr,+>]

即规则的指定方式与 @[aesop] 属性相同。然而，每个规则还必须指定应删除其规则的声明的名称。因此，rule_expr 语法扩展为 feature 也可以是声明名称。

请注意，使用默认构建器之一（safe_default、norm_default、unsafe_default）添加的规则将根据最终使用的构建器名称注册，例如 apply 或 simp。因此，如果你想删除此类规则，可能需要指定该构建器而不是默认构建器。

`aesop` 策略¶

在其最基本的形式中，你可以通过编写以下内容调用 Aesop 策略：

example : α → α := by
  aesop

这将使用默认规则集中的规则。开箱即用，这些是 default 规则集，包含未提及特定规则集的 @[aesop] 属性标记的规则，以及 builtin 规则集，包含 Aesop 内置的规则。然而，其他规则集也可以默认启用；参见 declare_aesop_rule_sets 命令。

该策略的行为也可以通过各种选项进行自定义。一个更复杂的 Aesop 调用可能如下所示：

aesop
  (add safe foo, 10% cases Or, safe cases Empty)
  (erase A, baz)
  (rule_sets := [A, B])
  (config := { maxRuleApplicationDepth := 10 })

在这里，我们使用 add 子句添加一些规则，使用 erase 子句删除其他规则，限制使用的规则集并设置一些选项。下面将更详细地讨论这些子句。

向 Aesop 调用添加规则¶

可以使用 add 子句向 Aesop 调用添加规则。这不会影响任何声明的规则集。add 子句的语法是：

(add <rule_expr,+>)

即规则的指定方式与 @[aesop] 属性相同。与 erase_aesop_rules 命令一样，每个规则必须指定应从其构建规则的声明的名称；例如：

(add safe [foo 1, bar 5])

将声明 foo 添加为惩罚为 1 的安全规则，将 bar 添加为惩罚为 5 的安全规则。

规则名称也可以引用目标上下文中的假设，但并非所有构建器都支持这一点。

从 Aesop 调用中删除规则¶

可以使用 erase 子句从 Aesop 调用中删除规则。同样，这仅影响当前的 Aesop 调用，而不影响声明的规则集。erase 子句的语法是：

(erase <rule_expr,+>)

它的工作方式与 erase_aesop_rules 命令完全相同。要删除与 x 和 y 关联的所有规则，请编写：

(erase x, y)

选择规则集¶

默认情况下，Aesop 使用 default 和 builtin 规则集，以及声明为默认规则集的规则集。可以给出 rule_sets 子句以包含其他规则集，例如：

(rule_sets := [A, B])

这将使用规则集 A、B、default 和 builtin（以及任何声明为默认规则集的规则集）。规则集也可以通过 rule_sets := [-default, -builtin] 禁用。

设置选项¶

可以使用 config 子句设置各种选项，其语法为：

(config := <term>)

该术语是类型为 Aesop.Options 的任意 Lean 表达式；有关详细信息，请参见该类型。值得注意的选项包括：

strategy 选择最佳优先、深度优先或广度优先搜索策略。默认为最佳优先。
useSimpAll := false 使内置的 simp 规则使用 simp at * 而不是 simp_all。
enableSimp := false 同时禁用内置的 simp 规则。

类似地，内置的规范化 simp 规则的选项可以通过以下方式设置：

(simp_config := <term>)

你可以在这里给出与 simp (config := ...) 相同的选项。

内置规则¶

内置规则集（即 builtin 规则集中的规则）目前还不太稳定，因此暂时不会详细记录。请参见 Aesop/BuiltinRules.lean 和 Aesop/BuiltinRules/*.lean。

证明脚本¶

通过调用 aesop? 而不是 aesop，你可以指示 Aesop 生成一个证明目标的策略脚本（如果 Aesop 成功）。脚本会以 Try this: 建议的形式打印出来，类似于 simp?。

目前，Aesop 生成的脚本有些特殊。例如，它们可能包含 aesop_cases 策略，这是标准 cases 策略的一个变体。此外，Aesop 偶尔会生成有问题的脚本，这些脚本无法解决目标。我们希望最终解决这些问题；在此之前，你可能需要手动稍微调整证明脚本。

追踪¶

要查看 Aesop 如何证明目标——或者为什么它没有证明目标，或者为什么它证明目标很慢——查看它在做什么是很有用的。为此，你可以启用各种追踪选项。这些选项使用通常的语法，例如：

set_option trace.aesop true

主要的选项包括：

trace.aesop：打印 Aesop 尝试解决哪些目标、尝试应用哪些规则（成功或失败）等的逐步日志。
trace.aesop.ruleSet：打印用于 Aesop 调用的规则集。
trace.aesop.proof：如果 Aesop 成功，打印生成的证明（作为 Lean 项）。你应该能够复制并粘贴此证明以替换 Aesop。

性能分析¶

要了解 Aesop 在哪些地方花费时间，可以使用：

set_option trace.aesop.stats true

Aesop 随后会打印有关此次 Aesop 运行的一些统计信息。

要获取多次 Aesop 调用的统计信息，请为相关文件（或某些调用）激活选项 aesop.collectStats，并在导入所有相关文件的文件中运行命令 #aesop_stats。例如，要评估 Aesop 在 Mathlib 中的性能，请在 Mathlib 的 lakefile.lean 中设置选项 aesop.collectStats，从头重新编译 Mathlib，并创建一个新的 Lean 文件，内容为：

import Mathlib

#aesop_stats

你还可以激活 profiler 选项，该选项会增强 trace.aesop 生成的追踪信息，包含每个步骤所花费的时间。请注意，只有与目标扩展和规则应用相关的时间信息是相关的。其他时间信息，例如与新 rapp 和目标相关的时间信息，只是 Lean 追踪 API 的产物。

检查内部不变量¶

如果你遇到看起来像 Aesop 内部错误的行为，设置选项 aesop.check.all（或更细粒度的 aesop.check.* 选项）可能会有所帮助。这会使 Aesop 在策略运行时检查各种不变量。这些检查有些昂贵，因此在报告错误后请记得取消设置该选项。

处理元变量¶

创建元变量的规则必须由 Aesop 特殊处理。例如，假设我们将 < 的传递性注册为 Aesop 规则。那么我们可能会得到以下形式的目标状态：

n k : Nat
⊢ n < ?m

n k : Nat
⊢ ?m < k

我们现在可以通过应用不同的规则来解决第一个目标。例如，我们可以应用定理 ∀ n, n < n + 1。我们也可以使用假设 n < a。这两个证明都会关闭第一个目标，但关键的是，它们会修改第二个目标：在第一种情况下，它变为 n + 1 < k；在第二种情况下，a < k。当然，其中一个可能是可证的，而另一个则不是。换句话说，第二个子目标现在依赖于第一个子目标的**证明**（而通常我们不在乎目标是如何证明的，只在乎它是否被证明）。Aesop 也可能决定先处理第二个子目标，在这种情况下，情况是对称的。

由于这种依赖性，Aesop 实际上将第二个子目标的实例化视为**额外的目标**。因此，当我们应用定理 ∀ n, n < n + 1 时，它关闭了第一个目标，Aesop 意识到由于应用了这个定理，我们现在还必须证明 n + 1 < k。因此，它将此目标添加为规则应用 ∀ n, n < n + 1 的额外子目标（否则该规则应用不会有任何子目标）。类似地，当应用假设 n < a 时，其规则应用会获得一个额外的子目标 a < k。

这种机制确保我们考虑所有潜在的证明。缺点是它相当爆炸性：当多个目标中有多个元变量时，Aesop 可能会以任何顺序访问它们，Aesop 可能会花费大量时间复制具有共享元变量的目标。它甚至可能多次尝试证明同一个目标，因为不同的规则可能会产生相同的元变量实例化。因此，最好将创建元变量的规则排除在全局规则集之外，并根据需要在个别 Aesop 调用中临时添加它们。

还值得注意的是，当安全规则分配元变量时，它被视为不安全规则（成功概率为 90%）。这是因为分配元变量几乎从来都不是安全的，原因与上述相同：通常完全安全的规则 ∀ n, n < n + 1 如果被视为安全规则，将迫使我们承诺元变量 ?m 的一个特定实例化。

有关元变量处理的更多详细信息，请参见 Aesop 论文。