3. 命题与证明🔗

前一章你已经看到了在 Lean 中定义对象和函数的一些方法。在本章中，我们还将开始解释如何用依值类型论的语言来编写数学命题和证明。

3.1. 命题即类型🔗

证明在依值类型论语言中定义的对象的断言（assertion）的一种策略是在定义语言之上分层断言语言和证明语言。但是，没有理由以这种方式重复使用多种语言：依值类型论是灵活和富有表现力的，我们也没有理由不能在同一个总框架中表示断言和证明。

例如，我们可引入一种新类型 Prop，来表示命题，然后引入用其他命题构造新命题的构造子。

def Implies (p q : Prop) : Prop := p → q

And (a b : Prop) : Prop#check And

And (a b : Prop) : Prop

Or (a b : Prop) : Prop#check Or

Or (a b : Prop) : Prop

Not (a : Prop) : Prop#check Not

Not (a : Prop) : Prop

Implies (p q : Prop) : Prop#check Implies

Implies (p q : Prop) : Prop

variable (p q r : Prop)

p ∧ q : Prop#check And p q

p ∧ q : Prop

p ∧ q ∨ r : Prop#check Or (And p q) r

p ∧ q ∨ r : Prop

Implies (p ∧ q) (q ∧ p) : Prop#check Implies (And p q) (And q p)

Implies (p ∧ q) (q ∧ p) : Prop

对每个元素 p : Prop，可以引入另一个类型 Proof p，作为 p 的证明的类型。“公理”是这个类型中的常值。

def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p

Proof (p : Prop) : Type#check Proof

Proof (p : Prop) : Type

axiom and_commut (p q : Prop) : Proof (Implies (And p q) (And q p))

variable (p q : Prop)

and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))#check and_commut p q

and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))

然而，除了公理之外，我们还需要从旧证明中建立新证明的规则。例如，在许多命题逻辑的证明系统中，我们有肯定前件式（modus ponens）推理规则:

如果能证明 Implies p q 和 p，则能证明 q。

我们可以如下地表示它：

def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p

axiom modus_ponens (p q : Prop) :
  Proof (Implies p q) → Proof p →
  Proof q

命题逻辑的自然演绎系统通常也依赖于以下规则：

假设以 p 为前提，我们有 q 的证明。那么我们可以“取消”该假设并获得 Implies p q 的证明。

我们可以将其呈现如下：

def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p

axiom implies_intro (p q : Prop) :
  (Proof p → Proof q) → Proof (Implies p q)

这种方法将为我们提供建立断言和证明的合理方式。确定表达式 t 是断言 p 的正确证明，只需检查 t 是否具有类型 Proof p。

然而，可以进行一些简化。首先，我们可以通过将 Proof p 与 p 本身合并来避免重复书写术语 Proof。换句话说，只要我们有 p : Prop，我们就可以将 p 解释为一个类型，即其证明的类型。然后我们可以将 t : p 读作 t 是 p 的证明的断言。

此外，一旦我们进行了这种识别，蕴涵规则表明我们可以在 Implies p q 和 p → q 之间来回转换。换句话说，命题 p 和 q 之间的蕴涵对应于拥有一个将 p 的任何元素映射到 q 的元素的函数。结果，连接词 Implies 的引入完全是多余的：我们可以使用依值类型论中通常的函数空间构造子 p → q 作为我们的蕴涵概念。

这是构造演算（Calculus of Constructions）所采用的方法，因此也是 Lean 所采用的方法。自然演绎证明系统中的蕴涵规则与控制函数抽象和应用的规则完全对应，这一事实是 Curry-Howard 同构（Curry-Howard isomorphism）的一个实例，有时称为 命题即类型（propositions-as-types）范式。事实上，类型 Prop 是 Sort 0 的语法糖，即上一章描述的类型层次结构的最底层。此外，Type u 也只是 Sort (u+1) 的语法糖。Prop 有一些特殊功能，但像其他类型宇宙一样，它在箭头构造子下是封闭的：如果我们有 p q : Prop，那么 p → q : Prop。

关于命题即类型，至少有两种思考方式。对于那些持逻辑和数学构造主义观点的人来说，这是对命题含义的忠实呈现：命题 p 代表一种数据类型，即构成证明的数据类型的规范。p 的证明仅仅是正确类型的对象 t : p。

那些不倾向于这种意识形态的人可以将其视为一种简单的编码技巧。对于每个命题 p，我们关联一个类型，如果 p 为假，则该类型为空；如果 p 为真，则该类型有一个元素，比如 *。在后一种情况下，我们说（与 p 关联的类型）是 有居留的（inhabited）。恰好函数应用和抽象的规则可以方便地帮助我们跟踪 Prop 的哪些元素是有居留的。因此，构造一个元素 t : p 告诉我们 p 确实为真。你可以将 p 的居留者视为“p 为真这一事实”。p → q 的证明使用“p 为真这一事实”来获得“q 为真这一事实”。

事实上，如果 p : Prop 是任何命题，Lean 的内核将任何两个元素 t1 t2 : p 视为定义上相等，就像它将 (fun x => t) s 和 t[s/x] 视为定义上相等一样。这被称为 证明无关性（proof irrelevance），并且与上一段中的解释一致。这意味着即使我们可以将证明 t : p 视为依值类型论语言中的普通对象，它们除了 p 为真这一事实之外不携带任何信息。

我们建议的思考命题即类型范式的两种方式在根本上有所不同。从构造主义的观点来看，证明是抽象的数学对象，由依值类型论中的适当表达式 指称（denoted）。相反，如果我们从上述编码技巧的角度思考，那么表达式本身并不指称任何有趣的东西。相反，正是我们可以写下它们并检查它们是否类型正确这一事实，确保了所讨论的命题为真。换句话说，表达式本身就是证明。

在下面的阐述中，我们将在这两种说法之间来回切换，有时说一个表达式“构造”或“产生”或“返回”一个命题的证明，有时只是说它“是”这样一个证明。这类似于计算机科学家偶尔模糊语法和语义之间区别的方式，有时说程序“计算”某个函数，有时又好像程序“是”所讨论的函数一样。

无论如何，真正重要的是底线。为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项 p : Prop。为了证明该断言，我们需要展示一个项 t : p。Lean 的任务，作为一个证明助手，是帮助我们构造这样一个项 t，并验证它的格式是否良好，类型是否正确。

3.2. 使用命题作为类型🔗

在命题即类型范式中，只涉及 → 的定理可以通过 lambda 抽象和应用来证明。在 Lean 中，theorem 命令引入了一个新的定理：

                set_option linter.unusedVariables false
---
variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

将此证明与类型为 α → β → α 的表达式 fun x : α => fun y : β => x 进行比较，其中 α 和 β 是数据类型。这描述了分别接受类型为 α 和 β 的参数 x 和 y 并返回 x 的函数。t1 的证明具有相同的形式，唯一的区别是 p 和 q 是 Prop 的元素，而不是 Type 的元素。直观地说，我们对 p → q → p 的证明假设 p 和 q 为真，并使用第一个假设（平凡地）建立结论 p 为真。

请注意，theorem 命令实际上是 def 命令的一个版本：在命题和类型对应下，证明定理 p → q → p 实际上与定义关联类型的元素是一样的。对于内核类型检查器，这两者之间没有区别。

然而，定义和定理之间有一些实用的区别。正常情况下，永远没有必要展开一个定理的“定义”；通过证明无关性，该定理的任何两个证明在定义上都是相等的。一旦一个定理的证明完成，通常我们只需要知道该证明的存在；证明是什么并不重要。鉴于这一事实，Lean 将证明标记为 不可还原（irreducible），作为对解析器（更确切地说，是 繁饰器（elaborator））的提示，在处理文件时一般不需要展开它。事实上，Lean 通常能够并行地处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。此外，在定义体中引用的章节变量会自动添加为参数，但只有在定理类型中引用的变量才会被添加。这是因为证明陈述的方式不应影响正在证明的陈述。

和定义一样，#print 命令可以展示一个定理的证明：

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp

请注意，lambda 抽象 hp : p 和 hq : q 可以被视为 t1 证明中的临时假设。Lean 还允许我们使用 show 语句显式指定最终项 hp 的类型：

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p :=
  fun hp : p =>
  fun hq : q =>
  show p from hp

添加此类额外信息可以提高证明的清晰度，并有助于在编写证明时检测错误。show 命令除了注释类型外什么也不做，在内部，我们看到的所有 t1 的表示都会产生相同的项。

与普通定义一样，我们可以将 lambda 抽象变量移到冒号左侧：

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 (hp : p) (hq : q) : p := hp

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp

我们可以像函数应用一样使用定理 t1：

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 (hp : p) (hq : q) : p := hp

axiom hp : p

theorem t2 : q → p := t1 hp

axiom 声明假设给定类型的元素存在，这可能会损害逻辑一致性。例如，我们可以使用它来假设空类型 False 有一个元素：

                axiom unsound : False
-- Everything follows from false
theorem ex : 1 = 0 :=
  False.elim unsound

声明“公理” hp : p 等同于声明 p 为真，由 hp 见证。将定理 t1 : p → q → p 应用于 p 为真这一事实 hp : p，得到定理 t1 hp : q → p。

回想一下，我们也可以将定理 t1 写成如下形式：

set_option linter.unusedVariables false

theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp

t1 的类型现在是 ∀ {p q : Prop}, p → q → p。我们可以将其读作断言“对于每一对命题 p q，我们有 p → q → p。”例如，我们可以将所有参数移到冒号右侧：

set_option linter.unusedVariables false

theorem t1 : ∀ {p q : Prop}, p → q → p :=
  fun {p q : Prop} (hp : p) (hq : q) => hp

如果 p 和 q 已被声明为变量，Lean 会自动为我们泛化它们：

                variable {p q : Prop}

theorem t1 : p → q → p := fun (hp : p) (unused variable `hq`

Note: This linter can be disabled with `set_option linter.unusedVariables false`hq : q) => hp

当我们以这种方式泛化 t1 时，我们就可以将它应用于不同的命题对，从而得到一般定理的不同实例。

set_option linter.unusedVariables false

theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp

variable (p q r s : Prop)

t1 p q : p → q → p#check t1 p q

t1 p q : p → q → p

t1 r s : r → s → r#check t1 r s

t1 r s : r → s → r

t1 (r → s) (s → r) : (r → s) → (s → r) → r → s#check t1 (r → s) (s → r)

t1 (r → s) (s → r) : (r → s) → (s → r) → r → s

variable (h : r → s)

t1 (r → s) (s → r) h : (s → r) → r → s#check t1 (r → s) (s → r) h

t1 (r → s) (s → r) h : (s → r) → r → s

同样，使用命题即类型对应，类型为 r → s 的变量 h 可以看作是 r → s 成立的假设或前提。

作为另一个例子，让我们考虑上一章讨论的组合函数，现在用命题代替类型。

                variable (p q r s : Prop)

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=
  fun h₃ : p =>
  show r from h₁ (h₂ h₃)

作为命题逻辑的定理，t2 说了什么？

请注意，使用数字 Unicode 下标（输入为 \0、\1、\2 等）作为假设通常很有用，就像我们在本例中所做的那样。

3.3. 命题逻辑🔗

Lean 定义了所有标准的逻辑连接词和符号。命题连接词具有以下符号：

ASCII	Unicode	Editor shortcut	Definition
`True`			`True`
`False`			`False`
`Not`	`¬`	`\not`, `\neg`	`Not`
`/\`	`∧`	`\and`	`And`
`\/`	`∨`	`\or`	`Or`
`->`	`→`	`\to`, `\r`, `\imp`
`<->`	`↔`	`\iff`, `\lr`	`Iff`

它们都取 Prop 中的值。

variable (p q : Prop)

p → q → p ∧ q : Prop#check p → q → p ∧ q

p → q → p ∧ q : Prop

¬p → p ↔ False : Prop#check ¬p → p ↔ False

¬p → p ↔ False : Prop

p ∨ q → q ∨ p : Prop#check p ∨ q → q ∨ p

p ∨ q → q ∨ p : Prop

运算顺序如下：一元否定 ¬ 结合力最强，然后是 ∧，然后是 ∨，然后是 →，最后是 ↔。例如，a ∧ b → c ∨ d ∧ e 意味着 (a ∧ b) → (c ∨ (d ∧ e))。请记住，→ 是右结合的（现在参数是 Prop 的元素，而不是其他 Type，这一点没有改变），其他二元连接词也是如此。因此，如果我们有 p q r : Prop，表达式 p → q → r 读作“如果 p，那么如果 q，那么 r。”这只是 p ∧ q → r 的“柯里化”形式。

在上一章中，我们观察到 lambda 抽象可以被视为 → 的“引入规则”。在当前的设置中，它展示了如何“引入”或建立蕴涵。应用可以被视为“消去规则”，展示了如何在证明中“消去”或使用蕴涵。其他命题连接词在 Lean 的库中定义，并自动导入。每个连接词都有其规范的引入和消去规则。

3.3.1. 合取🔗

variable (p q : Prop)

example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

fun hp hq => ⟨hp, hq⟩ : p → q → p ∧ q#check fun (hp : p) (hq : q) => And.intro hp hq

fun hp hq => ⟨hp, hq⟩ : p → q → p ∧ q

example 命令声明了一个没有名字也不会永久保存的定理。本质上，它只是检查给定项是否具有指定的类型。它便于说明，我们将经常使用它。

表达式 And.left h 从证明 h : p ∧ q 创建 p 的证明。类似地，And.right h 是 q 的证明。它们常被称为左和右 与消去（and-elimination） 规则。

                  variable (p q : Prop)

example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h

我们现在可以用以下证明项证明 p ∧ q → q ∧ p。

                  variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  And.intro (And.right h) (And.left h)

请注意，与引入和与消去类似于笛卡尔积的配对和投影操作。区别在于，给定 hp : p 和 hq : q，And.intro hp hq 具有类型 p ∧ q : Prop，而给定 a : α 和 b : β，Prod.mk a b 具有类型 α × β : Type。Prod 不能用于 Prop，And 不能用于 Type。∧ 和 × 之间的相似性是 Curry-Howard 同构的另一个实例，但与蕴涵和函数空间构造子不同，∧ 和 × 在 Lean 中是分开处理的。然而，通过类比，我们刚刚构造的证明类似于交换一对中的元素的函数。

我们将在结构体和记录中看到，Lean 中的某些类型是 结构体（structures），也就是说，该类型是用单个规范的 构造子（constructor） 定义的，该构造子从一系列合适的参数构建该类型的一个元素。对于每个 p q : Prop，p ∧ q 就是一个例子：构造一个元素的规范方法是将 And.intro 应用于合适的参数 hp : p 和 hq : q。Lean 允许我们在这种情况下使用 匿名构造子（anonymous constructor） 表示法 ⟨arg1, arg2, ...⟩，当相关类型是归纳类型并可以从上下文推断时。特别地，我们经常可以写 ⟨hp, hq⟩ 而不是 And.intro hp hq：

variable (p q : Prop)

variable (hp : p) (hq : q)

⟨hp, hq⟩ : p ∧ q#check (⟨hp, hq⟩ : p ∧ q)

⟨hp, hq⟩ : p ∧ q

这些尖括号分别通过输入 \< 和 \> 获得。

Lean 提供了另一个有用的语法小工具。给定一个归纳类型 Foo 的表达式 e（可能应用于一些参数），符号 e.bar 是 Foo.bar e 的简写。这为访问函数提供了一种方便的方式，而无需打开命名空间。例如，以下两个表达式的意思是相同的：

variable (xs : List Nat)

xs.length : Nat#check List.length xs

xs.length : Nat

xs.length : Nat#check xs.length

xs.length : Nat

因此，给定 h : p ∧ q，我们可以写 h.left 来表示 And.left h，用 h.right 来表示 And.right h。因此我们可以方便地将上面的示例证明重写如下：

                  variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  ⟨h.right, h.left⟩

简洁和晦涩之间只有一线之隔，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样直截了当的构造，当 h 的类型和构造的目标很显著时，这种表示法是干净有效的。

迭代像“And”这样的构造是很常见的。Lean 还允许你展平右结合的嵌套构造子，因此这两个证明是等价的：

                  variable (p q : Prop)

example (h : p ∧ q) : q ∧ p ∧ q :=
  ⟨h.right, ⟨h.left, h.right⟩⟩

example (h : p ∧ q) : q ∧ p ∧ q :=
  ⟨h.right, h.left, h.right⟩

这也通常很有用。

3.3.2. 析取🔗

表达式 Or.intro_left q hp 从证明 hp : p 创建 p ∨ q 的证明。类似地，Or.intro_right p hq 使用证明 hq : q 创建 p ∨ q 的证明。这些是左和右 或引入（or-introduction） 规则。

                  variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp
example (hq : q) : p ∨ q := Or.intro_right p hq

或消去（or-elimination） 规则稍微复杂一些。其思想是，我们可以通过证明 r 从 p 推出以及 r 从 q 推出，来从 p ∨ q 证明 r。换句话说，这是一个分情况证明。在表达式 Or.elim hpq hpr hqr 中，Or.elim 接受三个参数：hpq : p ∨ q、hpr : p → r 和 hqr : q → r，并产生 r 的证明。在以下示例中，我们使用 Or.elim 来证明 p ∨ q → q ∨ p。

                  variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  Or.elim h
    (fun hp : p =>
      show q ∨ p from Or.intro_right q hp)
    (fun hq : q =>
      show q ∨ p from Or.intro_left p hq)

在大多数情况下，Or.intro_right 和 Or.intro_left 的第一个参数可以由 Lean 自动推断出来。因此，Lean 提供了 Or.inr 和 Or.inl，它们可以被视为 Or.intro_right _ 和 Or.intro_left _ 的简写。因此，上面的证明项可以写得更简洁：

                  variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq)

请注意，完整表达式中有足够的信息供 Lean 推断 hp 和 hq 的类型。但是，在较长版本中使用类型注释可以使证明更具可读性，并有助于捕获和调试错误。

因为 Or 有两个构造子，所以我们不能使用匿名构造子表示法。但我们仍然可以写 h.elim 而不是 Or.elim h：

                  variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  h.elim (fun hp => Or.inr hp) (fun hq => Or.inl hq)

再一次，你应该判断这些缩写是增强还是降低了可读性。

3.3.3. 否定与假🔗

否定 ¬p 实际上定义为 p → False，所以我们通过从 p 导出一个矛盾来获得 ¬p。类似地，表达式 hnp hp 从 hp : p 和 hnp : ¬p 产生一个 False 的证明。下一个例子使用这两个规则来产生 (p → q) → ¬q → ¬p 的证明。（符号 ¬ 通过输入 \not 或 \neg 产生。）

                  variable (p q : Prop)

example (hpq : p → q) (hnq : ¬q) : ¬p :=
  fun hp : p =>
  show False from hnq (hpq hp)

连接词 False 只有一个消去规则 False.elim，它表达了一个事实，即任何事物都可以从矛盾中推出。这个规则有时被称为 ex falso（ex falso sequitur quodlibet 的缩写），或 爆炸原理（principle of explosion）。

                  variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)

从虚假中推出的任意事实 q 是 False.elim 中的隐式参数，并且会自动推断出来。这种从矛盾假设中推导出任意事实的模式非常常见，并由 absurd 表示。

                  variable (p q : Prop)

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

例如，这里是 ¬p → q → (q → p) → r 的证明：

                  variable (p q r : Prop)

example (hnp : ¬p) (hq : q) (hqp : q → p) : r :=
  absurd (hqp hq) hnp

顺便说一句，就像 False 只有一个消去规则一样，True 只有一个引入规则 True.intro : True。换句话说，True 仅仅是真的，并且有一个规范的证明 True.intro。

3.3.4. 逻辑等价🔗

表达式 Iff.intro h1 h2 从 h1 : p → q 和 h2 : q → p 产生 p ↔ q 的证明。表达式 Iff.mp h 从 h : p ↔ q 产生 p → q 的证明。类似地，Iff.mpr h 从 h : p ↔ q 产生 q → p 的证明。这是 p ∧ q ↔ q ∧ p 的证明：

variable (p q : Prop)

theorem and_swap : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (fun h : p ∧ q =>
     show q ∧ p from And.intro (And.right h) (And.left h))
    (fun h : q ∧ p =>
     show p ∧ q from And.intro (And.right h) (And.left h))

and_swap p q : p ∧ q ↔ q ∧ p#check and_swap p q

and_swap p q : p ∧ q ↔ q ∧ p

variable (h : p ∧ q)

example : q ∧ p := Iff.mp (and_swap p q) h

我们可以使用匿名构造子表示法从前向和后向的证明构造 p ↔ q 的证明，我们也可以对 mp 和 mpr 使用 . 表示法。因此，前面的示例可以简洁地写成如下形式：

                  variable (p q : Prop)

theorem and_swap : p ∧ q ↔ q ∧ p :=
  ⟨ fun h => ⟨h.right, h.left⟩, fun h => ⟨h.right, h.left⟩ ⟩

example (h : p ∧ q) : q ∧ p := (and_swap p q).mp h

3.4. 引入辅助子目标🔗

这是一个介绍 Lean 提供的另一个帮助构建长证明的工具的好地方，即 have 构造，它在证明中引入了一个辅助子目标。这是一个改编自上一节的小例子：

                variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  have hq : q := h.right
  show q ∧ p from And.intro hq hp

在内部，表达式 have h : p := s; t 产生项 (fun (h : p) => t) s。换句话说，s 是 p 的证明，t 是假设 h : p 的情况下所需结论的证明，两者通过 lambda 抽象和应用结合在一起。这个简单的工具在构建长证明时非常有用，因为我们可以使用中间的 have 作为通向最终目标的垫脚石。

Lean 还支持一种从目标向后推理的结构化方式，这模仿了普通数学中的“足以证明（suffices to show）”结构。下一个例子只是交换了前一个证明中的最后两行。

                variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq : q from And.intro hq hp
  show q from And.right h

写下 suffices hq : q 给我们留下了两个目标。首先，我们必须证明它确实足以证明 q，方法是用额外的假设 hq : q 证明 q ∧ p 的原始目标。最后，我们必须证明 q。

3.5. 经典逻辑🔗

到目前为止，我们看到的引入和消去规则都是构造性的，也就是说，它们反映了基于命题即类型对应的逻辑连接词的计算理解。普通经典逻辑在此基础上增加了排中律，p ∨ ¬p。要使用这个原则，你必须打开经典命名空间。

open Classical

variable (p : Prop)

em p : p ∨ ¬p#check em p

em p : p ∨ ¬p

直观地说，构造性的“或”非常强：断言 p ∨ q 相当于知道哪种情况成立。如果 RH 代表黎曼猜想，经典数学家愿意断言 RH ∨ ¬RH，即使我们还不能断言任何一个析取项。

排中律的一个推论是双重否定消去原理：

                open Classical

theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)

双重否定消去允许人们通过假设 ¬p 并推导出 False 来证明任何命题 p，因为这相当于证明 ¬¬p。换句话说，双重否定消去允许人们进行反证法，这在构造逻辑中通常是不可能的。作为练习，你可以尝试证明逆命题，即证明 em 可以从 dne 证明。

经典公理还允许你使用可以通过诉诸 em 来证明的其他证明模式。例如，人们可以进行分情况证明：

                open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byCases
    (fun h1 : p => h1)
    (fun h1 : ¬p => absurd h1 h)

或者你可以进行反证法：

                open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byContradiction
    (fun h1 : ¬p =>
     show False from h h1)

如果你不习惯构造性思考，可能需要一些时间才能理解在哪里使用经典推理。在下面的例子中需要它，因为从构造性的角度来看，知道 p 和 q 不都为真并不一定告诉你哪一个为假：

open Classical
variable (p q : Prop)

example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
  Or.elim (em p)
    (fun hp : p =>
      Or.inr
        (show ¬q from
          fun hq : q =>
          h ⟨hp, hq⟩))
    (fun hp : ¬p =>
      Or.inl hp)

我们稍后将看到，在构造逻辑中确实存在允许排中律和双重否定消去等原则的情况，并且 Lean 支持在这种情况下使用经典推理而不依赖于排中律。

Lean 中用于支持经典推理的完整公理列表在公理与计算中讨论。

3.6. 命题有效性的例子🔗

Lean 的标准库包含许多命题逻辑有效陈述的证明，你可以自由地在自己的证明中使用所有这些证明。以下列表包括许多常见的恒等式。

交换律：

p ∧ q ↔ q ∧ p
p ∨ q ↔ q ∨ p

结合律：

(p ∧ q) ∧ r ↔ p ∧ (q ∧ r)
(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)

分配律：

p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)
p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)

其他性质：

(p → (q → r)) ↔ (p ∧ q → r)
((p ∨ q) → r) ↔ (p → r) ∧ (q → r)
¬(p ∨ q) ↔ ¬p ∧ ¬q
¬p ∨ ¬q → ¬(p ∧ q)
¬(p ∧ ¬p)
p ∧ ¬q → ¬(p → q)
¬p → (p → q)
(¬p ∨ q) → (p → q)
p ∨ False ↔ p
p ∧ False ↔ False
¬(p ↔ ¬p)
(p → q) → (¬q → ¬p)

这些需要经典推理：

(p → r ∨ s) → ((p → r) ∨ (p → s))
¬(p ∧ q) → ¬p ∨ ¬q
¬(p → q) → p ∧ ¬q
(p → q) → (¬p ∨ q)
(¬q → ¬p) → (p → q)
p ∨ ¬p
(((p → q) → p) → p)

sorry 标识符神奇地产生任何东西的证明，或者提供任何数据类型的对象。当然，作为一种证明方法，它是不可靠的（例如，你可以用它来证明 False）当文件使用或导入依赖于它的定理时，Lean 会产生严重的警告。但它对于增量构建长证明非常有用。从上到下开始编写证明，使用 sorry 填充子证明。确保 Lean 接受带有所有 sorry 的项；如果没有，则说明你需要更正错误。然后回去用实际的证明替换每个 sorry，直到没有剩余。

这里有另一个有用的技巧。你可以使用下划线 _ 作为占位符，而不是使用 sorry。回想一下，这告诉 Lean 参数是隐式的，应该自动填充。如果 Lean 尝试这样做但失败了，它会返回一条错误消息“don't know how to synthesize placeholder”（不知道如何合成占位符），后面跟着它期望的项的类型，以及上下文中可用的所有对象和假设。换句话说，对于每个未解决的占位符，Lean 报告在该点需要填充的子目标。然后，你可以通过增量填充这些占位符来构造证明。

作为参考，这里有两个取自上面列表的有效性证明示例。

                open Classical

-- distributivity
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (fun h : p ∧ (q ∨ r) =>
      have hp : p := h.left
      Or.elim (h.right)
        (fun hq : q =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩)
        (fun hr : r =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩))
    (fun h : (p ∧ q) ∨ (p ∧ r) =>
      Or.elim h
        (fun hpq : p ∧ q =>
          have hp : p := hpq.left
          have hq : q := hpq.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩)
        (fun hpr : p ∧ r =>
          have hp : p := hpr.left
          have hr : r := hpr.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩))

-- an example that requires classical reasoning
-- 一个需要经典推理的例子
example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) :=
  fun h : ¬(p ∧ ¬q) =>
  fun hp : p =>
  show q from
    Or.elim (em q)
      (fun hq : q => hq)
      (fun hnq : ¬q => absurd (And.intro hp hnq) h)

3.7. 练习🔗

证明以下恒等式，用实际证明替换 sorry 占位符。

                variable (p q r : Prop)

-- commutativity of ∧ and ∨
declaration uses 'sorry'example : p ∧ q ↔ q ∧ p := sorry
declaration uses 'sorry'example : p ∨ q ↔ q ∨ p := sorry

-- associativity of ∧ and ∨
declaration uses 'sorry'example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
declaration uses 'sorry'example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

-- distributivity
declaration uses 'sorry'example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
declaration uses 'sorry'example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry

-- other properties
declaration uses 'sorry'example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
declaration uses 'sorry'example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
declaration uses 'sorry'example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
declaration uses 'sorry'example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
declaration uses 'sorry'example : ¬(p ∧ ¬p) := sorry
declaration uses 'sorry'example : p ∧ ¬q → ¬(p → q) := sorry
declaration uses 'sorry'example : ¬p → (p → q) := sorry
declaration uses 'sorry'example : (¬p ∨ q) → (p → q) := sorry
declaration uses 'sorry'example : p ∨ False ↔ p := sorry
declaration uses 'sorry'example : p ∧ False ↔ False := sorry
declaration uses 'sorry'example : (p → q) → (¬q → ¬p) := sorry

证明以下恒等式，用实际证明替换 sorry 占位符。这些需要经典推理。

                open Classical

variable (p q r : Prop)

declaration uses 'sorry'example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := sorry
declaration uses 'sorry'example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry
declaration uses 'sorry'example : ¬(p → q) → p ∧ ¬q := sorry
declaration uses 'sorry'example : (p → q) → (¬p ∨ q) := sorry
declaration uses 'sorry'example : (¬q → ¬p) → (p → q) := sorry
declaration uses 'sorry'example : p ∨ ¬p := sorry
declaration uses 'sorry'example : (((p → q) → p) → p) := sorry

在不使用经典逻辑的情况下证明 ¬(p ↔ ¬p)。