add leansearch

Author: subfish-zhou

docs/tool/aesop.md

@@ -2,11 +2,11 @@
 
 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` 永远不会被重新访问。
+- 与 `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 的性能损失。然而，脚本生成目前并不完全可靠，因此你可能需要调整生成的脚本。
@@ -86,12 +86,12 @@ inductive NonEmpty : MyList α → Prop
 
 在这里，我们看到了第一个真正的 Aesop 功能：我们使用 **`@[aesop]`** 属性构建了两个与 `NonEmpty` 类型相关的 Aesop 规则。这些规则被添加到一个全局规则集中。当 Aesop 搜索证明时，它会系统地应用每个可用的规则，然后递归地搜索由规则生成的子目标的证明，依此类推，构建一个搜索树。当 Aesop 应用一个不生成子目标的规则时，目标就被证明了。
 
-一般来说，规则可以是任意的策略。但由于你可能不想为每个规则编写策略，`aesop` 属性提供了几个**规则构建器**，用于构建常见类型的规则。在我们的示例中，我们构建了：
+一般来说，规则可以是任意的策略。但由于你可能不想为每个规则编写策略，`aesop` 属性提供了几个 **规则构建器**，用于构建常见类型的规则。在我们的示例中，我们构建了：
 
 - 一个 **`constructors`** 规则。该规则在目标为 `NonEmpty _` 时尝试应用 `NonEmpty` 的每个构造函数。
 - 一个 **`cases`** 规则。该规则搜索假设 `h : NonEmpty _` 并对它们进行案例分析（类似于 `cases` 策略）。
 
-上述两个规则都被添加为**安全**规则。当安全规则在证明搜索过程中成功应用于某个目标时，它会被应用，并且该目标永远不会被再次访问。换句话说，搜索不会回溯安全规则。我们稍后会看到**不安全**规则，它们可以回溯。
+上述两个规则都被添加为 **安全** 规则。当安全规则在证明搜索过程中成功应用于某个目标时，它会被应用，并且该目标永远不会被再次访问。换句话说，搜索不会回溯安全规则。我们稍后会看到 **不安全** 规则，它们可以回溯。
 
 有了这些规则，我们可以证明一个关于 `NonEmpty` 和 `append` 的定理：
 
@@ -128,11 +128,11 @@ apply MyList.NonEmpty.cons
 
 经过一些后处理，你可以使用这个脚本来代替 Aesop 调用。这样你可以避免反复让 Aesop 搜索证明的性能损失。目前，证明脚本生成有一些已知的错误，但大多数时候它生成的脚本是可用的。
 
-`nonEmpty_append₁` 上的 `@[aesop]` 属性将此引理作为**不安全**规则添加到默认规则集中。对于这个规则，我们使用了 **`apply`** 规则构建器，它生成一个规则，每当目标是 `NonEmpty (_ ++ _)` 形式时，尝试应用 `nonEmpty_append₁`。
+`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 在多个不安全规则之间进行选择时，它会优先选择成功概率最高的规则。（平局会以确定性的方式打破。）
+每个不安全规则都带有一个 **成功概率** ，这里是 50%。这是对规则成功证明的可能性的一个非常粗略的估计。它用于优先处理目标：初始目标的优先级为 100%，每当我们应用一个不安全规则时，其子目标的优先级是其父目标的优先级乘以应用规则的成功概率。因此，重复应用 `nonEmpty_append₁` 会给我们优先级为 50%、25% 等的目标。Aesop 总是首先考虑优先级最高的未解决目标，因此它更喜欢涉及较少且高概率规则的证明尝试。此外，当 Aesop 在多个不安全规则之间进行选择时，它会优先选择成功概率最高的规则。（平局会以确定性的方式打破。）
 
 在添加 `nonEmpty_append` 后，Aesop 可以证明这个引理的一些推论：
 
@@ -176,19 +176,19 @@ theorem append_assoc {xs ys zs : MyList α} :
 
 规则是一个策略加上一些相关的元数据。规则有三种类型：
 
-- **规范化规则**（关键字 `norm`）必须生成零个或一个子目标。（零意味着规则关闭了目标）。每个规范化规则都与一个整数**惩罚**（默认值为 1）相关联。规范化规则按惩罚顺序应用，惩罚最低的优先。对于惩罚相同的规则，顺序未指定。有关规范化算法的详细信息，请参见下文。
+- **规范化规则**（关键字 `norm`）必须生成零个或一个子目标。（零意味着规则关闭了目标）。每个规范化规则都与一个整数 **惩罚**（默认值为 1）相关联。规范化规则按惩罚顺序应用，惩罚最低的优先。对于惩罚相同的规则，顺序未指定。有关规范化算法的详细信息，请参见下文。
 
   规范化规则也可以是 simp 引理。这些引理使用 `simp` 构建器构建。它们在规范化过程中通过特殊的 `simp` 调用使用。
 
-- **安全规则**（关键字 `safe`）在规范化之后但在任何不安全规则之前应用。当安全规则成功应用于目标时，目标变为**非活动**，意味着不再考虑其他规则。与规范化规则一样，安全规则与惩罚（默认值为 1）相关联，惩罚决定了规则的尝试顺序。
+- **安全规则**（关键字 `safe`）在规范化之后但在任何不安全规则之前应用。当安全规则成功应用于目标时，目标变为 **非活动**，意味着不再考虑其他规则。与规范化规则一样，安全规则与惩罚（默认值为 1）相关联，惩罚决定了规则的尝试顺序。
 
   安全规则应该是保可证性的，意味着如果目标是可证的，并且我们对其应用了安全规则，生成的子目标仍然应该是可证的。这是一个不太精确的概念，因为可证性取决于整个 Aesop 规则集。
 
 - **不安全规则**（关键字 `unsafe`）仅在所有可用的安全规则都失败时才尝试。当不安全规则应用于目标时，目标不会被标记为非活动，因此其他（不安全）规则仍然可以应用于它。这些规则应用被认为是独立的，直到其中一个证明目标（或者直到我们耗尽了所有可用的规则并确定目标在当前规则集下不可证）。
 
-  每个不安全规则都有一个介于 0% 和 100% 之间的**成功概率**。这些概率用于确定目标的优先级。初始目标的优先级为 100%，每当我们应用一个不安全规则时，其子目标的优先级是规则父目标的优先级乘以规则的成功概率。安全规则被视为具有 100% 的成功概率。
+  每个不安全规则都有一个介于 0% 和 100% 之间的 **成功概率**。这些概率用于确定目标的优先级。初始目标的优先级为 100%，每当我们应用一个不安全规则时，其子目标的优先级是规则父目标的优先级乘以规则的成功概率。安全规则被视为具有 100% 的成功概率。
 
-规则也可以是**多规则**。这些规则向目标添加多个规则应用。例如，注册 `Or` 类型的构造函数将生成一个多规则，给定目标 `A ∨ B`，生成一个目标为 `A` 的规则应用和一个目标为 `B` 的规则应用。这相当于为每个构造函数注册一个规则，但多规则可以稍微更高效和更自然。
+规则也可以是 **多规则**。这些规则向目标添加多个规则应用。例如，注册 `Or` 类型的构造函数将生成一个多规则，给定目标 `A ∨ B`，生成一个目标为 `A` 的规则应用和一个目标为 `B` 的规则应用。这相当于为每个构造函数注册一个规则，但多规则可以稍微更高效和更自然。
 
 ### 搜索树
 
@@ -213,17 +213,17 @@ Aesop 的核心数据结构是一个搜索树。这棵树交替包含两种节
 - 如果我们尚未尝试将安全规则应用于 `G` 的目标，则尝试应用每个安全规则（惩罚最低的优先）。一旦规则成功，将相应的 rapp 和子目标添加到树中，并将 `G` 标记为非活动。子目标接收与 `G` 相同的优先级。
 - 否则，至少有一个不安全规则尚未在 `G` 上尝试（否则 `G` 将是非活动的）。尝试成功概率最高的不安全规则，如果成功，则将相应的 rapp 和子目标添加到树中。子目标接收 `G` 的优先级乘以应用规则的成功概率。
 
-如果目标的所有可能规则都已应用，并且所有生成的子 rapp 都不可证，则目标**不可证**。如果 rapp 的任何子目标不可证，则 rapp 不可证。
+如果目标的所有可能规则都已应用，并且所有生成的子 rapp 都不可证，则目标 **不可证**。如果 rapp 的任何子目标不可证，则 rapp 不可证。
 
-在搜索过程中，目标或 rapp 也可能变得**无关**。这意味着我们不需要再次访问它。非正式地说，目标和 rapp 是无关的，如果它们是搜索树的一个分支的一部分，该分支已经成功证明了其目标，或者永远无法证明其目标。更正式地说：
+在搜索过程中，目标或 rapp 也可能变得 **无关**。这意味着我们不需要再次访问它。非正式地说，目标和 rapp 是无关的，如果它们是搜索树的一个分支的一部分，该分支已经成功证明了其目标，或者永远无法证明其目标。更正式地说：
 
 - 如果目标的父 rapp 不可证，则目标无关。（这意味着目标的某个兄弟已经不可证，因此我们知道父 rapp 永远不会被证明。）
 - 如果 rapp 的父目标已被证明，则 rapp 无关。（这意味着 rapp 的某个兄弟已经被证明，我们只需要一个证明。）
 - 如果目标或 rapp 的任何祖先是无关的，则目标或 rapp 无关。
 
 ### 规则构建器
 
-**规则构建器**是一个元程序，它将一个表达式转换为 Aesop 规则。当你用 `@[aesop]` 属性标记一个声明时，构建器会应用于声明的常量。当你使用 `add` 子句时，如 `(add <phase> <builder> (<term))`，构建器会应用于给定的项，该项可能涉及目标中的假设。然而，某些构建器仅支持全局常量。如果 `term` 是单个标识符，例如假设的名称，可以省略其周围的括号。
+**规则构建器** 是一个元程序，它将一个表达式转换为 Aesop 规则。当你用 `@[aesop]` 属性标记一个声明时，构建器会应用于声明的常量。当你使用 `add` 子句时，如 `(add <phase> <builder> (<term))`，构建器会应用于给定的项，该项可能涉及目标中的假设。然而，某些构建器仅支持全局常量。如果 `term` 是单个标识符，例如假设的名称，可以省略其周围的括号。
 
 目前可用的构建器有：
 
@@ -252,7 +252,7 @@ Aesop 的核心数据结构是一个搜索树。这棵树交替包含两种节
   ⊢ T
   ```
 
-  前向构建器还可以接受一个**立即名称**列表：
+  前向构建器还可以接受一个 **立即名称** 列表：
 
   ```lean
   forward (immediate := [n]) even_or_odd
@@ -592,9 +592,9 @@ n k : Nat
 ⊢ ?m < k
 ```
 
-我们现在可以通过应用不同的规则来解决第一个目标。例如，我们可以应用定理 `∀ n, n < n + 1`。我们也可以使用假设 `n < a`。这两个证明都会关闭第一个目标，但关键的是，它们会修改第二个目标：在第一种情况下，它变为 `n + 1 < k`；在第二种情况下，`a < k`。当然，其中一个可能是可证的，而另一个则不是。换句话说，第二个子目标现在依赖于第一个子目标的**证明**（而通常我们不在乎目标是如何证明的，只在乎它是否被证明）。Aesop 也可能决定先处理第二个子目标，在这种情况下，情况是对称的。
+我们现在可以通过应用不同的规则来解决第一个目标。例如，我们可以应用定理 `∀ 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 实际上将第二个子目标的实例化视为 **额外的目标**。因此，当我们应用定理 `∀ n, n < n + 1` 时，它关闭了第一个目标，Aesop 意识到由于应用了这个定理，我们现在还必须证明 `n + 1 < k`。因此，它将此目标添加为规则应用 `∀ n, n < n + 1` 的额外子目标（否则该规则应用不会有任何子目标）。类似地，当应用假设 `n < a` 时，其规则应用会获得一个额外的子目标 `a < k`。
 
 这种机制确保我们考虑所有潜在的证明。缺点是它相当爆炸性：当多个目标中有多个元变量时，Aesop 可能会以任何顺序访问它们，Aesop 可能会花费大量时间复制具有共享元变量的目标。它甚至可能多次尝试证明同一个目标，因为不同的规则可能会产生相同的元变量实例化。因此，最好将创建元变量的规则排除在全局规则集之外，并根据需要在个别 Aesop 调用中临时添加它们。