本系列前三篇分别处理了开发环境（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 报错：

1
Error: No product even after head-reduction.

"head-reduction 之后仍然不是 product（依值函数类型）"就是这条消息的字面意思。此时需要先用其他 tactic 变换目标形式，例如用 unfold 展开定义暴露出被藏起来的 →。

另一个陷阱：intro 只能处理最外层的量词。目标是 (∀ n, P n) /\ Q 时，∀ 埋在合取的左支里，intro n 会报上面那条错。合取在目标位置要用 split 拆成两个子目标，进到左支之后才轮到 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
Lemma demo_exact_vs_apply : forall (P : Prop), P -> P.
Proof.
  intros P H.
  (* 当前目标：⊢ P，上下文有 H : P *)

  (* 这一处 apply H 和 exact H 都能关掉目标，因为 H 没有前提可剥 *)
  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，但前提是先 Require Import Setoid.——iff 的可重写性来自广义重写（generalized rewriting）机制，Setoid 模块把 SetoidTactics 连带 Morphisms_Prop 里 and / or / not / ex / all 对 iff 的 Proper 实例一起拉进来。不 Require 就只报"找不到关系"。

另一个陷阱：rewrite H 会把所有匹配到的位置一起换掉，这经常不是想要的。要限制位置用 at 子句（rewrite H at 2），或者给引理补足显式参数把模式钉死（rewrite (Nat.add_comm n m)）。反过来，如果该换的地方没被换掉，先开 Set Printing All. 看一眼隐式参数和 coercion——rewrite 匹配的是脱糖后的项，屏幕上看着一样的两个式子未必真的一样。

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.

as 模式里 | 分隔构造子分支、空格分隔同一分支内的参数，所以 as [HA HB] 是"一个分支两个参数"，as [HA | HB] 是"两个分支各一个参数"。嵌套可以再套一层方括号：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 的变量前移

intros 引入的变量，凡是在 induction 之前落进上下文的，都会被钉死在归纳假设里。intros n m; induction n 得到的 IH 是 n' + m = m + n'——只谈那个特定的 m。有时候这够用：

1
2
3
4
5
6
7
8
9
10
11
Lemma add_comm_fixed_m : 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 是固定的那一个 *)
    rewrite IH.
    rewrite Nat.add_succ_r.
    reflexivity.
Qed.

归纳步骤里 m 始终是同一个值，所以特化过的 IH 正好对得上。

真正会卡住的是归纳步骤需要换一个 m 的情形。典型例子是 double 的单射性：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Fixpoint double (n : nat) : nat :=
  match n with
  | 0    => 0
  | S k  => S (S (double k))
  end.

Lemma double_injective_stuck : forall (n m : nat), double n = double m -> n = m.
Proof.
  intros n m H.
  induction n as [| n' IH].
  (* IH : double n' = double m -> n' = m *)
  (* S n' 分支里必须先 destruct m 得到 m'，
     此时需要的是 double n' = double m' -> n' = m'，
     而 IH 只有 m 那一版，用不上 *)
Abort.

把 m 留在目标里就没这个问题：intros n. induction n as [| n' IH]. 之后 IH 的类型是 forall m, double n' = double m -> n' = m，destruct m 出 m' 后直接 apply IH 即可。已经 intros 进来的变量可以用 revert m 送回目标，效果相同。这条经验在第 13 篇讨论卡住模式时还会再遇到一次。

六条 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 完成，不需要 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 = 1 -> n * 1 = n.
Proof.
  (* 提示：destruct 析取拿到两条等式，各自 rewrite 后目标都是闭项，reflexivity 直接算得出来 *)
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 序列之后，用 Print Assumptions ex1. 自查：输出 Closed under the global context 才算真的证完。只要还留着 Admitted，Coq 会把该引理本身当成公理列出来。

参考资料