翻译-TPIL-03-命题与证明

至此你已了解过一些在 Lean 中定义对象和函数的方法。本章我们将介绍 如何将数学命题和证明也用依值类型论的方式书写。

3.1. 命题即类型 Propositions as Types

证明依值类型论中所定义对象的断言的一种策略是 在定义语言之上再叠加一层断言语言和证明语言。 但实际上完全没必要以这种方式增加语言层次： 依值类型论本身就足够灵活且富有表达力， 完全可以在同一个大框架内同时表示断言和证明。

比如我们可以引入一种新类型 Prop 来表示命题 并引入一些构造子以利用其他命题来构造新命题。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

def Implies (p q : Prop) : Prop := p → q
#check And
-- And (a b : Prop) : Prop
#check Or
-- Or (a b : Prop) : Prop
#check Not
-- Not (a : Prop) : Prop
#check Implies
-- Implies (p q : Prop) : Prop

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

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

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

-- and_comm 已被定义，这里起个别名 and_comm'
axiom and_comm' (p q : Prop) : Proof (Implies (And p q) (And q p))

variable (p q : Prop)
#check and_comm' p q     -- Proof (Implies (And p q) (And q p))
-- and_comm' p q : Proof (Implies (p ∧ q) (q ∧ p))

然而除了公理之外，我们还需要推理规则 以便从旧证明中建立新证明。例如， 在许多命题逻辑的证明系统中， 我们都有肯定前件 Modus Ponens 推理规则：

如果有关于 Implies p q 和 p 的证明，那么便可获得 q 的证明。

我们可用如下方式表示它：

1
2
3
4
5
6

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 →     -- (hpq ↦ hp) ↦
  Proof q                             --  hq

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

如果我们在 p 作为假设时有 q 的证明， 那么我们便有 Implies p q 的证明。

我们可用如下方式表示它：

1
2
3
4
5
6

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) →              -- (hp ↦ hq) ↦
  Proof (Implies p q)                --  hpq

这种尝试允许我们合理地构建断言和证明。 要确定表达式 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 来充当蕴含连结词。

这正是构造演算所遵循的方法，因此对于 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 的证明所构成的类型的描述。 一个 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 为真”这一证据之外。

我们所建议的两种看待“命题即类型”的方式在本质上是有差异的。 ①从构造的角度看， 证明就是抽象的数学对象， 它由依值类型论中合适的表达式所表示；相反， ②如果我们以刚才提到的编码技巧的角度来考虑， 表达式本身其实并不携带任何有趣的东西；相反，是“ 我们可以写下它们并 检查它们是否有良好的类型” 这一事实确保了有关命题为真。也就是说， 表达式本身就是证明。

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

无论如何，真正重要的只有结论。 为了用依值类型论的语言正式地描述一个数学命题， 我们需要提供一个项 p : Prop。 为了证明该断言， 我们需要展示一个项 t : p。 作为一个证明助手，Lean 的任务是 帮助我们构造这样的一个项 t 并 验证它的 格式是否良好以及 类型是否正确。

3.2. 以“命题即类型”的方式工作

在“命题即类型”范式中，任何仅涉及 → 的定理 都可以用 lambda 表达式的抽象和应用规则来证明。 Lean 里面 theorem 命令用于引入新的定理：

1
2
3
4
5
6
7

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 实际上和定义类型 p → q → p 下的元素是一样的， 对内核类型检查器而言两者没有任何区别。

然而定义和定理之间在实用性上还是有一些区别。 一般情况下我们完全没有必要去展开一个定理的“定义”： 由证明无关性可知一个定理的任何两个证明都是定义等价的， 一旦定理的证明被完成，我们通常只需要知道证明存在即可，至于证明具体是什么并不重要。 鉴于这一事实，Lean 会将证明标记为不可还原的 Irreducible， 以此来提示解析器 Parser，更确切地说是繁饰器 Elaborator 在处理文件时通常不需要将其展开。 事实上 Lean 通常可以并行地处理和检查证明， 因为在评估一个证明的正确性时并不需要知道另一个证明的细节。另外 定义中被引用的 section 变量会自动作为参数被添加进来，但 定理中只有那些在定理类型中被引用的变量才会被添加。 这是因为证明一个命题的方式不应影响该命题本身的陈述形式。

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := 
  fun hp : p ↦ -- 箭头引入
  fun hq : q ↦ -- 箭头引入 箭头消去
  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 的类型：

1
2
3
4
5
6
7

variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p :=
  fun hp : p ↦ -- 箭头引入
  fun hq : q ↦ -- 箭头引入
  show p from hp

添加这些额外信息可以 提高证明的清晰度并 帮助我们在书写证明时找出错误。 show 命令不过是个类型注解，并且 我们看到的所有版本的 t1 在 Lean 内部最终都会产生相同的项。

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

variable {p : Prop}
variable {q : Prop}

theorem t1 
  (hp : p) 
  (hq : q) : 
  p := hp
#print t1
-- theorem t1 : ∀ {p q : Prop}, p → q → p :=
-- fun {p q} hp hq ↦ hp

现在我们可以把定理 t1 作为一个函数来应用。

1
2
3
4
5
6
7
8
9

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 下存在一个元素：

1
2
3
4

axiom unsound : False
-- false可导出一切
theorem ex : 1 = 0 :=
  False.elim unsound

将 hp : p 声明为“公理”等同于声明 p 为真，正如 hp 所证明的那样。 把定理 t1 : p → q → p 应用到事实 hp : p（即 p 为真） 将会得到定理 t1 hp : q → p。

回想一下上一章的内容，我们也可以如下书写定理 t1：

1
2
3
4
5
6
7

theorem t1 {p q : Prop} 
  (hp : p) 
  (hq : q) : 
  p := 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”。 例如我们可以将所有参数移到冒号的右边：

1
2
3
4
5
6
7

theorem t1 : ∀ {p q : Prop}, p → q → p := fun {p q : Prop} 
  (hp : p) 
  (hq : q) ↦ 
  hp
#print t1
-- theorem t1 : ∀ {p q : Prop}, p → q → p :=
-- fun {p q} hp hq ↦ hp

如果 p 和 q 被声明为变量， 那么 Lean 会自动为我们推广它们：

1
2
3
4
5
6
7
8
9

variable {p q : Prop}

theorem t1 : p → q → p := fun 
  (hp : p) 
  (hq : q) ↦ 
  hp
#print t1
-- theorem t1 : ∀ {p q : Prop}, p → q → p :=
-- fun {p q} hp hq ↦ hp

在以这种方式推广 t1 之后， 我们就可以将其应用到任何一对命题上， 从而得到该一般性定理的不同实例。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

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

variable (p q r s : Prop)

#check t1 p q
-- t1 p q : p → q → p
#check t1 r s
-- t1 r s : r → s → r
#check t1 (r → s) (s → r)
-- t1 (r → s) (s → r) : (r → s) → (s → r) → r → s

variable (h : r → s)

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

同样，根据“命题即类型”范式， 类型为 r → s 的变量 h 可 视作是 r → s 成立的假设或前提。

作为另一个例子，让我们来考虑上一章提到的函数复合运算—— 不过这里用的是命题而非类型。

1
2
3
4
5

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. 命题逻辑 Propositional Logic

Lean 已经定义了所有标准的逻辑连接词和对应的记号。 命题连接词的记法如下：

它们都接收类型 Prop 下的值作为参数。

1
2
3
4
5
6
7
8

variable (p q : Prop)

#check p → q → p ∧ q
-- p → q → p ∧ q : Prop
#check ¬p → p ↔ False
-- ¬p → p ↔ False : Prop
#check p ∨ q → q ∨ p
-- p ∨ q → q ∨ p : Prop

操作符的优先级如下：一元连结词 ¬ 的结合力最强， 其次是 ∧，然后是 ∨，接着是 →，最后是 ↔。举例： a ∧ b → c ∨ d ∧ e 意为 (a ∧ b) → (c ∨ (d ∧ e))。 请记住 → 等二元关系是右结合的，因此如果我们有 p q r : Prop， 表达式 p → q → r 就应读作“如果有 p，那么如果有 q ，那么 r”。 此即为 p ∧ q → r 的柯里化形式。

在上一章中，我们发现： lambda 抽象可被视为 → 的“引入规则”，其展示了如何“引入”或构建一个蕴含；而 lambda 应用则可被视为一个 → 的“消去规则”，其展示了如何在证明中“消去”或使用一个蕴含。 其他命题连结词在 Lean 的库（见 Prelude.core）中皆有定义且会被自动导入。 每个连结词都有规范的引入和消去规则。

3.3.1. 合取 Conjunction

表达式 And.intro h1 h2 是 p ∧ q 的证明， 它用到了 h1 : p 和 h2 : q 两个证明。 通常我们把 And.intro 称为合取引入 And-Introduction 规则。下面的例子中 我们将用 And.intro 来构建 p → q → p ∧ q 的证明。

1
2
3
4
5
6

variable (p q : Prop)

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

#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.left/And.right 通常被分别称为左/右合取消去 And-Elimination 规则。

1
2
3
4

variable (p q : Prop)

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

现在我们可以用下方的代码 来证明 p ∧ q → q ∧ p：

1
2
3
4
5
6

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，也就是说， 该类型是通过单个规范的构造子定义的，此构造子 利用一系列合适的参数构建该类型的下一个元素。 对于每一组 p q : Prop， p ∧ q 就是一个例子： 构造一个元素的规范方法是将 And.intro 应用于合适的参数 hp : p 和 hq : q。 Lean 允许我们使用匿名构造子表示法 Anonymous Constructor ⟨arg1, arg2, ...⟩， 只要情况如刚才一样——当相关类型是归纳类型且可通过语境推断得出时。 比如我们通常可以用 ⟨hp, hq⟩ 来代替 And.intro hp hq：

1
2
3
4
5

variable (p q : Prop)
variable (hp : p) (hq : q)

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

这些尖括号可以通过输入 \< 和 \> 打出来。

Lean 提供了另一个有用的语法小工具： 对于一个归纳类型 Foo 下的表达式 e（可能会被应用到一些参数）， 记号 e.bar 即为 Foo.bar e 的缩写。 这便于我们访问函数，我们无需打开命名空间。 比如下面两个表达式就具有相同的效果：

1
2
3
4
5
6

variable (xs : List Nat)

#check List.length xs
-- xs.length : Nat
#check xs.length
-- xs.length : Nat

如此一来对于 h : p ∧ q 我们就可以用 h.left 来表示 And.left h ，并用 h.right 来表示 And.right h。 我们便可将上述证明简写为如下形式：

1
2
3
4
5

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  ⟨h.right, -- 合取消去
   h.left⟩  -- 合取消去

简洁与晦涩之间有一条微妙的界限， 以刚才这样的方式省略信息可能会使证明更难阅读； 但对于像上面这样简单的结构—— 当 h 的类型和证明目标都非常明显时， 这种记法既简洁又有效。

我们经常会需要迭代类似 And. 这样的结构。 Lean 也允许我们将右结合的嵌套构造子压扁， 因此下述两个证明是等价的：

1
2
3
4
5
6
7

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. 析取 Disjunction

表达式 Or.intro_left q hp 使用证明 hp : p 构建了 p ∨ q 的证明。类似地， 表达式 Or.intro_right p hq 使用证明 hq : q 构建了 p ∨ q 的证明。 这便是左/右析取引入 Or-Introduction 规则。

1
2
3

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 规则会稍微复杂一点，思路是： 要实现通过 p ∨ q 证明 r，可以先 展示 p 能证明 r ，再 展示 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。

1
2
3
4
5
6

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 _ 的缩写。因此 上面的证明可以变得更简洁:

1
2
3
4
5
6

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，

1
2
3
4
5
6

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. 否定和谬误 Negation and Falsity

否定 ¬p 的定义其实为 p → False， 因此要获得 ¬p 我们就需要从 p 导出一个矛盾；类似地， 表达式 hnq hq 要产生一个 False 的证明 可以通过 hq : q 和 hnq : ¬q 来实现。 下面的例子将用上述两条规则来证明 (p → q) → ¬q → ¬p （符号 ¬ 可以由 \not 或 \neg 打出）。

1
2
3
4
5

variable (p q : Prop)

example (hpq : p → q) (hnq : ¬q) : ¬p :=
  fun hp : p ↦                -- 否定引入 第一条规则 : p → False
  show False from hnq (hpq hp) -- 否定消去 第二条规则 : hnq (hpq hp) 产生 False ; 这里还用到了箭头消去

连接词 False 只有一个消去规则 False.elim， 这描述了一个事实：矛盾能导出一切。这个规则 有时被称作是 无稽之谈 Ex Falso Sequitur Quodlibet，Ex Falso，或爆炸原理 Principle of Explosion。

1
2
3
4
5
6
7
8

variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := 
  False.elim (hnp hp)  -- hnp hp : False , 然后用 False.elim 消去 False 导出任意命题
#print False.elim
-- def False.elim.{u} : {C : Sort u} → False → C :=
-- fun {C} h ↦ False.rec (fun x ↦ C) h
-- 对应谬误消去（直觉主义逻辑）

假命题所导出的任意事实 q 是 False.elim 的一个隐式参数， 而且是被自动推断出来的。这种从相互矛盾的假设中 推导出任意事实的模式很常见，可以用 absurd 来表示。

1
2
3
4
5
6
7

variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := 
  absurd hp hnp
#print absurd
-- def absurd.{v} : {a : Prop} → {b : Sort v} → a → ¬a → b :=
-- fun {a} {b} h₁ h₂ ↦ False.rec (fun x ↦ b) ⋯

再比如下面关于 ¬p → q → (q → p) → r 的证明：

1
2
3
4

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. 逻辑等价 Logical Equivalence

表达式 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 的证明：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

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

#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 来代替 Iff.mp 和 Iff.mpr。 因此刚才的例子可简写为如下形式：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

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. 引入辅助子目标 Introducing Auxiliary Subgoals

正好可以在这里介绍一下 Lean 提供的另一种 构造长证明的方法——即 have 结构： 它会在证明中引入一个辅助子目标。 下面是一个小例子，改编自 3.3.1 节：

1
2
3
4
5
6

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 …”的构造。 下面的例子不过是对调了上方证明的最后两行罢了。

1
2
3
4
5
6

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 h.right

写下 suffices hq : q 会留下两条目标： 首先需要解释证明 q 足以完成对原目标 q ∧ p 的证明， 然后我们再去证明 q。

3.5. 经典逻辑 Classical Logic

目前为止我们看到的引入和消去规则都是构造主义的，也就是说， 它们是以“命题即类型”基础对逻辑连结词的一种计算性理解。 普通经典逻辑在此基础上增加了排中律 Excluded Middle, EM。 要使用这个规则就必须打开经典逻辑命名空间。

1
2
3
4
5

open Classical
variable (p : Prop)

#check em p
-- em p : p ∨ ¬p

从直觉上看，构造主义的“或”非常强： 承认 p ∨ q 意味着知道具体哪一个命题成立。 如果 RH 代表黎曼猜想， 那么经典数学家宁愿宣称 RH ∨ ¬RH—— 尽管我们还无法断言析取式的任何一端。

排中律的一个推论是双重否定消去规则 Double-Negation Elimination, DNE：

1
2
3
4
5
6
7

open Classical

theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim 
    (em p)                         --  p ∨ ¬p
    (fun hp : p ↦ hp)              --  p →  p
    (fun hnp : ¬p ↦ absurd hnp h)  -- ¬p → (False → _)

双重否定消去规则允许我们证明任何命题 p ——即 依据 ¬p 推出 False。这相当于是证明 ¬¬p。 换句话说，双重否定消去允许我们使用反证法， 这在构造主义逻辑中通常是不可能的。作为练习， 你可以试着证明相反的情况， 即 em 可以由 dne 证明。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

variable {p : Prop}

open Classical

theorem dne : ¬¬p → p
  :=λ (hnnp : ¬¬p) ↦ byCases
      (λ (hp : p) ↦ hp)
      (λ (hnp : ¬p) ↦ absurd hnp hnnp)

example : p ∨ ¬p
  :=let cache1
    :=λ (h  : (p ∨ ¬p) → False) ↦
      λ (hp :  p) ↦
      show False from h (Or.inl hp)
    let cache2
    :=λ (h  : (p ∨ ¬p) → False) ↦
      show False from h (Or.inr (cache1 h))
    dne cache2

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

variable {p q : Prop}

def To.elim {p q : Prop} : (p → q) → p → q
  :=λ (hpq : p → q) (hp : p) ↦ hpq hp

open Classical

theorem dne : ¬¬p → p
  :=show ¬¬p → p from fun             -- → 引入
      (hnnp : ¬¬p) =>                  --
      (show p from Or.elim             -- ∨ 消去
        (show p ∨ ¬p from em p)         --
        (show p → p from fun            -- → 引入
          (hp : p) => hp)                --
        (show ¬p → p from fun           -- → 引入
          (hnp : ¬p) =>                  --
          (show p from False.elim        -- ⊥ 消去
            (show False from To.elim      -- ¬ 消去
              (show ¬¬p from hnnp)         --
              (show ¬p from hnp)))))       --

example : p ∨ ¬p
  :=let cache1
    :=show ((p ∨ ¬p) → False) → (p → False) from fun              -- → 引入
        (hpnp : (p ∨ ¬p) → False) =>                               --
        (show p → False from fun                                   -- → 引入
          (hp :  p) =>                                              --
          show False from To.elim                                   -- ¬ 消去
            (show (p ∨ ¬p) → False from hpnp)                        --
            (show  p ∨ ¬p from Or.inl                                -- ∨ 引入
              (show p from hp)))                                      --
    let cache2
    :=show ((p ∨ ¬p) → False) → False from fun                     -- → 引入
        (hpnp : (p ∨ ¬p) → False) =>                                --
        (show False from To.elim                                    -- ¬ 消去
          (show (p ∨ ¬p) → False from hpnp)                          --
          (show  p ∨ ¬p from Or.inr                                  -- ∨ 引入
            (show p → False from To.elim                              -- → 消去
              (show ((p ∨ ¬p) → False) → (p → False) from cache1)      --
              (show  (p ∨ ¬p) → False from hpnp))))                    --
    show p ∨ ¬p from To.elim                                       -- → 消去
      (show ¬¬(p ∨ ¬p) → (p ∨ ¬p) from dne)                         --
      (show ((p ∨ ¬p) → False) → False from cache2)                 --

经典逻辑公理还允许你使用额外的证明模式， 它们在 em 的支持下是合理的。比如 我们可以以分类讨论的方式完成证明：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byCases -- 实际上等同于 Or.elim (em p)
    (fun (h1 : p)  ↦ (h1 : p))
    (fun (h1 : ¬p) ↦ (absurd h1 h : p))  -- 这儿用到了 h : ¬¬p

#print byCases
-- theorem Classical.byCases :
-- ∀ {p q : Prop}, (p → q) → (¬p → q) → q :=
-- fun {p q} hpq hnpq ↦ Decidable.byCases hpq hnpq

或者你也可以用反证法来证明：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byContradiction -- 实际上等同于 dne
    (fun h1 : ¬p ↦
     show False from h h1)               -- 这儿用到了 h : ¬¬p

#print byContradiction
-- theorem Classical.byContradiction : 
-- ∀ {p : Prop}, 
-- (¬p → False) → p :=
-- fun {p} h ↦ Decidable.byContradiction h

如果你不习惯以构造主义的方式思考， 那么你可能需要花点时间来消化 经典逻辑推理的使用场景。 在下面的例子中它是必须的， 因为从构造主义的观点来看 知道 p 和 q 不同时为真 并不意味着知道哪一个是假的：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

open Classical
variable (p q : Prop)

example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
  Or.elim 
    (em p)              -- p ∨ ¬p
    (fun hp : p ↦       -- p → (¬p ∨ ¬q)
      Or.inr
        (show ¬q from
          fun hq : q ↦
          h ⟨hp, hq⟩))   -- 这里用到了 h : ¬(p ∧ q)
    (fun hp : ¬p ↦      -- p → (¬p ∨ ¬q)
      Or.inl hp)

稍后我们将看到，构造逻辑中某些情形下 “排中律”和“双重否定消去律”等是被允许的， 在这种情况下，Lean 允许在不依赖排中律的前提下 使用经典逻辑进行推理。

Lean 中用到的完整公理列表请参考公理与计算。

3.6. 逻辑命题的例子 Examples of Propositional Validities

Lean 的标准库证明了不少命题逻辑相关的正确结论， 供你在自己的证明中随便使用。 下面的列表包括一些常见的逻辑恒等式。

交换律 Commutativity：

1. p ∧ q ↔ q ∧ p

   答：

   简单版：

   1 2 3 4 5 6 7

   variable {p q : Prop} example : p ∧ q ↔ q ∧ p :=let cache {p q : Prop} :=λ (hpq : p ∧ q) ↦ And.intro hpq.right hpq.left ⟨cache, cache⟩

   复杂版：

   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18

   variable {p q : Prop} example : p ∧ q ↔ q ∧ p :=Iff.intro -- ↔ 引入 (show p ∧ q → q ∧ p from fun -- → 引入 (hpq : p ∧ q) => -- show q ∧ p from And.intro -- ∧ 引入 (show q from And.right -- ∧ 消去 (show p ∧ q from hpq)) -- (show p from And.left -- ∧ 消去 (show p ∧ q from hpq))) -- (show q ∧ p → p ∧ q from fun -- → 引入 (hqp : q ∧ p) => -- show p ∧ q from And.intro -- ∧ 引入 (show p from And.right -- ∧ 消去 (show q ∧ p from hqp)) -- (show q from And.left -- ∧ 消去 (show q ∧ p from hqp))) --

2. p ∨ q ↔ q ∨ p

   答：

   简单版：

   1 2 3 4 5 6 7 8

   variable {p q : Prop} example : p ∨ q ↔ q ∨ p :=let cache {p q : Prop} :=λ (hpq : p ∨ q) ↦ Or.elim hpq (λ (hp : p) ↦ Or.inr hp) (λ (hq : q) ↦ Or.inl hq) ⟨cache, cache⟩

   复杂版：

   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28

   variable {p q : Prop} example : p ∨ q ↔ q ∨ p :=Iff.intro -- ↔ 引入 (show p ∨ q → q ∨ p from fun -- → 引入 (hpq : p ∨ q) => -- (show q ∨ p from Or.elim -- ∨ 消去 (show p ∨ q from hpq) -- (show p → q ∨ p from fun -- → 引入 (hp : p) => -- show q ∨ p from Or.inr -- ∨ 引入 (show p from hp)) -- (show q → q ∨ p from fun -- → 引入 (hq : q) => -- show q ∨ p from Or.inl -- ∨ 引入 (show q from hq)))) -- (show q ∨ p → p ∨ q from fun -- → 引入 (hqp : q ∨ p) => -- show p ∨ q from Or.elim -- ∨ 消去 (show q ∨ p from hqp) -- (show q → p ∨ q from fun -- → 引入 (hq : q) => -- (show p ∨ q from Or.inr -- ∨ 引入 (show q from hq))) -- (show p → p ∨ q from fun -- → 引入 (hp : p) => -- (show p ∨ q from Or.inl -- ∨ 引入 (show p from hp)))) --