Lean 4 的 tactic mode 把证明分解成一系列目标变换步骤。每条 tactic 接收当前的目标状态（一组待证的 ⊢ 句），修改它，产生零个或多个新目标。当所有目标消除完毕，证明关闭。七条核心 tactic——intro、apply、exact、constructor、cases、induction、simp——覆盖了命题逻辑和结构归纳证明的绝大部分场景，各自有精确的语义模型和目标变换规则。

前置阅读：本系列 01 Lake 项目结构与依赖管理、02 Term-mode 与 Tactic-mode 切换心法、03 Universe 与类型层级实战；形式化方法系列 在 Lean 4 中证明经典命题。

intro

语义模型

intro h 处理目标形如 ⊢ A → B 或 ⊢ ∀ x, P x 的情形。它把 goal 的前件或全称绑定变量从目标中移走，引入上下文成为假设，同时把目标替换为后件或实例化的命题。

1
2
3
4
5
6
引入前：
⊢ A → B

执行 intro h 后：
h : A
⊢ B

∀ 的情形：

1
2
3
4
5
6
引入前：
⊢ ∀ (n : Nat), n + 0 = n

执行 intro n 后：
n : Nat
⊢ n + 0 = n

代码示例

1
2
3
4
5
6
7
theorem intro_demo (A B : Prop) : A → B → A := by
  intro ha _hb
  -- InfoView:
  --   ha : A
  --   _hb : B
  --   ⊢ A
  exact ha

intro 可以一次接受多个名字，按顺序引入多层蕴含或全称量词。以下划线开头的名字（_hb）告诉 Lean 该假设在后续证明中不使用，抑制"unused variable"警告。

解构引入

intro 允许直接解构复合类型：

1
2
3
4
5
6
7
theorem intro_destruct (A B : Prop) : A ∧ B → B ∧ A := by
  intro ⟨ha, hb⟩
  -- InfoView:
  --   ha : A
  --   hb : B
  --   ⊢ B ∧ A
  exact ⟨hb, ha⟩

⟨ha, hb⟩ 模式在 intro 里等价于先 intro h 再 obtain ⟨ha, hb⟩ := h。对于嵌套结构，⟨⟨ha, hb⟩, hc⟩ 同样合法。

陷阱

目标不是箭头形式或 ∀ 时调用 intro 会报错：

1
2
-- 报错示例：目标是 Nat，不能 intro
-- theorem bad : Nat := by intro n  -- error: intro tactic failed

在复杂的 simp/ring 目标前过早 intro 有时会让自动化 tactic 无法识别整体结构；遇到这种情况先用自动化 tactic 再 intro 更稳。

exact

语义模型

exact e 是最简单的关闭 tactic：提供一个 term e，要求 e 的类型与当前目标完全匹配（定义等价意义下），目标关闭，不产生新目标。

1
2
3
4
5
引入前：
⊢ A

执行 exact ha（ha : A）后：
No goals

代码示例

1
2
3
theorem exact_demo (A B : Prop) (h : A ∧ B) : A := by
  exact h.1
  -- InfoView: No goals

exact 在混合模式中最常见：tactic block 里用其他 tactic 准备好上下文，最后用 exact 加一个 term 关掉目标，兼顾可读性和紧凑性。

exact?：自动搜索

Lean 4 提供 exact? tactic，当不确定用哪个已知引理关闭目标时，exact? 会搜索局部上下文和已加载的库，返回候选的 exact 调用：

1
2
3
4
-- 在编辑器里写 exact?，InfoView 会提示候选：
-- Try this: exact h.left
theorem exact_question (A B : Prop) (h : A ∧ B) : A := by
  exact?

这不会改变已证明的定理；exact? 本身只是交互辅助工具。

与 term mode 的关系

exact e 等价于把整个 by 块直接替换为 e：

1
2
3
-- 两者完全等价
theorem demo_tac (A B : Prop) (h : A ∧ B) : A := by exact h.1
theorem demo_term (A B : Prop) (h : A ∧ B) : A := h.1

apply

语义模型

apply f 是反向推理（backward reasoning）的核心工具。给定 f : X₁ → X₂ → ... → Xₙ → Goal-Type，apply f 把当前目标 ⊢ Goal-Type 替换为若干新目标 ⊢ X₁、⊢ X₂……⊢ Xₙ，对应 f 的每个尚未满足的参数。

1
2
3
4
5
6
引入前：
⊢ A ∧ B

执行 apply And.intro 后（And.intro : A → B → A ∧ B）：
目标 1：⊢ A
目标 2：⊢ B

代码示例

1
2
3
4
5
6
7
8
9
10
theorem apply_demo (A B : Prop) (ha : A) (hb : B) : A ∧ B := by
  apply And.intro
  -- InfoView（第一个子目标）:
  --   ha : A, hb : B
  --   ⊢ A
  · exact ha
  -- InfoView（第二个子目标）:
  --   ha : A, hb : B
  --   ⊢ B
  · exact hb

apply 也接受带 ∀ 的引理，Lean 会对 universe 和类型参数做统一（unification）：

1
2
3
4
5
6
theorem apply_trans (A B C : Prop) (hab : A → B) (hbc : B → C) (ha : A) : C := by
  apply hbc
  -- InfoView: ⊢ B
  apply hab
  -- InfoView: ⊢ A
  exact ha

每次 apply 只处理结论的最外层箭头，前提变成新目标，从后往前形成一条证明链。

apply 与 exact 的选择

  • 目标的 term 已知且不需要进一步分解：用 exact
  • 目标需要借助某个引理分解成更小的子目标：用 apply

实践上，apply 常用于引入分支（apply Or.inl / apply Or.inr）或链式推理，而 exact 负责叶节点。

陷阱

apply 的统一可能在 universe 或隐式参数上失败，报错形如 failed to synthesize instance 或 type mismatch。这时可以用 @apply 展开所有隐式参数，手动提供歧义处。

constructor

语义模型

constructor 对具有单一构造子（或可以选择第一个构造子）的归纳类型自动拆目标。最常见的场景是 ∧（对应 And.intro）和 ↔（对应 Iff.intro）：

1
2
3
4
5
6
引入前（A ∧ B）：
⊢ A ∧ B

执行 constructor 后：
目标 1：⊢ A
目标 2：⊢ B

Iff 的情形：

1
2
3
4
5
6
引入前：
⊢ A ↔ B

执行 constructor 后：
目标 1：⊢ A → B
目标 2：⊢ B → A

代码示例

1
2
3
4
5
6
7
8
9
10
theorem iff_comm (A B : Prop) (h : A ↔ B) : B ↔ A := by
  constructor
  -- InfoView（第一个子目标）:
  --   h : A ↔ B
  --   ⊢ B → A
  · exact h.mpr
  -- InfoView（第二个子目标）:
  --   h : A ↔ B
  --   ⊢ A → B
  · exact h.mp

constructor 等价于 apply And.intro（对 ∧）或 apply Iff.intro（对 ↔），只是更短、不需要记住具体构造子名称。

对自定义归纳类型

1
2
3
4
5
6
7
8
inductive MyPair (A B : Prop) : Prop where
  | mk : A → B → MyPair A B

theorem mypair_demo (A B : Prop) (ha : A) (hb : B) : MyPair A B := by
  constructor
  -- InfoView: 两个子目标 ⊢ A 和 ⊢ B
  · exact ha
  · exact hb

当归纳类型有多个构造子时，constructor 只选择第一个。要选特定构造子，用 apply ConstructorName 或 refine ⟨_, _⟩。

cases

语义模型

cases h 对一个归纳类型的值 h 做情况分析，针对每个构造子产生一个子目标，同时把构造子的参数引入子目标的上下文。逻辑层面等价于 h.elim（或 Or.elim / And.elim）。

Or 的情形：

1
2
3
4
5
6
7
上下文：h : A ∨ B
目标：⊢ C

执行 cases h with | inl ha => ... | inr hb => ... 后：

子目标 1：ha : A ⊢ C
子目标 2：hb : B ⊢ C

代码示例

1
2
3
4
5
6
7
8
theorem or_elim_demo (A B C : Prop) (h : A ∨ B) (f : A → C) (g : B → C) : C := by
  cases h with
  | inl ha =>
    -- InfoView: ha : A, f : A → C, g : B → C ⊢ C
    exact f ha
  | inr hb =>
    -- InfoView: hb : B, f : A → C, g : B → C ⊢ C
    exact g hb

with | inl ha => | inr hb => 是 Lean 4 的具名情况语法，避免使用 · 分支时因顺序问题造成混淆。对于简单情况，点号语法同样合法：

1
2
3
4
theorem or_elim_dot (A B C : Prop) (h : A ∨ B) (f : A → C) (g : B → C) : C := by
  cases h
  · exact f ‹A›     -- ‹A› 从上下文中搜索类型为 A 的假设
  · exact g ‹B›

‹A› 是 by assumption 的紧凑写法，从上下文找类型匹配的假设。

Nat 上的 cases

1
2
3
4
5
6
7
8
theorem cases_nat (n : Nat) : n = 0 ∨ ∃ m, n = m + 1 := by
  cases n with
  | zero      =>
    -- InfoView: ⊢ 0 = 0 ∨ ∃ m, 0 = m + 1
    exact Or.inl rfl
  | succ m    =>
    -- InfoView: m : Nat ⊢ succ m = 0 ∨ ∃ m', succ m = m' + 1
    exact Or.inr ⟨m, rfl⟩

cases 不提供归纳假设；当证明需要"在更小的 n 上已证"时，应换用 induction。

陷阱

cases h 中如果 h : Prop（不是 Type），情况分析不能产生数据，只能产生 Prop 目标——即不能大消除（见系列第 03 篇）。试图从 h : A ∨ B 里提取一个 Bool 值会遇到 Or.rec can only eliminate into Prop。

induction

语义模型

induction n 对一个归纳类型的值做结构归纳，与 cases 的区别在于：递归构造子的分支里会增加归纳假设（ih）。

1
2
3
4
5
6
7
上下文：n : Nat
目标：⊢ P n

执行 induction n with | zero => ... | succ k ih => ... 后：

分支 zero：⊢ P 0
分支 succ：k : Nat, ih : P k ⊢ P (k + 1)

代码示例

n + 0 = n 的归纳证明，详细标注每步 InfoView：

1
2
3
4
5
6
7
8
9
10
11
12
13
theorem add_zero' (n : Nat) : n + 0 = n := by
  induction n with
  | zero =>
    -- InfoView: ⊢ 0 + 0 = 0
    rfl
  | succ k ih =>
    -- InfoView:
    --   k : Nat
    --   ih : k + 0 = k
    --   ⊢ k + 1 + 0 = k + 1
    rw [Nat.succ_add, ih]
    -- rw [Nat.succ_add] 将 ⊢ k + 1 + 0 = k + 1 变换为 ⊢ (k + 0) + 1 = k + 1
    -- rw [ih] 用 ih : k + 0 = k 将左侧替换，得 ⊢ k + 1 = k + 1，由 rfl 关闭

Nat.succ_add 在 Lean 4 核心库中的签名是 Nat.succ_add : ∀ (n m : Nat), n.succ + m = (n + m).succ；#check Nat.succ_add 可在编辑器里即时确认。

term mode 对比

同一命题，term mode 写法需要显式 Nat.rec：

1
2
3
4
5
6
-- term mode 写法（理解用，不推荐日常使用）
theorem add_zero_term (n : Nat) : n + 0 = n :=
  Nat.rec
    (show 0 + 0 = 0 from rfl)
    (fun k ih => show k.succ + 0 = k.succ from by rw [Nat.succ_add, ih])
    n

tactic mode 的 induction 把 Nat.rec 的参数对应成可读的具名分支，ih 自动出现在上下文，不需要手动传递。这是 tactic mode 在归纳证明上优于 term mode 的典型场景（系列第 02 篇详细讨论过此权衡）。

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

该定理仅依赖 Lean 4 内置的归纳原理，没有引入任何额外公理。

自定义归纳类型

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
inductive Tree (α : Type) : Type where
  | leaf : Tree α
  | node : α → Tree α → Tree α → Tree α

def depth : Tree α → Nat
  | .leaf        => 0
  | .node _ l r  => 1 + max (depth l) (depth r)

theorem depth_nonneg (t : Tree α) : 0 ≤ depth t := by
  induction t with
  | leaf         => simp [depth]
  | node _ l r ihl ihr =>
    -- InfoView:
    --   ihl : 0 ≤ depth l
    --   ihr : 0 ≤ depth r
    --   ⊢ 0 ≤ depth (Tree.node _ l r)
    simp [depth]
    omega

omega 处理线性算术目标，无需手动展开 max 的不等式。

simp

语义模型

simp 是重写自动化 tactic，维护一个等式引理集合（simp set），把目标中匹配的子项替换为等价的更简形式，反复应用直到不动点或超时。

1
2
3
4
5
6
7
simp 调用前：
⊢ (a + b) * 1 = a * 1 + b * 1

simp 调用后（利用 mul_one、mul_add 等标准引理）：
⊢ a + b = a + b

再一步 simp 用 eq_self_iff_true 关闭（或直接由 rfl 关闭）

simp 的语义是：若目标能在已知 simp 引理的反复应用下化简为 True 或 rfl 类的自明目标，则目标关闭。

代码示例

1
2
3
theorem simp_demo (n : Nat) : n * 1 + 0 = n := by
  simp
  -- simp 用 Nat.mul_one 和 Nat.add_zero 化简，直接关闭目标

带参数的 simp：

1
2
3
-- 加入额外引理
theorem simp_with_lemma (n m : Nat) (h : n = m + 1) : n - 1 = m := by
  simp [h, Nat.add_sub_cancel]

simp [h] 把假设 h 临时加入 simp set；simp [Nat.add_sub_cancel] 引入具体的库引理。

simp only

simp 默认使用大量引理（Mathlib 中有数千条），调试时引发意外改写较常见。simp only [lemma₁, lemma₂] 只用指定引理，结果更可预测：

1
2
3
theorem simp_only_demo (n : Nat) : n + 0 = n := by
  simp only [Nat.add_zero]
  -- 只用 Nat.add_zero，目标直接关闭

simp 与 rw 的区别

rw [h] 是单次精确改写：找到目标里与 h 左侧匹配的第一个子项，替换为右侧。simp 是迭代重写，会处理整个目标树并反复应用直到稳定。

  • 目标有固定的一步等式变换：用 rw，清晰可控
  • 目标涉及多步算术/布尔化简，且已知标准库引理可以覆盖：用 simp
  • 需要在证明脚本里留下明确的推导痕迹：用 simp only 列出引理

陷阱

simp 有时把目标化简成一个更复杂的形式，或因引理左右两侧不当循环而死循环（报 maximum recursion depth exceeded）。向 simp set 加入 h : A ↔ B 时，若 A 和 B 都含共同子项，容易触发循环；改用 simp only 并选择单向引理可规避。

term mode 与 tactic mode 的直接对照

以 or_comm 为例，term mode 与 tactic mode 并排展示，对照各 tactic 的等价 term 构造：

1
2
3
4
5
6
7
8
9
10
11
12
-- term mode
theorem or_comm_term (A B : Prop) : A ∨ B → B ∨ A :=
  fun h => h.elim Or.inr Or.inl

-- tactic mode
theorem or_comm_tac (A B : Prop) : A ∨ B → B ∨ A := by
  intro h            -- ← fun h =>
  cases h with
  | inl ha =>        -- ← h.elim (fun ha => ...)
    exact Or.inr ha  -- ← Or.inr ha
  | inr hb =>        -- ←        (fun hb => ...)
    exact Or.inl hb  -- ← Or.inl hb

cases 对应 term 里的 .elim；intro 对应 fun；exact 对应直接写出 term。两版本经过 elaboration 后产生的核心 term 相同，类型检查器看到的是完全等价的证明。

#print axioms 可同时验证：

1
2
3
#print axioms or_comm_term
#print axioms or_comm_tac
-- 两者均输出: does not depend on any axioms

速查表

tactic 典型目标形式 目标变换
intro h ⊢ A → B 或 ⊢ ∀ x, P x 把前件/绑定变量移入上下文，目标变为后件/实例
exact e ⊢ T 提供 e : T，目标关闭
apply f ⊢ C（f : A → B → C） 目标变为 ⊢ A 和 ⊢ B
constructor ⊢ A ∧ B 或 ⊢ A ↔ B 按单构造子拆成子目标
cases h h : T（T 有多个构造子） 按构造子分支产生子目标，无归纳假设
induction n n : T（归纳类型） 按构造子分支，递归分支含 ih
simp [l] 任意目标 用 simp 引理集反复改写，尝试关闭目标

练习

练习 1

补全下面的 tactic 证明，并在每条 tactic 后注释 InfoView 的 ⊢ 状态：

1
2
3
4
theorem and_imp (A B C : Prop) : (A ∧ B) → (A → B → C) → C := by
  intro ⟨ha, hb⟩ f
  -- 此处补全
  sorry

不允许出现未解释的 sorry；去掉 sorry 并完成证明。

练习 2

用 induction 证明加法交换律，仅用 rfl 和 rw（不用 simp）：

1
2
3
4
theorem add_comm' (n m : Nat) : n + m = m + n := by
  induction n with
  | zero      => sorry  -- 提示：用 Nat.add_zero 和 Nat.zero_add
  | succ k ih => sorry  -- 提示：用 Nat.succ_add 和 Nat.add_succ

练习 3

以下证明使用 simp，但 simp 有时过于隐蔽。把它改写为只用 rw 和 exact 的显式版本，并逐行标注 InfoView 中目标的变化：

1
2
3
4
5
6
7
-- 原版（允许 simp）
theorem and_true_iff (A : Prop) : A ∧ True ↔ A := by
  simp

-- 改写为显式版本（不允许 simp）
theorem and_true_iff' (A : Prop) : A ∧ True ↔ A := by
  sorry

提示：需要 constructor、intro、exact，以及 And.intro 的第二个参数用 trivial 关闭。

参考资料