命题即类型
Curry-Howard 对应、证明就是程序、Prop 与 Type 的实际差别，以及为什么这让机器检查成为可能。
这是全书的转折点。读懂这一章，Lean 的一切都会变得自然；读不懂，后面全是死记硬背。
核心对应
命题 ←→ 类型
证明 ←→ 该类型的项「证明命题 P」 = 「构造一个类型为 P 的项」。
theorem trivial_proof : True := True.intro
-- ^^^^^^^^^^^^^ ^^^^ ^^^^^^^^^^
-- 名字 类型 项对比一个普通定义：
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（零个构造子） |
每一行都不是比喻，是字面相等。
蕴含就是函数
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（分离规则）就是函数应用。 逻辑里的推理规则，在这里是编程里最基本的操作。
再看蕴含的引入：
theorem imp_intro (p q : Prop) (hq : q) : p → q :=
fun _ => hq「要证 p → q，就构造一个函数」——fun 引入的正是逻辑里的「假设 p，推出 q」。
False 与否定
inductive False : Prop
-- 没有任何构造子False 是空类型——没有构造子，所以不可能构造出它的项。这正好对应「假命题没有证明」。
否定的定义：
def Not (p : Prop) : Prop := p → False
-- 记作 ¬p¬p 就是「从 p 能推出矛盾」。
爆炸原理（ex falso quodlibet）也自然得出：
theorem absurd_example (p q : Prop) (hp : p) (hnp : ¬p) : q :=
absurd hp hnp因为 False 没有构造子，对它做模式匹配零个分支就穷尽了——于是可以返回任何类型：
example (h : False) : q := h.elim这就是「从矛盾能推出一切」在类型论里的解释。不是逻辑学的奇怪约定，是空类型的必然性质。
存在量词是 Sigma
theorem exists_example : ∃ n : Nat, n > 5 :=
⟨6, by decide⟩存在性证明 = 给出见证 + 证明它满足性质。这是一个配对。
用它的时候要拆开：
theorem use_exists (h : ∃ n : Nat, n > 5) : True := by
obtain ⟨n, hn⟩ := h -- 拆出见证 n 和性质 hn
trivial这解释了为什么构造性数学在 Lean 里是默认的：证明 ∃ x, P x 必须真的给出那个 x。
经典逻辑的存在性证明（「反证法：假设不存在，导出矛盾」）在 Lean 里需要 Classical.byContradiction 这类公理。Mathlib 默认引入了经典公理，所以可以用——但它不是内置的，是显式假设的。
用 #print axioms myTheorem 可以查一个定理依赖了哪些公理：
'myTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]这三个是 Mathlib 的标准公理。若看到 sorryAx 就是没证完。
Prop 与 Type 到底差在哪
既然结构一样，为什么要分开？
Prop | Type | |
|---|---|---|
| Proof irrelevance | 有：任意两个证明相等 | 无 |
| 编译后 | 被擦除 | 保留 |
| 消去限制 | 一般不能消去到 Type | 无限制 |
| 非直谓性 | 是（∀ p : Prop, p 仍是 Prop） | 否（要升宇宙） |
三个实际后果：
一、证明不占运行时开销。 一个用 Vec 和大量证明写的程序，编译后与手写 C 的性能相当——所有验证信息在编译期消失。
二、不能从证明里「提取数据」。 知道「存在一个满足条件的 x」不等于「能算出那个 x」。要能算，命题得放在 Type 里（用 Σ 而非 ∃）。
三、Prop 的非直谓性让逻辑更简洁。 ∀ p : Prop, p → p 本身还是一个 Prop，不用升到更高宇宙。这对形式化数学很方便，代价是不能随意消去到 Type（否则会不一致）。
一个完整的类比
-- 程序：给定 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 一样：
structure And (a b : Prop) : Prop where
intro ::
left : a
right : b
structure Prod (α β : Type) : Type where
mk ::
fst : α
snd : β唯一的差别是住在 Prop 还是 Type。
为什么这让机器检查成为可能
传统的数学证明是自然语言写的，机器无法验证。Curry-Howard 把它变成了类型检查问题：
「这个证明对吗？」
↓ 翻译
「这个项的类型是不是那个命题？」
↓
类型检查器的日常工作而类型检查是可判定的、机械的、可信的——Lean 的内核（kernel）只有几千行，负责最终验证。所有 tactic、自动化、宏，产出的都是普通的项，最后都要过内核这一关。
这就是「小内核」（de Bruijn 判据）的意义：你不需要信任几十万行的 tactic 代码，只需要信任那个小内核。tactic 出 bug 最多是证不出来或造出错误的项，而错误的项会被内核拒绝。
这是形式化验证可信度的来源。
观念转换检查表
读完这章，下面这些说法应该都成立：
- 「证明一个定理」= 「写一个函数」。
h : p → q是一个函数，h hp是应用它。¬p就是p → False。∀和→是同一个东西。- 定理的名字可以像函数一样被调用、部分应用、传给其他函数。
theorem和def可以互换（只是不该）。
最后一条的演示：
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 那部分才好理解——tactic 只是「帮你写这个函数」的工具。
下一篇：逻辑联结词。