`classical tacs` 在一个作用域内运行 `tacs`，其中 `Classical.propDecidable` 是低优先级局部实例。请注意，`classical` 是作用域策略：它只在该策略的作用域内加入此实例。

`assumption` 尝试使用类型兼容的假设解决主目标，否则失败。 另请注意项记法 `‹ t ›`，它是 `show t by assumption` 的简写。

`apply_assumption` 寻找形如 `... → ∀ _ , ... → head` 的假设，其中 `head` 与当前目标匹配。可以使用 `apply_assumption [ ... ]` 指定要应用的附加规则。 默认情况下，`apply_assumption` 还会尝试 `rfl`、`trivial`、`congrFun` 和 `congrArg`。如果不希望使用这些内容，或者不希望使用所有假设，请使用 `apply_assumption only [ ... ]`。 可以使用 `apply_assumption [ - h ]` 排除局部假设。可以使用 `apply_assumption using [ a₁ , ... ]` 来使用所有以属性 `aᵢ` 标记的引理（这些属性必须使用 `register_label_attr` 创建）。 `apply_assumption` 会使用通过 `symm` 从局部假设得到的推论。如果 `apply_assumption` 失败，它会调用 `exfalso` 后重试。因此，如果存在形如 `P → ¬ Q` 的假设，新的证明状态将有两个目标：`P` 和 `Q`。 可以通过语法 `apply_rules ( config := { ... } ) lemmas` 传入进一步的配置。所支持的选项与 `solve_by_elim` 相同（并包括 `apply` 的所有选项）。

`exists e₁ , e₂ , ...` 是 `refine ⟨ e₁ , e₂ , ... ⟩ ; try trivial` 的简写。它适用于存在量词目标。

引入一个或多个假设，并可选择为其命名和／或对其进行模式匹配。对于每个要引入的假设，剩余主目标的目标类型必须是 `let` 类型或函数类型。 单独使用 `intro` 会引入一个匿名假设，例如可通过 `assumption` 访问它。它等价于 `intro _`。 `intro x y` 引入两个假设并为其命名。单个假设可以使用 `_` 匿名化、带上类型标注，或与模式匹配： `intro ( a , b ) -- ..., a : α, b : β ⊢ ...` 如果 `h` 是一个左侧或右侧为变量的等式，那么 `intro rfl` 是 `intro h ; subst h` 的简写。 此外，`intro` 可以与模式匹配结合使用，其方式与 `fun` 很相似： `intro | n + 1, 0 => tac | ...`

`intros` 反复应用 `intro`，引入零个或多个假设，直到目标不再是绑定表达式（即全称量词、函数类型、蕴涵或 `have`/`let`），并且不执行任何定义约简（不展开，也不进行 beta、eta 等约简）。引入的假设会获得不可访问的（卫生的）名称。`intros x y z` 等价于 `intro x y z`，仅因历史原因而存在；此时应优先使用 `intro` 策略。 性质与关系 即使没有引入任何假设，`intros` 也会成功。`repeat intro` 与 `intros` 类似，但它会执行定义约简以暴露绑定项，因此可能比 `intros` 引入更多假设。`intros` 等价于 `intro _ _ … _`，其中尾部 `_` 占位符的数量取使目标不再是绑定表达式所需的最小值。这些尾部引入不会执行任何定义约简。 示例 蕴涵： `example ( p q : Prop ) : p → q → p := by p : Prop q : Prop ⊢ p → q → p intros p : Prop q : Prop a✝¹ : p a✝ : q ⊢ p /- Tactic state a✝¹ : p a✝ : q ⊢ p -/ assumption All goals completed! 🐙` `let` 绑定： `example : let n := 1 ; let k := 2 ; n + k = 3 := by ⊢ let n := 1 ; let k := 2 ; n + k = 3 intros n✝ : Nat := 1 k✝ : Nat := 2 ⊢ n✝ + k✝ = 3 /- n✝ : Nat := 1 k✝ : Nat := 2 ⊢ n✝ + k✝ = 3 -/ rfl All goals completed! 🐙` 不会展开定义： `def AllEven ( f : Nat → Nat ) := ∀ n , f n % 2 = 0 declaration uses \` sorry \` example : ∀ ( f : Nat → Nat ) , AllEven f → AllEven ( fun k => f ( k + 1 ) ) := by ⊢ ∀ ( f : Nat → Nat ), AllEven f → AllEven fun k => f ( k + 1 ) intros f✝ : Nat → Nat a✝ : AllEven f✝ ⊢ AllEven fun k => f✝ ( k + 1 ) /- Tactic state f✝ : Nat → Nat a✝ : AllEven f✝ ⊢ AllEven fun k => f✝ (k + 1) -/ sorry All goals completed! 🐙`

`rintro` 策略把 `intros` 策略与 `rcases` 结合起来，从而允许在引入变量时使用解构模式。支持的模式请参阅 `rcases` 的说明。 例如，`rintro ( a | ⟨ b , c ⟩ ) ⟨ d , e ⟩` 会引入两个变量，随后对二者都进行情况拆分，产生两个子目标：其中一个具有变量 `a d e`，另一个具有变量 `b c d e`。 与 `rcases` 不同，`rintro` 还支持形如 `( x y : ty )` 的形式，可像绑定器一样一次引入多个变量并为其标注类型。

此策略适用于目标形如 `x ~ x` 的情况，其中 `~` 是等式、异构等式，或任何具有以属性 `@[refl]` 标记的自反性引理的关系。

`rfl'` 类似于 `rfl`，但会禁用智能展开，并展开所有种类的定义，包括定理（这与通过良基递归定义的声明有关）。

与 `rfl` 相同，但最后不会尝试 `eq_refl`。

refl 属性将引理标记为某个关系的自反性证明。 这些引理由 rfl、rfl' 和 apply_rfl 策略使用。

attr ::= ...
    | refl

`symm` 适用于目标形如 `t ~ u` 的目标，其中 `~` 是对称关系，即具有用属性 `[symm]` 标记的对称性引理的关系。它将目标替换为 `u ~ t`。 `symm at h` 会把假设 `h : t ~ u` 重写为 `h : u ~ t`。

对于每个假设 `h : a ~ b`，若有可用的 `@[ symm ]` 引理，则加入假设 `h_symm : b ~ a`。

symm 属性将引理标记为某个关系具有对称性的证明。 这些引理由 symm 和 symm_saturate 策略使用。

attr ::= ...
    | symm

对传递关系进行逐步推理。`calc a = b := pab b = c := pbc ... y = z := pyz` 根据给定的逐步证明得到 `a = z`。`=` 可以替换为实现类型类 `Trans` 的任意关系。 无需重复右侧，后续的左侧可以替换为 `_`： `calc a = b := pab _ = c := pbc ... _ = z := pyz` 也可以把第一个关系写为 `< lhs > \ n _ = < rhs > := < proof >`。这有助于对齐关系符号，尤其是在标识符较长时： `calc abc _ = bce := pabce _ = cef := pbcef ... _ = xyz := pwxyz` `calc` 可作为项、策略或 `conv` 策略使用。更多信息请参阅《Theorem Proving in Lean 4》。

关系复合的类型类。它接收两个“输入”关系 r 与 s，并产生一个“输出”关系 t； 若 r a b 与 s b c 成立，就可得到 t a c。calc 策略用它连接关系不同的相邻步骤。

Trans.mk.{u, v, w, u_1, u_2, u_3}

trans : {a : α} → {b : β} → {c : γ} → r a b → s b c → t a c

`ac_nf` 在模结合且交换的运算符应用意义下规范化等式。 `ac_nf` 规范化所有假设以及目标。 `ac_nf at l` 在位置 `l` 处进行规范化，其中 `l` 是 `*` 或局部上下文中的假设列表。在后一种情况下，还可以使用证明分隔符 `⊢` 或 `|-` 表示目标。 instance : Std.Associative ( α := Nat ) ( . + . ) := ⟨ Nat.add_assoc ⟩ instance : Std.Commutative ( α := Nat ) ( . + . ) := ⟨ Nat.add_comm ⟩ example ( a b c d : Nat ) : a + b + c + d = d + ( b + c ) + a := by a : Nat b : Nat c : Nat d : Nat ⊢ a + b + c + d = d + ( b + c ) + a ac_nf All goals completed! 🐙 -- goal: a + (b + (c + d)) = a + (b + (c + d))

`ac_nf` 的实现（完整的 `ac_nf` 随后还会调用 `trivial`）。

如果主目标的目标类型与 `e` 的类型匹配，`exact e` 会关闭主目标。

`apply e` 尝试将当前目标与 `e` 的类型的结论相匹配。如果成功，该策略返回的子目标数等于未由类型推断或类型类解析确定的前提数。非依赖前提会添加在依赖前提之前。 `apply` 策略使用高阶模式匹配、类型类解析以及带依赖类型的一阶合一。

`refine e` 的行为类似 `exact e`，不同之处在于：`e` 中未通过与主目标的目标类型合一而得到解决的具名空洞（`? x`）或匿名空洞（`? _`）会转换为新目标；如果空洞有名称，则用该名称作为目标分支名称。

`refine' e` 的行为与 `refine e` 类似，区别是未解决的占位符（`_`）和隐式参数也会转换为新目标。

`solve_by_elim` 在主目标上调用 `apply`，以寻找头部匹配的假设；随后在生成的子目标上反复调用 `apply`，直到不再剩余子目标，最多执行 `maxDepth`（默认为 `6`）个递归步骤。`solve_by_elim` 会解决当前目标，否则失败。如果子目标无法解决，`solve_by_elim` 会进行回溯。 默认传给 `apply` 的假设为局部上下文、`rfl`、`trivial`、`congrFun` 和 `congrArg`。可以使用与 `simp` 类似的语法修改这些假设： `solve_by_elim [ h₁ , h₂ , ... , hᵣ ]` 还会应用给定表达式。 `solve_by_elim only [ h₁ , h₂ , ... , hᵣ ]` 不会包含局部上下文、`rfl`、`trivial`、`congrFun` 或 `congrArg`，除非显式列出它们。 `solve_by_elim [ - h₁ , ... - hₙ ]` 移除给定的局部假设。 `solve_by_elim using [ a₁ , ... ]` 使用所有以属性 `aᵢ` 标记的引理（这些属性必须使用 `register_label_attr` 创建）。 `solve_by_elim *` 尝试一起解决所有目标；如果一个目标的解使其他目标不可能解决，则进行回溯。（以多个目标开始时，添加或移除局部假设的行为可能不稳定。） 可通过配置参数 `solve_by_elim ( config := { ... } )` 传入的可选参数： `maxDepth`：尝试解决所生成子目标的次数。 `symm`：添加所有由 `symm` 导出的假设（默认为 `true`）。 `exfalso`：如果 `solve_by_elim` 失败，允许调用 `exfalso` 后重试（默认为 `true`）。 `transparency`：更改调用 `apply` 时的透明度模式。默认为 `.default`，但改为 `.reducible` 往往很有用，这样在尝试应用引理时就不会展开半可归约定义。 另请参阅 `Lean.Meta.Tactic.Backtrack.BacktrackConfig` 的文档注释，其中介绍了 `proc`、`suspend` 和 `discharge` 选项，可进一步定制 `solve_by_elim`。`apply_assumption` 和 `apply_rules` 都通过这些钩子实现。

`apply_rules [ l₁ , l₂ , ... ]` 尝试通过反复应用引理列表 `[ l₁ , l₂ , ... ]` 或应用局部假设来解决主目标。如果 `apply` 生成新目标，`apply_rules` 会反复尝试解决这些目标。 可以使用 `apply_rules [ - h ]` 排除局部假设。`apply_rules` 还会使用 `rfl`、`trivial`、`congrFun` 和 `congrArg`。使用 `apply_rules only [ ... ]` 可以禁用这些内容以及局部假设。 可以使用 `apply_rules using [ a₁ , ... ]` 来使用所有以属性 `aᵢ` 标记的引理（这些属性必须使用 `register_label_attr` 创建）。 可以通过语法 `apply_rules ( config := { ... } )` 传入进一步的配置。所支持的选项与 `solve_by_elim` 相同（并包括 `apply` 的所有选项）。 `apply_rules` 会按需尝试对假设调用 `symm`，并对目标调用 `exfalso`。可以使用 `apply_rules ( config := { symm := false , exfalso := false } )` 禁用这些行为。 可以使用语法 `apply_rules ( config := { maxDepth := n } )` 限制迭代深度。与 `solve_by_elim` 不同，`apply_rules` 不会回溯，而是贪心地应用列表中的引理，直到无法继续。

`as_aux_lemma => tac` 与 `tac` 执行相同操作，但会将所得表达式包装进一个辅助引理。 在某些情况下，由于证明项不会重复，这会显著减小表达式的大小。

`exfalso` 通过应用 `False.elim`，把目标 `⊢ tgt` 转换为 `⊢ False`。

如果主目标的假设“显然矛盾”，`contradiction` 就会关闭主目标。 没有适用构造器的归纳类型/族： `example ( h : False ) : p := by p : Sort ?u.3 h : False ⊢ p contradiction All goals completed! 🐙` 构造器的单射性： `example ( h : none = some true ) : p := by p : Sort ?u.6 h : none = some true ⊢ p contradiction All goals completed! 🐙` 可判定的假命题： `example ( h : 2 + 2 = 3 ) : p := by p : Sort ?u.13 h : 2 + 2 = 3 ⊢ p contradiction All goals completed! 🐙` 相互矛盾的假设： `example ( h : p ) ( h' : ¬ p ) : q := by p : Prop q : Sort ?u.5 h : p h' : ¬ p ⊢ q contradiction All goals completed! 🐙` 其他简单矛盾，例如： `example ( x : Nat ) ( h : x ≠ x ) : p := by p : Sort ?u.5 x : Nat h : x ≠ x ⊢ p contradiction All goals completed! 🐙`

把目标改为 `False`，同时尽可能多地保留信息： * 如果目标是 `False`，则不执行任何操作。 * 如果目标是蕴涵或函数类型，则引入参数并重新开始。（特别地，如果目标是 `x ≠ y`，则引入 `x = y`。） * 否则，对于命题目标 `P`，把它替换为 `¬ ¬ P`（尝试寻找 `Decidable` 实例；若找不到，则退回经典逻辑方式），并引入 `¬ P`。 * 对于非命题目标，使用 `False.elim`。

给定主目标 `ctx ⊢ t`，`suffices h : t' from e` 把主目标替换为 `ctx ⊢ t'`；在上下文 `ctx , h : t'` 中，`e` 必须具有类型 `t`。变体 `suffices h : t' by tac` 是 `suffices h : t' from by tac` 的简写。如果省略 `h :`，则使用名称 `this`。

`change tgt'` 会把目标从 `tgt` 改为 `tgt'`，前提是二者定义相等。 `change t' at h` 会把假设 `h : t` 的类型改为 `t'`，前提是 `t` 与 `t'` 定义相等。 `change a with b` 会把目标中出现的 `a` 改为 `b`，前提是 `a` 与 `b` 定义相等。 `change a with b at h` 类似地把假设 `h` 的类型中出现的 `a` 改为 `b`。

`generalize ( [ h : ] e = x ) ,+` 把主目标中出现的所有 `e` 替换为新的假设 `x`。如果给出了 `h`，还会引入 `h : e = x`。 `generalize e = x at h₁ ... hₙ` 还会概括 `h₁ , ..., hₙ` 内出现的 `e`。 `generalize e = x at *` 会概括所有位置出现的 `e`。

`specialize h a₁ ... aₙ` 等价于 `replace h := h a₁ ... aₙ`。它使用具体项 `a₁ ... aₙ` 实例化全称量词和蕴含，从而特化局部假设 `h`。该策略加入一个同名的新假设，并尽可能尝试移除原来的 `h`。 示例：给定 `h : ∀ ( n : Nat ) , p n → q n` 和 `h' : p 2`，`specialize h 2 h'` 会把 `h` 替换为 `h : q 2`。 该策略还支持使用具名实参语法实例化特定的全称量词。示例：给定 `h : ∀ ( m n : Nat ) , p m n`，`specialize h ( n := 2 )` 会把 `h` 替换为 `h : ∀ ( m : Nat ) , p m 2`。

`obtain` 策略是 `have` 与 `rcases` 的组合。关于支持的模式，请参阅 `rcases`。 `obtain ⟨patt⟩ : type := proof` 等价于： `have h : type := proof rcases h with ⟨patt⟩` 如果省略 `⟨ patt ⟩`，`rcases` 会尝试推断模式。如果省略 `type`，则必须提供 `:= proof`。

`show t` 查找目标能与 `t` 合一的第一个目标。它将该目标设为主目标，执行合一，并把目标替换为合一后的 `t` 版本。

`show_term tac` 运行 `tac`；如果仍有子目标，则以 `"exact X Y Z"` 或 `"refine X ?_ Z"` 的形式打印生成的项（必要时以 `expose_names` 为前缀）。（对于某些策略，打印出的项不便于人类阅读。）

`norm_cast` 策略族用于规范化表达式中的某些强制转换（cast）。`norm_cast` 规范化目标中的强制转换。`norm_cast at h` 规范化假设 `h` 中的强制转换。 该策略基本上是一个配有特定引理集的 `simp` 版本，用于在表达式中将强制转换向上移动。因此，即使在不鼓励非终结 `simp` 调用（因为它们较脆弱）的情形中，`norm_cast` 仍被认为是安全的。它还会特别处理数值。 例如，给定假设 `a b : ℤ h : ↑a + ↑b < (10 : ℚ)`，写下 `norm_cast at h` 会将 `h` 变为 `h : a + b < 10`。 此外，一些基本策略还有在操作过程中使用 `norm_cast` 规范化表达式的变体，从而能更灵活地接受表达式（我们称其为模 `norm_cast` 效果的策略）： - `exact` 对应 `exact_mod_cast`，`apply` 对应 `apply_mod_cast`。写下 `exact_mod_cast h` 和 `apply_mod_cast h` 会先规范化目标和 `h` 中的强制转换，再使用 `exact h` 或 `apply h`。 - `rw` 对应 `rw_mod_cast`。它在重写步骤之间应用 `norm_cast`。 - `assumption` 对应 `assumption_mod_cast`。它实际上相当于 `norm_cast at * ; assumption`，但效率更高。它会规范化目标中的强制转换，并针对上下文中的每个假设 `h`，尝试规范化 `h` 中的强制转换并使用 `exact h`。 另请参阅 `push_cast`；它将强制转换向内移动，而不是将其向外提升。

`push_cast` 重写目标，把某些强制转换（cast）向内移动到叶节点。它以前向方式使用 `norm_cast` 引理。例如，`↑ ( a + b )` 会被写为 `↑ a + ↑ b`。 `push_cast` 在目标中向内移动强制转换。`push_cast at h` 在假设 `h` 中向内移动强制转换。也可以附加额外的 `simp` 引理，例如 `push_cast [ Int.add_zero ]`。 示例： example ( a b : Nat ) ( h1 : ( ( a + b : Nat ) : Int ) = 10 ) ( h2 : ( ( a + b + 0 : Nat ) : Int ) = 10 ) : ( ( a + b : Nat ) : Int ) = 10 := by a : Nat b : Nat h1 : ↑ ( a + b ) = 10 h2 : ↑ ( a + b + 0 ) = 10 ⊢ ↑ ( a + b ) = 10 /- h1 : ↑(a + b) = 10 h2 : ↑(a + b + 0) = 10 ⊢ ↑(a + b) = 10 -/ push_cast a : Nat b : Nat h1 : ↑ ( a + b ) = 10 h2 : ↑ ( a + b + 0 ) = 10 ⊢ ↑ a + ↑ b = 10 /- 此时 ⊢ ↑a + ↑b = 10 -/ push_cast at h1 a : Nat b : Nat h1 : ↑ a + ↑ b = 10 h2 : ↑ ( a + b + 0 ) = 10 ⊢ ↑ a + ↑ b = 10 push_cast [ Int.add_zero ] at h2 a : Nat b : Nat h1 : ↑ a + ↑ b = 10 h2 : ↑ a + ↑ b = 10 ⊢ ↑ a + ↑ b = 10 /- 此时 h1 h2 : ↑a + ↑b = 10 -/ exact h1 All goals completed! 🐙 另请参阅 `norm_cast`。

规范化目标和给定表达式中的强制转换，然后使用 `exact` 关闭目标。

规范化目标和给定表达式中的类型转换，然后把该表达式应用于目标。

使用给定规则进行重写，并在每一步之前规范化强制转换。

`assumption_mod_cast` 是 `assumption` 的一个变体，它使用假设求解目标。与 `assumption` 不同，它会先预处理目标和每个假设，把类型转换尽可能向外移动，因此适用范围更广。 具体而言，它对目标运行 `norm_cast`。对于每个局部假设 `h`，它也使用 `norm_cast` 规范化 `h`，并尝试用所得结果关闭目标。

从目标式或局部假设内部提取 `let` 和 `have` 表达式，并引入新的局部定义。`extract_lets` 从目标式提取所有 `let`。`extract_lets x y z` 从目标式提取所有 `let`，并把 `x`、`y`、`z` 用作最先的名称。用 `_` 作为名称会使其保持匿名。 `extract_lets x y z at h` 对局部假设 `h` 而不是目标式执行操作。例如，给定形如 `h : let x := v ; b x` 的局部假设，`extract_lets z at h` 会引入新的局部定义 `z := v`，并把 `h` 改为 `h : b z`。

尽可能把项内部的 `let` 和 `have` 表达式向外提升。它类似于 `extract_lets + lift`，但过程结束时最外层的 `let` 不会提取为局部假设。 `lift_lets` 提升目标中的 `let` 表达式。`lift_lets at h` 提升给定局部假设中的 `let` 表达式。 例如： `example : (let x := 1; x) = 1 := by lift_lets -- ⊢ let x := 1; x = 1 ...`

在可能时把 `let` 表达式转换为 `have` 表达式。 `let_to_have` 转换目标中的 `let`。 `let_to_have at h` 转换给定局部假设中的 `let`。

`clear_value x ...` 清除给定局部定义的值。局部定义 `x : α := v` 会变为假设 `x : α`。 `clear_value ( h : x = _ )` 在清除 `x` 的值之前添加假设 `h : x = v`。这是 `have h : x = v := rfl ; clear_value x` 的简写。任何在定义上等于 `v` 的值都可以代替 `_`。 `clear_value *` 清除所有可清除假设的值。如果一个都无法清除，则失败。 这些语法可以组合使用。例如，`clear_value x y *` 确保清除 `x` 和 `y`，同时尝试清除所有其他局部定义；`clear_value ( hx : x = _ ) y * with hx` 具有相同效果，但会先添加假设 `hx : x = v`。

应用以 `@[ ext ]` 属性注册的外延性引理。 `ext pat *` 会尽可能多地应用外延性定理，并使用模式 `pat *` 通过 `rintro` 引入外延性定理中的变量。例如，这些模式用于命名由 `funext` 等引理引入的变量。 若不提供模式，`ext` 会尽可能多地应用外延性引理，但在需要时引入匿名假设。 `ext pat * : n` 只在深度不超过 `n` 的范围内应用 `ext` 定理。 `ext1 pat *` 策略与 `ext pat *` 类似，区别是它只应用一个外延性定理。 未使用的模式会产生警告。不能与变量匹配的模式通常会导致引入匿名假设。

`ext1 pat *` 类似于 `ext pat *`，区别是它只应用一个外延性定理，而不会递归应用尽可能多的外延性定理。`pat *` 模式使用 `rintro` 策略处理。如果未提供模式，则使用 `intros` 策略匿名引入变量。

向当前目标应用一个外延性定理。

应用函数外延性并引入新假设。策略 `funext` 会持续应用 `funext` 引理，直到目标式不能再约简为 `|- ((fun x => ...) = (fun x => ...))`。 变体 `funext h₁ ... hₙ` 应用 `funext` 共 `n` 次，并用给定标识符命名新假设。可以像在 `intro` 策略中一样使用模式。例如，给定目标 `|- ((fun x : Nat × Bool => ...) = (fun x => ...))`，`funext ( a , b )` 会应用一次 `funext`，并对新引入的序对执行模式匹配。

`grind` 是一种受现代 SMT 求解器启发的策略。可以想象有一块虚拟白板：每当 `grind` 发现新的等式、不等式或逻辑事实时，它就把该事实写到白板上，把已知相等的项归为一组，并让各个推理引擎读取共享工作区中的内容并向其中贡献信息。这些引擎协同工作，处理等式推理、应用已知定理、传播新事实、执行情况分析，并针对线性算术和交换环等领域运行专用求解器。更多信息请参阅参考手册中关于 `grind` 的章节。 `grind` 并非为搜索空间发生组合爆炸的目标而设计，例如大型鸽巢原理实例、图着色归约、高阶 N 皇后棋盘，或编码为布尔约束的 200 变量数独。这类编码需要成千上万（乃至数百万）次情况拆分，会压垮 `grind` 的分支搜索。对于位级或组合问题，请考虑使用 `bv_decide`。`bv_decide` 会调用先进的 SAT 求解器（CaDiCaL），随后返回紧凑且可由机器检查的证书。 等式推理 `grind` 使用同余闭包跟踪项之间的等式。当已知两个项相等时，同余闭包会自动推出由它们构成的更复杂表达式之间的等式。例如，若 `a = b`，则对于任意函数 `f`，同余闭包也会得出 `f a = f b`。这构成了 `grind` 中高效等式推理的基础。示例如下： example ( f : Nat → Nat ) ( h : a = b ) : f ( f b ) = f ( f a ) := by a : Nat b : Nat f : Nat → Nat h : a = b ⊢ f ( f b ) = f ( f a ) grind All goals completed! 🐙 使用 E-matching 应用定理 为了应用现有定理，`grind` 使用一种称为 E-matching 的技术；它在考虑等式的同时，为已知定理的模式寻找匹配。E-matching 与同余闭包相结合，可帮助 `grind` 自动发现定理和等式中并不显然的推论。考虑以下函数和定理： def f ( a : Nat ) : Nat := a + 1 def g ( a : Nat ) : Nat := a - 1 @[ grind = ] theorem gf ( x : Nat ) : g ( f x ) = x := by x : Nat ⊢ g ( f x ) = x simp [ f , g ] All goals completed! 🐙 定理 `gf` 断言，对所有自然数 `x`，都有 `g ( f x ) = x`。属性 `[ grind = ]` 指示 `grind` 使用等式左侧 `g ( f x )` 作为 E-matching 的模式。假设现在有如下目标： example {a b} (h : f b = a) : g a = b := by grind 尽管 `g a` 不是模式 `g ( f x )` 的实例，但模等式 `f b = a` 后它就是。将 `g a` 中的 `a` 替换为 `f b`，便得到项 `g ( f b )`；在赋值 `x := b` 下，它与模式 `g ( f x )` 匹配。因此，定理 `gf` 以 `x := b` 实例化，并断言新等式 `g ( f b ) = b`。随后，`grind` 使用同余闭包推出隐含的等式 `g a = g ( f b )` 并完成证明。 用于实例化定理的模式会影响 `grind` 的效果。例如，在下例中，模式 `g ( f x )` 过于严格：由于目标甚至不含函数符号 `g`，定理 `gf` 不会被实例化。 example (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind 可以使用命令 `grind_pattern` 为给定定理手动选择模式。在下例中，我们指示 `grind` 使用 `f x` 作为模式，使其能够自动解决目标： grind_pattern gf => f x example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by grind 可以启用选项 `trace.grind.ematch.instance`，让 `grind` 为其生成的每个定理实例打印跟踪消息。还可以指定多模式，以控制 `grind` 应在何时应用定理。多模式要求所有指定模式都已在当前上下文中匹配，之后才应用定理。对于传递性规则之类的定理，这很有用，因为应用规则前必须同时存在多个前提。下例使用二元关系 `R` 的传递性公理演示此功能： opaque R : Int → Int → Prop axiom Rtrans { x y z : Int } : R x y → R y z → R x z grind_pattern Rtrans => R x y , R y z example { a b c d } : R a b → R b c → R c d → R a d := by a : Int b : Int c : Int d : Int ⊢ R a b → R b c → R c d → R a d grind All goals completed! 🐙 通过指定多模式 `R x y , R y z`，我们指示 `grind` 仅在上下文中同时有 `R x y` 和 `R y z` 时实例化 `Rtrans`。在此例中，`grind` 应用 `Rtrans`，从 `R a b` 和 `R b c` 推出 `R a c`，随后可重复同一推理，从 `R a c` 和 `R c d` 推出 `R a d`。 除了使用 `grind_pattern` 显式指定模式之外，还可以使用属性 `@[ grind ]` 或它的某个变体；这些属性会使用启发式方法生成（多）模式。完整列表见参考手册。主要变体如下： * `@[ grind → ]` 从定理的假设中选择多模式（即使用该定理进行前向推理）。更具体地说，它会从左到右遍历定理的假设；每当遇到一个最小的、可索引的（即以常量为首部的）子表达式，且该表达式“覆盖”（即确定其值）了此前尚未覆盖的实参时，就将该子表达式加入模式，直到所有实参都被覆盖。 * `@[ grind ← ]` 从定理的结论中选择多模式（即使用该定理进行后向推理）。若定理的实参并非全都出现在结论中，此操作可能失败。 * `@[ grind ]` 先遍历结论，再从左到右遍历假设，并在模式能提高覆盖率时将其加入；当所有实参都被覆盖时停止。 * `@[ grind = ]` 检查定理的结论是否为等式，随后使用等式左侧作为模式。若实参并非全都出现在左侧，此操作可能失败。 下面再次给出先前的例子，但改用属性 `[ grind → ]`： opaque R : Int → Int → Prop @[ grind → ] axiom Rtrans { x y z : Int } : R x y → R y z → R x z example { a b c d } : R a b → R b c → R c d → R a d := by a : Int b : Int c : Int d : Int ⊢ R a b → R b c → R c d → R a d grind All goals completed! 🐙 为了控制定理实例化并避免生成无界数量的实例，`grind` 使用代计数器。原始目标中的项被赋予第 0 代。当 `grind` 使用代满足 `generation ≤ n` 的项应用定理时，它创建的所有新项都被赋予第 `n + 1` 代。这会限制策略在应用定理时探索的深度，并有助于防止实例化数量过多。 关键选项： * `grind ( ematch := < num > )` 控制 E-matching 的轮数。 * `grind [ < name > , ... ]` 指示 `grind` 在 E-matching 期间使用声明 `name`。 * `grind only [ < name > , ... ]` 与 `grind [ < name > , ... ]` 类似，但不使用带有 `@[ grind ]` 标记的定理。 * `grind ( gen := < num > )` 设置最大代。 线性整数算术（`lia`） `grind` 可以使用名为 `lia` 的集成判定过程，解决可归约为线性整数算术（LIA）的目标。它理解： * 等式 `p = 0` * 不等式 `p ≤ 0` * 不等关系 `p ≠ 0` * 整除关系 `d ∣ p` 求解器以增量方式为变量赋整数值；当某个部分赋值违反约束时，它会加入一个新的隐含约束并重试。此基于模型的搜索对于 LIA 是完备的。 关键选项： * `grind - lia` 禁用求解器（调试时有用）。 * `grind + qlia` 接受有理数模型（可缩小搜索空间，但对于 `ℤ` 不完备）。 * `grind ( liaSteps := n )` 限制模型搜索所执行的步数（达到阈值后，求解器将变得不完备）。 示例： example { x y : Int } : 2 * x + 4 * y ≠ 5 := by x : Int y : Int ⊢ 2 * x + 4 * y ≠ 5 grind All goals completed! 🐙 -- 混合使用等式与不等式。 example { x y : Int } : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by x : Int y : Int ⊢ 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 grind All goals completed! 🐙 -- 使用整除关系推理。 example ( a b : Int ) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by a : Int b : Int ⊢ 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a grind All goals completed! 🐙 example ( x y : Int ) : 27 ≤ 11 * x + 13 * y → 11 * x + 13 * y ≤ 45 → - 10 ≤ 7 * x - 9 * y → 7 * x - 9 * y ≤ 4 → False := by x : Int y : Int ⊢ 27 ≤ 11 * x + 13 * y → 11 * x + 13 * y ≤ 45 → - 10 ≤ 7 * x - 9 * y → 7 * x - 9 * y ≤ 4 → False grind All goals completed! 🐙 -- 实现 `ToInt` 类型类的类型。 example ( a b c : UInt64 ) : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by a : UInt64 b : UInt64 c : UInt64 ⊢ a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 grind All goals completed! 🐙 代数求解器（`ring`） `grind` 自带一个昵称为 `ring` 的代数求解器，用于可表述为交换环、半环或域上的多项式方程（或不等方程）的目标。 开箱即用 所有核心数值类型以及相关的 Mathlib 类型都已提供所需的类型类实例，因此该求解器在大多数开发中可直接使用。 它可以判定： * 形如 `p = q` 的等式 * 形如 `p ≠ q` 的不等关系 * 域中关于逆元的基本推理（`a / b := a * b ⁻¹`） * 将环事实与其他 `grind` 引擎混合使用的目标 关键选项： * `grind - ring` 关闭求解器（调试时有用）。 * `grind ( ringSteps := n )` 限制此过程执行的步数。 示例： open Lean Grind example [ CommRing α ] ( x : α ) : ( x + 1 ) * ( x - 1 ) = x ^ 2 - 1 := by α : Type u_1 inst✝ : CommRing α x : α ⊢ ( x + 1 ) * ( x - 1 ) = x ^ 2 - 1 grind All goals completed! 🐙 -- 特征为 256 意味着 16 * 16 = 0。 example [ CommRing α ] [ IsCharP α 256 ] ( x : α ) : ( x + 16 ) * ( x - 16 ) = x ^ 2 := by α : Type u_1 inst✝¹ : CommRing α inst✝ : IsCharP α 256 x : α ⊢ ( x + 16 ) * ( x - 16 ) = x ^ 2 grind All goals completed! 🐙 -- 也适用于 `UInt8` 等内置环。 example ( x : UInt8 ) : ( x + 16 ) * ( x - 16 ) = x ^ 2 := by x : UInt8 ⊢ ( x + 16 ) * ( x - 16 ) = x ^ 2 grind All goals completed! 🐙 example [ CommRing α ] ( a b c : α ) : a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 = 9 - c ^ 4 := by α : Type u_1 inst✝ : CommRing α a : α b : α c : α ⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 = 9 - c ^ 4 grind All goals completed! 🐙 example [ Field α ] [ NoNatZeroDivisors α ] ( a : α ) : 1 / a + 1 / ( 2 * a ) = 3 / ( 2 * a ) := by α : Type u_1 inst✝¹ : Field α inst✝ : NoNatZeroDivisors α a : α ⊢ 1 / a + 1 / ( 2 * a ) = 3 / ( 2 * a ) grind All goals completed! 🐙 其他选项 * `grind ( splits := < num > )` 限制搜索树的深度。一旦某个分支执行了 `num` 次拆分，`grind` 就停止在该分支中继续拆分。 * `grind - splitIte` 禁止对 if-then-else 表达式进行情况拆分。 * `grind - splitMatch` 禁止对 `match` 表达式进行情况拆分。 * `grind + splitImp` 指示 `grind` 对前件 `A` 为命题的任意假设 `A → B` 进行拆分。 * `grind - linarith` 禁用用于（有序）模和环的线性算术求解器。 更多示例 example { a b } { as bs : List α } : ( as ++ bs ++ [ b ] ) . getLastD a = b := by α : Type u_1 a : α b : α as : List α bs : List α ⊢ ( as ++ bs ++ [ b ] ) . getLastD a = b grind All goals completed! 🐙 example ( x : BitVec ( w + 1 ) ) : ( BitVec.cons x . msb ( x . setWidth w ) ) = x := by w : Nat x : BitVec ( w + 1 ) ⊢ BitVec.cons x . msb ( BitVec.setWidth w x ) = x grind All goals completed! 🐙 example ( as : Array α ) ( lo hi i j : Nat ) : lo ≤ i → i < j → j ≤ hi → j < as . size → min lo ( as . size - 1 ) ≤ i := by α : Type u_1 as : Array α lo : Nat hi : Nat i : Nat j : Nat ⊢ lo ≤ i → i < j → j ≤ hi → j < as . size → min lo ( as . size - 1 ) ≤ i grind All goals completed! 🐙

`grind?` 接受与 `grind` 相同的参数，但会报告一个足以关闭目标的等价 `grind only` 调用。这有助于缩减局部调用中 `grind` 定理集的大小。

`lia` 求解线性整数算术目标。它是 `grind` 策略的一个薄包装器，只启用 `lia` 求解器。如果需要更多功能，请改用 `grind`。

`grobner` 使用 Gröbner 基算法解决可表述为交换（半）环上的多项式等式（并可具有更多多项式等式作为假设）的目标。 它实现为 `grind` 策略的一层薄包装，仅启用 `grobner` 求解器。如果需要其他能力，请改用 `grind`。

`simp` 策略使用引理和假设来化简主目标的目标式或非依赖假设。它有许多变体： * `simp` 使用带有属性 `[ simp ]` 的引理化简主目标的目标式。 * `simp [ h₁ , h₂ , ... , hₙ ]` 使用带有属性 `[ simp ]` 的引理以及给定的各个表达式 `hᵢ` 化简主目标的目标式。如果某个 `hᵢ` 是已定义常量 `f`，则展开 `f`。如果 `f` 有相关的等式引理（且不是投影或可约定义），则使用这些引理对 `f` 进行重写。 * `simp [ * ]` 使用带有属性 `[ simp ]` 的引理和所有假设化简主目标的目标式。 * `simp only [ h₁ , h₂ , ... , hₙ ]` 类似于 `simp [ h₁ , h₂ , ... , hₙ ]`，但不使用 `[ simp ]` 引理。 * `simp [ - id₁ , ... , - idₙ ]` 使用带有属性 `[ simp ]` 的引理化简主目标的目标式，但移除名为 `idᵢ` 的引理。 * `simp at h₁ h₂ ... hₙ` 化简假设 `h₁ : T₁ ... hₙ : Tₙ`。如果目标式或另一个假设依赖于 `hᵢ`，则会引入一个新的已化简假设 `hᵢ`，但旧假设仍保留在局部上下文中。 * `simp at *` 化简所有假设和目标式。 * `simp [ * ] at *` 使用其他假设化简目标式和所有（命题性）假设。

`simp!` 是启用 `autoUnfold := true` 的 `simp` 的简写。当模式匹配定义的函数应用符合某个模式时，它会展开该应用。这可以用来对许多定义进行部分求值。

`simp?` 接受与 `simp` 相同的实参，但会报告一个等价的、足以关闭目标的 `simp only` 调用。这有助于缩小局部调用中的 `simp` 集，从而加快处理速度。 example ( x : Nat ) : ( if True then x + 2 else 3 ) = x + 2 := by x : Nat ⊢ ( if True then x + 2 else 3 ) = x + 2 Try this: [apply] simp only [↓reduceIte, Nat.add_left_cancel_iff] simp? All goals completed! 🐙 -- prints "Try this: simp only [ite_true]" 此命令也可用于 `simp_all` 和 `dsimp`。

`simp?` 接受与 `simp` 相同的实参，但会报告一个等价的、足以关闭目标的 `simp only` 调用。这有助于缩小局部调用中的 `simp` 集，从而加快处理速度。 example ( x : Nat ) : ( if True then x + 2 else 3 ) = x + 2 := by x : Nat ⊢ ( if True then x + 2 else 3 ) = x + 2 Try this: [apply] simp only [↓reduceIte, Nat.add_left_cancel_iff] simp? All goals completed! 🐙 -- prints "Try this: simp only [ite_true]" 此命令也可用于 `simp_all` 和 `dsimp`。

`simp_arith` 已弃用。它曾是 `simp + arith + decide` 的简写。请注意，自从 Lean 加入化简过程后，归约算术项不再需要 `+ decide`。

`simp_arith!` 已被弃用。它曾是 `simp! + arith + decide` 的简写。 请注意，由于 Lean 中已经添加了化简过程，归约算术项不再需要 `+ decide`。

`dsimp` 策略是定义化简器。它与 `simp` 类似，但只应用通过自反性成立的定理。因此，结果保证与输入定义相等。

`dsimp!` 是 `dsimp with autoUnfold := true` 的简写。当模式匹配定义的某个模式适用时，这会展开此类函数的应用。可用它对许多定义进行部分求值。

`simp?` 接受与 `simp` 相同的实参，但会报告一个等价的、足以关闭目标的 `simp only` 调用。这有助于缩小局部调用中的 `simp` 集，从而加快处理速度。 example ( x : Nat ) : ( if True then x + 2 else 3 ) = x + 2 := by x : Nat ⊢ ( if True then x + 2 else 3 ) = x + 2 Try this: [apply] simp only [↓reduceIte, Nat.add_left_cancel_iff] simp? All goals completed! 🐙 -- prints "Try this: simp only [ite_true]" 此命令也可用于 `simp_all` 和 `dsimp`。

`simp?` 接受与 `simp` 相同的实参，但会报告一个等价的、足以关闭目标的 `simp only` 调用。这有助于缩小局部调用中的 `simp` 集，从而加快处理速度。 example ( x : Nat ) : ( if True then x + 2 else 3 ) = x + 2 := by x : Nat ⊢ ( if True then x + 2 else 3 ) = x + 2 Try this: [apply] simp only [↓reduceIte, Nat.add_left_cancel_iff] simp? All goals completed! 🐙 -- prints "Try this: simp only [ite_true]" 此命令也可用于 `simp_all` 和 `dsimp`。

`simp_all` 是 `simp [ * ] at *` 的更强版本；它会多次化简假设和目标，直到再无可应用的化简。只考虑非依赖命题假设。

`simp_all!` 是 `simp_all with autoUnfold := true` 的简写。当模式匹配定义的某个模式适用时，这会展开此类函数的应用。可用它对许多定义进行部分求值。

`simp?` 接受与 `simp` 相同的实参，但会报告一个等价的、足以关闭目标的 `simp only` 调用。这有助于缩小局部调用中的 `simp` 集，从而加快处理速度。 example ( x : Nat ) : ( if True then x + 2 else 3 ) = x + 2 := by x : Nat ⊢ ( if True then x + 2 else 3 ) = x + 2 Try this: [apply] simp only [↓reduceIte, Nat.add_left_cancel_iff] simp? All goals completed! 🐙 -- prints "Try this: simp only [ite_true]" 此命令也可用于 `simp_all` 和 `dsimp`。

`simp?` 接受与 `simp` 相同的实参，但会报告一个等价的、足以关闭目标的 `simp only` 调用。这有助于缩小局部调用中的 `simp` 集，从而加快处理速度。 example ( x : Nat ) : ( if True then x + 2 else 3 ) = x + 2 := by x : Nat ⊢ ( if True then x + 2 else 3 ) = x + 2 Try this: [apply] simp only [↓reduceIte, Nat.add_left_cancel_iff] simp? All goals completed! 🐙 -- prints "Try this: simp only [ite_true]" 此命令也可用于 `simp_all` 和 `dsimp`。

`simp_all_arith` 已被弃用。它曾是 `simp_all + arith + decide` 的简写。 请注意，由于 Lean 中已经添加了化简过程，归约算术项不再需要 `+ decide`。

`simp_all_arith!` 已弃用。它曾是 `simp_all! + arith + decide` 的简写。请注意，自从 Lean 加入化简过程后，约简算术项不再需要 `+ decide`。

这是 `simp` 的一种“收尾”策略变体。它有两种形式。 `simpa [ rules , ⋯ ] using e` 使用 `rules` 化简目标和 `e` 的类型，然后尝试用 `e` 关闭目标。化简 `e` 的类型使它更有可能与同样已化简的目标匹配。这种写法面对 simp 引理集的变化时通常也更稳健。已化简的 `e` 与已化简目标之间的最终匹配使用可约透明度，因此不会展开半可约定义。若要在环境的（默认/半可约）透明度下执行匹配，请写 `simpa [ rules , ⋯ ] using! e`。 `simpa [ rules , ⋯ ]` 会化简目标；如果上下文中存在名为 `this` 的假设，还会化简其类型，然后尝试使用 `assumption` 策略关闭目标。与 `simp` 一样，`simpa` 后的 `!` 修饰符会启用 simp 集中定义的自动展开。

这是 `simp` 的一种“收尾”策略变体。它有两种形式。 `simpa [ rules , ⋯ ] using e` 使用 `rules` 化简目标和 `e` 的类型，然后尝试用 `e` 关闭目标。化简 `e` 的类型使它更有可能与同样已化简的目标匹配。这种写法面对 simp 引理集的变化时通常也更稳健。已化简的 `e` 与已化简目标之间的最终匹配使用可约透明度，因此不会展开半可约定义。若要在环境的（默认/半可约）透明度下执行匹配，请写 `simpa [ rules , ⋯ ] using! e`。 `simpa [ rules , ⋯ ]` 会化简目标；如果上下文中存在名为 `this` 的假设，还会化简其类型，然后尝试使用 `assumption` 策略关闭目标。与 `simp` 一样，`simpa` 后的 `!` 修饰符会启用 simp 集中定义的自动展开。

这是 `simp` 的一种“收尾”策略变体。它有两种形式。 `simpa [ rules , ⋯ ] using e` 使用 `rules` 化简目标和 `e` 的类型，然后尝试用 `e` 关闭目标。化简 `e` 的类型使它更有可能与同样已化简的目标匹配。这种写法面对 simp 引理集的变化时通常也更稳健。已化简的 `e` 与已化简目标之间的最终匹配使用可约透明度，因此不会展开半可约定义。若要在环境的（默认/半可约）透明度下执行匹配，请写 `simpa [ rules , ⋯ ] using! e`。 `simpa [ rules , ⋯ ]` 会化简目标；如果上下文中存在名为 `this` 的假设，还会化简其类型，然后尝试使用 `assumption` 策略关闭目标。与 `simp` 一样，`simpa` 后的 `!` 修饰符会启用 simp 集中定义的自动展开。

这是 `simp` 的一种“收尾”策略变体。它有两种形式。 `simpa [ rules , ⋯ ] using e` 使用 `rules` 化简目标和 `e` 的类型，然后尝试用 `e` 关闭目标。化简 `e` 的类型使它更有可能与同样已化简的目标匹配。这种写法面对 simp 引理集的变化时通常也更稳健。已化简的 `e` 与已化简目标之间的最终匹配使用可约透明度，因此不会展开半可约定义。若要在环境的（默认/半可约）透明度下执行匹配，请写 `simpa [ rules , ⋯ ] using! e`。 `simpa [ rules , ⋯ ]` 会化简目标；如果上下文中存在名为 `this` 的假设，还会化简其类型，然后尝试使用 `assumption` 策略关闭目标。与 `simp` 一样，`simpa` 后的 `!` 修饰符会启用 simp 集中定义的自动展开。

展开良基关系定义中常用的定义。从 Lean 4.12 起，Lean 会在向用户呈现目标之前自动展开这些定义，因此该策略应不再需要。 可以删除对 `simp_wf` 的调用，或将其替换为普通的 `simp` 调用。

`rw` 类似 `rewrite`，但之后还会尝试使用“廉价的”（可归约的）`rfl` 关闭目标。

`rewrite [ e ]` 把恒等式 `e` 作为重写规则应用于主目标的目标式。如果 `e` 前有左箭头（`←` 或 `<-`），则反向应用重写。如果 `e` 是已定义常量，则使用与 `e` 关联的等式定理。这提供了一种展开 `e` 的便捷方式。 `rewrite [ e₁ , ... , eₙ ]` 依次应用给定规则。`rewrite [ e ] at l` 在位置 `l` 重写 `e`，其中 `l` 可以是 `*`，也可以是局部上下文中的假设列表。后一种情况下，还可使用回转符 `⊢` 或 `| -` 表示目标的目标式。 使用 `rw ( occs := .pos L ) [ e ]`（其中 `L : List Nat`）可以控制重写哪些“出现位置”。（此选项应用于每条规则，因此通常只与单条规则一起使用。）出现位置从 `1` 开始计数。在每个允许的位置，重写规则 `e` 的参数都可能被实例化，从而限制之后能找到哪些重写。（不允许的位置不会导致实例化。）`( occs := . neg L )` 可以跳过指定的出现位置。

`erw [ rules ]` 是 `rw ( transparency := .default ) [ rules ]` 的简写。它进行重写时可展开普通定义；相比之下，普通 `rw` 只展开带有 `@[ reducible ]` 标记的定义。

`rwa` 是 `rw ; assumption` 的简写。

配置 rewrite 与 rw 策略的行为。

Lean.Meta.Rewrite.Config.mk

transparency : Lean.Meta.TransparencyMode

offsetCnstrs : Bool

occs : Lean.Meta.Occurrences

newGoals : Lean.Meta.Rewrite.NewGoals

指定与某表达式匹配的哪些出现位置应被重写。

Lean.Meta.Occurrences.all : Lean.Meta.Occurrences

Lean.Meta.Occurrences.pos (idxs : List Nat) :
  Lean.Meta.Occurrences

Lean.Meta.Occurrences.neg (idxs : List Nat) :
  Lean.Meta.Occurrences

控制精化器在判断定义相等时可以展开哪些常量。

Lean.Meta.TransparencyMode.all : Lean.Meta.TransparencyMode

Lean.Meta.TransparencyMode.default :
  Lean.Meta.TransparencyMode

Lean.Meta.TransparencyMode.reducible :
  Lean.Meta.TransparencyMode

Lean.Meta.TransparencyMode.instances :
  Lean.Meta.TransparencyMode

Lean.Meta.TransparencyMode.none : Lean.Meta.TransparencyMode

Lean.Meta.TransparencyMode.implicit :
  Lean.Meta.TransparencyMode

控制重写产生的新目标如何加入目标列表。

unfold id 展开目标中定义 id 的所有出现位置。unfold id1 id2 ... 等价于 unfold id1 ; unfold id2 ; ...。unfold id at h 在假设 h 中进行展开。定义既可以是全局定义，也可以是局部定义。对于非递归全局定义，该策略与 delta 完全相同。对于递归全局定义，它使用“展开引理” id.eq_def；系统会为每个递归定义生成该引理，以便按照用户给出的递归定义进行展开。这里只执行一层展开；与之相反，simp only [ id ] 会递归展开定义 id。 由 Lean.Elab.Tactic.evalUnfold 实现。

`replace h := e` 与 `have h := e` 类似，但它会尽可能移除先前同名的假设。例如，如果状态为： f : α → β h : α ⊢ goal 那么执行 `replace h := f h` 后，状态将变为： f : α → β h : β ⊢ goal 而 `have h := f h` 会产生： f : α → β h† : α h : β ⊢ goal 策略 `specialize h a₁ ... aₙ` 是书写 `replace h := h a₁ ... aₙ` 的一种方式，它会自动推断应替换哪个假设。 `replace` 策略可用于模拟 Rocq 的 `apply at` 策略。

`delta id1 id2 ...` 对定义 `id1`、`id2` 等进行 delta 展开。这是一个底层策略，它会暴露 Lean 编译递归定义的方式。

在环境中搜索能用 `exact` 解决目标的定义或定理，其中条件由 `solve_by_elim` 解决。 可选的 `using` 子句提供局部上下文中的标识符；`exact?` 在关闭目标时必须使用这些标识符。当目标有多种解决方式，而用户希望引导它选用某个引理时，这最有用。 使用 `+ grind` 可启用 `grind` 作为子目标的后备解决器。使用 `+ try?` 可启用 `try?` 作为子目标的后备解决器。使用 `- star` 可禁用回退到带星号索引的引理（如 `Empty.elim`、`And.left`）。使用 `+ all` 可收集所有成功的引理，而不是在找到第一个时停止。

在环境中搜索能够使用 `apply` 精化目标的定义或定理，并尽可能使用 `solve_by_elim` 解决条件。 可选的 `using` 子句提供局部上下文中的标识符；关闭目标时必须使用这些标识符。 使用 `+ grind` 启用 `grind`，作为子目标的后备解决器。 使用 `+ try?` 启用 `try?`，作为子目标的后备解决器。 使用 `- star` 禁止回退到带星号索引的引理。 使用 `+ all` 收集所有成功的引理，而不是在第一个引理处停止。

`rw?` 尝试寻找能够重写目标的引理。不应把 `rw?` 留在证明中；它与 `apply?` 一样是搜索工具。建议会打印为 `rw [ h ]` 或 `rw [ ← h ]`。可以使用 `rw? [ - my_lemma , - my_theorem ]` 阻止 `rw?` 使用指定名称的引理。

`split` 策略适合将嵌套的 `if-then-else` 和 `match` 表达式拆成独立分支。对于具有 `n` 个分支的 `match` 表达式，`split` 策略最多生成 `n` 个子目标。 例如，给定 `n : Nat` 和目标 `if n = 0 then Q else R`，`split` 会生成一个具有假设 `n = 0` 和目标 `Q` 的目标，以及第二个具有假设 `¬ n = 0` 和目标 `R` 的目标。 请注意，引入的假设没有名称，通常使用 `case` 或 `next` 策略为其重命名。 `split` 拆分目标。`split at h` 拆分假设 `h`。

`by_cases ( h : ) ? p` 把主目标拆分为两个分支：第一个分支假设 `h : p`，第二个分支假设 `h : ¬ p`。

`decide` 尝试通过合成 `Decidable p` 的实例，随后归约该实例以求出 `p` 的真值，来证明主目标（目标类型为 `p`）。如果它归约为 `isTrue h`，那么 `h` 就是一个关闭目标的 `p` 的证明。目标中不允许包含局部变量或元变量。如果存在局部变量，可以先尝试对这些局部变量使用 `revert` 策略，将它们移入目标；也可以使用下述 `+ revert` 选项。 选项： `decide + revert` 首先清理局部上下文中的无关变量，然后还原目标所依赖的局部变量。如果一个变量出现在目标中、出现在某个相关变量中，或它是一个引用了相关变量的命题，那么该变量就是相关的。 `decide + kernel` 使用内核而非精化器进行归约。它有两个关键性质：(1) 因为使用内核，所以它忽略透明度并且可以展开一切；(2) 它只归约一次 `Decidable` 实例，而不是两次。 `decide + native` 使用原生代码编译器（`#eval`）求值 `Decidable` 实例，并通过一个公理接纳结果。它可能比使用归约高效得多，但代价是增大可信代码基的规模。具体而言，它依赖 Lean 编译器以及所有带有 `@[ implemented_by ]` 属性的定义的正确性。与 `+ kernel` 一样，`Decidable` 实例只会求值一次。 限制：在默认模式或 `+ kernel` 模式下，由于 `decide` 使用归约来求值项，通过良基递归定义的 `Decidable` 实例可能无法工作，因为求值它们需要归约证明。归约也可能卡在含有 `Eq.rec` 项的 `Decidable` 实例上。这些项可能出现在使用策略（例如 `rw` 和 `simp`）定义的实例中。为避免此问题，请改用诸如 `decidable_of_iff` 等定义来创建这类实例。 示例 证明不等式： `example : 2 + 2 ≠ 5 := by ⊢ 2 + 2 ≠ 5 decide All goals completed! 🐙` 尝试证明一个假命题： `example : 1 ≠ 1 := by decide /- tactic 'decide' proved that the proposition 1 ≠ 1 is false -/` 尝试证明一个其 `Decidable` 实例归约失败的命题： `opaque unknownProp : Prop open scoped Classical in example : unknownProp := by decide /- tactic 'decide' failed for proposition unknownProp since its 'Decidable' instance reduced to Classical.choice ⋯ rather than to the 'isTrue' constructor. -/` 性质与关系 对于具有可判定相等性的类型上的等式目标，通常可以用 `rfl` 代替 `decide`。 `example : 1 + 1 = 2 := by ⊢ 1 + 1 = 2 decide All goals completed! 🐙` `example : 1 + 1 = 2 := by ⊢ 1 + 1 = 2 rfl All goals completed! 🐙`

`native_decide` 是 `decide + native` 的同义形式。它会尝试通过合成 `Decidable p` 的实例并将其求值为 `isTrue ..`，来证明类型为 `p` 的目标。与 `decide` 不同，它使用 `#eval` 对可判定性实例求值。 使用时应谨慎，因为它会把整个 Lean 编译器加入可信部分；对于使用此方法的定理以及传递依赖这些定理的任何内容，`#print axioms` 中都会出现一个新公理。不过，由于它经过编译，效率可能显著高于 `decide`；对于非常大的计算，这是运行外部程序并信任其结果的一种方式。 `example : ( List.range 1000 ) . length = 1000 := by ⊢ ( List.range 1000 ) . length = 1000 native_decide All goals completed! 🐙`

`omega` 策略用于解决整数和自然数的线性算术问题。它目前还不是完整的判定过程（没有“暗影”或“灰影”），但应能有效处理许多问题。 我们处理形如 `x = y`、`x < y`、`x ≤ y` 和 `k ∣ x` 的假设，其中 `x y` 属于 `Nat` 或 `Int`（而 `k` 是字面量），也处理这些陈述的否定。我们把不等式两侧分解为原子的线性组合。如果遇到字面整数 `k` 对应的 `x / k` 或 `x % k`，就引入新的辅助变量和相关不等式。 第一次处理时，我们不对自然数减法进行情况拆分。如果 `omega` 失败，则递归地对假设中出现的某个自然数减法进行情况拆分，然后重试。 选项 `omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax` 可用于： * `splitDisjunctions`：若问题无法以其他方式解决，则拆分上下文中发现的所有析取。 * `splitNatSub`：对于每个 `((a - b : Nat) : Int)`，必要时按 `a ≤ b` 拆分。 * `splitNatAbs`：对于每个 `Int.natAbs a`，必要时按 `0 ≤ a` 拆分。 * `splitMinMax`：对于每个 `min a b`，按 `min a b = a ∨ min a b = b` 拆分。 目前，所有这些选项默认启用。

`bv_omega` 是带有额外预处理器的 `omega`；该预处理器把关于 `BitVec` 的陈述转换为关于 `Nat` 的陈述。目前，该预处理器实现为 `try simp only [ bitvec_to_nat ] at *`。 `bitvec_to_nat` 是一个 `@[ simp ]` 属性，可以（谨慎地）将更多定理加入其中。

`tactic ::= ... | `cbv`` 执行与按值求值非常相似的化简。它使用定义方程展开定义并应用匹配器方程来归约项。展开是命题式的，因此 `cbv` 也适用于通过良基递归或部分不动点定义的函数。 `cbv` 使用按值求值来归约目标类型（以及可选的假设类型）。对于等式目标（`lhs = rhs`），`cbv` 会在归约后自动尝试 `refl` 以关闭目标。 `cbv` 支持标准的 `at` 位置语法： - `cbv`——归约目标； - `cbv at h`——归约假设 `h`； - `cbv at h |-`——归约假设 `h` 和目标； - `cbv at *`——归约目标以及所有非依赖命题假设。 如果某个假设归约为 `False`，目标会立即关闭。一般而言，`cbv` 不是终结策略：它可能留下一个新的（更简单的）目标。 `cbv` 生成的证明只使用三个标准公理。特别是，它们无需信任代码生成器的正确性。 位置规约由许多既能作用于假设也能作用于目标的策略使用。相关语法骨架为 `cbv ( at ( term | locationType ) * )?`，其中位置可以由 `at` 后的一处或多处位置组成。它可以采用以下形式之一： - “空”实际上不会出现在该语法中，但多数策略使用 `(location)?` 匹配器；它表示只以目标为作用位置； - `at h₁ ... hₙ`：以假设 `h₁`、……、`hₙ` 为作用位置； - `at h₁ h₂ ⊢`：以假设 `h₁`、`h₂` 和目标为作用位置； - `at *`：以所有假设和目标为作用位置。 `at` 后是一处或多处策略应作用的位置。这些位置可以包括局部假设和表示目标的 `⊢`。`⊢` 位置指当前目标。

`cbv` 执行一种紧密模拟按值求值的化简。它通过使用定义方程展开定义并应用匹配器方程来归约项。这种展开是命题式的，因此 `cbv` 也适用于通过良基递归或部分不动点定义的函数。 `cbv` 使用按值求值来归约目标类型（以及可选的假设类型）。对于等式目标（`lhs = rhs`），`cbv` 会在归约后自动尝试 `refl` 以关闭目标。 `cbv` 支持标准的 `at` 位置语法： * `cbv`——归约目标； * `cbv at h`——归约假设 `h`； * `cbv at h |-`——归约假设 `h` 和目标； * `cbv at *`——归约目标以及所有非依赖的命题假设。 如果某个假设归约为 `False`，目标会立即关闭。一般而言，`cbv` 不是终结策略：它可能留下一个新的（更简单的）目标。`cbv` 生成的证明只使用三个标准公理。特别是，这些证明不需要信任代码生成器的正确性。

`with_reducible tacs` 使用可归约透明度设置执行 `tacs`。在此设置下，只展开标记为 `[ reducible ]` 的定义。

`with_reducible_and_instances tacs` 使用 `.instances` 透明度设置执行 `tacs`。在此设置下，只展开标记为 `[ reducible ]` 的定义或类型类实例。

`with_unfolding_all tacs` 使用 `.all` 透明度设置执行 `tacs`。在此设置下，会展开所有非不透明定义。

`with_unfolding_none tacs` 使用 `.none` 透明度设置执行 `tacs`。在此设置下，不展开任何定义。

`skip` 不执行任何操作。

此策略检查具名假设是否具有给定的类型和／或值。 * `guard_hyp h : t` 在可归约定义相等意义下检查类型； * `guard_hyp h :~ t` 在默认定义相等意义下检查类型； * `guard_hyp h :ₛ t` 在语法相等意义下检查类型； * `guard_hyp h :ₐ t` 在 alpha 相等意义下检查类型； * `guard_hyp h := v` 在可归约定义相等意义下检查值； * `guard_hyp h :=~ v` 在默认定义相等意义下检查值； * `guard_hyp h :=ₛ v` 在语法相等意义下检查值； * `guard_hyp h :=ₐ v` 在 alpha 相等意义下检查值。 值 `v` 使用 `h` 的类型作为预期类型进行精译。

用于检查目标是否与给定表达式一致的策略。 `guard_target = e` 检查目标在可归约透明度下是否在定义上等于 `e`。 `guard_target =~ e` 检查目标在默认透明度下是否在定义上等于 `e`。 `guard_target =ₛ e` 检查目标是否在语法上等于 `e`。 `guard_target =ₐ e` 检查目标是否与 `e` α 等价。 项 `e` 以目标类型作为预期类型进行精译；这主要在 `conv` 模式中有用。

用于检查两个表达式是否相等的策略。`guard_expr e = e'` 检查 `e` 和 `e'` 在可约透明度下定义相等。`guard_expr e =~ e'` 检查二者在默认透明度下定义相等。`guard_expr e =ₛ e'` 检查二者在语法上相等。`guard_expr e =ₐ e'` 检查二者 alpha 等价。 `e` 和 `e'` 都会先经过精译，然后在相等性检查前实例化其中的元变量。在处理合成元变量之前，会先统一它们的类型（使用 `isDefEqGuarded`），这有助于处理默认实例。

当且仅当没有剩余目标时，`done` 成功。

策略 `sleep ms` 休眠 `ms` 毫秒，除此之外不执行任何操作。它仅用于调试。

`stop` 是一个用于“丢弃”证明剩余部分的辅助策略：其定义为 `repeat sorry`。 在处理复杂证明的中间部分时，它很有用，并且比注释掉证明剩余部分更整洁。

通过先化简、再应用字典序引理、最后使用 `ts` 解决基本情况，构造沿良基关系递减的证明。如果失败，它会打印消息，帮助用户诊断非良基的递归定义。

`get_elem_tactic` 是记法 `arr [ i ]` 自动调用的策略，用于证明构造该项时产生的任何附带条件（例如索引位于数组范围内）。它只是委托给 `get_elem_tactic_extensible`；若失败则给出诊断错误消息。建议用户扩展 `get_elem_tactic_extensible`，而不是扩展此策略。

`get_elem_tactic_trivial` 已弃用，推荐改用 `get_elem_tactic_extensible`。

`sorry` 策略是不完整策略证明的临时占位符，它使用 `exact sorry` 关闭主目标。其用途是在仍保有语法正确的证明骨架的同时，为证明中尚未完成的部分放置占位符。 每当证明使用 `sorry` 时，Lean 都会发出警告，因此一般不会遗漏它。不过，可以在 `#print axioms my_thm` 命令的输出中查找 `sorryAx`，以再次确认某个定理是否依赖 `sorry`；`sorryAx` 是 `sorry` 实现所使用的公理。

`admit` 是 `sorry` 的同义形式。

`dbg_trace "foo"` 在精译时打印 `foo`。它有助于调试策略控制流： `example : False ∨ True := by ⊢ False ∨ True first | apply Or.inl ⊢ False ; trivial ⊢ False ; dbg_trace "left" | apply Or.inr ⊢ True ; trivial All goals completed! 🐙 ; dbg_trace "right"`

`trace_state` 在信息视图中显示当前状态。

`trace msg` 在信息视图中显示 `msg`。

`∎`（输入为 `\qed`）是一个宏，在策略模式中展开为 `try?`。

`# suggestions` 使用当前注册的库建议引擎，为当前目标推荐库中的相关定理。建议按置信度从高到低的顺序打印。

`trivial` 尝试使用各种简单策略（例如 `rfl`、`contradiction` 等）关闭当前目标。可以使用命令 `macro_rules` 扩展所用策略的集合。 示例： macro_rules | `(tactic| trivial ) => `(tactic| simp )

类似于 `first`，但仅当给定策略之一解决当前目标时才成功。

`and_intros` 反复应用 `And.intro`，直到无法取得进展。

`infer_instance` 是 `exact inferInstance` 的缩写。它通过类型类推断合成任意目标类型的值。

`expose_names` 将所有不可访问变量重命名为可访问名称，使生成的策略能够引用它们。但是，这种重命名会引入不完全受用户控制的机器生成名称。 `expose_names` 主要用作自动生成的收尾策略脚本的序言。它也可作为 `set_option tactic.hygienic false` 的替代方案。 如果需要在策略脚本中途显式控制重命名，请考虑使用带有 `match .. with`、`induction .. with` 或带显式用户定义名称的 `intro` 的结构化策略脚本，以及 `next`、`case` 和 `rename_i` 等策略。

`unhygienic tacs` 在禁用名称卫生性的情况下运行 `tacs`。这意味着，通常会创建不可访问名称的策略将改为创建普通变量。 警告：策略随时可能改变变量命名策略，因此依赖自动生成名称的代码很脆弱。用户应尽可能避免使用 `unhygienic`。 `example : ∀ x : Nat , x = x := by ⊢ ∀ ( x : Nat ), x = x unhygienic intro x : Nat ⊢ x = x -- x 通常会以不可访问名称引入 exact Eq.refl x All goals completed! 🐙 -- 引用 x`

`run_tac doSeq` 策略执行 `TacticM Unit` 中的代码。

只要 `prog` 中使用的所有函数都具有以 `@[ spec ]` 注册的规约，`mvcgen` 就会把形如 `⦃ P ⦄ prog ⦃ Q ⦄` 的霍尔三元组证明目标分解为验证条件。 验证条件与规约 验证条件是 `Std.Do.SPred` 有状态逻辑中的一个蕴涵，其中原程序 `prog` 已不再出现。验证条件由 `mspec` 策略引入；其形式请参阅 `mspec` 策略。当没有适用的 `mspec` 规约时，`mvcgen` 会尝试使用以 `@[ spec ]` 注册的 simp 集重写应用 `prog = f a b c`。 功能 当像 `mvcgen + noLetElim [ foo_spec , bar_def , instBEqFloat ]` 这样使用时，`mvcgen` 还会： * 对 `prog` 中出现的函数 `foo`，把霍尔三元组规约 `foo_spec : ... → ⦃ P ⦄ foo ... ⦃ Q ⦄` 加入 spec 集； * 在 `prog` 中展开定义 `def bar_def ... := ...`； * 在 `prog` 中展开实例 `instBEqFloat : BEq Float` 的任意方法； * 不再替换掉在 `P`、`Q` 或 `prog` 中至多出现一次的 `let` 表达式。 配置选项 `+ noLetElim` 只是众多配置选项之一。所有选项请查看 `Lean.Elab.Tactic.Do.VCGen.Config`。特别值得注意的是 `stepLimit = some 42`，它有助于二分定位 `mvcgen` 中的错误并跟踪其执行。 扩展语法 `mvcgen` 经常会这样使用： `mvcgen [...] case inv1 => exact I1 case inv2 => exact I2 all_goals (mleave; try grind)` 对此有专门语法： `mvcgen [...] invariants · I1 · I2 with grind` 当 `I1` 和 `I2` 需要引用不可访问名称时（`mvcgen` 会为程序变量引入很多这样的名称），可以使用分支标签语法： `mvcgen [...] invariants | inv1 _ acc _ => I1 acc | _ => I2 with grind` 这比等价形式 `· by rename_i _ acc _ ; exact I1 acc` 更方便。 不变式建议 如果使用 `invariants?` 关键字，`mvcgen` 会为你建议不变式。 `mvcgen [...] invariants?` 当你记不清构造不变式的确切语法时，这很有用。此外，它会通过查看相应的验证条件，建议一个表示“此性质在循环开始时成立，并且必须在循环结束时成立”的具体不变式。建议的不变式虽是良好起点，但它过强，用户需要对其进行插值，使归纳步骤能够得到证明。 示例： `def mySum (l : List Nat) : Nat := Id.run do let mut acc := 0 for x in l do acc := acc + x return acc /-- info: Try this: invariants · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝ -/ #guard_msgs (info) in theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by generalize h : mySum l = r apply Id.of_wp_run_eq h mvcgen invariants? all_goals admit`