证明中断不是随机的。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 的记号、隐式参数和强制转换会把真实项目遮住，打开这个选项后目标才算"裸眼可读"。

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

错误现场

1
2
3
4
5
Error: ?n has type nat while it is expected to have type nat.
(* 或者目标显示为 *)
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(0) : Type(1) : Type(2) : ...，Set 是 Type(0) 的别名（在某些模式下）。宇宙不一致的核心原因是试图把某个 Type(i) 的值放进需要 Type(j) 的位置，而 i ≥ j，违反了层级约束。

常见触发场景：

1
2
3
(* 错误示例：试图定义一个以 Type 为元素的类型，放入同一层级 *)
Fail Definition bad : Type := Type.
(* Error: Universe inconsistency *)

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

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 出现在等号右边的类型中，而不是参数类型中。

模式三：无法合一（Cannot 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".

根因分析

Cannot 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 或 convert_concl_no_check 把目标改写成等价但更便于 tactic 匹配的形式。
1
2
3
4
5
6
(* change 显式替换等价目标 *)
Lemma example : 1 + 1 = 2.
Proof.
  change (S (S 0) = S (S 0)).  (* 展开定义后的等价形式 *)
  reflexivity.
Qed.

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

错误现场

证明没有报错，但 induction 完成后归纳假设里缺少必要的泛化，导致后续 tactic 无法完成：

1
2
3
IH : P n   (* 假设 *)
goal : P (S n)   (* 目标中有不在 IH 里的自由变量 *)
Error: Unable to apply the induction hypothesis.

根因分析

对变量 n 做 induction n 之前，如果上下文中已经有其他变量 m 绑定在 n 上，归纳假设就不够强。经典场景：

1
2
3
4
5
6
Lemma plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n.
  (* 归纳假设是 IHn : n + m = m + n，但 m 已经被 intro 固定了 *)
  (* 在递归步里，无法对不同的 m 使用 IHn *)

正确做法是在 induction 之前，把需要泛化的变量用 revert 放回目标，或者用 generalize dependent 直接泛化：

1
2
3
4
5
6
7
Lemma plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n.
  induction n.
  - intros m. simpl. rewrite Nat.add_0_r. reflexivity.
  - intros m. simpl. rewrite IHn. rewrite Nat.add_succ_r. reflexivity.
Qed.

或者使用 generalize dependent m 在 induction 之前把 m 泛化回目标：

1
2
3
4
5
6
7
8
Lemma plus_comm' : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  generalize dependent n.
  induction m.
  - intros n. rewrite Nat.add_0_r. reflexivity.
  - intros n. simpl. rewrite <- IHm. rewrite Nat.add_succ_r. reflexivity.
Qed.

泛化的判断准则

一个实用的规则是：对 n 做 induction 之前，检查目标和上下文中是否有其他量词变量依赖 n，或者在递归步里需要对这些变量取不同值。如果有，就用 revert 或 generalize dependent 先把它们放回目标。

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

错误现场

1
2
Error: Cannot unfold <ident> since it is opaque.
(* 或者 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
About Nat.add.
(* 输出包含: Opaque definition. 或 Transparent definition. *)

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

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

错误现场

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

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

根因分析

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

功能 需要导入
lia（线性算术） Require Import Lia.
omega（旧版线性算术） Require Import Omega.（8.14 后已弃用，改用 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：下面的证明会因为泛化不足而失败，修改它使其通过：

1
2
3
4
5
6
7
Lemma rev_length : forall A (l : list A), length (rev l) = length l.
Proof.
  Require Import List.
  intros A l.
  induction l.
  (* 此处 IHl 是否足够强？ *)
  Admitted.

提示：检查 induction l 之前是否需要 revert 某个变量。如果不需要，找到 rev_length 在标准库中对应的完整证明，对比归纳假设的形式。

练习 2：下面的代码触发宇宙不一致，找出原因并修复：

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

提示：用 Set Printing Universes 观察层级标注，再考虑 Universe Polymorphism 是否适用。

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

1
2
3
4
5
6
7
Lemma double_def (n : nat) : n + n = 2 * n.
Proof. ring. Defined.

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

(* 尝试在后续引理中 unfold double_def 和 double_qed，观察差异 *)