Lean 语言参考

14.2. 阅读校样状态🔗

验证状态下的目标按顺序显示，主要目标位于顶部。 目标可以是命名的，也可以是匿名的。 命名目标在顶部用 case 表示（称为 case label），而匿名目标则没有此类指示符。 策略通常根据构造函数名称、参数名称、结构字段名称或策略实现的推理步骤的性质来分配目标名称。

Named goals

该证明状态包含四个目标，所有目标均已命名。 这是Monad Option实例合法的证明的一部分（即提供LawfulMonad Option实例），并且案例名称（下面突出显示）来自LawfulMonad的字段名称。

α:Type ?u.9β:Type ?u.9f:α → βx:Option α⊢ (do let a ← x pure (f a)) = f <$> xα:Type ?u.9β:Type ?u.9f:Option (α → β)x:Option α⊢ (do let x_1 ← f x_1 <$> x) = f <*> xα:Type ?u.9β:Type ?u.9x:αf:α → Option β⊢ pure x >>= f = f xα:Type ?u.9β:Type ?u.9γ:Type ?u.9x:Option αf:α → Option βg:β → Option γ⊢ x >>= f >>= g = x >>= fun x => f x >>= g
Anonymous Goals

该证明状态包含单个匿名目标。

n:Natk:Nat⊢ n + k = k + n

case 和 case'策略可用于使用所需目标的名称来选择新的主要目标。 当在本身具有名称的目标上下文中分配名称时，新目标的名称将附加到主目标的名称中，并在它们之间加一个点 ('.', Unicode FULL STOP (0x2e))。

Hierarchical Goal Names

在尝试证明 ∀ (n k : Nat), n + k = k + n 的过程中，可能会出现以下证明状态：

k:Nat⊢ 0 + k = k + 0k:Natn✝:Nata✝:n✝ + k = k + n✝⊢ n✝ + 1 + k = k + (n✝ + 1)

在 ⊢ 0 + 0 = 0 + 0n✝:Nata✝:0 + n✝ = n✝ + 0⊢ 0 + (n✝ + 1) = n✝ + 1 + 0k:Natn✝:Nata✝:n✝ + k = k + n✝⊢ n✝ + 1 + k = k + (n✝ + 1) 之后，两个新案例的名称以 zero 作为前缀，因为它们是在名为 zero 的目标中创建的：

⊢ 0 + 0 = 0 + 0n✝:Nata✝:0 + n✝ = n✝ + 0⊢ 0 + (n✝ + 1) = n✝ + 1 + 0k:Natn✝:Nata✝:n✝ + k = k + n✝⊢ n✝ + 1 + k = k + (n✝ + 1)

每个目标都包含一系列假设和期望的结论。 每个假设都有一个名称和类型；结论是一种类型。 假设是某种类型的任意元素或被假定为真的陈述。

Assumption Names and Conclusion

这个目标有四个假设：

α:Type ?u.3x:αxs:List αih:xs ++ [] = xs⊢ x :: xs ++ [] = x :: xs

他们是：

  • α，任意类型

  • x、任意α

  • xs，任意 List α

  • ih，归纳假设，断言将空列表附加到 xs 等于 xs。

结论是这样的陈述：在归纳假设中的等式两边添加 x 会产生相等的列表。

一些假设是 inaccessible、 ，这意味着它们不能通过名称显式引用。 当创建假设时没有指定名称或假设的名称被后来的假设所掩盖时，就会出现无法访问的假设。 无法获得的假设应被视为匿名；它们被呈现得好像它们有名称一样，因为它们可能会在后面的假设或结论中被引用，并且显示名称可以使这些引用彼此区分。 特别是，难以接近的假设在其名称后用匕首（†）表示。

Accessible Assumption Names

在这种证明状态下，所有假设都是可以实现的。

α:Type ?u.3β:Type ?u.3f:α → βx:Option α⊢ (do let a ← x pure (f a)) = f <$> x
Inaccessible Assumption Names

在这个证明状态下，只有第一个和第三个假设是可用的。 第二个和第四个是无法访问的，它们的名字中包含一把匕首，以表明它们无法被引用。

α:Type ?u.3β✝:Type ?u.3f:α → β✝x✝:Option α⊢ (do let a ← x✝ pure (f a)) = f <$> x✝

仍然可以使用无法达到的假设。 策略（例如 assumption 或 simp）可以扫描整个假设列表，找到有用的假设，而 contradiction 可以通过找到不可能的假设而不命名它来消除当前目标。 其他策略（例如 rename_i 和 next）可用于命名不可访问的假设，从而使它们可访问。 此外，假设可以通过其类型来引用，方法是将类型写在单个 guillemets 中。

syntaxAssumptions by Type

术语周围的单个 guillemets 表示对该类型范围内某个术语的引用。

term ::= ...
    | `‹t›` resolves to an (arbitrary) hypothesis of type `t`.
It is useful for referring to hypotheses without accessible names.
`t` may contain holes that are solved by unification with the expected type;
in particular, `‹_›` is a shortcut for `by assumption`.
‹term›

这可以用来通过定理陈述而不是名称来引用局部引理，或者用来引用假设，无论它们是否有明确的名称。

Assumptions by Type

在下面的证明中，重复使用 cases 来分析数字。 在证明的开始，该数字被命名为 x，但 cases 为后续数字生成了一个不可访问的名称。 该证明没有提供名称，而是利用了这样一个事实：在任何给定时间都存在一个 Nat 类型的假设，并使用 ‹Nat› 来引用它。 迭代后，有一个假设 n + 3 < 3，contradiction 可使用该假设从考虑中删除目标。

example : x < 3 → x ∈ [0, 1, 2] := x:Nat⊢ x < 3 → x ∈ [0, 1, 2] x:Nata✝:x < 3⊢ x ∈ [0, 1, 2] iterate 3 a✝:0 + 1 + 1 < 3⊢ 0 + 1 + 1 ∈ [0, 1, 2]n✝:Nata✝:n✝ + 1 + 1 + 1 < 3⊢ n✝ + 1 + 1 + 1 ∈ [0, 1, 2] a✝:0 + 1 + 1 < 3⊢ 0 + 1 + 1 ∈ [0, 1, 2] All goals completed! 🐙 All goals completed! 🐙
Live ↪
Assumptions by Type, Outside Proofs

Single-guillemet 语法也适用于证明之外：

2#eval let x := 1 let y := 2 ‹Nat› 
2

然而，对于非命题来说，这通常不是一个好主意——当选择类型的哪个元素很重要时，最好显式选择它。

Live ↪

14.2.1. 隐藏证明和大项🔗

证明状态中的项可能相当大，并且可能有很多假设。 由于定义证明的无关性，证明术语通常提供很少的有用信息。 默认情况下，它们不会显示在证明状态的目标中，除非它们是 atomic，这意味着它们不包含子项。 隐藏校样由两个选项控制：pp.proofs 打开和关闭该功能，而 pp.proofs.threshold 确定校样隐藏的大小阈值。

Hiding Proof Terms

在此证明状态下，0 < n 的证明被隐藏。

n:Nati:Fin ngt:↑i > 5⊢ ⟨0, ⋯⟩ < i
🔗option
pp.proofs

Default value: false

(pretty printer) display proofs when true, and replace proofs appearing within expressions by ⋯ when false

🔗option
pp.proofs.threshold

Default value: 0

(pretty printer) when pp.proofs is false, controls the complexity of proofs at which they begin being replaced with ⋯

此外，当非证明项太大时，它们可能会被隐藏。 特别是，Lean 将隐藏低于可配置深度阈值的术语，并且一旦打印了一定数量的术语，它将隐藏术语的其余部分。 可以使用选项 pp.deepTerms 启用或禁用显示深度术语，并且可以使用选项 pp.deepTerms.threshold 配置深度阈值。 漂亮打印机步骤的最大数量可以使用选项 pp.maxSteps 进行配置。 打印非常大的术语可能会导致工具速度减慢甚至堆栈溢出；调整这些选项的值时请保持保守。

🔗option
pp.deepTerms

Default value: false

(pretty printer) display deeply nested terms, replacing them with ⋯ if set to false

🔗option
pp.deepTerms.threshold

Default value: 50

(pretty printer) when pp.deepTerms is false, the depth at which terms start being replaced with ⋯

🔗option
pp.maxSteps

Default value: 5000

(pretty printer) maximum number of expressions to visit, after which terms will pretty print as ⋯

14.2.2. 元变量🔗

以问号开头的术语是 metavariables，对应于未知值。 它们可能代表 universe 级别或术语。 当还没有足够的信息来确定值时，一些元变量会作为 Lean 的精化过程的一部分出现。 这些元变量的名称末尾有一个数字部分，例如 ?m.392 或 ?u.498。 其他元变量是由于策略或 合成孔而出现的。 这些元变量的名称没有数字部分。 由策略生成的元变量经常显示为 case labels 与元变量名称匹配的目标。

Universe Level Metavariables

在这个证明状态下，α 的 宇宙层级 是未知的：

α:Type ?u.4x:αxs:List αelem:x ∈ xs⊢ xs.length > 0
Type Metavariables

在此证明状态下，列表元素的类型未知。 元变量会重复，因为未知类型在两个位置必须相同。

x:?m.8xs:List ?m.8elem:x ∈ xs⊢ xs.length > 0
Metavariables in Proofs

在这种证明状态下，

i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < k

应用策略i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?mi:Natj:Natk:Nath1:i < jh2:j < k⊢ ?m < ki:Natj:Natk:Nath1:i < jh2:j < k⊢ Nat 会导致以下证明状态，其中传递性步骤 ?m 的中间值未知：

i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?mi:Natj:Natk:Nath1:i < jh2:j < k⊢ ?m < ki:Natj:Natk:Nath1:i < jh2:j < k⊢ Nat
Explicitly-Created Metavariables

显式命名的漏洞由元变量表示，并且还产生证明目标。 在这种证明状态下，

i:Natj:Natk:Nath1:i < jh2:j < k⊢ i < k

应用策略i:Natj:Natk:Nath1:i < jh2:j < k⊢ Nati:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?middlei:Natj:Natk:Nath1:i < jh2:j < k⊢ ?middle < k 会导致以下证明状态，其中传递性步骤 ?middle 的中间值未知，并且已为术语中的每个命名孔创建了目标：

i:Natj:Natk:Nath1:i < jh2:j < k⊢ Nati:Natj:Natk:Nath1:i < jh2:j < k⊢ i < ?middlei:Natj:Natk:Nath1:i < jh2:j < k⊢ ?middle < k

可以使用 pp.mvars 禁用元变量编号的显示。 当使用 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd` and checks that they match the contents of the docstring. Basic example: ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` This checks that there is such an error and then consumes the message. By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings: ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` or only errors ```lean #guard_msgs(error) in example : α := sorry ``` In the previous example, since warnings are not captured there is a warning on `sorry`. We can drop the warning completely with ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses: ``` #guard_msgs (configElt,*) in cmd ``` By default, the configuration list is `(check all, whitespace := normalized, ordering := exact, positions := false)`. Message filters select messages by severity: - `info`, `warning`, `error`: (non-trace) messages with the given severity level. - `trace`: trace messages - `all`: all messages. The filters can be prefixed with the action to take: - `check` (the default): capture and check the message - `drop`: drop the message - `pass`: let the message pass through If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in left-to-right order, with an implicit `pass all` at the end. Whitespace handling (after trimming leading and trailing whitespace): - `whitespace := exact` requires an exact whitespace match. - `whitespace := normalized` converts all newline characters to a space before matching (the default). This allows breaking long lines. - `whitespace := lax` collapses whitespace to a single space before matching. Message ordering: - `ordering := exact` uses the exact ordering of the messages (the default). - `ordering := sorted` sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering. Position reporting: - `positions := true` reports the ranges of all messages relative to the line on which `#guard_msgs` appears. - `positions := false` does not report position info. Substring matching: - `substring := true` checks that the docstring appears as a substring of the output (after whitespace normalization). This is useful when you only care about part of the message. - `substring := false` (the default) requires exact matching (modulo whitespace normalization). Stabilizing output: When messages contain autogenerated names (e.g., metavariables like `?m.47`), the output may differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like `_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. The command elaborator has special support for `#guard_msgs` for linting. The `#guard_msgs` itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for *all* top-level commands, which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if `#guard_msgs` is not present. #guard_msgs 等将 Lean 的输出与所需字符串进行匹配的功能时，这非常有用，这在为自定义策略编写测试时非常有用。

🔗option
pp.mvars

Default value: true

(pretty printer) display names of metavariables when true, and otherwise display them as '?' (for expression metavariables) and as '' (for universe level metavariables)