第 07 篇把 Lean 4 环境装好了。本篇真在 Lean 4 里写一组经典命题的完整证明：合取交换律、析取交换律、等价、自然数加法交换律、列表拼接长度。每条命题给出 term mode 与 tactic mode 两种写法。

读完本篇之后，"在 Lean 4 中写一段非平凡证明"对读者来说不再是抽象。系列的主线问题"为什么编译通过就是定理得证"也由这些可在 InfoView 里看到 No goals 的具体证明落到肌肉记忆。

推荐的最小工程结构

把本篇所有代码放进 FormalIntro/First_Theorems.lean：

1
2
3
4
5
6
namespace FormalIntro.First

-- 后面的代码都在这里
-- ...

end FormalIntro.First

每条命题都写两遍：term mode 优先，tactic mode 对照。看到等价的两种形态可以加深"tactic 是构造项的元程序"这条直觉。

命题逻辑

合取交换律

1
2
3
4
5
6
7
8
-- term mode
theorem and_comm_t (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

-- tactic mode
theorem and_comm_b (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro ⟨p, q⟩
  exact ⟨q, p⟩

⟨p, q⟩ 是 anonymous constructor，用同一个语法构造 And、Prod、Sigma、Exists——四件事在 Lean 内部都是单构造子的归纳类型。

合取结合律

1
2
3
4
5
6
theorem and_assoc_t (P Q R : Prop) : (P ∧ Q) ∧ R → P ∧ (Q ∧ R) :=
  fun ⟨⟨p, q⟩, r⟩ => ⟨p, q, r⟩

theorem and_assoc_b (P Q R : Prop) : (P ∧ Q) ∧ R → P ∧ (Q ∧ R) := by
  intro ⟨⟨p, q⟩, r⟩
  exact ⟨p, q, r⟩

term mode 利用嵌套解构一步到位。Lean 4 的 anonymous constructor 支持自动右结合：⟨p, q, r⟩ 等同 ⟨p, ⟨q, r⟩⟩。

析取交换律

1
2
3
4
5
6
7
8
9
10
theorem or_comm_t (P Q : Prop) : P ∨ Q → Q ∨ P :=
  fun h => match h with
    | Or.inl p => Or.inr p
    | Or.inr q => Or.inl q

theorem or_comm_b (P Q : Prop) : P ∨ Q → Q ∨ P := by
  intro h
  cases h with
  | inl p => exact Or.inr p
  | inr q => exact Or.inl q

Or 是两构造子的归纳类型，所以析取的证明必须做分情况讨论：term mode 用 match，tactic mode 用 cases。

等价

1
2
3
4
theorem and_comm_iff (P Q : Prop) : (P ∧ Q) ↔ (Q ∧ P) := by
  constructor
  · intro ⟨p, q⟩; exact ⟨q, p⟩
  · intro ⟨q, p⟩; exact ⟨p, q⟩

Iff 的构造子也是 anonymous ⟨_, _⟩（两个方向）。constructor 把目标拆成两个子目标，分别对应 → 与 ←。· 是分支项目符号，让两条子证明视觉对齐。

不被构造的命题

故意写一条直觉主义证不出来的命题，看 Lean 怎么拒绝：

1
2
-- theorem em (P : Prop) : P ∨ ¬P := by
--   sorry  -- 不展开

直接 by exact ? 会卡在没有"通用方法"区分 P 与 ¬P。Lean 4 不阻止你引入 Classical.em 公理来强行接受排中律——但这会把信任面扩大（第 09 篇展开）。

自然数

Nat 的加法在 Lean 4 里定义为：

1
2
n + 0       = n
n + succ m  = succ (n + m)

按第二参数递归。意味着 n + 0 = n 定义性成立，0 + n = n 需要归纳。

n + 0 = n：定义性等式

1
2
theorem my_add_zero (n : Nat) : n + 0 = n :=
  rfl

rfl 在这里直接走通：两边按定义同形。Lean 内核的判等过程把 n + 0 归约成 n，比较两个 Nat 项相同。

0 + n = n：要走归纳

1
2
3
4
5
6
theorem my_zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih =>
      show 0 + (k + 1) = k + 1
      rw [Nat.add_succ, ih]

induction n with 调用 Nat.rec 给出 zero 与 succ 两个分支：

  • zero 分支需要证 0 + 0 = 0，按定义 rfl。
  • succ 分支需要证 0 + (k + 1) = k + 1，假设已有 ih : 0 + k = k。rw 用 Nat.add_succ : n + succ m = succ (n + m) 把左侧改写成 succ (0 + k)，再用 ih 把 0 + k 改写成 k，得到 succ k = k + 1，即 k + 1 = k + 1，自动归约成立。

n + succ m = succ (n + m)

1
2
theorem my_add_succ (n m : Nat) : n + (m + 1) = (n + m) + 1 :=
  rfl

直接 rfl，是 Nat.add 的第二条递归 case 的字面形式。

加法交换律

1
2
3
4
5
6
7
8
theorem my_add_comm (n m : Nat) : n + m = m + n := by
  induction m with
  | zero =>
      show n + 0 = 0 + n
      rw [Nat.add_zero, my_zero_add]
  | succ k ih =>
      show n + (k + 1) = (k + 1) + n
      rw [Nat.add_succ, ih, ← Nat.succ_add]

证明走 m 上的归纳。两个分支：

  • m = 0：两边经 add_zero 与 zero_add 归约到同一形式。
  • m = k + 1：把左侧用 Nat.add_succ 展开，用归纳假设 ih : n + k = k + n 替换，再把右侧用 Nat.succ_add 反向收回。

工业用法里大多数读者会直接 exact Nat.add_comm n m——Lean 4 标准库已经证过。但手写一遍是练熟 tactic 的最直接路径。

列表

List α 在 Lean 4 里定义：

1
2
List α := nil | cons α (List α)
xs ++ ys = ...  按 xs 递归

长度可加

1
2
3
4
5
6
7
theorem length_append (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length := by
  induction xs with
  | nil =>
      simp
  | cons x xs ih =>
      simp [ih, Nat.succ_add]

simp 在这里展开 List.length、List.append、Nat.add 这些定义，把两边归约到同形。simp [ih] 把 ih 当成重写规则使用。

反转两次等于原列表

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
def myReverse : List α → List α
  | []      => []
  | x :: xs => myReverse xs ++ [x]

theorem myReverse_append (xs ys : List α) :
    myReverse (xs ++ ys) = myReverse ys ++ myReverse xs := by
  induction xs with
  | nil => simp [myReverse]
  | cons x xs ih => simp [myReverse, ih, List.append_assoc]

theorem myReverse_myReverse (xs : List α) :
    myReverse (myReverse xs) = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
      simp [myReverse, myReverse_append, ih]

证明的骨架严格按"列表归纳"走：nil 用 simp 或 rfl 把两边按定义归约；cons 用归纳假设 ih 加几条已证引理改写。这正是第 06 篇所说的"递归即归纳法"——一段证明的 tactic 脚本几乎就是按数据结构滑过的递归调用。

用 #print 看证明的真实形态

tactic 写的证明最终被 Lean 4 编译成 term mode 的项。#print 可以把它显式打印出来：

1
#print and_comm_b

InfoView 显示形如：

1
2
3
theorem FormalIntro.First.and_comm_b :
    ∀ (P Q : Prop), P ∧ Q → Q ∧ P :=
  fun P Q h => ⟨h.right, h.left⟩

tactic 脚本被 elaboration 翻译回 term。这正是"tactic 不绕过类型检查"的实证：所有 tactic 最终落到一段被类型检查通过的 term。

常用 tactic 速查表

下面这八条 tactic 覆盖系列里 90% 的需求：

tactic 作用
intro x 把目标 A → B 的假设引入上下文
exact e 用具体 term e 关闭当前目标
apply f 用函数 f 反推，需要进一步构造其前提
cases h / match h with 对归纳类型的项做分情况讨论
induction n 调用归纳子，对归纳类型做归纳证明
rfl 用定义性归约关闭 = 目标
rw [h] 用等式 h 改写当前目标或假设
simp / simp [...] 自动用一组等式与规则归约目标

constructor / repeat / try / by_contra / omega 之类后续接触。前八条已经足够把本篇所有定理跑通。

错误的样态与修法

写错的几种典型情形：

错误信息 含义 通常的修法
unknown identifier 'foo' 引用了不存在的名字 检查拼写、检查 import、检查 namespace
type mismatch ... 项与期望类型不匹配 比较 InfoView 给的"推断 vs 期望"，找差异
failed to prove ... tactic 走完仍有目标未关闭 看剩余 goal 是什么，补对应 tactic
unsolved goals 同上 用 sorry 临时占位，回头补
simp made no progress simp 没找到能用的等式 显式 rw 或者 simp [lemma1, lemma2] 列出引理

读 Lean 错误的肌肉记忆：先看错误类型，再看 InfoView 当前 goal，再看 Messages 里的具体行号。三段对齐后大概率能定位。

关于 sorry

Lean 4 允许写：

1
theorem todo : ∀ n : Nat, n + 0 = n := by sorry

sorry 接受任何目标，跳过证明义务。它是开发期的临时占位。这条机制的代价是：一旦 sorry 出现，整个文件不再可信。Lean 会用警告标出 sorry，最终发布的库要求零 sorry。

Mathlib 的 CI 会拒绝任何含 sorry 的合并。形式化项目对"信任面"的边界严苛到这个程度。

模式提炼

模式 内容
写两遍 term mode 与 tactic mode 互译，加深"tactic 是元程序"的直觉
按定义归约 等式两边如能按 def 归约同形，rfl 即可关
不齐则归纳 等式两边按定义不能归约同形时，找一个能归纳的变量
引理即等式 常用引理（Nat.add_succ、List.append_assoc）就是 rw 与 simp 的弹药
sorry 是临时记号 永远不要把 sorry 留到最终库；它的存在意味着信任面破口

给读者的练习

  1. 证 theorem or_assoc (P Q R : Prop) : (P ∨ Q) ∨ R ↔ P ∨ (Q ∨ R)。
  2. 证 theorem nat_add_assoc (a b c : Nat) : (a + b) + c = a + (b + c)，给出 term mode 与 tactic mode 两种写法。
  3. 证 theorem length_myReverse (xs : List α) : (myReverse xs).length = xs.length。
  4. 试试故意省略一条 tactic（比如把 induction n 写完后只写 | zero => rfl 不写 succ 分支），观察 InfoView 怎样列出剩余目标。
  5. 把 (fun x : Nat => x + 0) 与 (fun x : Nat => x) 用 #check 看类型；用 #eval (fun x => x + 0) 5 与 #eval id 5 比较。

衔接到下一篇

本篇让"在 Lean 中证经典命题"变成肌肉记忆。但写完证明后总会有一个问题挂在头顶：

我相信 Lean 编译通过等价于定理得证。但这条信任传到底是信什么？

下一篇专门讨论类型检查器的可信基底（TCB）：内核是什么、坏公理会怎样让整个系统崩、sorry 与 Classical.choice 这类"逃生门"分别在信任面上打了多大的洞、为什么"信内核"是形式化方法在工程上能站稳脚跟的根本原因。

参考资料