Lean 语言参考

19.3. 量词🔗

正如蕴涵在 Prop 中实现为普通函数类型一样，全称量化在 Prop 中实现为依赖函数类型。 由于 Prop 是 必然，因此 codomain 是 Prop 的任何函数类型本身也是 Prop，即使 domain 是 Type 也是如此。 依赖函数的类型规则与全称量化的引入和消除规则精确匹配：如果谓词对于任意选择的类型元素成立，那么它就全称成立。 如果一个谓词普遍成立，那么它可以实例化为任何个体的证明。

syntaxUniversal Quantification
term ::= ...
    | ∀ ident ident* (: term)?, term
term ::= ...
    | forall ident ident* (: term)?, term
term ::= ...
    | ∀ (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole | bracketedBinder) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole | bracketedBinder)*, term
term ::= ...
    | forall (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole | bracketedBinder) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole | bracketedBinder)*, term

通用量词绑定一个或多个变量，这些变量随后位于最终术语的范围内。 标识符也可以是_。 使用带括号的类型注释，多个绑定变量可以具有不同的类型，而不带括号的变体则要求所有变量具有相同的类型。

尽管全称量词由函数表示，但它们的证明不应被视为计算。 由于证明无关性和命题的消除限制，无法使用这些证明来实际计算数据。 因此，他们可以自由地使用不易计算的推理原理，例如经典的选择公理。

存在量化被实现为类似于 Subtype 和 Sigma 的结构：它包含 witness，它是满足谓词的值，以及见证人实际上满足谓词的证明。 换句话说，它是依赖对类型的一种形式。 与 Subtype 和 Sigma 不同，它是一个 命题；这意味着程序通常不能使用存在语句的证明来获取满足谓词的值。

编写证明时，exists策略允许为（可能嵌套的）存在性陈述指定一个（或多个）证人。 另一方面，constructor策略为见证人创建一个 元变量；提供谓词的证明也可以解决元变量。 存在假设的组成部分可以通过模式匹配与 let 或 match 以及使用 cases 或 rcases 单独提供。

Proving Existential Statements

当证明存在一些自然数是 4 和 5 之和时，exists策略期望提供总和，使用 trivial 构造相等证明：

theorem ex_four_plus_five : ∃ n, 4 + 5 = n := ⊢ ∃ n, 4 + 5 = n All goals completed! 🐙

另一方面，constructor策略需要一个证明。 rfl策略导致总和被确定为检查 定义等价 的副作用。

theorem ex_four_plus_five' : ∃ n, 4 + 5 = n := ⊢ ∃ n, 4 + 5 = n ⊢ 4 + 5 = ?w⊢ Nat All goals completed! 🐙
Live ↪
🔗inductive predicate
Exists.{u} {α : Sort u} (p : α → Prop) : Prop
Exists.{u} {α : Sort u} (p : α → Prop) :
  Prop

Existential quantification. If p : α → Prop is a predicate, then ∃ x : α, p x asserts that there is some x of type α such that p x holds. To create an existential proof, use the exists tactic, or the anonymous constructor notation ⟨x, h⟩. To unpack an existential, use cases h where h is a proof of ∃ x : α, p x, or let ⟨x, hx⟩ := h where `.

Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal. One consequence of this is that it is impossible to recover the witness of an existential from the mere fact of its existence. For example, the following does not compile:

example (h : ∃ x : Nat, x = x) : Nat :=
  let ⟨x, _⟩ := h  -- fail, because the goal is `Nat : Type`
  x

The error message recursor 'Exists.casesOn' can only eliminate into Prop means that this only works when the current goal is another proposition:

example (h : ∃ x : Nat, x = x) : True := let ⟨x, _⟩ := h -- ok, because the goal is `True : Prop` trivial

Constructors

Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α)
  (h : p w) : Exists p

Existential introduction. If a : α and h : p a, then ⟨a, h⟩ is a proof that ∃ x : α, p x.

syntaxExistential Quantification
term ::= ...
    | ∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident* (: term)?, term
term ::= ...
    | exists `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident* (: term)?, term
term ::= ...
    | ∃ bracketedExplicitBinders bracketedExplicitBinders*, term
term ::= ...
    | exists bracketedExplicitBinders bracketedExplicitBinders*, term

存在量词绑定一个或多个变量，这些变量在最后一项的范围内。 标识符也可以是_。 使用带括号的类型注释，多个绑定变量可以具有不同的类型，而不带括号的变体则要求所有变量具有相同的类型。 如果绑定多个变量，则结果是 Exists 的多个实例，嵌套在右侧。

🔗def
Exists.choose.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : α
Exists.choose.{u_1} {α : Sort u_1}
  {p : α → Prop} (P : ∃ a, p a) : α

Extract an element from an existential statement, using Classical.choose.