Lean 语言参考手册

19.2. 逻辑连接词🔗

合取实现为归纳定义的命题 And。 构造器 And.intro 表示合取的引入规则：要证明合取，只需分别证明两个合取项。 类似地，And.elim 表示消去规则：给定合取的证明，以及一个假设两个合取项成立的其他命题的证明，就可以证明该命题。 由于 And 是 至多单元素类型，And.elim 也可参与数据计算。 但它不应与 PProd 混淆：使用选择公理等不可计算的推理原则定义数据（包括 Prod）会使 Lean 无法编译和运行所得程序，而在命题证明中使用它们则没有这个问题。

在 策略证明中，可以显式使用 And.intro，并通过 apply 证明合取，但更常见的是使用 constructor。 当证明目标中嵌套了多个合取时，可以使用 and_intros 在各个相关位置应用 And.intro。 上下文中的合取假设可以用 cases、使用 let 或 match 进行模式匹配，或用 rcases 化简。

🔗结构体
And (a b : Prop) : Prop
And (a b : Prop) : Prop

And a b（或 a ∧ b）是命题的合取。它可以像一对值一样构造和解构：若 ha : a 且 hb : b，则 ⟨ha, hb⟩ : a ∧ b；若 h : a ∧ b，则 h.left : a 且 h.right : b。

标识符中记法的约定：

  • 标识符中 ∧ 的推荐拼写是 and。

构造子

And.intro

And.intro : a → b → a ∧ b 是 And 运算的构造子。

字段

left : a

从合取中提取左合取项。若 h : a ∧ b，则 h.left（也记作 h.1）是 a 的证明。

right : b

从合取中提取右合取项。若 h : a ∧ b，则 h.right（也记作 h.2）是 b 的证明。

🔗定义
And.elim.{u_1} {a b : Prop} {α : Sort u_1} (f : a → b → α) (h : a ∧ b) :
  α
And.elim.{u_1} {a b : Prop} {α : Sort u_1}
  (f : a → b → α) (h : a ∧ b) : α

And 的非依赖消去器。

析取实现为归纳定义的命题 Or。 它有两个构造器，分别对应两个引入规则：证明任一析取项即可证明析取。 虽然 Or 的定义与 Sum 类似，但实际使用时差异很大。 由于 Sum 是类型，可以检查给定值由哪一个构造器创建。 另一方面，Or 构成命题：无法检查证明析取的项来确定哪一项为真。 换言之，由于 Or 不是 至多单元素类型，其证明不能参与计算。

在 策略证明中，可以显式使用任一构造器（Or.inl 或 Or.inr），并通过 apply 证明析取。 left 和 right 策略分别选择左、右析取项。 上下文中的析取假设可以用 cases、使用 match 进行模式匹配，或用 rcases 化简。

🔗归纳谓词
Or (a b : Prop) : Prop
Or (a b : Prop) : Prop

Or a b（或 a ∨ b）是命题的析取。Or 有两个构造子，分别是 Or.inl : a → a ∨ b 和 Or.inr : b → a ∨ b；可使用 match 或 cases 把一个 Or 假设解构成两种情形。

标识符中记法的约定：

  • 标识符中 ∨ 的推荐拼写是 or。

构造子

Or.inl {a b : Prop} (h : a) : a ∨ b

Or.inl 是向 Or 的“左注入”。若 h : a，则 Or.inl h : a ∨ b。

Or.inr {a b : Prop} (h : b) : a ∨ b

Or.inr 是向 Or 的“右注入”。若 h : b，则 Or.inr h : a ∨ b。

当任一析取项是 可判定的时，就可以使用 Or 计算数据。 这是因为判定过程的结果提供了合适的分支条件。

🔗定义
Or.by_cases.{u} {p q : Prop} [Decidable p] {α : Sort u} (h : p ∨ q)
  (h₁ : p → α) (h₂ : q → α) : α
Or.by_cases.{u} {p q : Prop} [Decidable p]
  {α : Sort u} (h : p ∨ q) (h₁ : p → α)
  (h₂ : q → α) : α

当左析取项可判定时，按 Or 的情形构造一个非 Prop 值。

🔗定义
Or.by_cases'.{u} {q p : Prop} [Decidable q] {α : Sort u} (h : p ∨ q)
  (h₁ : p → α) (h₂ : q → α) : α
Or.by_cases'.{u} {q p : Prop}
  [Decidable q] {α : Sort u} (h : p ∨ q)
  (h₁ : p → α) (h₂ : q → α) : α

当右析取项可判定时，按 Or 的情形构造一个非 Prop 值。

否定并不编码为归纳类型；¬P 定义为 P → False。 换言之，要证明否定，只需假设被否定的陈述并推出矛盾。 这也意味着，可以从某命题及其否定的证明立即推出 False，再用它证明任意命题或构造任意类型的元素。

🔗定义
Not (a : Prop) : Prop
Not (a : Prop) : Prop

Not p（或 ¬p）是 p 的否定。它定义为 p → False，因此若目标为 ¬p，可使用 intro h 将目标变为 h : p ⊢ False；若已有 hn : ¬p 和 h : p，则 hn h : False，而 (hn h).elim 可证明任何命题。 更多信息：命题逻辑

标识符中记法的约定：

  • 标识符中 ¬ 的推荐拼写是 not。

🔗定义
absurd.{v} {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b
absurd.{v} {a : Prop} {b : Sort v}
  (h₁ : a) (h₂ : ¬a) : b

任何命题都可由两个互相矛盾的假设推出。示例：

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

更多信息：命题逻辑

🔗定义
Not.elim.{u_1} {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) : α
Not.elim.{u_1} {a : Prop} {α : Sort u_1}
  (H1 : ¬a) (H2 : a) : α

否定的 ex falso：由 ¬a 和 a 可推出任何命题。它等同于交换实参后的 absurd，但位于 Not 命名空间中，因而可使用投影记法。

蕴含使用 命题 宇宙中的函数类型表示。 要证明 A → B，只需证明 B，同时假设 A。 这对应于 Lean.Parser.Term.fun : termfun 的类型规则。 类似地，函数应用的类型规则对应于肯定前件：给定 A → B 的证明和 A 的证明，就可以证明 B。

真值函数蕴含

将蕴含表示为命题宇宙中的函数，等价于传统定义 A → B 为 (¬A) ∨ B。 这可以使用命题外延和排中律证明：

theorem truth_functional_imp {A B : Prop} : ((¬ A) ∨ B) = (A → B) := A:PropB:Prop⊢ (¬A ∨ B) = (A → B) A:PropB:Prop⊢ ¬A ∨ B ↔ A → B A:PropB:Prop⊢ ¬A ∨ B → A → BA:PropB:Prop⊢ (A → B) → ¬A ∨ B A:PropB:Prop⊢ ¬A ∨ B → A → B A:PropB:Proph:¬Aa:A⊢ BA:PropB:Proph:Ba:A⊢ B A:PropB:Proph:¬Aa:A⊢ BA:PropB:Proph:Ba:A⊢ B All goals completed! 🐙 A:PropB:Prop⊢ (A → B) → ¬A ∨ B A:PropB:Proph:A → B⊢ ¬A ∨ B A:PropB:Proph:A → Bh✝:A⊢ ¬A ∨ BA:PropB:Proph:A → Bh✝:¬A⊢ ¬A ∨ B A:PropB:Proph:A → Bh✝:A⊢ ¬A ∨ B A:PropB:Proph:A → Bh✝:A⊢ B; All goals completed! 🐙 A:PropB:Proph:A → Bh✝:¬A⊢ ¬A ∨ B A:PropB:Proph:A → Bh✝:¬A⊢ ¬A; All goals completed! 🐙
在线查看 ↪

逻辑等价（即“当且仅当”）使用一个结构表示，该结构等价于两个方向蕴含的合取。

🔗结构体
Iff (a b : Prop) : Prop
Iff (a b : Prop) : Prop

当且仅当，即逻辑双蕴含。a ↔ b 表示 a 蕴含 b，反之亦然。 由 propext 可知，这意味着 a 与 b 相等，因此任何包含 a 的表达式都等价于把其中 a 换成 b 后的对应表达式。

标识符中记法的约定：

  • 标识符中 ↔ 的推荐拼写是 iff。

  • 标识符中 <-> 的推荐拼写是 iff（应优先使用 ↔，而不是 <->）。

构造子

Iff.intro

若 a → b 且 b → a，则 a 与 b 等价。

字段

mp : a → b

当且仅当的肯定前件式。若 a ↔ b 且 a，则 b。

mpr : b → a

反向的当且仅当肯定前件式。若 a ↔ b 且 b，则 a。

🔗定义
Iff.elim.{u_1} {a b : Prop} {α : Sort u_1} (f : (a → b) → (b → a) → α)
  (h : a ↔ b) : α
Iff.elim.{u_1} {a b : Prop} {α : Sort u_1}
  (f : (a → b) → (b → a) → α)
  (h : a ↔ b) : α

Iff 的非依赖消去器。

语法命题连接词

除蕴含外，逻辑连接词通常使用专用语法，而不是使用它们的定义名称：

term ::= ...
    | term ∧ term
term ::= ...
    | term ∨ term
term ::= ...
    | ¬ term
term ::= ...
    | term ↔ term