深入 Coq 02：目标窗口与 tactic 交互模型

Coq 的证明过程不是一次性写出完整的证明项，而是通过 tactic 序列逐步缩减待完成的工作。每执行一条 tactic，Coq 会更新"当前需要证明的内容"，直到不再有任何待证目标，Qed 才能通过。这个状态驱动的交互过程有一个专用的视图——目标窗口（goal window）。

证明状态机

每个 Proof. 之后，Coq 内部维护一个证明状态（proof state），其结构是一个目标列表，每个目标由两部分组成：

context (上下文 / 假设区)
━━━━━━━━━━━━━━━━━━━━━━━━━━
goal (当前要证明的命题)

在 CoqIDE 或 VS Code vscoq2 插件里，这个结构对应右侧的 Goals 面板。在 Proof General (Emacs) 里，它出现在 *goals* 缓冲区。在命令行 coqtop 里，每执行完一条 tactic 后，Coq 打印出更新后的状态。

分隔符 ============================ 是可视化的 ⊢ 符号。分隔符上方是已知假设，下方是当前目标。

初始状态（刚进入 Proof. 时）：

1 goal(s)
  
A, B : Prop
H : A /\ B
============================
B /\ A

这意味着：上下文里有三个已知量——A、B 是 Prop 类型，H 是 A /\ B 的证据；要证明的是 B /\ A。每执行一条 tactic，这个状态就转移一次。

tactic 执行是不可逆的提交（在 coqtop 里）。CoqIDE 和 vscoq2 支持双向步进，即向前执行也可向后撤回，本质上是维护了一条状态历史链。

逐步演示：A /\ B → B /\ A

以 forall A B : Prop, A /\ B -> B /\ A 为例，记录目标窗口在每条 tactic 后的状态。

起点

Lemma and_swap : forall A B : Prop, A /\ B -> B /\ A.
Proof.

状态：

1 goal(s)
  
============================
forall A B : Prop, A /\ B -> B /\ A

执行 intros A B H.

intros A B H.

intros 把 forall 约束的变量和函数参数逐一移入上下文。执行后：

1 goal(s)
  
A, B : Prop
H : A /\ B
============================
B /\ A

目标从 forall A B : Prop, A /\ B -> B /\ A 变成 B /\ A，三个量（A、B、H）出现在假设区。

执行 destruct H as [HA HB].

destruct H as [HA HB].

destruct 拆解归纳类型的构造子。A /\ B 在 Coq 里定义为 Inductive and (A B : Prop) : Prop := conj : A -> B -> A /\ B，destruct 把 H 拆成两个分量：

1 goal(s)
  
A, B : Prop
HA : A
HB : B
============================
B /\ A

执行 split.

split.

split 是 constructor 1 的别名，对于 and 只有一个构造子 conj，所以它把单个目标 B /\ A 分裂成两个子目标：

2 goal(s)
  
goal 1:
A, B : Prop
HA : A
HB : B
============================
B

goal 2:
A, B : Prop
HA : A
HB : B
============================
A

此时 Coq 进入多目标状态，默认焦点在第一个目标。

用 bullet point 依次完成两个子目标

- exact HB.
- exact HA.

- 是最常见的 bullet 标记（还有 +、*），用于明确标注当前处理哪个子目标，便于阅读和调试。每个 bullet 下只处理一个目标：

• exact HB.：目标是 B，HB : B 精确匹配，Goal 1 完成。
• exact HA.：目标是 A，HA : A 精确匹配，Goal 2 完成。

Qed

Qed.

所有目标消除，Qed 通过，Coq 打印 and_swap is defined。

完整代码：

Lemma and_swap : forall A B : Prop, A /\ B -> B /\ A.
Proof.
  intros A B H.
  destruct H as [HA HB].
  split.
  - exact HB.
  - exact HA.
Qed.

Show Proof. 暴露证明项

tactic 序列是构造证明项的指令流。每执行一条 tactic，Coq 内部就在逐步填充一个 lambda 项，其中尚未完成的位置用 hole（?Goal）占位。Show Proof. 命令在任意时刻打印这个部分构建的项。

在 intros A B H. 之后执行 Show Proof.，输出类似：

(fun (A B : Prop) (H : A /\ B) => ?Goal)

在 destruct H as [HA HB]. 之后：

(fun (A B : Prop) (H : A /\ B) =>
   match H with
   | conj HA HB => ?Goal
   end)

在 split. 之后（两个 goal，所以有两个 hole）：

(fun (A B : Prop) (H : A /\ B) =>
   match H with
   | conj HA HB => conj ?Goal1 ?Goal2
   end)

完成两个 exact 后，Show Proof. 打印完整项：

(fun (A B : Prop) (H : A /\ B) =>
   match H with
   | conj HA HB => conj HB HA
   end)

这就是 and_swap 的证明项实体——一个接收 A、B、H 三个参数，对 H 做模式匹配，重新打包成 conj HB HA 的函数。

直接写项：同一个证明

Coq 支持不使用 tactic，直接用 Definition 或 Lemma ... := 形式给出证明项：

Lemma and_swap_term : forall A B : Prop, A /\ B -> B /\ A :=
  fun A B H =>
    match H with
    | conj HA HB => conj HB HA
    end.

这与 tactic 版本等价——两者最终提交给 Coq kernel 检查的证明项完全相同。区别仅在于写法：tactic 交互式地逐步填充项；直接写项则要求一次性给出完整的 lambda 表达式。

前置系列「命题即类型：Curry-Howard 同构」中讨论过，A /\ B 对应积类型，match 对应消费积类型，conj 对应构造积类型。tactic destruct 对应 match，tactic split + exact 对应 conj。目标窗口里看到的每一步变化，都是对 Curry-Howard 对应表的一次具体操作。

失败的尝试

一个常见错误是直接用 apply 配合错误的假设名：

Lemma and_swap_fail : forall A B : Prop, A /\ B -> B /\ A.
Proof.
  intros A B H.
  split.
  - apply H.  (* 失败 *)

此时目标是 B，H : A /\ B。apply H 会尝试把 H 的类型 A /\ B 当作函数 ? -> B 来用，但 A /\ B 不是函数类型，unification 失败，Coq 报错：

Error: Unable to apply lemma of type "A /\ B" on a term of type "B"

正确做法是先 destruct H as [HA HB]，得到 HB : B，再 exact HB.。

另一个常见错误是忘记 split 直接尝试构造：

exact (conj HB HA).  (* 假设还未 destruct H *)

如果还未执行 destruct，上下文里没有 HA、HB，Coq 报 Unbound value HA。tactic 错误的诊断方式是观察当前上下文——只有上下文里存在的名字才能使用。

多目标导航：{ } 与 bullet

当目标数量超过一个时，有两种常见的导航写法。

Bullet 写法（推荐，用于目标层级较浅的情况）：

split.
- exact HB.
- exact HA.

-、+、* 分别对应三级 bullet，嵌套使用时按层级交替：

split.
- split.
  + exact HB.
  + exact HA.
- exact HA.

花括号写法（适合每个子目标需要多条 tactic 的情况）：

split.
{ exact HB. }
{ exact HA. }

{ 和 } 明确划定一个子目标的处理范围，括号内所有 tactic 只针对进入 { 时的当前目标。括号关闭时 Coq 验证该目标已消除；若未消除则报错，不会静默遗漏。

两种写法可以混用，但同一层次的子目标应该统一使用同一种符号，否则影响可读性。

Print Assumptions. 查依赖公理

Print Assumptions. 打印一个已证明引理所依赖的全部公理。标准库里大量结论依赖经典逻辑公理 classic : forall P : Prop, P \/ ~ P 或函数外延性 functional_extensionality。

对刚才的 and_swap：

Print Assumptions and_swap.

输出：

Closed under the global context

含义是 and_swap 只依赖 Coq 的 CIC（Calculus of Inductive Constructions）内核规则，不依赖任何额外公理。这是构造性证明的理想状态。

如果一个定理的 Print Assumptions 输出包含 Axiom Classical_Prop.classic 或 Axiom propext : forall A B : Prop, (A <-> B) -> A = B，则该定理在 ZFC 意义下是有效的，但在 Curry-Howard 意义下可能失去计算内容（classical axioms 破坏程序提取的效果）。

前置系列「类型检查器的可信基底：编译通过到底信什么」中讨论了公理对可信基底（trusted computing base）的影响，Print Assumptions 是在 Coq 里直接量化这种影响的工具。

tactic 与状态变换速查

tactic	作用描述	状态变化
intros x y H	将前缀 forall/-> 的量移入上下文	目标减少 forall x, ... 或 P -> Q 前缀；x, y, H 出现在假设区
apply H	用 H : A -> B（或更高阶）将目标 B 变为 A	目标从 B 变成 H 的所有前提
exact H	断言 H 的类型与当前目标精确匹配	当前目标消除
destruct H as [...]	拆解归纳类型 H 的构造子	H 消失，其组成部分出现在假设区；可能产生多个子目标
split	对积类型目标（/\、exists 等）调用构造子	当前目标替换为各分量目标，目标数增加
constructor n	调用目标类型的第 n 个构造子	类似 split，更通用
induction n	对变量 n 做归纳，产生基础情形和归纳步	当前目标替换为归纳模式的各个情形
rewrite H	用 H : a = b 将目标中的 a 替换为 b	目标中 a 的出现被替换
reflexivity	证明 a = a 形式的目标	目标消除
assumption	在上下文里寻找与目标精确匹配的假设	找到则目标消除，找不到则报错
simpl	执行计算规则（beta/delta/iota 规约）	目标化简，但不消除
Show Proof.	打印当前部分构建的证明项（非 tactic，元命令）	状态不变，仅输出

给读者的练习

练习一（基础）

不使用 tauto 或 auto，用 intros、destruct、split、exact 证明以下引理，并在每条 tactic 之后用 Show Proof. 观察项的构建过程：

Lemma and_assoc_lr : forall A B C : Prop,
  (A /\ B) /\ C -> A /\ (B /\ C).
Proof.
  (* 补全 *)
Admitted.

练习二（中级）

用 { } 花括号风格（而非 bullet）完成以下证明，并用 Print Assumptions. 验证没有依赖额外公理：

Lemma or_comm : forall A B : Prop, A \/ B -> B \/ A.
Proof.
  (* 补全，用 { } *)
Admitted.

提示：A \/ B 的 destruct 会产生两个情形（InL/InR 对应的两个子目标），每个情形里分别用 left. 或 right. 选择 B \/ A 的哪个分量。

练习三（进阶）

用直接写项的方式（不使用 tactic）给出 or_comm 的证明：

Lemma or_comm_term : forall A B : Prop, A \/ B -> B \/ A :=
  (* 补全：fun A B H => match H with | or_introl HA => ... | or_intror HB => ... end *).

参考 Coq 标准库里 or 的定义：Inductive or (A B : Prop) : Prop := or_introl : A -> A \/ B | or_intror : B -> A \/ B。

---

本篇完整可运行代码

以下代码可保存为 goal_window.v，用 coqc goal_window.v 编译，应零 warning 通过。

(* goal_window.v — 深入 Coq 02 配套代码 *)
(* Coq 8.19+ *)

(** * 1. tactic 版本 *)
Lemma and_swap : forall A B : Prop, A /\ B -> B /\ A.
Proof.
  intros A B H.
  destruct H as [HA HB].
  split.
  - exact HB.
  - exact HA.
Qed.

(** * 2. 直接写项版本（等价） *)
Lemma and_swap_term : forall A B : Prop, A /\ B -> B /\ A :=
  fun A B H =>
    match H with
    | conj HA HB => conj HB HA
    end.

(** * 3. Print Assumptions 验证 *)
Print Assumptions and_swap.
(* 输出: Closed under the global context *)
Print Assumptions and_swap_term.
(* 输出: Closed under the global context *)

(** * 4. 花括号风格示例 *)
Lemma and_swap_braces : forall A B : Prop, A /\ B -> B /\ A.
Proof.
  intros A B H.
  destruct H as [HA HB].
  split.
  { exact HB. }
  { exact HA. }
Qed.

(** * 5. 练习参考答案 *)

(** 练习一答案 *)
Lemma and_assoc_lr : forall A B C : Prop,
  (A /\ B) /\ C -> A /\ (B /\ C).
Proof.
  intros A B C H.
  destruct H as [[HA HB] HC].
  split.
  - exact HA.
  - split.
    + exact HB.
    + exact HC.
Qed.

(** 练习二答案 *)
Lemma or_comm : forall A B : Prop, A \/ B -> B \/ A.
Proof.
  intros A B H.
  destruct H as [HA | HB].
  { right. exact HA. }
  { left. exact HB. }
Qed.

Print Assumptions or_comm.
(* 输出: Closed under the global context *)

(** 练习三答案 *)
Lemma or_comm_term : forall A B : Prop, A \/ B -> B \/ A :=
  fun A B H =>
    match H with
    | or_introl HA => or_intror HA
    | or_intror HB => or_introl HB
    end.

参考资料

• Pierce et al., Software Foundations, Volume 1 “Logical Foundations”：https://softwarefoundations.cis.upenn.edu/lf-current/index.html
• Coq Reference Manual 8.19, “Tactics” 章节：https://coq.inria.fr/doc/V8.19.1/refman/proof-engine/tactics.html
• Coq Reference Manual 8.19, “Show Proof” 命令：https://coq.inria.fr/doc/V8.19.1/refman/proof-engine/proof-handling.html
• 前置系列「命题即类型：Curry-Howard 同构」：/2026/05/26/命题即类型-Curry-Howard-同构/
• 前置系列「类型检查器的可信基底」：/2026/05/26/类型检查器的可信基底-编译通过到底信什么/