Lean 4 提供两种写证明的语法面：term mode 直接给出构造该类型的项；tactic mode 通过一系列指令逐步缩减未完成的目标。两者在语义上等价——任何 tactic 证明最终都被 elaboration 翻译成一个 term，类型检查器只检查 term 层。选择哪种写法是风格决策，但这个决策在实践中有明确的倾向规则。

本篇是"深入 Lean"系列第 02 篇。系列前置知识见《在 Lean 4 中证明经典命题》，该篇已展示了两种模式的基本对照；本篇专注于切换判断本身：什么情况下 term mode 更短、更清晰，什么情况下 tactic mode 更易读、更可维护，以及两种模式如何在同一个证明里混合使用。

Term mode 基础

Term mode 把证明写成一个表达式，该表达式的类型就是命题。Lean 4 的类型论里，命题是类型，证明是居民（inhabitant），“证明成立"等价于"该类型有居民”。

fun、⟨⟩、点投影

1
2
3
4
5
6
7
8
-- 蕴含：函数抽象
theorem impl_intro (A B : Prop) (h : A → B) (a : A) : B := h a

-- 合取：匿名构造子
theorem and_intro (A B : Prop) (ha : A) (hb : B) : A ∧ B := ⟨ha, hb⟩

-- 析取：具名构造子
theorem or_inl (A B : Prop) (ha : A) : A ∨ B := Or.inl ha

从假设里取出合取分量用点投影：

1
2
3
theorem and_elim_left  (A B : Prop) (h : A ∧ B) : A := h.1
theorem and_elim_right (A B : Prop) (h : A ∧ B) : B := h.2
-- h.left / h.right 与 h.1 / h.2 等价；具名字段用前者可读性更好

show 可在 term 里插入局部类型注解：

1
2
theorem and_elim_left' (A B : Prop) (h : A ∧ B) : A :=
  show A from h.1

show 在 elaboration 上不做任何事，只起文档作用。在嵌套项里，它是告诉读者"此处期望类型是 T"的最轻量标记。

解构绑定

Lean 4 允许在 fun 参数里直接解构：

1
2
theorem and_comm_term (A B : Prop) : A ∧ B → B ∧ A :=
  fun ⟨ha, hb⟩ => ⟨hb, ha⟩

嵌套解构同样合法：

1
2
theorem and_assoc_term (A B C : Prop) : (A ∧ B) ∧ C → A ∧ (B ∧ C) :=
  fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩

匿名构造子 ⟨ha, hb, hc⟩ 对 A ∧ (B ∧ C) 自动右结合，等同于 ⟨ha, ⟨hb, hc⟩⟩。

#check 验证类型

在任意 term 上调用 #check 可确认类型，无需跑完整的 lake build：

1
2
#check @And.intro  -- And.intro : ∀ {a b : Prop}, a → b → a ∧ b
#check @Or.inl     -- Or.inl : ∀ {a b : Prop}, a → a ∨ b

Tactic mode 基础

by 关键字打开一个 tactic 块。进入 tactic mode 后，编辑器右栏（InfoView）显示当前待证的目标（⊢），每一步 tactic 消费或转换目标，直到 No goals。

核心 tactic 速查

tactic 典型用途
intro h 把 ⊢ A → B 里的前件 A 引入上下文为 h : A
exact e 用 term e 关闭当前目标
apply f 用 f : X → ⊢-goal 反推，把目标替换为 X
constructor 对单构造子目标（And、Iff 等）拆成多个子目标
cases h 对多构造子归纳类型分情况
induction n 对归纳类型做归纳
simp 自动用一组等式归约目标
rw [h] 用等式 h 改写目标

InfoView 的 goal 状态跟踪

and_comm 的 tactic 版本，逐步展示 InfoView 的变化：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
theorem and_comm_tac (A B : Prop) : A ∧ B → B ∧ A := by
  intro h
  -- InfoView:
  --   h : A ∧ B
  --   ⊢ B ∧ A
  constructor
  -- InfoView（两个子目标，当前是第一个）:
  --   h : A ∧ B
  --   ⊢ B
  · exact h.2
  -- InfoView（第二个子目标）:
  --   h : A ∧ B
  --   ⊢ A
  · exact h.1

每一行 tactic 之后光标悬停，InfoView 刷新；Lean 4 的标准工作方式是写一步、看一步目标，不是盲写整段再回头检查。

#print axioms 可查看一个已证定理依赖了哪些公理，确认证明没有悄悄引入不期望的假设：

1
2
#print axioms and_comm_tac
-- 输出: 'and_comm_tac' does not depend on any axioms

两种模式的直接对照

同一个定理 A ∧ B → B ∧ A，三种写法并排：

1
2
3
4
5
6
7
8
9
10
11
12
13
-- 纯 term mode
theorem and_comm_term' (A B : Prop) : A ∧ B → B ∧ A :=
  fun ⟨ha, hb⟩ => ⟨hb, ha⟩

-- 纯 tactic mode
theorem and_comm_tac' (A B : Prop) : A ∧ B → B ∧ A := by
  intro ⟨ha, hb⟩
  exact ⟨hb, ha⟩

-- 混合：tactic 外壳 + term 内核
theorem and_comm_hybrid (A B : Prop) : A ∧ B → B ∧ A := by
  intro h
  exact ⟨h.2, h.1⟩

三者被 elaboration 处理后产生的 term 完全相同。区别纯粹在于书写时的脚手架。

蕴含链的例子展示 term mode 更简洁的场景：

1
2
3
4
5
6
7
8
9
10
11
-- (A → B) → (B → C) → (A → C) 的证明

-- term mode：直接复合
theorem comp_term (A B C : Prop) (f : A → B) (g : B → C) : A → C :=
  fun a => g (f a)

-- tactic mode：相对冗长
theorem comp_tac (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
  intro a
  apply g
  exact f a

(A → B) → (B → C) → (A → C) 的证明结构就是函数复合，没有任何分支；term mode 一行表达完毕，tactic mode 反而引入了多余的语法噪声。

何时选 term mode，何时选 tactic mode

term mode 适合的情形

  • 证明结构与类型签名直接对应：看到类型就知道该写什么
  • 单一路径的构造（无分支、无归纳）：fun、⟨⟩、点投影足够
  • 引理组合：已有若干引理，证明只是把它们串起来

tactic mode 适合的情形

  • 证明路径不直接可见：需要 InfoView 辅助探索
  • 需要分情况讨论（cases）或归纳（induction）
  • simp 或 omega 等自动化 tactic 能处理的算术/等式目标
  • 多步推理时 tactic 的"一步一目标"比 term 嵌套更清楚

自然数归纳是 tactic mode 明显更优的场景：

1
2
3
4
5
6
7
8
9
10
-- 0 + n = n，需要在 n 上归纳
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih =>
      -- InfoView:
      --   k : Nat
      --   ih : 0 + k = k
      --   ⊢ 0 + (k + 1) = k + 1
      rw [Nat.add_succ, ih]

term mode 写同一个证明需要显式 Nat.rec：

1
2
3
-- 不推荐的写法，仅供对照
theorem zero_add_term (n : Nat) : 0 + n = n :=
  Nat.rec rfl (fun k ih => by rw [Nat.add_succ, ih]) n

Nat.rec 调用里的 ih 参数在 term 层是一个普通的函数参数，没有 tactic 的"在上下文里看到 ih"这种形式——因此 term mode 在归纳证明里几乎总是更难读。

混合写法

exact (term) 在 tactic 块里

一旦目标的 term 构造已知，直接 exact 提供 term，无需继续展开 tactic：

1
2
theorem and_comm_exact (A B : Prop) (h : A ∧ B) : B ∧ A := by
  exact ⟨h.2, h.1⟩   -- tactic 块里用 term 构造直接关掉目标

(by tactic) 在 term 里

term 的某个分量难以直接给出时，可在 term 里局部切换到 tactic：

1
2
3
-- 复杂构造的某一项用 tactic 处理
theorem complex_mix (A B C : Prop) (h : A ∧ (B ∧ C)) : C ∧ A :=
  ⟨by exact h.2.2, h.1⟩

by exact h.2.2 和直接写 h.2.2 效果完全相同；真正有用的场景是 by 里有多步推理，比如需要 rw 或 simp 才能关掉的分量。

have 的两种形式

have 在两种模式里都可用，且可以跨模式赋值：

1
2
3
4
5
6
7
8
9
10
-- tactic 块里，have 的值既可是 term 也可是 by 块
theorem have_demo (A B C : Prop) (f : A → B) (g : B → C) (a : A) : C := by
  have hb : B := f a           -- term 赋值
  have hc : C := by exact g hb -- by 块赋值，效果相同
  exact hc

-- 等价的全 term 写法
theorem have_demo_term (A B C : Prop) (f : A → B) (g : B → C) (a : A) : C :=
  let hb : B := f a
  g hb

tactic 里的 have 对应 term 里的 let（非递归绑定）。两者在 elaboration 后是同一个 let 节点。

决策框架

情况 推荐模式 原因
类型签名已完全确定证明结构 term 无需脚手架
单一构造，无分支 term fun/⟨⟩ 比多行 tactic 短
需要分情况（Or、自定义归纳类型） tactic cases 语法更清晰
需要归纳 tactic InfoView 能看到每步归纳假设
目标涉及算术等式 tactic simp/omega 自动化
多步推导，需要可读性 tactic 步骤可逐行读懂
已知引理直接串联 term 或混合 exact (f ∘ g) 等风格
某一分量难以直接写出 混合 主体 term，局部 by

Lean/Mathlib 社区的惯例：简单的单步或双步命题倾向于 term mode；需要 simp、ring、linarith、omega 等自动化策略的几乎都是 tactic mode；库代码里大量出现 by simp [...] 或 by rw [...]; simp，极少见纯 term 写的归纳证明。

练习

练习 1

用 term mode 证明：

1
2
theorem impl_trans (A B C : Prop) (f : A → B) (g : B → C) : A → C :=
  sorry

提示：答案是一个字面的函数复合表达式。

练习 2

用 tactic mode 证明，并在关键步骤注释 InfoView 的 ⊢ 状态：

1
2
theorem or_comm_tac (A B : Prop) : A ∨ B → B ∨ A := by
  sorry

提示：需要 intro、cases、Or.inl/Or.inr。

练习 3

将下面的 tactic 证明改写为等价的 term mode 版本，使用 fun 和解构绑定：

1
2
3
4
5
6
7
8
-- 已有的 tactic 版本（不要修改）
theorem and_swap_tac (A B C : Prop) : A ∧ B ∧ C → B ∧ C ∧ A := by
  intro ⟨ha, hb, hc⟩
  exact ⟨hb, hc, ha⟩

-- 请完成 term mode 版本
theorem and_swap_term (A B C : Prop) : A ∧ B ∧ C → B ∧ C ∧ A :=
  sorry

参考资料