# 命题即类型

> Curry-Howard 对应、证明就是程序、Prop 与 Type 的实际差别，以及为什么这让机器检查成为可能。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/propositions-as-types
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

这是全书的转折点。**读懂这一章，Lean 的一切都会变得自然；读不懂，后面全是死记硬背。**

## 核心对应

```text
命题  ←→  类型
证明  ←→  该类型的项
```

「证明命题 P」 = 「构造一个类型为 P 的项」。

```lean
theorem trivial_proof : True := True.intro
--      ^^^^^^^^^^^^^   ^^^^   ^^^^^^^^^^
--      名字            类型   项
```

对比一个普通定义：

```lean
def some_number : Nat := 42
--  ^^^^^^^^^^^   ^^^   ^^
--  名字          类型  项
```

**结构完全一样**。`theorem` 与 `def` 的区别只是习惯与优化，不是本质。

## Curry-Howard 对应表

| 逻辑 | 类型论 | Lean |
| --- | --- | --- |
| 命题 P | 类型 P | `P : Prop` |
| P 的证明 | P 类型的项 | `h : P` |
| P → Q（蕴含） | 函数类型 | `P → Q` |
| P ∧ Q（合取） | 积类型 | `And P Q` |
| P ∨ Q（析取） | 和类型 | `Or P Q` |
| ¬P（否定） | P → 空 | `P → False` |
| ∀ x, P x | Pi 类型 | `(x : α) → P x` |
| ∃ x, P x | Sigma 类型 | `Exists P` |
| True | 单元类型 | `True`（一个构造子） |
| False | 空类型 | `False`（零个构造子） |

**每一行都不是比喻，是字面相等。**

## 蕴含就是函数

```lean
theorem imp_example (p q : Prop) (hpq : p → q) (hp : p) : q :=
  hpq hp
```

读作：

- `hpq : p → q` —— 一个「从 p 的证明造出 q 的证明」的**函数**。
- `hp : p` —— 一个 p 的证明。
- `hpq hp` —— **函数应用**，得到 q 的证明。

**Modus ponens（分离规则）就是函数应用。** 逻辑里的推理规则，在这里是编程里最基本的操作。

再看蕴含的引入：

```lean
theorem imp_intro (p q : Prop) (hq : q) : p → q :=
  fun _ => hq
```

「要证 `p → q`，就构造一个函数」——`fun` 引入的正是逻辑里的「假设 p，推出 q」。

## False 与否定

```lean
inductive False : Prop
-- 没有任何构造子
```

**`False` 是空类型**——没有构造子，所以不可能构造出它的项。这正好对应「假命题没有证明」。

否定的定义：

```lean
def Not (p : Prop) : Prop := p → False
-- 记作 ¬p
```

**`¬p` 就是「从 p 能推出矛盾」**。

爆炸原理（ex falso quodlibet）也自然得出：

```lean
theorem absurd_example (p q : Prop) (hp : p) (hnp : ¬p) : q :=
  absurd hp hnp
```

因为 `False` 没有构造子，对它做模式匹配**零个分支**就穷尽了——于是可以返回任何类型：

```lean
example (h : False) : q := h.elim
```

这就是「从矛盾能推出一切」在类型论里的解释。**不是逻辑学的奇怪约定，是空类型的必然性质。**

## 存在量词是 Sigma

```lean
theorem exists_example : ∃ n : Nat, n > 5 :=
  ⟨6, by decide⟩
```

**存在性证明 = 给出见证 + 证明它满足性质**。这是一个配对。

用它的时候要拆开：

```lean
theorem use_exists (h : ∃ n : Nat, n > 5) : True := by
  obtain ⟨n, hn⟩ := h      -- 拆出见证 n 和性质 hn
  trivial
```

<Callout type="info">
  **这解释了为什么构造性数学在 Lean 里是默认的**：证明 `∃ x, P x` 必须真的**给出**那个 x。

  经典逻辑的存在性证明（「反证法：假设不存在，导出矛盾」）在 Lean 里需要 `Classical.byContradiction` 这类公理。Mathlib 默认引入了经典公理，所以可以用——但它不是内置的，是显式假设的。

  用 `#print axioms myTheorem` 可以查一个定理依赖了哪些公理：

  ```text
  'myTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]
  ```

  这三个是 Mathlib 的标准公理。若看到 `sorryAx` 就是没证完。
</Callout>

## Prop 与 Type 到底差在哪

既然结构一样，为什么要分开？

| | `Prop` | `Type` |
| --- | --- | --- |
| Proof irrelevance | **有**：任意两个证明相等 | 无 |
| 编译后 | **被擦除** | 保留 |
| 消去限制 | 一般不能消去到 `Type` | 无限制 |
| 非直谓性 | **是**（`∀ p : Prop, p` 仍是 `Prop`） | 否（要升宇宙） |

三个实际后果：

**一、证明不占运行时开销。** 一个用 `Vec` 和大量证明写的程序，编译后与手写 C 的性能相当——所有验证信息在编译期消失。

**二、不能从证明里「提取数据」。** 知道「存在一个满足条件的 x」不等于「能算出那个 x」。要能算，命题得放在 `Type` 里（用 `Σ` 而非 `∃`）。

**三、`Prop` 的非直谓性让逻辑更简洁。** `∀ p : Prop, p → p` 本身还是一个 `Prop`，不用升到更高宇宙。这对形式化数学很方便，代价是不能随意消去到 `Type`（否则会不一致）。

## 一个完整的类比

```lean
-- 程序：给定 Nat 和 String，造一个 Nat × String
def prog (n : Nat) (s : String) : Nat × String := (n, s)

-- 证明：给定 p 和 q 的证明，造一个 p ∧ q 的证明
theorem proof (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩
```

**两行代码结构完全相同**——都是「接受两个参数，用匿名构造子打包」。

甚至连 `And` 的定义都和 `Prod` 一样：

```lean
structure And (a b : Prop) : Prop where
  intro ::
  left  : a
  right : b

structure Prod (α β : Type) : Type where
  mk ::
  fst : α
  snd : β
```

**唯一的差别是住在 `Prop` 还是 `Type`。**

## 为什么这让机器检查成为可能

传统的数学证明是自然语言写的，机器无法验证。Curry-Howard 把它变成了**类型检查问题**：

```text
「这个证明对吗？」
   ↓ 翻译
「这个项的类型是不是那个命题？」
   ↓
类型检查器的日常工作
```

而类型检查是**可判定的、机械的、可信的**——Lean 的内核（kernel）只有几千行，负责最终验证。所有 tactic、自动化、宏，产出的都是普通的项，最后都要过内核这一关。

<Callout type="info">
  **这就是「小内核」（de Bruijn 判据）的意义**：你不需要信任几十万行的 tactic 代码，只需要信任那个小内核。tactic 出 bug 最多是证不出来或造出错误的项，而错误的项会被内核拒绝。

  这是形式化验证可信度的来源。
</Callout>

## 观念转换检查表

读完这章，下面这些说法应该都成立：

- 「证明一个定理」= 「写一个函数」。
- `h : p → q` 是一个函数，`h hp` 是应用它。
- `¬p` 就是 `p → False`。
- `∀` 和 `→` 是同一个东西。
- 定理的名字可以像函数一样被调用、部分应用、传给其他函数。
- `theorem` 和 `def` 可以互换（只是不该）。

最后一条的演示：

```lean
theorem foo (p : Prop) (hp : p) : p ∧ p := ⟨hp, hp⟩

-- 定理可以被部分应用，和函数一样
#check foo                    -- ∀ (p : Prop), p → p ∧ p
#check @foo True              -- True → True ∧ True
#check foo True True.intro    -- True ∧ True
```

**定理就是函数。** 接受这一点，[tactic 那部分](https://daiw.org/manual/lean4/tactics-basics)才好理解——tactic 只是「帮你写这个函数」的工具。

下一篇：[逻辑联结词](https://daiw.org/manual/lean4/logic-connectives)。