深入 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 打印出更新后的状态。

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

一个典型的中间状态（已经把 forall 和前提引入上下文之后）：

1 goal
  
  A, B : Prop
  H : A /\ B
  ============================
  B /\ A

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

回退在 coqtop 里要显式敲 Undo、Undo n、Restart 或 Abort；CoqIDE 和 vscoq2 把这条状态历史链做成了光标级的双向步进，移动光标就等于前进或撤回。能力是一样的，差别只在要不要手打命令——命令行里卡住时记得有 Undo 可用。

逐步演示：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
  
  ============================
  forall A B : Prop, A /\ B -> B /\ A

执行 intros A B H.

intros A B H.

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

1 goal
  
  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
  
  A, B : Prop
  HA : A
  HB : B
  ============================
  B /\ A

执行 split.

split.

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

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

goal 2 is:
 A

这里有个容易误判的细节：只有第一个目标会显示局部上下文，第二个及之后只打印 goal N is: 加一行结论。上下文没消失，只是没重复打印。想看第二个目标的完整上下文，得先用 bullet 或 2: { ... } 把焦点切过去。

用 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 ?Goal ?Goal0
   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/Theorem 不接受 :=，只能走 Proof. … Qed.）：

Definition 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 报错：

In environment
A, B : Prop
H : A /\ B
Unable to unify "A /\ B" with "B".

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

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

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

如果还未执行 destruct，上下文里没有 HA、HB，Coq 报：

Error: The reference HA was not found in the current environment.

（Unbound value HA 是 OCaml 的措辞，不是 Coq 的。）tactic 错误的诊断方式是观察当前上下文——只有上下文里存在的名字才能使用。

多目标导航：{ } 与 bullet

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

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

split.
- exact HB.
- exact HA.

-、+、* 没有固定的层级绑定，Coq 只要求同一层用同一个符号；嵌套时换一个符号即可，也可以用 --、*** 这类重复形式扩展出更多层：

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 里直接量化这种影响的工具。

这里要连带交代两件容易踩的事。第一，Admitted 会静默生成一条公理，而且沿引用链传染：任何用到该引理的下游定理，Print Assumptions 都会把它列进 Axioms:。下面练习里的 Admitted. 只是占位，真做的时候别把它留在成品里。第二，Qed 产生的是 opaque 常量，Defined 产生的是 transparent 常量——只有后者能被 simpl、unfold 这类规约 tactic 展开。写计算用的定义时选错关键字，后面会撞上「明明定义在那里却展不开」的问题，这一类症状在第 13 篇有专门的诊断。

tactic 与状态变换速查

下面这张表只给状态变换的轮廓，每条 tactic 的完整语义（intro pattern、apply ... in、rewrite 方向、destruct 的信息丢失）在第 04 篇逐条展开。

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 w	为 exists x, P x 提供见证 w	目标变为 P w（split 在这里不适用，因为 constructor 1 猜不出见证）
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 会产生两个情形（or_introl / or_intror 对应的两个子目标），每个情形里分别用 left. 或 right. 选择 B \/ A 的哪个分量。

练习三（进阶）

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

Definition 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.20 *)

(** * 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. 直接写项版本（等价） *)
Definition 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 *)

(** 练习三答案 *)
Definition 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 8.20.0 Reference Manual，“Tactics” 章节：https://rocq-prover.org/doc/V8.20.0/refman/proof-engine/tactics.html
• Coq 8.20.0 Reference Manual，“Show Proof” 命令：https://rocq-prover.org/doc/V8.20.0/refman/proof-engine/proof-handling.html
• 前置系列「命题即类型：Curry-Howard 同构」：/2026/05/26/命题即类型-Curry-Howard-同构/
• 前置系列「类型检查器的可信基底」：/2026/05/26/类型检查器的可信基底-编译通过到底信什么/