19.3. 量词🔗

正如蕴含在 Prop 中实现为普通函数类型，全称量化在 Prop 中实现为依赖函数类型。由于 Prop 是非直谓的，任何陪域为 Prop 的函数类型本身也是 Prop，即使定义域是 Type。依赖函数的类型规则与全称量化的引入、消去规则完全对应：若谓词对类型中任意选取的元素都成立，则它对所有元素成立。若谓词对所有元素都成立，则可将其实例化为任意个体的证明。

语法全称量化

term ::= ...
    | ∀ ident ident* (: term)?, term

term ::= ...
    | forall ident ident* (: term)?, term

term ::= ...
    | ∀ (ident | hole | bracketedBinder) (ident | hole | bracketedBinder)*, term

term ::= ...
    | forall (ident | hole | bracketedBinder) (ident | hole | bracketedBinder)*, term

全称量词绑定一个或多个变量，这些变量随后在最终项中处于作用域内。标识符也可以是 _。带括号的类型注解允许多个绑定变量具有不同类型，而不带括号的形式要求它们类型相同。

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

存在量化实现为类似于 Subtype 和 Sigma 的结构：它包含一个见证（满足谓词的值），以及该见证确实满足谓词的证明。换言之，它是一种依赖对类型。与 Subtype 和 Sigma 不同，它是一个命题；这意味着程序通常不能使用存在性陈述的证明来取得满足谓词的值。

编写证明时，exists 策略允许为（可能嵌套的）存在性陈述指定一个或多个见证。另一方面，constructor 策略会为见证创建一个元变量；提供谓词证明也可能同时解出该元变量。可以使用 let 或 match 进行模式匹配，或使用 cases、rcases，分别取得存在性假设的各个组成部分。

证明存在性陈述

证明存在某个自然数等于四与五之和时，exists 策略要求提供该和，并使用 trivial 构造等式证明：

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

另一方面，constructor 策略要求提供证明。 rfl 策略在检查定义等价时会顺带确定该和。

theorem ex_four_plus_five' : ∃ n, 4 + 5 = n := by⊢ ∃ n, 4 + 5 = n
  constructorh⊢ 4 + 5 = ?ww⊢ Nat
  rflAll goals completed! 🐙

在线查看 ↪

归纳谓词

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

存在量化。若 p : α → Prop 是谓词，则 ∃ x : α, p x 断言存在某个 x，其类型为 α，并且 p x 成立。要创建存在性证明，可使用 exists 策略，或匿名构造子记法 ⟨x, h⟩。要解包存在量词，可使用 cases h，其中 h 是 ∃ x : α, p x 的证明，或使用 let ⟨x, hx⟩ := h。

由于 Lean 具有证明无关性，任意两个存在性证明都定义相等。其后果之一是，无法仅从见证存在这一事实恢复存在量词的见证。例如，以下代码无法编译：

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

错误消息 recursor 'Exists.casesOn' can only eliminate into Prop 表示，只有当前目标也是命题时，这样做才有效：

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

构造子

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

存在量词引入。若 a : α 且 h : p a，则 ⟨a, h⟩ 是 ∃ x : α, p x 的证明。

语法存在量化

term ::= ...
    | ∃ ident ident* (: term)?, term

term ::= ...
    | exists ident ident* (: term)?, term

term ::= ...
    | ∃ bracketedExplicitBinders bracketedExplicitBinders*, term

term ::= ...
    | exists bracketedExplicitBinders bracketedExplicitBinders*, term

存在量词绑定一个或多个变量，这些变量随后在最终项中处于作用域内。标识符也可以是 _。带括号的类型注解允许多个绑定变量具有不同类型，而不带括号的形式要求它们类型相同。如果绑定了多个变量，结果就是多个向右嵌套的 Exists 实例。

定义

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) : α

使用 Classical.choose 从存在性陈述中提取元素。