本系列前三篇分别处理了开发环境（01）、目标窗口与证明状态机（02）、Gallina 核心语法（03）。有了这些基础，证明编写的核心工具就是 tactic。Coq 的 tactic 语言（称为 Ltac）本质上是一套操作证明状态的指令集，每条 tactic 执行后，目标列表发生确定性的转移。本篇覆盖最常用的六条 tactic：intro、apply、exact、rewrite、destruct、induction。

tactic 的语义模型

在 Coq 的 Curry-Howard 对应下，每个证明目标 ⊢ T 等价于构造一个类型为 T 的项。tactic 是"构造证明项"这个任务的分解策略：intro 对应 λ 抽象，apply 对应函数应用，exact 对应直接给出项，rewrite 对应等式替换，destruct 对应模式匹配，induction 对应递归定义。

理解这个对应关系有助于预判 tactic 的行为。每条 tactic 执行后，目标要么减少（一个目标被完成或被拆分），要么上下文增加新的假设。若想看 tactic 序列最终构造出了什么样的证明项，可以在证明结束前使用 Show Proof.。

intro

目标变换

intro h 将目标中最外层的全称量词 ∀ x : T, ... 或蕴含 P → Q 的前件移入上下文，命名为 h。

1
2
3
4
5
6
初始目标：⊢ ∀ (n : nat), n + 0 = n

执行 intro n 后：

n : nat
⊢ n + 0 = n

对蕴含：

1
2
3
4
5
6
初始目标：⊢ P → Q

执行 intro h 后：

h : P
⊢ Q

intros 不带参数时一次性引入所有可以引入的量词和蕴含前件；intros h1 h2 h3 依次命名。

示例

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Lemma and_comm_intro : forall (A B : Prop), A /\ B -> B /\ A.
Proof.
  intros A B H.
  (* 目标窗口：
     A B : Prop
     H : A /\ B
     ============================
     B /\ A
  *)
  destruct H as [HA HB].
  split.
  - exact HB.
  - exact HA.
Qed.

常见错误

目标不是 ∀ 或 → 形式时，intro 报错 Nothing to introduce。此时需要先用其他 tactic 变换目标形式，例如用 unfold 展开定义，或用 apply 把目标变成蕴含形式。

另一个陷阱：intro 只能处理最外层的量词。目标是 (∀ n, P n) /\ Q 时，不能直接 intro n，需要先 destruct 拆开合取。

apply

目标变换

apply h 把当前目标与 h 的结论类型进行合一（unification），若成功则将 h 的前提作为新的子目标。

1
2
3
4
5
6
上下文：H : A -> B -> C
当前目标：⊢ C

执行 apply H 后，产生两个子目标：
子目标 1：⊢ A
子目标 2：⊢ B

apply 实现的是逆向推理（backward reasoning）：从结论往前推需要什么前提。

示例

1
2
3
4
5
6
7
8
9
10
11
Lemma modus_ponens : forall (P Q : Prop), P -> (P -> Q) -> Q.
Proof.
  intros P Q HP HPQ.
  apply HPQ.
  (* 目标变换：
     之前：⊢ Q
     apply HPQ 后：⊢ P
     因为 HPQ : P -> Q，apply 用 Q 合一结论，剩下前提 P
  *)
  exact HP.
Qed.

apply 与 exact 的对比（失败 vs 成功）

一个常见误用是在应该用 exact 的地方写 apply，或反过来。

1
2
3
4
5
6
7
8
9
10
11
12
Lemma demo_exact_vs_apply : forall (P : Prop), P -> P.
Proof.
  intros P H.
  (* 当前目标：⊢ P，上下文有 H : P *)

  (* 错误写法 1：apply H 其实也能成功，但行为略有不同 *)
  (* apply H. *)

  (* 当 H 的类型恰好等于目标类型时，exact 更直接 *)
  exact H.
  (* exact H 表示：这个目标的证明项就是 H，无需进一步拆解 *)
Qed.

区别：exact H 要求 H 的类型与目标完全相同（up to definitional equality）；apply H 要求 H 的类型与目标的结论部分合一，可以留下前提子目标。若 H : P -> P 而目标是 ⊢ P，exact H 会失败（类型不匹配），apply H 会生成子目标 ⊢ P。

更典型的失败案例：

1
2
3
4
5
6
7
8
Lemma apply_needs_unification : forall (n : nat), n = n.
Proof.
  intro n.
  (* 尝试 exact eq_refl 会成功，因为 eq_refl : ?x = ?x 与 n = n 合一 *)
  (* 尝试 exact (eq_refl n) 同样成功 *)
  (* 如果写 apply eq_refl，Coq 同样可以处理，因为 eq_refl 没有前提 *)
  exact eq_refl.
Qed.

apply 有一个变体 eapply，允许延迟合一（unification variables 可以在后续 tactic 中再被实例化），适合在某些参数类型尚不明确时使用。

exact

目标变换

exact t 直接提供一个类型为当前目标类型的项 t，证明立即完成（该目标消除）。

1
2
3
4
当前目标：⊢ P
H : P

执行 exact H 后：目标消除，证明完成（若这是唯一子目标）

exact 是最"底层"的 tactic，也最明确：告诉 Coq “这个目标的证明项就是 t，不需要再拆分”。

用 Show Proof. 看证明项

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Lemma show_proof_demo : forall (A : Prop), A -> A.
Proof.
  intros A H.
  Show Proof.
  (* 此时输出类似：
     (fun (A : Prop) (H : A) => ?Goal)
     ?Goal 是还未填入的部分
  *)
  exact H.
  Show Proof.
  (* 此时输出：
     (fun (A : Prop) (H : A) => H)
     即完整的 λ 表达式
  *)
Qed.

Print Assumptions show_proof_demo. 可以列出该定理依赖的公理，确保证明在预期的公理系统内。

1
2
3
Print Assumptions show_proof_demo.
(* 输出：Closed under the global context *)
(* 表示不依赖任何额外公理，完全从 CIC 的规则导出 *)

rewrite

目标变换

rewrite H 利用等式假设 H : a = b，把目标中所有出现 a 的地方替换为 b（从左到右）。rewrite <- H 是反向替换（b 替换为 a）。

1
2
3
4
5
上下文：H : n = m
当前目标：⊢ n + 1 = m + 1

执行 rewrite H 后：
⊢ m + 1 = m + 1

替换后目标变为 m + 1 = m + 1，可用 reflexivity 或 exact eq_refl 完成。

示例

1
2
3
4
5
6
7
Lemma rewrite_demo : forall (n m : nat), n = m -> n + 1 = m + 1.
Proof.
  intros n m H.
  rewrite H.
  (* 目标由 n + 1 = m + 1 变为 m + 1 = m + 1 *)
  reflexivity.
Qed.

链式重写（rewriting chains）可以用 rewrite H1, H2 或多次 rewrite：

1
2
3
4
5
6
7
8
9
Lemma rewrite_chain : forall (a b c : nat), a = b -> b = c -> a = c.
Proof.
  intros a b c H1 H2.
  rewrite H1.
  (* 目标：b = c *)
  rewrite H2.
  (* 目标：c = c *)
  reflexivity.
Qed.

常见错误

rewrite 要求 H 的类型是 lhs = rhs 形式。若 H : P <-> Q 想用 rewrite，需要先提取 H.(proj1) 或 H.(proj2)，或改用 rewrite H 在命题 ⊢ P 时（Coq 8.x 对 iff 的 rewrite 支持有限，需要 setoid_rewrite 或转换）。

另一个陷阱：若 H : a = b 而目标里 a 出现在隐式参数位置，rewrite 可能无法匹配，需要用 rewrite (H : a = b) 显式指定。

destruct

目标变换

destruct H 对 H 进行模式匹配，按 H 的归纳类型的构造子数目拆分为多个子目标，每个子目标对应一个构造子分支。

对合取 H : A /\ B：

1
2
3
4
执行 destruct H as [HA HB] 后，产生一个目标，上下文增加：
HA : A
HB : B
（合取只有一个构造子 conj，所以不分支）

对析取 H : A \/ B：

1
2
3
执行 destruct H as [HA | HB] 后，产生两个子目标：
子目标 1：HA : A ⊢ ...
子目标 2：HB : B ⊢ ...

对自然数 n : nat（destruct 当前目标的变量时不需要 H，直接 destruct n）：

1
2
3
执行 destruct n as [| n'] 后，产生两个子目标：
子目标 1（O 分支）：⊢ ...[n := O]
子目标 2（S n' 分支）：n' : nat ⊢ ...[n := S n']

示例

1
2
3
4
5
6
7
8
9
10
11
12
Lemma destruct_or : forall (P Q R : Prop),
    (P -> R) -> (Q -> R) -> P \/ Q -> R.
Proof.
  intros P Q R HPR HQR H.
  destruct H as [HP | HQ].
  - (* 分支 1：H 是 P *)
    apply HPR.
    exact HP.
  - (* 分支 2：H 是 Q *)
    apply HQR.
    exact HQ.
Qed.

destruct 配合 as 模式（as [...] | [...]）可以同时解包嵌套的构造子。对于更复杂的模式，Coq 8.x 支持嵌套写法 as [[HA HB] | HC]。

destruct vs induction

destruct 对变量进行有限模式分析，不引入归纳假设（induction hypothesis，IH）。若被分析的变量在结论的递归位置出现，需要用 induction 而不是 destruct；用 destruct 后归纳步骤里缺少 IH，证明会卡住。

induction

目标变换

induction n 对自然数（或其他归纳类型）进行归纳，产生若干子目标，并在归纳步骤的上下文中引入归纳假设（IH）。

1
2
3
4
5
6
对 n : nat 执行 induction n as [| n' IH] 后，产生两个子目标：
子目标 1（基础情形 O）：⊢ P O
子目标 2（归纳步骤 S n'）：
  n' : nat
  IH : P n'
  ⊢ P (S n')

归纳假设 IH : P n' 是 destruct 所没有的，它让归纳步骤可以用前一步的结论推导当前步。

示例

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Require Import Arith.

Lemma add_n_O : forall (n : nat), n + 0 = n.
Proof.
  induction n as [| n' IH].
  - (* 基础情形：n = O *)
    (* 目标：O + 0 = O，由 nat 的加法定义 simpl 化简即可 *)
    simpl.
    reflexivity.
  - (* 归纳步骤：n = S n' *)
    (* 归纳假设：IH : n' + 0 = n' *)
    (* 目标：S n' + 0 = S n' *)
    simpl.
    (* simpl 把 S n' + 0 化简为 S (n' + 0) *)
    (* 目标：S (n' + 0) = S n' *)
    rewrite IH.
    reflexivity.
Qed.

Print Assumptions add_n_O. 输出 Closed under the global context，表明这个引理只依赖 CIC 的基础规则和 Arith 库中已有的定义，没有额外公理。

induction 的变量前移

归纳时若被归纳变量之后还有其他变量，这些变量需要在 induction 之前用 revert 移回目标，否则归纳假设会被过度特化（overly specialized IH），导致归纳步骤中 IH 的适用范围太窄。

1
2
3
4
5
6
7
8
9
10
11
12
13
(* 反面示例：IH 被过度特化 *)
Lemma add_comm_wrong_attempt : forall (n m : nat), n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IH].
  - simpl. rewrite <- Nat.add_0_r. reflexivity.
  - simpl.
    (* IH : n' + m = m + n'，此处 m 是固定的 *)
    (* 这个方向通常够用，但若需要对 m 再归纳则 IH 过窄 *)
    rewrite IH.
    rewrite Nat.add_succ_r.
    reflexivity.
Qed.

若 m 也需要在 IH 中保持通用，应在 induction n 之前 revert m，使 IH 的类型变为 ∀ m, n' + m = m + n'。

六条 tactic 的综合示例

以下证明 le_plus_l（n ≤ n + m）综合使用多条 tactic：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Lemma le_plus_l_manual : forall (n m : nat), n <= n + m.
Proof.
  intros n m.
  induction m as [| m' IH].
  - (* m = O：n <= n + O = n，即 n <= n *)
    rewrite Nat.add_0_r.
    (* 目标：n <= n，即 le_n *)
    apply Nat.le_refl.
  - (* m = S m'：归纳假设 IH : n <= n + m' *)
    (* 目标：n <= n + S m' *)
    rewrite Nat.add_succ_r.
    (* 目标：n <= S (n + m') *)
    apply Nat.le_le_succ_r.
    exact IH.
Qed.

目标变换路径：

1
2
3
4
5
6
⊢ n <= n + S m'
→ rewrite Nat.add_succ_r →
⊢ n <= S (n + m')
→ apply Nat.le_le_succ_r →
⊢ n <= n + m'
→ exact IH → 完成

练习

以下三道练习难度递增，均可用本篇六条 tactic 完成，不需要 omega、lia 或 auto。

练习 1（intro + exact）

1
2
3
4
Lemma ex1 : forall (A B C : Prop), A -> B -> C -> A.
Proof.
  (* 提示：intro 三个前提后，exact 正确的假设即可 *)
Admitted.

练习 2（destruct + rewrite）

1
2
3
4
Lemma ex2 : forall (n : nat), n = 0 \/ n <> 0 -> n * 1 = n.
Proof.
  (* 提示：destruct 析取，O 分支用 simpl+reflexivity，S 分支用 Nat.mul_1_r *)
Admitted.

练习 3（induction + rewrite）

1
2
3
4
Lemma ex3 : forall (n : nat), 0 + n = n.
Proof.
  (* 提示：induction n，基础情形 simpl+reflexivity，归纳步骤 simpl+rewrite IH *)
Admitted.

三道练习的参考答案可通过把 Admitted 替换为对应的 tactic 序列后在 Coq 8.19 下编译零警告来验证。

参考资料