证明中断不是随机的。Coq 报错信息有规律，每种卡住模式都有对应的诊断手段和修复路径。本文整理六类高频卡住模式，逐一给出错误现场、根因和处理方法，附诊断工具用法。

诊断工具速览

下列诊断命令不参与证明，只用于观察状态，本文各节均会用到。

1
2
3
4
5
6
7
Set Printing All.        (* 显示所有隐式参数、强制转换、记号展开 *)
Set Printing Universes.  (* 在类型中显示宇宙层级标注 *)
Check @term.             (* 显示 term 的完整类型，含所有显式参数 *)
About ident.             (* 显示 ident 的来源、类型、透明度等元信息 *)
Print ident.             (* 显示 ident 的定义或公理 *)
Show Proof.              (* 在证明过程中打印当前 proof term 的骨架 *)
Print Assumptions thm.   (* 列出 thm 依赖的全部公理和假设 *)

Set Printing All 是最常用的第一步：Coq 的记号、隐式参数和强制转换会把真实项目遮住，打开这个选项后目标才算"裸眼可读"。

模式一：目标中出现未预期的存在变量

错误现场

evar 留在目标里时，报错分三个时机，文本各不相同：

1
2
3
4
5
6
7
8
(* 时机一：refine / _ 留下的洞无法从上下文推断 *)
Error: Cannot infer this placeholder of type nat.

(* 时机二：apply ex_intro 之后见证始终没被定下来 *)
Error: Unable to find an instance for the variable n.

(* 时机三：前面都没报，一路拖到 Qed 才炸 *)
Error: Attempt to save an incomplete proof (unresolved existential variables).

或者根本不报错，目标里就明摆着一个洞：

1
2
3
4
1 goal
  
  ============================
  ?Goal

存在变量（existential variable，evar）在目标或上下文中以 ?x、?Goal 的形式出现。某些情况下 Coq 不报错，而是让 evar 留在目标里，直到某个 tactic 试图匹配它才失败。

根因分析

evar 的主要来源有三个。

第一，eapply 留下了未解决的参数。eapply f 会为 f 的每个无法立即推断的参数生成 evar，这些 evar 必须在后续 tactic 中被实例化。

1
2
3
4
5
Example evar_demo : exists n : nat, n = 0.
Proof.
  eapply ex_intro.  (* 此时目标变为 ?n = 0，?n 是 evar *)
  reflexivity.      (* reflexivity 把 ?n 实例化为 0 *)
Qed.

第二，refine 留下了占位符。refine 允许在项中留 _，每个 _ 产生一个 evar 子目标。

第三，某些 tactic 组合在非预期的顺序下，产生了循环依赖的 evar，Coq 无法自动解开。

修复方法

用 instantiate 显式给出 evar 的值：

1
2
3
4
5
Proof.
  eapply ex_intro.
  instantiate (1 := 0).  (* 将第一个 evar 实例化为 0 *)
  reflexivity.
Qed.

或者改用 apply 加完整参数，完全避免 evar：

1
2
3
4
Proof.
  apply (ex_intro _ 0).
  reflexivity.
Qed.

诊断步骤：出现奇怪 evar 时，先执行 Show Proof. 查看当前 proof term，evar 在输出中以 ?evar_N 标注，结合上下文可以判断哪一步引入了它。

1
2
3
4
5
6
Lemma check_evar : 1 + 1 = 2.
Proof.
  Show Proof.  (* 当前是 ?Goal，proof term 还是空的 *)
  reflexivity.
  Show Proof.  (* 变成 @eq_refl nat 2 *)
Qed.

模式二：宇宙不一致错误

错误现场

1
2
Error: The term "T" has type "Type@{i}" while it is expected to have type
"Type@{j}" (Universe inconsistency: Cannot enforce j < i because i < j).

或者更简短的版本：

1
Error: Universe inconsistency.

根因分析

Coq 的类型层级是 Prop : Type(1)、Set : Type(1)、Type(i) : Type(i+1)，层级从 i ≥ 1 起——没有 Type(0)，Set 也不是 Type(0) 的别名，它是与 Prop 并列的 base sort。宇宙不一致的核心原因是试图把某个 Type(i) 的值放进需要 Type(j) 的位置，而约束解不出来。

这里有个反直觉的地方要先排掉：

1
2
(* 这个是合法的，Fail 会报 The command has not failed! *)
Definition ok : Type := Type.

原因是每次写 Type 都会分配一个新的宇宙变量，上面这行的约束是 i < j，可解。从用户视角看 Coq 里就是 Type : Type。真正炸掉需要让常量把宇宙固定住：

1
2
3
4
Definition U := Type.
Fail Definition inconsistent : U := U.
(* U := Type@{u} : Type@{u+1}，这行要求 Type@{u+1} <= Type@{u}，
   即 u+1 <= u，无解 *)

另一个典型场景是多态函数被实例化到过高的层级：

1
2
Definition identity (A : Type) (x : A) := x.
(* identity 本身是宇宙多态的，但某些用法会强制层级关系 *)

修复方法

打开宇宙层级显示，先观察：

1
2
3
Set Printing Universes.
Check @identity.
(* 输出: forall (A : Type@{u}), A -> A *)

如果需要量化所有宇宙层级，使用 Universe Polymorphism：

1
2
Set Universe Polymorphism.
Definition poly_id (A : Type) (x : A) : A := x.

如果错误来自 Prop 和 Type 的混用，检查是否把 Prop 中的命题当作计算层的数据使用。Prop 的居民不能流入 Set/Type 的非 Prop 数据类型：

1
2
3
4
(* Prop 到 Type 的提取是受限的 *)
Definition extract_from_prop (P : Prop) (proof : P) : bool := 
  (* 这里不能直接用 proof 构造 bool 值 *)
  true.  (* 这样写绕过了，但失去了 proof 的内容 *)

实践中，宇宙不一致错误多出现在尝试定义涉及"类型的类型"的结构时。检查点是：Type 出现在等号右边的类型中，而不是参数类型中。

模式三：无法合一（Unable to unify）

错误现场

1
2
3
4
Error: Unable to unify "f a b" with "f b a".
(* 或 *)
Error: In environment ...
The term "X" has type "A" while it is expected to have type "B".

根因分析

Unable to unify X with Y 背后通常有三种原因。

第一类是参数顺序错误，也是最常见的。某个函数的参数顺序与直觉不符：

1
2
3
4
5
6
7
8
9
(* Nat.add 的参数顺序 *)
Check Nat.add.  (* : nat -> nat -> nat *)

Lemma order_mistake : Nat.add 1 2 = Nat.add 2 1.
Proof.
  (* reflexivity 会失败，因为 1+2 ≠ 2+1 在定义层是不同的 *)
  (* 需要 Nat.add_comm *)
  apply Nat.add_comm.
Qed.

第二类是隐式参数不匹配。打开 Set Printing All 后才能看到真实的参数列表：

1
2
3
4
Set Printing All.
Check @eq_refl.
(* @eq_refl : forall (A : Type) (x : A), @eq A x x *)
(* 而不是简写的 eq_refl : ?x = ?x *)

隐式参数被自动推断时，如果上下文不够，推断结果可能与期望不符。用 @ 前缀可以显式指定所有参数：

1
2
3
4
(* 当 apply eq_refl 失败时，改用 *)
apply @eq_refl.
(* 或者 *)
exact (@eq_refl nat 0).

第三类是强制转换（coercion）隐藏了类型差异。Coq 会自动应用已注册的强制转换，这可能让目标看起来满足，实际上类型路径不同：

1
2
3
(* 检查是否有强制转换在起作用 *)
Set Printing Coercions.
(* 现在目标里会显示所有强制转换路径 *)

修复方法

诊断的标准流程是：

  1. Set Printing All 展开所有记号和隐式参数；
  2. Check @f 查看函数的完整签名；
  3. 对比目标中的实际类型和 tactic 提供的类型，找到不匹配点；
  4. 用 change 或 change_no_check 把目标改写成等价但更便于 tactic 匹配的形式（convert_concl_no_check 在 8.14 已被删除，替代品就是 change_no_check）。
1
2
3
4
5
6
(* change 显式替换等价目标 *)
Lemma example : 1 + 1 = 2.
Proof.
  change (S (S 0) = S (S 0)).  (* 展开定义后的等价形式 *)
  reflexivity.
Qed.

模式四：对错误变量做 induction 导致泛化不足

错误现场

这一类的特征是 induction 本身不报错，卡在后面用归纳假设的那一步。Coq 没有「归纳假设用不上」这种专门的报错，实际看到的是普通的合一失败——apply IH 报

1
Error: Unable to unify "..." with "...".

rewrite IH 则报

1
Error: Found no subterm matching "..." in the current goal.

真正的诊断信号不在报错文本里，而在归纳步的目标形态：归纳假设被某个已经 intro 进上下文的变量钉死在一个具体值上，而当前目标需要它取另一个值。

根因分析

判据不是「上下文里有没有别的变量」——forall n m, n + m = m + n 就是个反例，intros n m. induction n. 完全能证完（第 14 篇里正是这么写的），因为归纳步里 m 始终取同一个值，钉死它不影响推进。

真正会卡住的是归纳步需要对那个变量取别的值的情形。经典例子是单射性：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Require Import PeanoNat.

Fixpoint double (n : nat) : nat :=
  match n with
  | O   => O
  | S k => S (S (double k))
  end.

(* 卡住的写法 *)
Lemma double_injective_stuck : forall n m, double n = double m -> n = m.
Proof.
  intros n m. induction n as [|n' IH].
  (* 归纳步目标：double (S n') = double m -> S n' = m
     要用 IH 就得让它作用在 m 的前驱上，但 m 已经被 intro 钉死 *)
Abort.

m 在归纳步里必须变成 m'（它的前驱），而 intros n m 已经把它固定了。修法是让 m 留在目标里，在每个分支各自 intro：

1
2
3
4
5
6
Lemma double_injective : forall n m, double n = double m -> n = m.
Proof.
  intros n. induction n as [|n' IH]; intros [|m'] H; simpl in H; try discriminate.
  - reflexivity.
  - f_equal. apply IH. injection H. auto.
Qed.

generalize dependent 是同一件事的另一种写法：变量已经 intro 进来了，用它推回目标再做归纳。

泛化的判断准则

问一句话就够：**归纳步里，这个变量需不需要取跟当前不同的值？**需要就把它留在目标里（或用 revert / generalize dependent 推回去），不需要就随便 intro。像 n + m = m + n 这种 m 全程不动的，泛化与否都能过；像 double_injective 这种要对 m 的前驱递归的，不泛化必卡。

模式五：不透明定义阻塞化简

错误现场

1
2
Error: Cannot coerce add_zero_qed to an evaluable reference.
(* 或者 simpl 执行后目标没有变化，不报错但也不化简 *)

根因分析

Coq 中定义的透明度分三档：

  • Definition（透明）：simpl 和 unfold 都可以展开；
  • Opaque：只能用于类型检查，不能被 simpl/unfold 展开；
  • Qed 结尾的引理：对外部是不透明的，simpl 无法展开其定义体。

后一点是高频陷阱：用 Qed 封闭的证明，其 proof term 对后续证明不透明，只有类型（命题）可见。用 Defined 结尾的证明则是透明的，proof term 可被计算：

1
2
3
4
5
6
7
8
9
(* 用 Qed 封闭：后续无法展开 body *)
Lemma add_zero_qed : forall n, n + 0 = n.
Proof. intros n. induction n; simpl; [reflexivity | f_equal; exact IHn]. Qed.

(* 用 Defined 封闭：后续可以 unfold *)
Lemma add_zero_def : forall n, n + 0 = n.
Proof. intros n. induction n; simpl; [reflexivity | f_equal; exact IHn]. Defined.

Definition test_unfold : 3 + 0 = 3 := add_zero_def 3.

修复方法

如果定义被标记为 Opaque 但需要展开，用 Transparent 临时解除：

1
2
3
4
5
6
7
8
9
10
Opaque Nat.add.

Lemma opaque_example : 1 + 1 = 2.
Proof.
  Transparent Nat.add.  (* 临时开放 *)
  simpl.
  reflexivity.
Qed.

(* 之后可以再 Opaque Nat.add. 恢复 *)

如果问题是 Qed 封闭的引理无法展开，有两条路：

  1. 把引理改为 Defined 结尾（需要该引理的 proof term 有计算意义）；
  2. 不展开定义体，而是直接用引理本身做重写：rewrite add_zero_qed。

About ident 会显示透明度信息：

1
2
3
4
5
About Nat.add.
(* 输出包含: Nat.add is transparent
   若先执行 Opaque Nat.add. 则变成:
   Nat.add is basically transparent but considered opaque for reduction
   —— 这个措辞正好区分「Qed 产生的真 opaque」和「被 oracle 标成 opaque 的 transparent 定义」 *)

Print ident 则显示定义体本身，用于确认定义是否是预期的内容。

模式六：缺少 Require Import 导致 tactic 静默失败

错误现场

这一类没有明显错误信息，症状是 tactic 不报错但也不工作，或报出莫名其妙的找不到名字：

1
2
3
4
Error: The reference omega was not found in the current environment.
(* 或者 *)
Error: The reference lia was not found in the current environment.
(* 或者 tactic 执行了但没有解决任何目标 *)

根因分析

Coq 的标准库分模块，许多 tactic 和引理需要显式导入对应的库才可用。常见的遗漏：

功能 需要导入
lia（线性算术） Require Import Lia.
omega（旧版线性算术） 无——8.12 废弃、8.14 已从标准库删除，8.20 里只有 lia
ring、field Require Import Ring. 或 Require Import Field.
auto 的扩展引理 视需要导入对应库
List 相关引理 Require Import List. Import ListNotations.
Nat 模块 Require Import Arith. 或 Require Import PeanoNat.

另一类静默失败来自 Hint 数据库没有导入。auto 和 eauto 依赖 Hint 数据库，如果相关引理的 Hint 注册在未导入的模块里，auto 会默默失败。

修复方法

诊断顺序：

  1. 确认 tactic 名称拼写正确；
  2. 用 Locate tactic_name. 查找该 tactic 来自哪个模块；
  3. 在文件顶部加入对应的 Require Import；
  4. 对于 auto 失败，用 info_auto 或 debug auto 打印搜索轨迹，确认 Hint 数据库内容。
1
2
3
4
5
6
7
(* 查找 lia 的来源 *)
Locate "lia".
(* 如果找不到，说明没有 Require Import Lia *)

Require Import Lia.
Lemma lia_example : forall n : nat, n + 0 = n.
Proof. intros n. lia. Qed.

对 Hint 数据库，Print HintDb core. 可以列出 core 数据库中的所有引理，用于排查 auto 为何找不到某个引理：

1
2
Print HintDb core.
(* 列出 auto 使用的核心引理集 *)

诊断工作流总结

面对卡住的证明，按以下顺序排查通常能定位根因。

第一步，Set Printing All 展开目标，排除记号和隐式参数的干扰，确认目标的真实形态。

第二步，Show Proof. 打印当前 proof term，检查是否有 evar 或意外的 admit 留在骨架里。

1
2
3
4
5
6
7
Lemma debug_example : forall n : nat, n = n.
Proof.
  intros n.
  Show Proof.      (* 显示 fun n : nat => ?Goal *)
  reflexivity.
  Show Proof.      (* 显示 fun n : nat => @eq_refl nat n *)
Qed.

第三步，对类型错误，Check @term 显示完整类型签名，About ident 显示透明度和来源模块。

第四步，对宇宙错误，加 Set Printing Universes 后重新触发错误，读取层级约束冲突点。

第五步，证明完成后，Print Assumptions 检查是否意外依赖了公理或 admit：

1
2
Print Assumptions lia_example.
(* 如果只输出 Closed under the global context 说明无 admit（无句号） *)

练习

练习 1：下面这个证明会因为泛化不足而卡住，修改它使其通过。注意 rev_append 的第二个参数在归纳步里必须取别的值：

1
2
3
4
5
6
7
8
9
10
Require Import List.
Import ListNotations.

Lemma rev_append_spec : forall A (l acc : list A),
  rev_append l acc = rev l ++ acc.
Proof.
  intros A l acc.
  induction l.
  (* 此处 IHl 里的 acc 已被钉死，够不够用？ *)
Abort.

提示：先判断归纳步需不需要让 acc 取不同的值，再决定 revert acc 还是原样 intro。顺带一提，8.20 里 rev 的长度引理叫 length_rev，旧名 rev_length 只剩一个 only parsing 的兼容记号。

练习 2：下面这行不会触发宇宙不一致，Fail 会报 The command has not failed!。先解释为什么它是合法的，再改造出一个真会炸的版本：

1
2
Fail Definition universe_ok : Type :=
  forall (T : Type), T -> T.

提示：每次写 Type 都会分配新的宇宙变量，所以内层 Type@{i} 和整体 Type@{i+1} 的约束是可解的。想让约束无解，得先用 Definition U := Type. 把宇宙固定在常量上。用 Set Printing Universes 观察标注。

练习 3：定义一个以 Defined 结尾的函数，验证它可以被 unfold 展开，而同名的以 Qed 结尾的版本不能：

1
2
3
4
5
6
7
8
9
10
11
12
13
Require Import Arith.   (* ring 需要它 *)

Lemma double_def (n : nat) : n + n = 2 * n.
Proof. ring. Defined.

Lemma double_qed (n : nat) : n + n = 2 * n.
Proof. ring. Qed.

(* 对比 Print double_def. 与 Print double_qed. 的输出：
   前者给出完整 proof term，后者只给
   *** [ double_qed : forall n : nat, n + n = 2 * n ]
   不给 body —— 这是观察 Qed/Defined 差异最直接的方式。
   注意别指望 unfold double_def：它是命题的证明，不会出现在别的目标里。 *)

参考资料