Some content in this article was created with AI assistance. Please verify as needed.

本篇参考 Mathematics in Lean，按证明中常见的操作重新组织，不逐章翻译原书。

示例统一放在 mathlib 项目中，并从下面的导入开始：

1
import Mathlib

实际项目可以只导入需要的模块，学习阶段直接 import Mathlib 更方便。

证明项与 tactic 基础

命题也是类型

Lean 使用 Prop 表示命题的类型：

1
2
3
4
#check 2 + 2 = 4       -- Prop
#check 3 < 5           -- Prop
#check True            -- Prop
#check False           -- Prop

一个命题的值就是该命题的证明。声明定理和声明普通定义的语法非常接近：

1
2
theorem two_add_two : 2 + 2 = 4 := by
  norm_num

theorem 和 lemma 在内核层面没有本质区别，只是名称传达的用途不同。临时示例可以使用 example，它不会创建全局名称：

1
2
example : 10 ≤ 20 := by
  norm_num

证明项

最简单的相等可以直接用 rfl：

1
example (x : Nat) : x = x := rfl

这里 rfl 是类型为 x = x 的证明项。也可以使用 tactic 模式写成：

1
2
example (x : Nat) : x = x := by
  rfl

by 后面的 tactic 会逐步修改证明目标，最后构造出一个交给内核检查的证明项。tactic 不是绕过内核的脚本。

前提和目标

一个证明状态由局部上下文和当前目标组成：

1
2
example (a b : Nat) (h : a = b) : b = a := by
  exact h.symm

上下文中有 a b : Nat 和 h : a = b，目标是 b = a。exact 要求给出的项类型与目标一致。

assumption 会在上下文中寻找正好匹配目标的前提：

1
2
example (P : Prop) (h : P) : P := by
  assumption

intro 与 apply

证明函数类型或蕴含时，使用 intro 引入参数：

1
2
3
example (P Q : Prop) : P → Q → P := by
  intro hP hQ
  exact hP

hQ 没有使用，这没有逻辑问题，只可能触发未使用变量的提示。

apply 使用一个结论能匹配当前目标的定理，并把它的前提变成新目标：

1
2
3
example (a b c : Nat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
  apply Nat.le_trans hab
  exact hbc

也可以一次给出完整证明：

1
2
example (a b c : Nat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c :=
  Nat.le_trans hab hbc

短证明使用证明项通常很清楚，步骤较多时 by 块更容易调试。

have

have 在证明中建立中间结论：

1
2
3
example (a b c : ℝ) (hab : a < b) (hbc : b < c) : a < c := by
  have hac : a < c := lt_trans hab hbc
  exact hac

中间结论的类型可以显式写出，也可以让 Lean 推断：

1
2
3
example (n : Nat) : n + 0 = n := by
  have h := Nat.add_zero n
  exact h

show 和 change

show 重申当前目标，适合在长证明中标明正在证明什么：

1
2
3
example (x : Nat) : x = x := by
  show x = x
  rfl

change 把目标替换为定义上相等的形式：

1
2
3
4
5
def twice (n : Nat) := n + n

example (n : Nat) : twice n = n + n := by
  change n + n = n + n
  rfl

如果两个表达式只是在展开定义以后相同，change 很合适；如果需要使用一个数学等式改写，则应该用后续笔记中的 rw。

定理参数

使用 mathlib 前先查看定理的完整类型：

1
2
3
4
#check add_comm
#check add_assoc
#check Nat.le_trans
#check mul_pos

名称记不准时，在编辑器中搜索或输入前缀查看补全；名称确定以后再用 #check 看隐式参数、参数顺序和结论。Lean 报错经常不是证明思路错误，而是选错定理版本或参数顺序不对。

sorry

sorry 暂时接受一个未完成目标：

1
2
example : 1 = 2 := by
  sorry

它会产生警告，并在环境中引入不受信任的占位。写草稿时可以用来隔离后续代码，但完成文章和正式项目时不应保留。构建时使用 lake build --wfail 可以把这类警告当作错误。

逻辑连接词与量词

Lean 的逻辑连接词不是孤立的特殊语法，它们都有对应的构造器和消去方式。记住“目标是什么就构造什么，前提是什么就拆开什么”，大多数基础逻辑证明都很机械。

1
import Mathlib

本篇沿用 Unicode 逻辑记号。→、↔、∀、∃ 有直接的 ASCII 语法 ->、<->、forall、exists；∧、∨、¬ 分别展开为 And、Or、Not。后一组命名写法更适合解释原理或搜索声明，组合命题中通常还是符号更清楚。

蕴含与全称量词

证明 P → Q 时引入 P 的证明；证明 ∀ x, P x 时引入任意的 x：

1
2
3
4
5
6
7
example (P : Prop) : P → P := by
  intro hP
  exact hP

example (α : Type) : ∀ x : α, x = x := by
  intro x
  rfl

使用时则像调用普通函数：

1
2
example (P Q : Prop) (h : P → Q) (hP : P) : Q := by
  exact h hP

rintro 可以一边引入一边拆解结构，复杂前提下比连续 intro、rcases 更紧凑。

合取

P ∧ Q 同时保存 P 和 Q 的证明。目标是合取时用 constructor：

1
2
3
4
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · exact hP
  · exact hQ

也可以直接使用构造器：

1
2
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
  ⟨hP, hQ⟩

拆解合取可以使用字段或 rcases：

1
2
3
example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  rcases h with ⟨hP, hQ⟩
  exact ⟨hQ, hP⟩

析取

证明 P ∨ Q 时选择一个分支：

1
2
3
example (P Q : Prop) (hP : P) : P ∨ Q := by
  left
  exact hP

使用析取前提时必须覆盖两种情况：

1
2
3
4
5
6
example (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  rcases h with hP | hQ
  · right
    exact hP
  · left
    exact hQ

圆点表示当前分支的 tactic 块。保持每个分支缩进一致，可以直观看出目标层级。

等价

P ↔ Q 由两个方向的蕴含构成：

1
2
3
4
5
6
example (P Q : Prop) : P ∧ Q ↔ Q ∧ P := by
  constructor
  · rintro ⟨hP, hQ⟩
    exact ⟨hQ, hP⟩
  · rintro ⟨hQ, hP⟩
    exact ⟨hP, hQ⟩

已有 h : P ↔ Q 时，h.mp 把 P 变成 Q，h.mpr 做反方向转换。h.1 和 h.2 也可以使用，但方向名称更明确。

存在量词

证明 ∃ x, P x 时需要给出见证和见证满足性质的证明：

1
2
3
example : ∃ n : Nat, n > 10 := by
  use 11
  norm_num

也可以直接写成一对：

1
2
example : ∃ n : Nat, n > 10 :=
  ⟨11, by norm_num⟩

拆解存在前提使用 rcases 或 obtain：

1
2
3
example (P : Nat → Prop) (h : ∃ n, P n) : ∃ m, P m := by
  obtain ⟨n, hn⟩ := h
  exact ⟨n, hn⟩

否定和矛盾

¬ P 的定义就是 P → False：

1
2
example (P : Prop) (hP : P) (hnP : ¬ P) : False := by
  exact hnP hP

从矛盾可以推出任意命题：

1
2
3
example (P Q : Prop) (hP : P) (hnP : ¬ P) : Q := by
  exfalso
  exact hnP hP

反证法使用 by_contra：

1
2
3
example (n : Nat) : ¬ (n < n) := by
  intro h
  exact Nat.lt_irrefl n h

当目标不是显式否定时，by_contra h 会加入结论的否定并把目标改成 False。

分类讨论

对可判定命题使用 by_cases：

1
2
3
4
example (P : Prop) [Decidable P] : P ∨ ¬ P := by
  by_cases h : P
  · exact Or.inl h
  · exact Or.inr h

mathlib 默认提供经典逻辑环境，因此很多命题不必手动写 [Decidable P]。不过，知道分类讨论依赖可判定性，有助于区分可计算程序与纯逻辑证明。

常用拆解语法

前提或目标 常用 tactic
P → Q、∀ x, P x 目标 intro、rintro
P ∧ Q 目标 constructor、exact ⟨..., ...⟩
P ∧ Q 前提 rcases h with ⟨hP, hQ⟩
P ∨ Q 目标 left、right
P ∨ Q 前提 `rcases h with hP
∃ x, P x 目标 use、refine ⟨?_, ?_⟩
∃ x, P x 前提 obtain ⟨x, hx⟩ := h
False contradiction、exact hnp hp

逻辑结构尚未熟悉时，把构造和拆解步骤写出来。一行自动化虽然短，却可能隐藏目标如何变化。

等式改写与化简

等式推理经常要替换子表达式。Lean 明确记录替换方向、位置和所用规则，常用工具是 rw、simp 和 calc。

1
import Mathlib

rw

rw [h] 按等式 h 从左向右改写目标：

1
2
example (a b : Nat) (h : a = b) : a + a = b + b := by
  rw [h]

反向改写使用左箭头：

1
2
example (a b : Nat) (h : a = b) : b = a := by
  rw [h]

这里 Lean 选择了能完成目标的方向。需要明确控制时写：

1
2
example (a b : Nat) (h : a = b) : b = a := by
  rw [← h]

多个规则按顺序使用：

1
2
example (a b c : Nat) (hab : a = b) (hbc : b = c) : a = c := by
  rw [hab, hbc]

默认改写目标，在前提中改写使用 at：

1
2
3
example (a b : Nat) (h : a = b) (ha : a > 0) : b > 0 := by
  rw [h] at ha
  exact ha

rw [h] at * 会改写所有前提和目标，影响范围较大，应该确认不会破坏有用的原始形式。

simp

simp 使用带有 [simp] 标记的引理进行定向化简：

1
2
example (xs : List Nat) : ([] ++ xs).reverse = xs.reverse := by
  simp

可以额外提供规则或定义：

1
2
3
4
def triple (n : Nat) := n + n + n

example (n : Nat) : triple n + 0 = n + n + n := by
  simp [triple]

simp only [...] 只使用列出的规则以及最基本的化简步骤，适合希望证明行为稳定、依赖明确的地方：

1
2
example (n : Nat) : n + 0 = n := by
  simp only [Nat.add_zero]

simp at h ⊢ 可以同时化简前提 h 和当前目标。符号 ⊢ 表示目标。

simp 与 rw 的区别

rw 是受控的一次或数次替换，规则顺序和方向由代码指定；simp 会反复使用化简规则直到不能继续。

一般可以这样选择：

  • 已知这一步具体要用哪个等式：rw；
  • 目标包含大量 + 0、if true、列表空值等标准化简：simp；
  • 希望严格限制自动化依赖：simp only。

不要把两个方向的等式都随意加入 simp 集，否则可能导致循环或难以预测的规范形式。

calc

calc 把一串关系按中间表达式连接起来：

1
2
3
4
example (a b c : ℝ) (h1 : a = b) (h2 : b = c) : a = c := by
  calc
    a = b := h1
    _ = c := h2

关系不必都是等号：

1
2
3
4
example (a b c : ℝ) (h1 : a < b) (h2 : b ≤ c) : a < c := by
  calc
    a < b := h1
    _ ≤ c := h2

下划线代表上一行的右侧。calc 很接近自然语言推导，适合保留证明中的关键中间式。

unfold 与 dsimp

unfold name 展开指定定义：

1
2
3
4
5
def quadruple (n : Nat) := n * 4

example (n : Nat) : quadruple n = n * 4 := by
  unfold quadruple
  rfl

dsimp 只做定义性化简，例如展开局部 let、投影和可以直接计算的定义：

1
2
example : (let x := 40; x + 2) = 42 := by
  dsimp

如果 rfl 能完成，那么两边通常是定义上相等；如果需要引用数学定理，则是命题上的相等，不要混淆。

congr 与 congrArg

等式两边处在同一个函数下时，可以把问题缩小到参数：

1
2
example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = f b := by
  exact congrArg f h

congr tactic 会自动生成函数参数相等的目标：

1
2
example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  congr

函数和结构外延

证明两个函数相等，使用 funext 把目标变成逐点相等：

1
2
3
example (f g : Nat → Nat) (h : ∀ x, f x = g x) : f = g := by
  funext x
  exact h x

证明集合或结构相等经常使用 ext：

1
2
3
example (s t : Set Nat) (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := by
  ext x
  exact h x

ext 会查找对应类型注册的外延引理。执行后先观察它生成了什么目标，再决定使用 simp、constructor 或已有前提。

simpa

simpa 先化简目标和给定证明的类型，再尝试精确匹配：

1
2
example (n : Nat) : (0 + n) + 0 = n := by
  simpa using Nat.zero_add n

它特别适合已有定理只与目标相差记号、参数顺序或少量标准化简的场景。若 simpa 失败，先分别 #check 定理并查看化简后的目标，不要盲目追加大量规则。

Curry–Howard 与逻辑基础

Curry–Howard 对应

“命题即类型，证明即程序”常被一句话带过。更具体地说：

逻辑 类型系统
命题 P 类型 P : Prop
P 的证明 类型 P 的项
P → Q 从 P 的证明构造 Q 的证明的函数
P ∧ Q 同时包含两个证明的结构
P ∨ Q 指明左分支或右分支的归纳类型
∀ x, P x 对任意 x 返回证明的依赖函数
∃ x, P x 携带见证与性质证明的依赖结构
False 没有构造器的空命题

因此：

1
2
example (P Q : Prop) : P → Q → P :=
  fun hP _ => hP

既是一个 lambda 表达式，也是一个蕴含证明。intro tactic 只是在交互式地构造同一个函数。

合取证明：

1
2
example (P Q : Prop) : P → Q → P ∧ Q :=
  fun hP hQ => And.intro hP hQ

析取证明：

1
2
example (P Q : Prop) : P → P ∨ Q :=
  fun hP => Or.inl hP

存在证明：

1
2
example : ∃ n : Nat, n + 1 = 3 :=
  ⟨2, rfl⟩

tactic 让构造过程更方便，但逻辑连接词最终仍由这些构造器和 recursor 解释。

Prop 与 Type

并非所有类型都表示命题。Nat : Type 的值包含运行时数据；2 + 2 = 4 : Prop 的值只用于证明。

Lean 对 Prop 做了两个重要设计：

  1. proof irrelevance：同一命题的不同证明在逻辑上不可区分；
  2. 证明擦除：编译普通程序时，纯证明数据通常不会保留到运行时。

因此在结构中携带边界证明：

1
2
3
structure BoundedNat where
  value : Nat
  bound : value < 100

不等于运行时必须保存一份庞大的证明树。bound 帮助类型检查和推理，生成程序时通常被擦除。

Type 中的数据不能任意从 Prop 消去，否则可能让“选择哪个证明”影响可计算结果，破坏 proof irrelevance。Lean 对命题到数据的消去施加限制；False、相等和某些单构造命题有特殊允许情况。

构造性逻辑与经典逻辑

在构造性逻辑中，证明 P ∨ Q 必须指出哪一边成立；证明 ∃ x, P x 必须给出见证。排中律：

1
P ∨ ¬ P

对任意命题并不能仅靠核心构造规则计算出来。

mathlib 广泛使用经典逻辑，可以显式开启：

1
2
3
4
open Classical

example (P : Prop) : P ∨ ¬ P := by
  exact Classical.em P

经典公理不会破坏内核一致性，但会影响可计算内容：一个依赖经典选择构造的数学对象通常不能直接提取为算法，因此需要 noncomputable。

这与“证明存在”和“计算出一个见证”的区别有关。经典数学可以证明某对象存在，却不一定给出有效算法；构造性证明往往同时包含见证算法。

Decidable

Decidable P 表示可以决定命题 P：

1
2
#check Decidable
#synth Decidable (3 < 5)

若 P 可判定，Lean 可以在程序中写：

1
2
def chooseText (P : Prop) [Decidable P] : String :=
  if P then "yes" else "no"

有限比较、自然数相等等具有可计算实例。经典逻辑也能为任意命题提供非计算性的 decidable 实例，但这不意味着突然获得了一个可执行的全能判定算法。

在证明代码中 by_cases h : P 常使用经典判定；在需要执行的程序中则应确认实例确实可计算。

内核与证明执行

可信内核

Lean 的可信计算基很小：parser、编辑器、自动化 tactic 可以很复杂，但最终声明必须由 kernel 检查。

1
2
3
4
5
tactic / automation / external search
             ↓ 产生
          proof term
             ↓ 检查
           kernel

即使 ring、linarith 或某个外部程序实现有 bug，只要它最终提交的是普通证明项，错误结果应被内核拒绝。

这与直接信任计算机代数系统输出字符串不同。Lean 自动化通常包含“计算答案”和“生成可检查证书”两个层面。

可信边界仍然不是零：

  • Lean 内核实现；
  • 使用的公理；
  • unsafe/FFI 不应被用来伪造内核证明；
  • 编译器正确性影响程序执行，但不直接替代内核证明检查。

检查定理依赖的公理可以使用：

1
2
#print axioms Classical.choice
#print axioms Nat.add_comm

theorem、opaque 与 def

定理声明通常是不透明的：后续类型检查不会随意展开巨大证明体。普通 def 则可以参与定义归约。

这有两个作用：

  • proof irrelevance 下，通常没有必要计算证明内部结构；
  • 避免大型证明展开导致 elaboration 和内核检查失控。

证明一个定理以后，后续应通过它的类型使用，而不是依赖证明脚本内部实现。这个抽象边界与模块封装类似。

证明状态

一个 tactic 接收包含局部上下文和目标的 metavariable，再完成目标或产生若干子目标。

例如：

1
2
3
4
5
6
example (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro h
  rcases h with ⟨hP, hQ⟩
  constructor
  · exact hQ
  · exact hP

可以逐步理解为：

  1. intro h：把蕴含前提加入上下文；
  2. rcases：用合取 recursor 拆出两个证明；
  3. constructor：选择 And.intro，产生两个参数目标；
  4. 两次 exact：填入构造器参数。

所谓“tactic 编程”不是另一个独立逻辑，而是在 metavariable 上交互式构造项。

自动化层级

常用证明方式按自动化程度大致排列如下：

1
2
3
4
5
6
7
8
9
显式证明项
  ↓
exact / apply / constructor
  ↓
rw / calc / simp only
  ↓
simp / aesop
  ↓
领域自动化 ring / omega / linarith

越靠下不代表越好。选择取决于：

  • 证明意图是否清楚；
  • 自动化搜索空间是否稳定；
  • 失败时能否定位原因；
  • 是否需要保留关键数学步骤；
  • 定理未来变化时是否容易维护。

短小的逻辑胶水适合自动化；论文中的核心推导通常更值得用 calc 和中间 have 保留结构。

证明构造与搜索

apply 与 refine

apply 让 Lean 根据目标匹配定理结论：

1
2
example (a b c : Nat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
  apply le_trans hab hbc

refine 可以显式留下洞：

1
2
3
4
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  refine And.intro ?_ ?_
  · exact hP
  · exact hQ

?_ 是待填 metavariable。复杂结构中，refine 比连续 constructor 更能显示最终证明项形状。

命名洞可以在多个位置共享，但会增加约束传播复杂度。一般只在确实需要从后文反推前文类型时使用。

证明搜索

mathlib 提供搜索型 tactic：

1
2
example (a b : Nat) (h : a = b) : b = a := by
  exact?

编辑器会建议类似：

1
exact Eq.symm h

建议命令适合探索，不适合原样长期保留，因为每次构建都重新搜索会更慢，也可能随环境变化给出不同结果。找到答案后应替换成具体证明。

同理：

  • rw? 寻找改写；
  • simp? 给出可复制的 simp 规则集合；
  • apply? 寻找结论可匹配的定理；
  • aesop? 给出更稳定的 tactic 建议。

等式消去与规范化

相等的消去原理

若 h : a = b，任何依赖 a 的性质都可以沿等式运输到 b。rw、subst、Eq.mp 等最终都建立在相等 recursor 上。

简单函数下保持相等：

1
2
example (f : α → β) {a b : α} (h : a = b) : f a = f b :=
  congrArg f h

依赖类型下，运输会更明显：若有 v : Vector α n 和 h : n = m，把 v 当作 Vector α m 使用需要沿 h 改写类型。

纸面数学常把“相等对象可替换”当作无形步骤；依赖类型要求 elaborator 或证明脚本明确完成运输，因此复杂索引类型的错误信息常出现 Eq.rec、cast 等底层项。

subst 与变量消去

上下文中有变量等式时，subst 可以用一边替换另一边并删除等式：

1
2
3
example (a b : Nat) (h : a = b) : a + b = b + b := by
  subst a
  rfl

相比 rw [h] at *，subst 更明确表达“这两个变量现在视作同一个”，常用于消去构造器注入产生的等式。

simp 的规范方向

simp 不是任意等式搜索器。simp lemma 通常有一个减少复杂度的规范方向，例如：

1
2
3
x + 0  → x
map id  → id
if True → then 分支

交换律通常不直接作为全局 simp 规则，因为：

1
a + b → b + a → a + b → ...

可能循环，或者至少无法定义明显更简单的一边。

给自定义定理加 [simp] 以前应检查：

  • 右侧是否更小、更规范；
  • 是否可能与已有规则形成循环；
  • 是否会过度展开抽象定义；
  • 是否真的适用于几乎所有调用位置。

局部偶尔需要的规则直接写 simp [lemma] 即可，不必注册为全局规则。

simp 的边界

当 simp 完成证明时，它实际上使用了具体的重写定理、逻辑化简和决策过程。可以使用：

1
2
3
set_option trace.Meta.Tactic.simp.rewrite true in
example (n : Nat) : 0 + n + 0 = n := by
  simp

查看改写轨迹，但输出可能很多。更实用的做法是使用 simp? 获得精简建议。

若文章中的关键数学步骤只写 by simp，读者可能不知道用了哪些事实。对于教学代码，可以改成 simp only [...] 或先写自然语言解释。

关系传递

calc 不限于等式，只要环境中有相应的传递关系：

1
2
3
4
5
6
example (a b c d : ℝ)
    (hab : a = b) (hbc : b < c) (hcd : c ≤ d) : a < d := by
  calc
    a = b := hab
    _ < c := hbc
    _ ≤ d := hcd

Lean 会选择等式替换和 </≤ 的传递实例。这样写保留了纸面推导链，比一次 linarith 更能说明证明结构。

证明风格

同一个定理常有多种写法。长期维护时可以遵循：

  1. 一两步能完成时用证明项或 simpa；
  2. 逻辑结构明显时使用 intro、constructor、rcases；
  3. 等式推导使用 calc 或明确的 rw；
  4. 标准化细节交给 simp；
  5. 代数归一化交给领域 tactic；
  6. 核心中间结论用有意义的 have 名称保存；
  7. 自动搜索得到答案后换成稳定、具体的脚本；
  8. 不以最短字符数作为证明质量标准。

证明脚本还要供人阅读。自动化可以处理归一化和重复分支；决定证明思路的中间结论应留在源码中，并使用能说明含义的名称。