14.3. 策略语言🔗

策略脚本由策略序列组成，用分号或换行符分隔。当用换行符分隔时，策略必须缩进到同一级别。可以使用显式的花括号和分号来代替缩进。策略序列可以用括号分组。这允许在语法上预期为单个策略的位置使用策略序列。

一般来说，执行是从上到下进行的，每个策略都在前一个策略留下的证明状态下运行。策略语言包含许多可以修改此流程的控制结构。

每个策略都是 tactic 类别中的语法扩展。这意味着策略可以自由定义自己的具体语法和解析规则。然而，除了少数例外，大多数策略都可以通过前导关键字来识别；例外情况通常是常用的内置控制结构，例如 <;>。

14.3.1. 控制结构🔗

严格来说，控制结构与其他策略没有根本区别。任何策略都可以自由地将其他人作为参数，并在它认为合适的任何上下文中安排它们的执行。然而，即使这种区别是任意的，它仍然是有用的。本节中的策略类似于编程中的传统控制结构，或者仅重组其他策略而不是本身取得进展。

14.3.1.1. 成功与失败🔗

在验证状态下运行时，每个策略要么成功，要么失败。策略故障类似于异常：故障通常会“冒泡”直到得到处理。与异常不同的是，没有操作符来区分失败的原因； first 仅采用第一个成功的分支。

tactic

fail

fail msg is a tactic that always fails, and produces an error using the given message.

tactic

fail_if_success

fail_if_success t fails if the tactic t succeeds.

tactic

try

try tac runs tac and succeeds even if tac failed.

tactic

first

first | tac | ... runs each tac until one succeeds, or else fails.

14.3.1.2. 分枝🔗

策略证明可以使用模式匹配和条件。然而，它们的含义与术语中的含义并不完全相同。虽然术语预计在其变量值已知后执行，但证明是在其变量保持抽象的情况下执行的，并且应同时考虑所有情况。因此，当策略中使用if和match时，它们的含义是案例推理而不是选择具体分支。它们的所有分支都会被执行，并且条件或模式匹配用于通过每个分支中的更多信息来细化主要目标，而不是选择单个分支。

tactic

if

In tactic mode, if t then tac1 else tac2 is alternative syntax for:

by_cases t
· tac1
· tac2

It performs case distinction on h† : t or h† : ¬t, where h† is an anonymous hypothesis, and tac1 and tac2 are the subproofs. (It doesn't actually use nondependent if, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an ite application use refine if t then ?_ else ?_.)

The assumptions in each subgoal can be named. if h : t then tac1 else tac2 can be used as alternative syntax for:

by_cases h : t
· tac1
· tac2

It performs case distinction on h : t or h : ¬t.

You can use ?_ or _ for either subproof to delay the goal to after the tactic, but if a tactic sequence is provided for tac1 or tac2 then it will require the goal to be closed by the end of the block.

Reasoning by cases with if

在 Lean.Parser.Tactic.tacIfThenElse : tacticIn tactic mode, `if t then tac1 else tac2` is alternative syntax for: ``` by_cases t · tac1 · tac2 ``` It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an `ite` application use `refine if t then ?_ else ?_`.) The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as alternative syntax for: ``` by_cases h : t · tac1 · tac2 ``` It performs case distinction on `h : t` or `h : ¬t`. You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed by the end of the block.if 的每个分支中，添加一个假设来反映 n = 0 是否成立。

example (n : Nat) : if n = 0 then n < 1 else n > 0 := byn:Nat⊢ if n = 0 then n < 1 else n > 0
  if n = 0 thenn:Nath✝:n = 0⊢ if n = 0 then n < 1 else n > 0
    simp [*]All goals completed! 🐙
  elsen:Nath✝:¬n = 0⊢ if n = 0 then n < 1 else n > 0
    simp only [↓reduceIte, gt_iff_lt, *]n:Nath✝:¬n = 0⊢ 0 < n
    omegaAll goals completed! 🐙

Live ↪

tactic

match

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := byn:Nat⊢ n = n
  match n with
  | 0 =>n:Nat⊢ 0 = 0 rflAll goals completed! 🐙
  | i+1 =>n:Nati:Nat⊢ i + 1 = i + 1 simpAll goals completed! 🐙

当模式匹配时，目标中判别式的实例将替换为每个分支中与它们匹配的模式。然后每个分支必须证明细化的目标。与 cases策略相比，使用 match 可以在执行的案例分析中提供更大程度的灵活性，但每个分支完全解决其目标的要求使得合并到更大的自动化脚本中变得更加困难。

Reasoning by cases with match

在 Lean.Parser.Tactic.match : tactic`match` performs case analysis on one or more expressions. See [Induction and Recursion][tpil4]. The syntax for the `match` tactic is the same as term-mode `match`, except that the match arms are tactics instead of expressions. ``` example (n : Nat) : n = n := by match n with | 0 => rfl | i+1 => simp ``` [tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.htmlmatch 的每个分支中，判别式 n 已替换为 0 或 k + 1。

example (n : Nat) : if n = 0 then n < 1 else n > 0 := byn:Nat⊢ if n = 0 then n < 1 else n > 0
  match n with
  | 0 =>n:Nat⊢ if 0 = 0 then 0 < 1 else 0 > 0
    simpAll goals completed! 🐙
  | k + 1 =>n:Natk:Nat⊢ if k + 1 = 0 then k + 1 < 1 else k + 1 > 0
    simpAll goals completed! 🐙

Live ↪

14.3.1.3. 目标选择🔗

大多数策略影响主要目标。目标选择策略提供了一种将不同目标视为主要目标的方法，从而重新排列证明状态中的目标顺序。

tactic

case

case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.
case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.
case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).

tactic

case'

case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

tactic

rotate_left

rotate_left n rotates goals to the left by n. That is, rotate_left 1 takes the main goal and puts it to the back of the subgoal list. If n is omitted, it defaults to 1.

tactic

rotate_right

Rotate the goals to the right by n. That is, take the goal at the back and push it to the front n times. If n is omitted, it defaults to 1.

14.3.1.3.1. 测序🔗

除了逐个运行策略（每个都用于解决主要目标）之外，策略语言还支持根据目标生成方式对策略进行排序。 <;>策略组合器允许将策略应用于由其他策略生成的every 子目标。如果没有生成新目标，则不会运行第二个策略。

tactic

<;>

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

如果策略在任何子目标上失败，则整个 <;>策略失败。

Subgoal Sequencing

在这个证明状态下：

x:Nath:x = 1 ∨ x = 2⊢ x < 3

策略cases hinlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 产生以下两个目标：

inlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3

运行 cases hinlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 ; simp [*]inrx:Nath✝:x = 2⊢ x < 3 会导致 simp 解决第一个目标，留下第二个目标：

inrx:Nath✝:x = 2⊢ x < 3

用 <;> 替换 ; 并运行 cases hinlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 <;>inlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 simp [*]All goals completed! 🐙 可以通过 simp 解决两个新目标：

All goals completed! 🐙

14.3.1.3.2. 致力于多个目标🔗

策略all_goals 和 any_goals 允许将策略应用于证明状态下的每个目标。它们之间的区别在于，如果策略在任何一个目标中失败，all_goals 本身就会失败，而 any_goals 仅当策略在所有目标中失败时才失败。

tactic

all_goals

all_goals tac runs tac on each goal, concatenating the resulting goals. If the tactic fails on any goal, the entire all_goals tactic fails.

14.3.1.4. 聚焦🔗

关注策略会从一些进一步的策略的考虑中删除证明目标的一些子集（通常只留下主要目标）。除了此处描述的策略之外，case 和 case'策略重点关注选定的目标。

tactic

·

· tac focuses on the main goal and tries to solve it using tac, or else fails.

每当策略线产生多个新子目标时，通常认为使用子弹是良好的 Lean 风格。这使得阅读和维护证明变得更加容易，因为推理步骤之间的联系更加清晰，并且编辑证明时子目标数量的任何变化都会产生局部效果。

tactic

next

next => tac focuses on the next goal and solves it using tac, or else fails. next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

tactic

focus

focus tac focuses on the main goal, suppressing all other goals, and runs tac on it. Usually · tac, which enforces that the goal is closed by tac, should be preferred.

14.3.1.5. 重复与迭代🔗

tactic

iterate

iterate n tac runs tac exactly n times. iterate tac runs tac repeatedly until failure.

iterate's argument is a tactic sequence, so multiple tactics can be run using iterate n (tac₁; tac₂; ⋯) or

iterate n
  tac₁
  tac₂
  ⋯

tactic

repeat

repeat tac repeatedly applies tac so long as it succeeds. The tactic tac may be a tactic sequence, and if tac fails at any point in its execution, repeat will revert any partial changes that tac made to the tactic state.

The tactic tac should eventually fail, otherwise repeat tac will run indefinitely.

14.3.2. 姓名和卫生🔗

策略在幕后生成证明项。这些证明项存在于局部上下文中，因为证明状态中的假设对应于局部绑定项。假设的使用对应于变量引用。假设的命名是可预测的，这一点非常重要；否则，对策略的内部实现进行微小更改可能会导致变量捕获，或者如果导致选择不同的名称，则会导致引用损坏。

Lean 的策略语言是卫生。这意味着策略语言遵循词法范围：策略中出现的名称引用源代码中的封闭绑定，而不是由生成的代码确定，并且策略框架负责维护此属性。策略脚本中的变量引用引用脚本开头范围内的名称或作为策略的一部分显式引入的绑定，而不是选择在幕后证明术语中使用的名称。

卫生策略的结果是引用假设的唯一方法是明确命名它。策略不能自己分配假设名称，而必须接受用户的名称；用户相应地有义务提供他们希望引用的假设的名称。当假设没有用户提供的名称时，它会在证明状态中显示为匕首 ('†', DAGGER 0x2020)。匕首表明该名称不可访问且无法显式引用。

可以通过将选项 tactic.hygienic 设置为 false 来禁用卫生功能。不建议这样做，因为许多策略依赖卫生系统来防止捕获，因此不会产生仔细的手动名称选择的开销。

option

tactic.hygienic

Default value: true

make sure tactics are hygienic

Tactic hygiene: inaccessible assumptions

证明∀ (n : Nat), 0 + n = n时，初始证明状态为：

⊢ ∀ (n : Nat), 0 + n = n

策略intron✝:Nat⊢ 0 + n✝ = n✝ 导致证明状态具有无法访问的假设：

n✝:Nat⊢ 0 + n✝ = n✝

Tactic hygiene: accessible assumptions

证明∀ (n : Nat), 0 + n = n时，初始证明状态为：

⊢ ∀ (n : Nat), 0 + n = n

策略intro nn:Nat⊢ 0 + n = n 具有显式名称 n，会产生具有可访问命名假设的证明状态：

n:Nat⊢ 0 + n = n

14.3.2.1. 获取假设🔗

许多策略提供了一种为其引入的假设指定名称的方法。例如，intro 和 intros 将假设名称作为参数，而 induction 的 Lean.Parser.Tactic.induction : tacticAssuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well. For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `induction n` produces one goal with hypothesis `h : P 0` and target `Q 0`, and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`. Here the names `a` and `ih₁` are chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor. - `induction e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then performs induction on the resulting variable. - `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a term whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables - `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. - Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case.with 形式允许同时进行案例选择、假设命名和聚焦。当假设没有名称时，可以使用 next、case 或 rename_i 进行分配。

tactic

rename_i

rename_i x_1 ... x_n renames the last n inaccessible names using the given names.

14.3.3. 假设管理🔗

更大的证明可以受益于证明状态的管理，消除不相关的假设并使它们的名称更容易理解。与这些运算符一起，rename_i 允许重命名无法访问的假设，并且 intro、intros 和 rintro 将暗示或全称量化的目标转换为具有附加假设的目标。

tactic

rename

rename t => x renames the most recent hypothesis whose type matches t (which may contain placeholders) to x, or fails if no such hypothesis could be found.

tactic

revert

revert x... is the inverse of intro x...: it moves the given hypotheses into the main goal's target type.

tactic

clear

clear x... removes the given hypotheses, or fails if there are remaining references to a hypothesis.

14.3.4. 局部定义和证明🔗

have 和 let 均创建局部假设。一般来说，证明中间引理时应使用have； let 应保留用于本地定义。

tactic

have

The have tactic is for adding opaque definitions and hypotheses to the local context of the main goal. The definitions forget their associated value and cannot be unfolded, unlike definitions added by the let tactic.

have h : t := e adds the hypothesis h : t if e is a term of type t.
have h := e uses the type of e for t.
have : t := e and have := e use this for the name of the hypothesis.
have pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.
The syntax have (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the have term.

Properties and relations

It is not possible to unfold a variable introduced using have, since the definition's value is forgotten. The let tactic introduces definitions that can be unfolded.
The have h : t := e is like doing let h : t := e; clear_value h.
The have tactic is preferred for propositions, and let is preferred for non-propositions.
Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons. Consider using the equivalent let +nondep to indicate the intent.

tactic

have

have h : t := e adds the hypothesis h : t if e is a term of type t.
have h := e uses the type of e for t.
have : t := e and have := e use this for the name of the hypothesis.
have pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.
The syntax have (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the have term.

Properties and relations

It is not possible to unfold a variable introduced using have, since the definition's value is forgotten. The let tactic introduces definitions that can be unfolded.
The have h : t := e is like doing let h : t := e; clear_value h.
The have tactic is preferred for propositions, and let is preferred for non-propositions.
Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons. Consider using the equivalent let +nondep to indicate the intent.

tactic

have'

Similar to have, but using refine'

tactic

let

The let tactic is for adding definitions to the local context of the main goal. The definition can be unfolded, unlike definitions introduced by have.

let x : t := e adds the definition x : t := e if e is a term of type t.
let x := e uses the type of e for t.
let : t := e and let := e use this for the name of the hypothesis.
let pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that let only one applicable constructor. For example, given p : α × β × γ, let ⟨x, y, z⟩ := p produces the local variables x : α, y : β, and z : γ.
The syntax let (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the let term.

Properties and relations

Unlike have, it is possible to unfold definitions introduced using let, using tactics such as simp, dsimp, unfold, and subst.
The clear_value tactic turns a let definition into a have definition after the fact. The tactic might fail if the local context depends on the value of the variable.
The let tactic is preferred for data (non-propositions).
Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons.

tactic

let rec

let rec f : t := e adds a recursive definition f to the current goal. The syntax is the same as term-mode let rec.

The tactic supports all the same syntax variants and options as the let term.

tactic

letI

letI behaves like let, but inlines the value instead of producing a let term.

tactic

let'

Similar to let, but using refine'

14.3.5. 配置🔗

许多策略是可配置的。按照惯例，策略共享配置语法，使用 optConfig 进行描述。策略的文档中介绍了每个策略可用的特定选项。

syntaxTactic Configuration

策略配置由零个或多个配置项组成：

Configuration options for tactics. optConfig ::=
    Configuration options for tactics. A configuration item for a tactic configuration. configItem*

syntaxTactic Configuration Items

每个配置项都有一个与基础策略选项相对应的名称。可以使用前缀 + 和 - 启用或禁用布尔选项：

A configuration item for a tactic configuration. configItem ::=
    A configuration item for a tactic configuration. `+opt` is short for `(opt := true)`. It sets the `opt` configuration option to `true`.
+ident

A configuration item for a tactic configuration. configItem ::= ...
    | A configuration item for a tactic configuration. `-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
-ident

可以使用类似于命名函数参数的语法为选项分配特定值：

A configuration item for a tactic configuration. configItem ::= ...
    | A configuration item for a tactic configuration. `(opt := val)` sets the `opt` configuration option to `val`.

As a special case, `(config := ...)` sets the entire configuration.
(ident := term)

最后保留名称config；它用于将一整套选项作为数据结构传递。预期的具体类型取决于策略。

A configuration item for a tactic configuration. configItem ::= ...
    | A configuration item for a tactic configuration. `(opt := val)` sets the `opt` configuration option to `val`.

As a special case, `(config := ...)` sets the entire configuration.
(config := term)

14.3.6. 命名空间和选项管理🔗

可以使用与术语中相同的语法在策略脚本中调整命名空间和选项。

tactic

set_option

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

tactic

open

open Foo in tacs (the tactic) acts like open Foo at command level, but it opens a namespace only within the tactics tacs.

14.3.6.1. 控制展开🔗

默认情况下，仅展开标记为可简化的定义，检查定义等价时除外。这些运算符允许针对策略脚本的某些部分调整此默认值。

tactic

with_reducible_and_instances

with_reducible_and_instances tacs executes tacs using the .instances transparency setting. In this setting only definitions tagged as [reducible] or type class instances are unfolded.

tactic

with_reducible

with_reducible tacs executes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

tactic

with_unfolding_all

with_unfolding_all tacs executes tacs using the .all transparency setting. In this setting all definitions that are not opaque are unfolded.

14.1.	运行策略
14.2.	阅读校样状态
14.3.	策略语言
14.4.	选项
14.5.	策略参考
14.6.	使用 `conv` 进行有针对性的重写
14.7.	命名绑定变量
14.8.	定制策略