Coq 的自动化 tactic 不是万能的黑盒，而是针对特定目标形状设计的搜索算法。auto 和 eauto 在 hint 数据库上做反向链推导；lia 在线性整数/自然数算术上调用决策程序；ring 和 field 把多项式等式规约到规范形式再比较。了解每个 tactic 的适用边界，才能在恰当的地方放手让机器搜，而不是在它注定失败的地方反复重试。前置阅读：《深入 Coq 02：目标窗口与 tactic 交互模型》和《深入 Coq 03：Gallina 核心语法速查》。

auto 与 hint 数据库

auto 的核心机制是反向链推导（backward chaining）：从当前 goal 出发，匹配 hint 数据库中的引理头部，将 goal 替换为引理的前提，递归直到所有 subgoal 都被 assumption 或 reflexivity 关闭，或达到搜索深度上限（默认 5）。

1
2
3
4
Goal forall (P Q R : Prop), P -> (P -> Q) -> (Q -> R) -> R.
Proof.
  auto.
Qed.

目标窗口在 auto 前：

1
2
3
4
5
6
P Q R : Prop
H : P
H0 : P -> Q
H1 : Q -> R
------
R

auto 成功，因为本地假设就是 hint（局部 intro 后的假设自动进入搜索空间）。

Hint 数据库机制

Coq 维护若干命名数据库，auto 默认使用 core 库。向数据库添加条目的命令：

1
2
3
4
5
6
7
8
9
10
11
12
(* 把引理加入 core 库 *)
Hint Resolve le_refl : core.

(* 把构造子加入指定库（推荐：避免污染 core） *)
Hint Constructors le : mydb.

(* 展开定义后再尝试匹配 *)
Hint Unfold lt : mydb.

(* 创建一个新的命名库 *)
Create HintDb arith_extra.
Hint Resolve Nat.add_comm : arith_extra.

调用时指定数据库：

1
2
auto with arith_extra.
auto with arith_extra core.

Hint Resolve 把引理的结论与 goal 匹配；Hint Constructors T 等价于对 T 的每个构造子都做 Hint Resolve；Hint Unfold f 在尝试匹配前先展开 f。

深度参数

默认深度 5 常常不够。两种调整方式：

1
2
auto 10.          (* 本次搜索深度 10 *)
Set Hint Depth 8. (* 全局修改默认深度；8.19+ 支持 *)

深度越大，搜索时间指数增长。超过 20 时应改用 eauto 的 iterative deepening 或手动引导。

失败情形

auto 不处理等式变换、算术、量词实例化。以下 goal 对 auto 是死局：

1
2
3
4
5
6
7
Goal forall n : nat, n + 0 = n.
Proof.
  intro n.
  (* auto 失败：需要 Nat.add_0_r，但它不在 core 库 *)
  Fail auto.
  auto with arith.  (* arith 库包含 Nat.add_0_r，成功 *)
Qed.

eauto 与存在变量

eauto 是 auto 的扩展版本，允许在搜索过程中创建存在元变量（evar），在后续 subgoal 中延迟实例化。这使它能处理 auto 无法处理的存在量词和参数尚未确定的目标。

1
2
3
4
Goal exists n : nat, n + 1 = 2.
Proof.
  eauto.   (* 创建 evar ?n，推断 ?n = 1，关闭目标 *)
Qed.

auto 在同一目标上失败，因为它不会引入 evar。

更实际的例子：利用传递性引理构造链式证明：

1
2
3
4
5
6
7
8
Require Import Coq.Arith.Arith.

Lemma le_chain : forall a b c d : nat,
  a <= b -> b <= c -> c <= d -> a <= d.
Proof.
  intros.
  eauto using Nat.le_trans.
Qed.

Nat.le_trans 的类型是 forall n m p, n <= m -> m <= p -> n <= p，中间项 m 和 p 在链式应用时需要被推断，eauto 通过 evar 延迟绑定完成。

eauto 的代价

eauto 搜索空间比 auto 大得多，相同深度下运行时间可能差一个量级。高度依赖 evar 的搜索还会产生难以调试的失败信息。实践原则：先用 auto，失败且目标含存在量词或需要延迟实例化时再换 eauto。

omega（已废弃）与 lia

omega 的历史地位

omega 曾是 Coq 的标准线性整数算术决策程序，处理含加法、减法、常量乘法的整数/自然数等式和不等式。在 Coq 8.14 中被标记为废弃，8.19 中仍可用但会产生警告：

1
Warning: omega is deprecated since 8.14. Please use lia instead.

遗留代码库和教材中仍大量出现 omega。遇到时直接替换为 lia，行为基本兼容。

lia 的能力范围

lia（Linear Integer Arithmetic）是 omega 的替代品，底层实现了 Simplex 的整数扩展。能处理：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
Require Import Lia.

Goal forall n m : nat, n + m = m + n.
Proof. intros. lia. Qed.

Goal forall n : nat, 0 < n -> n - 1 + 1 = n.
Proof. intros. lia. Qed.

Goal forall n : nat, 2 * n + 1 <> 2 * n.
Proof. intros. lia. Qed.

(* Z 类型上的整数运算 *)
Require Import ZArith.
Open Scope Z_scope.

Goal forall a b : Z, (a + b) * (a - b) = a^2 - b^2.
Proof.
  intros.
  (* lia 不处理乘法，需要 ring *)
  Fail lia.
  ring.
Qed.

lia 无法处理的情形

lia 限于线性算术。乘法、除法（除以常数以外）、模运算、指数均超出范围：

1
2
3
4
5
6
Goal forall n : nat, n * n >= n.
Proof.
  intro n.
  Fail lia.  (* n * n 是非线性 *)
  induction n; simpl; lia.  (* 手动归纳，归纳步骤是线性的 *)
Qed.

这里的修复路径：lia 在归纳步 n * n >= n -> (S n) * (S n) >= S n 上成功，因为展开后得到 n*n + 2*n + 1 >= n + 1，n*n 此时作为已知假设可当作一个整体处理。

omega 能做而 lia 不能的情形

lia 在绝大多数场景优于 omega。唯一已知的退步是极少数涉及自然数减法下界推理的特殊模式，但在 Coq 8.16+ 中已修复。实际使用中两者对同一 goal 的行为一致。

ring 与多项式等式

ring 证明交换环（commutative ring）上的多项式等式，包括 nat、Z、Q、R 以及用户定义的环结构。它把两边都规约到同一规范形式（按字典序排列的单项式之和），再做语法比较。

1
2
3
4
5
6
7
8
9
10
Require Import Ring.
Require Import ZArith.
Open Scope Z_scope.

Goal forall x y : Z, (x + y)^2 = x^2 + 2*x*y + y^2.
Proof. intros. ring. Qed.

Goal forall a b c : Z,
  (a - b) * (a + b) + b^2 = a^2 - b^2 + b^2.
Proof. intros. ring. Qed.

ring 的成功前提是目标是纯等式且两边都是多项式表达式，不包含假设中的等式。带条件的等式需要先用 rewrite 替换，再交给 ring：

1
2
3
4
5
6
Goal forall x y z : Z, x = y + 1 -> x * z = (y + 1) * z.
Proof.
  intros x y z H.
  rewrite H.
  ring.
Qed.

ring_simplify 与 ring_iff

ring_simplify 化简目标中的多项式子表达式，而不要求两边完全相等。ring 也可通过 ring_iff 用于等价命题（<->），但语法稍有不同，通常不如直接 split; intro; ring 简洁。

field 与有理表达式

field 是 ring 在域（field）上的扩展，处理带除法的等式。它在内部调用 ring，并附加非零条件的侧目标。

1
2
3
4
5
6
7
8
9
10
11
12
Require Import Field.
Require Import Reals.
Open Scope R_scope.

Goal forall x y : R, x <> 0 -> y <> 0 ->
  x / y + y / x = (x^2 + y^2) / (x * y).
Proof.
  intros x y Hx Hy.
  field.
  (* field 生成非零侧目标 *)
  split; [exact Hy | exact Hx].
Qed.

field 完成后往往留下若干 <> 0 形式的 subgoal，需要手动提供非零证明。这是它与 ring 最显著的差异——ring 对无除法的表达式无副作用，field 必须处理除数。

失败案例与修复对照：

1
2
3
4
5
6
7
8
9
(* 失败：分母中含假设，field 生成的侧目标用 auto 关不上 *)
Goal forall a b : R, b <> 0 -> a / b * b = a.
Proof.
  intros a b Hb.
  (* 尝试 field 后手动关闭侧目标 *)
  field.
  (* 剩余 goal: b <> 0 *)
  exact Hb.
Qed.

自定义 hint 数据库：完整示例

下面构造一个小型例子，展示从定义到证明的完整流程，包含自定义 hint 数据库、auto 的成功与失败、以及 Show Proof. 的输出。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
Require Import Coq.Lists.List.
Import ListNotations.

(* 定义一个谓词：列表中所有元素都满足 P *)
Inductive All {A : Type} (P : A -> Prop) : list A -> Prop :=
  | All_nil  : All P []
  | All_cons : forall x xs, P x -> All P xs -> All P (x :: xs).

(* 建立专属 hint 库 *)
Create HintDb all_db.
Hint Constructors All : all_db.

Lemma all_map :
  forall {A B : Type} (P : B -> Prop) (f : A -> B) (xs : list A),
  All (fun x => P (f x)) xs ->
  All P (map f xs).
Proof.
  intros A B P f xs H.
  induction H.
  - (* base case: All P (map f []) *)
    simpl.
    auto with all_db.
  - (* inductive case *)
    simpl.
    auto with all_db.
Qed.

(* 查看 Coq 生成了什么证明项 *)
Show Proof.

Show Proof. 在证明完成后输出：

1
2
3
4
5
6
7
(fun (A B : Type) (P : B -> Prop) (f : A -> B) (xs : list A)
     (H : All (fun x : A => P (f x)) xs) =>
 All_ind (fun (l : list A) _ => All P (map f l))
   (All_nil P)
   (fun (x : A) (xs0 : list A) _ (IH : All P (map f xs0)) Hx =>
     All_cons P (f x) (map f xs0) Hx IH)
   xs H)

这证明了 auto with all_db 在归纳步骤中确实在使用 All_cons，而不是不透明的 magic。

失败示例与修复路径

尝试一：直接用 auto 证明排列引理

1
2
3
4
5
6
Require Import Coq.Sorting.Permutation.

Lemma perm_example : Permutation [1; 2; 3] [3; 1; 2].
Proof.
  Fail auto.           (* auto 对 Permutation 构造子不熟悉 *)
  Fail auto with *.    (* 用所有库也不够，需要多步构造 *)

auto with * 失败是因为 Permutation 的证明需要多个构造子连续组合，单步匹配无法收敛。

修复：手动展开后交给 auto

1
2
3
4
5
6
  apply perm_trans with (l' := [1; 3; 2]).
  - apply perm_swap.
  - apply perm_trans with (l' := [3; 1; 2]).
    + apply perm_swap.
    + apply perm_refl.  (* 或 auto *)
Qed.

对于 Permutation 这类组合深度大的谓词，手动指定中间步骤、最后几步交给 auto 是比依赖全自动搜索更稳健的做法。

证明完成后 Print Assumptions 列出证明树中用到的所有公理，用于确认没有引入意外的经典逻辑或排中律：

1
2
3
4
Lemma nat_add_comm : forall n m : nat, n + m = m + n.
Proof. intros. lia. Qed.

Print Assumptions nat_add_comm.

输出：

1
2
Axioms:
<none>

这表明 lia 的证明完全在 CIC（构造性演算）框架内，无需额外公理。若某个证明引入了 Classical.classic 或 FunctionalExtensionality.functional_extensionality，Print Assumptions 会如实列出，方便判断是否符合当前项目对构造性的要求。

各 tactic 选用判断

目标形状 优先尝试 备注
命题逻辑，局部假设充足 auto 不够就加深度或 tauto
存在量词，需延迟实例化 eauto 深度大时运行慢
线性整数/自然数算术 lia 非线性先归纳再 lia
交换环多项式等式 ring 含 rewrite 时先替换再 ring
域（含除法）等式 field 注意非零侧目标
无规律的命题 手动 + 局部 auto 自动化做收尾，不做主干

练习

练习 1：证明下列引理，要求在最终步骤使用 lia，不使用 omega：

1
Lemma div2_spec : forall n : nat, n / 2 * 2 <= n < n / 2 * 2 + 2.

提示：Nat.div_mod 说明 n = n / 2 * 2 + n mod 2，Nat.mod_upper_bound 给出 n mod 2 < 2。先用 rewrite (Nat.div_mod n 2) 展开，再用 lia（结合 Nat.mod_upper_bound n 2 的结论）关闭。

练习 2：创建一个 hint 库 even_db，加入以下两条引理，再用 auto with even_db 证明 Even 4：

1
2
3
Inductive Even : nat -> Prop :=
  | Even_O  : Even 0
  | Even_SS : forall n, Even n -> Even (S (S n)).

练习 3：用 ring 证明：

1
2
Require Import ZArith. Open Scope Z_scope.
Goal forall a b : Z, (a + b)^3 = a^3 + 3*a^2*b + 3*a*b^2 + b^3.

如果 ring 直接失败（某些版本对 ^3 展开策略不同），尝试先 ring_simplify，再 ring，或手动展开 ^3 后再调用。

参考资料