`fail msg` 是一个总会失败的策略，并使用给定消息产生错误。
14.3. 策略语言
策略脚本由一列策略组成，各策略之间用分号或换行分隔。 使用换行分隔时，各策略必须具有相同的缩进层级。 可以用显式的花括号和分号代替缩进。 策略序列可以用圆括号分组。 这样便可在语法上原本只接受单个策略的位置使用一列策略。
通常，执行从上到下进行，每个策略都在前一策略留下的证明状态中运行。 策略语言包含多种可以修改这一流程的控制结构。
每个策略都是 tactic 类别中的语法扩展。
这意味着策略可以自由定义自己的具体语法和解析规则。
不过，除少数例外，大多数策略都可以通过开头的关键字识别；例外通常是 <;> 这类常用的内置控制结构。
14.3.1. 控制结构
严格来说，控制结构与其他策略之间没有根本区别。 任何策略都可以自由地接受其他策略作为参数，并安排它们在其认为合适的任意上下文中执行。 不过，即使这种区分是人为的，它仍然可能有用。 本节中的策略要么类似于编程中的传统控制结构，要么仅仅重新组合其他策略而自身不推进证明。
14.3.1.1. 成功与失败
在证明状态中运行时，每个策略要么成功，要么失败。
策略失败类似于异常：失败通常会不断“向上冒泡”，直至被处理。
与异常不同，没有运算符可以区分失败原因；first 只是采用第一个成功的分支。
14.3.1.2. 分支
策略证明可以使用模式匹配和条件表达式。
不过，它们的含义与在项中并不完全相同。
项应在变量值已知后执行；而证明执行时变量仍保持抽象，因此应同时考虑所有情况。
因此，在策略中使用 if 和 match 时，它们表示分类推理，而不是选择某个具体分支。
它们的所有分支都会执行；条件或模式匹配用于在每个分支中以更多信息精化主目标，而不是选出单个分支。
策略
if
在策略模式中，`if t then tac1 else tac2` 是以下写法的替代语法： by_cases t · tac1 · tac2 它对 `h† : t` 或 `h† : ¬t` 进行情况区分，其中 `h†` 是匿名假设，而 `tac1` 和 `tac2` 是子证明。（它实际上并不使用非依赖的 `if`，因为那不会向上下文加入任何内容，因而对证明定理毫无用处。若确实要插入一个 `ite` 应用，请使用 `refine if t then ? _ else ? _`。） 可以为各子目标中的假设命名。`if h : t then tac1 else tac2` 可用作以下写法的替代语法： by_cases h : t · tac1 · tac2 它对 `h : t` 或 `h : ¬ t` 进行情况区分。可以对任一子证明使用 `? _` 或 `_`，将该目标延后到此策略之后；但如果为 `tac1` 或 `tac2` 提供了策略序列，则要求在该代码块结束前关闭目标。
使用 if 分类推理
在 Lean.Parser.Tactic.tacIfThenElse : tacticif 的每个分支中，都会加入一个反映 n = 0 是否成立的假设。
example (n : Nat) : if n = 0 then n < 1 else n > 0 := n:Nat⊢ if n = 0 then n < 1 else n > 0
if n = 0 n:Nath✝:n = 0⊢ if n = 0 then n < 1 else n > 0
All goals completed! 🐙
n:Nath✝:¬n = 0⊢ if n = 0 then n < 1 else n > 0
n:Nath✝:¬n = 0⊢ 0 < n
All goals completed! 🐙
策略
match
match 对一个或多个表达式进行分类分析。参见《归纳与递归》。match 策略的语法与项模式的 match 相同，不同之处在于 match 的分支是策略而不是表达式。example ( n : Nat ) : n = n := by n : Nat ⊢ n = n match n with | 0 => n : Nat ⊢ 0 = 0 rfl All goals completed! 🐙 | i + 1 => n : Nat i : Nat ⊢ i + 1 = i + 1 simp All goals completed! 🐙 进行模式匹配时，目标中 判别项 的各个实例会在每个分支中替换为与之匹配的模式。 随后每个分支都必须证明精化后的目标。 与 cases 策略相比，使用 match 可以让分类分析更加灵活；但每个分支都必须彻底解决其目标，因此更难将其纳入较大的自动化脚本。
使用 match 分类推理
在 Lean.Parser.Tactic.match : tacticmatch 的每个分支中，判别项 n 都被替换为 0 或 k + 1。
example (n : Nat) : if n = 0 then n < 1 else n > 0 := n:Nat⊢ if n = 0 then n < 1 else n > 0
match n with
n:Nat⊢ if 0 = 0 then 0 < 1 else 0 > 0
All goals completed! 🐙
n:Natk:Nat⊢ if k + 1 = 0 then k + 1 < 1 else k + 1 > 0
All goals completed! 🐙
14.3.1.3. 目标选择
大多数策略会影响主目标。 目标选择策略提供了将其他目标视作主目标的方法，会重新排列证明状态中的目标序列。
策略
case
`case tag => tac` 聚焦于分支名为 `tag` 的目标，并使用 `tac` 求解它，否则失败。`case tag x₁ ... xₙ => tac` 还会把最近的 `n` 个具有不可访问名称的假设重命名为给定名称。`case tag₁ | tag₂ => tac` 等价于 `( case tag₁ => tac ) ; ( case tag₂ => tac )`。
策略
case'
`case'` 与 `case tag => tac` 策略类似，但它既不确保应用 `tac` 后目标已经解决，也不会在 `tac` 失败时承认该目标。回想一下，当 `tac` 失败时，`case` 会使用 `sorry` 关闭目标，并且不会中断策略执行。
策略
rotate_left
`rotate_left n` 将目标向左轮转 `n` 次。也就是说，`rotate_left 1` 取出主目标并将其放到子目标列表末尾。如果省略 `n`，则默认为 `1`。
14.3.1.3.1. 顺序执行
除了依次运行策略、让每个策略解决主目标之外，策略语言还支持根据目标的产生方式来顺序执行策略。
策略组合子 <;> 可以将某个策略应用到另一策略产生的每个子目标。
如果没有产生新目标，就不会运行第二个策略。
策略
<;>
tac <;> tac' 先在主目标上运行 tac，再对产生的每个目标运行 tac'，并将 tac' 产生的所有目标串接起来。 如果该策略在任一 子目标 上失败，整个 <;> 策略就会失败。
子目标顺序执行
在此证明状态中：
策略 x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 会产生以下两个目标：
运行 x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 ; x:Nath✝:x = 2⊢ x < 3 后，simp 会解决第一个目标，留下第二个目标：
将 ; 替换为 <;> 并运行 x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 x:Nath✝:x = 1⊢ x < 3x:Nath✝:x = 2⊢ x < 3 All goals completed! 🐙，会用 simp 解决新产生的两个目标：
All goals completed! 🐙
14.3.1.3.2. 处理多个目标
策略 all_goals 和 any_goals 允许将一个策略应用到证明状态中的每个目标。
两者的区别在于：如果策略在任一目标上失败，all_goals 自身就会失败；而只有策略在所有目标上都失败时，any_goals 才会失败。
策略
all_goals
`all_goals tac` 在每个目标上运行 `tac`，并连接所得目标。如果该策略在任何目标上失败，则整个 `all_goals` 策略失败。 另请参阅 `any_goals tac`。
策略
any_goals
`any_goals tac` 对每个目标应用策略 `tac`，并拼接策略应用成功后产生的目标。如果该策略在所有目标上都失败，则整个 `any_goals` 策略失败。 此策略与 `all_goals try tac` 类似，但如果 `tac` 的所有应用都未成功，它就会失败。
14.3.1.4. 聚焦
聚焦策略会让后续策略不再考虑证明目标的某个子集（通常只留下主目标）。
除这里介绍的策略外，case 和 case' 策略也会聚焦于所选目标。
策略
·
· tac 聚焦于主目标，并尝试使用 tac 解决它，否则便失败。 通常认为，只要一行策略产生了多个新子目标，使用项目符号就是良好的 Lean 风格。 这样证明更易阅读和维护，因为推理步骤之间的联系更加清晰，而且编辑证明时子目标数量的任何变化都只会产生局部影响。
策略
next
`next => tac` 聚焦下一个目标并使用 `tac` 解决它，否则失败。 `next x₁ ... xₙ => tac` 还会使用给定名称，重命名最近引入的 `n` 个具有不可访问名称的假设。
14.3.1.5. 重复与迭代
策略
iterate
`iterate n tac` 恰好运行 `tac` 共 `n` 次。`iterate tac` 反复运行 `tac`，直到失败。`iterate` 的参数是策略序列，因此可以使用 `iterate n ( tac₁ ; tac₂ ; ⋯ )` 或 `iterate n tac₁ tac₂ ⋯` 运行多个策略。
策略
repeat
只要 `tac` 成功，`repeat tac` 就反复应用 `tac`。策略 `tac` 可以是策略序列；如果 `tac` 在执行过程中的任意时刻失败，`repeat` 会撤销 `tac` 对策略状态所作的任何部分更改。策略 `tac` 最终应当失败，否则 `repeat tac` 会无限运行。 另请参阅：`try tac` 类似于 `repeat tac`，但至多应用 `tac` 一次。`repeat' tac` 对每个目标递归应用 `tac`。`first | tac1 | tac2` 实现 `repeat` 所使用的回溯。
策略
repeat'
只要 `tac` 成功，`repeat' tac` 就会在所有目标上递归应用 `tac`。也就是说，如果 `tac` 产生多个子目标，那么会对每个子目标应用 `repeat' tac`。 另请参阅：`repeat tac` 只是反复应用 `tac`。`repeat1' tac` 与 `repeat' tac` 相同，但要求 `tac` 至少在某个目标上成功一次。
策略
repeat1'
只要成功，`repeat1' tac` 就会在所有目标上递归应用 `tac`；但如果 `tac` 在所有初始目标上都没有成功，`repeat1' tac` 就会失败。 另请参阅：`repeat tac` 只是反复应用 `tac`。`repeat' tac` 类似于 `repeat1' tac`，但不要求 `tac` 至少成功一次。
14.3.2. 名称与卫生性
在幕后，策略会生成证明项。 这些证明项存在于局部上下文中，因为证明状态中的假设对应项中的局部绑定器。 使用假设对应于引用变量。 假设的命名必须可预测，这一点非常重要；否则，策略内部实现的微小变更一旦导致选中不同的名称，就可能引发变量捕获或引用失效。
Lean 的策略语言具有卫生性。 这意味着策略语言遵守词法作用域：策略中出现的名称引用源代码中包围它的绑定，而不是由生成的代码决定；策略框架负责维持这一性质。 策略脚本中的变量引用，要么指向脚本开始时就在作用域内的名称，要么指向策略显式引入的绑定，而不是幕后为证明项选用的名称。
策略具有卫生性的一个结果是：引用假设的唯一方式是显式为其命名。
策略不能自行分配假设名称，而必须接受用户提供的名称；相应地，用户若想引用某个假设，就必须为其提供名称。
当假设没有用户提供的名称时，它在证明状态中显示时会带有剑标（'†', DAGGER\t0x2020）。
剑标表示该名称不可访问，无法被显式引用。
将选项 tactic.hygienic 设为 false 可以禁用卫生性。
不建议这样做，因为许多策略依赖卫生系统来防止捕获，因而无需付出仔细手动选择名称的开销。
策略卫生性：不可访问的假设
策略卫生性：可访问的假设
14.3.2.1. 访问假设
许多策略提供了为其引入的假设指定名称的方法。
intro 和 intros 例如会接受假设名称作为参数；induction 的 Lean.Parser.Tactic.induction : tacticwith 形式则可以同时选择分支、命名假设并聚焦。
假设没有名称时，可以使用 next、case 或 rename_i 为其分配名称。
14.3.3. 假设管理
较大的证明可受益于证明状态管理：移除无关假设，并使假设名称更易理解。
除这些运算符外，rename_i 可以重命名不可访问的假设；intro、intros 和 rintro 则把蕴含或全称量化目标转换为带有额外假设的目标。
14.3.4. 局部定义与证明
have 和 let 都会创建局部假设。
一般来说，证明中间引理时应使用 have；let 应留给局部定义。
策略
have
`have` 策略用于向主目标的局部上下文添加不透明定义和假设。与由 `let` 策略添加的定义不同，这些定义会忘记其关联值，因而无法展开。 如果 `e` 是类型 `t` 的项，`have h : t := e` 会添加假设 `h : t`。`have h := e` 使用 `e` 的类型作为 `t`。`have : t := e` 和 `have := e` 使用 `this` 作为假设名称。 对于模式 `pat`，`have pat := e` 等价于 `match e with | pat => _`，其中 `_` 代表此策略之后的策略。这对于只有一个适用构造器的类型很方便。例如，给定 `h : p ∧ q ∧ r`，`have ⟨ h₁ , h₂ , h₃ ⟩ := h` 会产生假设 `h₁ : p`、`h₂ : q` 和 `h₃ : r`。 语法 `have ( eq := h ) pat := e` 等价于 `match h : e with | pat => _`，它会把等式 `h : e = pat` 添加到局部上下文。 该策略支持与 `have` 项完全相同的所有语法变体和选项。 性质与关系 无法展开使用 `have` 引入的变量，因为定义的值已被遗忘。`let` 策略引入的定义则可以展开。`have h : t := e` 类似于执行 `let h : t := e ; clear_value h`。 对于命题，首选 `have`；对于非命题，首选 `let`。有时会对非命题使用 `have`，以确保变量永不展开，这一点可能对性能很重要。可考虑使用等价的 `let + nondep` 来表明这一意图。
策略
let
`let` 策略用于向主目标的局部上下文添加定义。与由 `have` 引入的定义不同，该定义可以展开。如果 `e` 是类型 `t` 的项，`let x : t := e` 会添加定义 `x : t := e`。`let x := e` 使用 `e` 的类型作为 `t`。`let : t := e` 和 `let := e` 使用 `this` 作为假设名。 对于模式 `pat`，`let pat := e` 等价于 `match e with | pat => _`，其中 `_` 代表后续策略。这对于只有一个适用构造器的类型很方便。例如，给定 `p : α × β × γ`，`let ⟨ x , y , z ⟩ := p` 会生成局部变量 `x : α`、`y : β` 和 `z : γ`。 语法 `let ( eq := h ) pat := e` 等价于 `match h : e with | pat => _`，它会向局部上下文添加等式 `h : e = pat`。该策略支持与 `let` 项完全相同的所有语法变体和选项。 性质与关系 与 `have` 不同，可以使用 `simp`、`dsimp`、`unfold` 和 `subst` 等策略展开由 `let` 引入的定义。`clear_value` 策略可在事后把 `let` 定义变为 `have` 定义。如果局部上下文依赖变量的值，该策略可能失败。对于数据（非命题），优先使用 `let` 策略。有时也对非命题使用 `have`，以确保变量永不展开；这对性能可能很重要。
14.3.5. 配置
许多策略都可配置。
按照约定，各策略共享一种配置语法，以 optConfig 描述。
每个策略可用的具体选项会在该策略的文档中说明。
语法策略配置项
每个配置项都有一个名称，对应底层的策略选项。
布尔选项可以使用前缀 + 和 - 启用或禁用：
configItem ::=+ident
configItem ::= ... |-ident
可以使用类似于具名函数参数的语法，为选项赋予具体值：
configItem ::= ... |(ident := term)
最后，名称 config 是保留名称，用于将整组选项作为数据结构传递。
所需的具体类型取决于策略。
configItem ::= ... |(config := term)
14.3.6. 命名空间与选项管理
在策略脚本中，可以使用与项中相同的语法调整命名空间和选项。
14.3.6.1. 控制展开
默认情况下，除检查定义相等性时外，只有标记为可归约的定义才会展开。 这些运算符可以在策略脚本的某一部分调整此默认行为。
策略
with_reducible_and_instances`with_reducible_and_instances tacs` 使用 `.instances` 透明度设置执行 `tacs`。在此设置下，只展开标记为 `[ reducible ]` 的定义或类型类实例。
策略
with_reducible`with_reducible tacs` 使用可归约透明度设置执行 `tacs`。在此设置下，只展开标记为 `[ reducible ]` 的定义。
策略
with_unfolding_all`with_unfolding_all tacs` 使用 `.all` 透明度设置执行 `tacs`。在此设置下，会展开所有非不透明定义。