等式推理是 Coq 证明中出现频率最高的操作之一。从 n + 0 = n 这类基础引理到复杂的代数化简，绝大多数数学和程序正确性证明都会涉及等式的替换、传递、对称和合同推导。Coq 提供了一批专门处理等式的 tactic，每一条背后都对应一种不同的推理路径。选择合适的 tactic 不仅影响证明的可读性，也直接决定自动化程度。

等式相关 tactic 各有不同的适用边界：rewrite、subst、symmetry、transitivity、congruence、f_equal、replace 覆盖了从单步替换到合同闭包自动求解的完整光谱。选错 tactic 不会让证明错误，但会让证明变长、可读性下降，或在自动化程度上留下空间。

等式在 Coq 类型论中的地位

Coq 的等式类型 @eq A a b，通常写作 a = b，是一个归纳命题，定义为：

1
2
Inductive eq (A : Type) (x : A) : A -> Prop :=
  | eq_refl : x = x.

唯一的构造子 eq_refl 表明 x = x 永远成立。证明 a = b 的本质是构造一个类型为 a = b 的项。等式的消去规则（即重写）由 eq_ind 给出：给定 a = b 和 P a 的证明，可以得到 P b 的证明。这就是 rewrite tactic 的理论基础。

与第 02 篇的证明状态机模型对应：每一条等式 tactic 都是对当前目标或上下文中某个等式项的一次消去或构造操作。

rewrite：在目标中替换等式

基本形式

rewrite H 在目标中用 H 右侧替换左侧的所有出现。假设 H : a = b，目标中每处 a 都被替换为 b。

1
2
3
4
5
6
7
8
Lemma rewrite_demo : forall (n m : nat), n = m -> n + 1 = m + 1.
Proof.
  intros n m H.
  (* 此时 H : n = m，目标：n + 1 = m + 1 *)
  rewrite H.
  (* 目标变为：m + 1 = m + 1 *)
  reflexivity.
Qed.

反向重写

rewrite <- H 用左侧替换右侧的出现。当 H : a = b 而目标中出现 b 需要变成 a 时使用。

1
2
3
4
5
6
7
Lemma rewrite_backward : forall (n m : nat), n = m -> m + 1 = n + 1.
Proof.
  intros n m H.
  rewrite <- H.
  (* 目标中 m 被替换为 n：n + 1 = n + 1 *)
  reflexivity.
Qed.

在假设中重写

rewrite H in H2 在假设 H2 中执行替换，而非在目标中。rewrite H in * 在所有假设和目标中执行替换。

1
2
3
4
5
6
7
8
9
Lemma rewrite_in_hyp : forall (n m k : nat),
    n = m -> n + k = 5 -> m + k = 5.
Proof.
  intros n m k Heq H.
  (* H : n + k = 5，Heq : n = m *)
  rewrite Heq in H.
  (* H 变为：m + k = 5 *)
  exact H.
Qed.

重写失败的情形

rewrite 依赖模式匹配，若目标的语法形式与期望不符，重写会失败。一个常见的失败案例：

1
2
3
4
5
6
7
8
9
10
(* 失败示例：rewrite 无法跨越 beta-delta 归约的边界 *)
Lemma rewrite_fail_demo : forall (f : nat -> nat) (n m : nat),
    n = m -> f n = f m.
Proof.
  intros f n m H.
  (* 错误尝试：直接 reflexivity 会失败，因为 f n 和 f m 不是定义相等 *)
  (* reflexivity. (* Error: Unable to unify *) *)
  rewrite H.
  reflexivity.
Qed.

直接用 reflexivity 试图结束这个目标会失败，因为 f n 和 f m 在 n ≠ m 的一般情形下不是定义相等。正确做法是先用 rewrite H 将 n 替换为 m，再用 reflexivity。

subst：消去被等式定义的变量

当上下文中存在形如 x = t 或 t = x 的假设，且 x 是局部变量时，subst x 将 x 的所有出现替换为 t，然后从上下文移除该变量和等式假设。subst 不带参数时对所有可消去的变量执行此操作。

1
2
3
4
5
6
7
8
9
Lemma subst_demo : forall (n m k : nat),
    n = 3 -> m = n + k -> m = 3 + k.
Proof.
  intros n m k H1 H2.
  (* H1 : n = 3，H2 : m = n + k *)
  subst n.
  (* n 被消去，H2 变为：m = 3 + k，目标变为 m = 3 + k *)
  exact H2.
Qed.

subst 的适用条件是变量必须是上下文中引入的局部变量，不能是全局定义的常量。若等式两侧都不是简单变量，subst 会报错。此时应改用 rewrite。

与第 04 篇介绍的 rewrite 相比，subst 更具破坏性——它把变量从上下文中彻底移除。在需要保留变量名以提高可读性的场合，rewrite ... in * 是更温和的替代。

symmetry 与 transitivity：目标级的等式变形

symmetry

symmetry 将目标 a = b 变换为 b = a。symmetry in H 则对假设 H : a = b 执行同样的翻转，将其变为 H : b = a。

1
2
3
4
5
6
7
8
Lemma plus_comm_sym : forall (n m : nat), n + m = m + n.
Proof.
  intros n m.
  symmetry.
  (* 目标变为：m + n = n + m *)
  (* 现在可以使用已知的 plus_comm 或再次 symmetry 来匹配 *)
  apply Nat.add_comm.
Qed.

symmetry 的典型使用场景：某条引理的结论形式是 b = a，而当前目标是 a = b，通过 symmetry 对齐方向后再 apply。

transitivity

transitivity t 将目标 a = c 拆分为两个子目标：a = t 和 t = c，其中 t 是用户提供的中间项。

1
2
3
4
5
6
7
8
Lemma transitivity_demo : forall (a b c : nat),
    a = b -> b = c -> a = c.
Proof.
  intros a b c H1 H2.
  transitivity b.
  - exact H1.
  - exact H2.
Qed.

等价地，这个例子也可以用 rewrite H1; exact H2 完成，但 transitivity 在需要明确展示推理链条时更具表达力。etransitivity 是 transitivity 的存在量词版本，无需显式提供中间项，由 Coq 推断（但并非总能成功）。

congruence：合同闭包的自动求解

congruence 是一个判定过程，基于合同闭包（congruence closure）算法。给定上下文中的一组等式假设，它能自动推导出由这些等式和函数应用合同性所能推出的所有等式结论。

能处理的情形

1
2
3
4
5
6
Lemma congruence_demo : forall (f : nat -> nat) (a b c : nat),
    a = b -> b = c -> f a = f c.
Proof.
  intros f a b c H1 H2.
  congruence.
Qed.

congruence 能处理：

  • 等式的自反、对称、传递推导
  • 函数应用的合同性（若 a = b 则 f a = f b）
  • 构造子的单射性（若 S n = S m 则 n = m）
  • 构造子的不相交性（若上下文中能推出矛盾，如 0 = S n，则目标任意）

不能处理的情形

congruence 是纯等式的合同推导，不做算术计算。以下情形会失败：

1
2
3
4
5
6
7
8
9
10
(* congruence 无法处理算术等式 *)
Lemma congruence_arithmetic_fail : forall (n : nat),
    n + 0 = n.
Proof.
  intro n.
  (* congruence. (* 失败：n + 0 不能被 congruence 化简为 n *) *)
  (* 正确做法：使用 simpl 或 ring 或直接用标准库引理 *)
  rewrite Nat.add_0_r.
  reflexivity.
Qed.

congruence 不理解算术，也不展开定义。需要算术推理时，应改用 ring（环论等式）、omega（线性算术）或 lia（线性整数/自然数算术）。

f_equal：函数应用的合同分解

f_equal 将目标 f a1 ... an = f b1 ... bn 分解为 n 个子目标 a1 = b1、…、an = bn，前提是 f 在等号两侧相同。这是合同性（congruence）在单步上的手动版本。

1
2
3
4
5
6
7
8
9
Lemma f_equal_demo : forall (n m k : nat),
    n = m -> (n, k) = (m, k).
Proof.
  intros n m k H.
  f_equal.
  (* 生成两个子目标：n = m 和 k = k *)
  - exact H.
  - reflexivity.
Qed.
1
2
3
4
5
6
7
Lemma f_equal_unary : forall (n m : nat),
    n = m -> S n = S m.
Proof.
  intros n m H.
  f_equal.
  exact H.
Qed.

f_equal 与 congruence 的关系：f_equal 是手动分解一步合同性，congruence 是自动求解合同闭包。若 congruence 能直接关闭目标，无需 f_equal；若需要对子目标分别施加不同的推理，f_equal 更合适。

replace：带局部证明的目标替换

replace a with b 将目标中所有 a 替换为 b，同时生成一个额外的子目标 b = a（注意顺序是 b = a 而非 a = b）。replace a with b by tac 用 tac 立即关闭该额外子目标。

1
2
3
4
5
6
7
Lemma replace_demo : forall (n : nat), n + 0 + 1 = n + 1.
Proof.
  intro n.
  replace (n + 0) with n by (rewrite Nat.add_0_r; reflexivity).
  (* 目标简化为：n + 1 = n + 1 *)
  reflexivity.
Qed.

replace 适合在目标的某个子表达式处进行局部等式替换，且替换的正确性需要独立的一小段证明。相比 rewrite，它不要求上下文中有一条现成的等式假设，等式可以在 by 子句中即席证明。

若 by 子句省略，replace 会把 b = a 作为一个独立子目标留下，由用户稍后证明。

使用 Show Proof. 观察证明项结构

等式 tactic 执行后，Coq 内部构造的证明项体现了不同的消去路径。Show Proof. 在证明过程中输出当前的部分证明项，有助于理解 tactic 的底层语义。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Lemma show_proof_eq : forall (n m : nat), n = m -> m = n.
Proof.
  intros n m H.
  symmetry.
  Show Proof.
  (* 输出类似：
     (fun (n m : nat) (H : n = m) =>
       ?Goal)
     其中 ?Goal 仍待填充，当前目标已被 symmetry 变换为 n = m *)
  exact H.
  Show Proof.
  (* 完整项：
     (fun (n m : nat) (H : n = m) =>
       eq_sym H) *)
Qed.

symmetry 对应证明项中的 eq_sym，rewrite H 对应 eq_ind 或其变体，transitivity 对应 eq_trans。Print Assumptions. 可以在定理证明完成后检查该定理是否依赖任何公理（除 Coq 内建公理外）：

1
2
Print Assumptions show_proof_eq.
(* 输出：Closed under the global context *)

Closed under the global context 表明该证明不依赖额外公理。

策略选择：不同等式场景下的决策路径

面对一个等式目标，选择 tactic 的思路如下：

  • 目标是 a = a 或可定义展开为此形式：用 reflexivity
  • 上下文中有 H : a = b，目标中含 a：用 rewrite H；目标中含 b：用 rewrite <- H
  • 上下文中的等式涉及某个局部变量的完整定义（x = expr）：用 subst x
  • 目标是 b = a 而手头有 a = b 的证明：用 symmetry 对齐后 apply
  • 需要经过中间值推导 a = c：用 transitivity，或多次 rewrite
  • 等式可由上下文中多个等式和函数合同性自动推出：用 congruence
  • 目标形如 f a = f b，需要分解为 a = b：用 f_equal
  • 目标某个子表达式需要局部替换，替换条件需要即席证明：用 replace ... with ... by ...
  • 含算术等式：用 ring（纯环论）或 lia（线性算术）

一个综合示例

下面的证明将 subst、rewrite <-、reflexivity 串联起来处理一个两步等式消去：

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

Lemma combined_eq_reasoning :
  forall (f : nat -> nat) (a b c : nat),
    a = b + 1 ->
    b = c ->
    f (c + 1) = f a.
Proof.
  intros f a b c H1 H2.
  (* H1 : a = b + 1，H2 : b = c *)
  (* 目标：f (c + 1) = f a *)
  subst b.
  (* H2 被消去，H1 变为：a = c + 1 *)
  (* 目标：f (c + 1) = f a *)
  rewrite <- H1.
  (* 目标变为：f a = f a *)
  reflexivity.
Qed.

Print Assumptions combined_eq_reasoning.
(* Closed under the global context *)

这里先用 subst b 消去 b，再用 rewrite <- H1 把 c + 1 变回 a，最后 reflexivity 关闭目标。

失败尝试与修正

congruence 对算术等式的处理有明确边界，下面的对比展示了它在哪一步会失效、该用什么替代：

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
Lemma eq_wrong_approach :
  forall (n m : nat), n = m -> n + 1 = m + 1.
Proof.
  intros n m H.
  (* 错误尝试 1：congruence 能处理此目标吗？ *)
  (* congruence. *)
  (* 结果：Succeeded。congruence 确实能处理这个目标，因为 +1 是函数应用 *)

  (* 但若目标是 n + n = m + m，情形不同 *)
Abort.

Lemma eq_double :
  forall (n m : nat), n = m -> n + n = m + m.
Proof.
  intros n m H.
  (* 错误尝试：仅用 rewrite H 只替换一侧 *)
  rewrite H.
  (* 目标变为：m + m = m + m *)
  reflexivity.
Qed.

(* 另一种等价写法，展示 congruence 也能处理此情形 *)
Lemma eq_double_congruence :
  forall (n m : nat), n = m -> n + n = m + m.
Proof.
  intros n m H.
  congruence.
Qed.

第一次尝试中，rewrite H 把目标中两处 n 一并替换为 m，直接关闭了目标。congruence 同样有效。两种方式均正确，选哪个取决于证明链中是否还需要进一步推理。

与标准库等式引理的配合

Coq 标准库在 Coq.Arith.Arith、Coq.Lists.List 等模块中提供了大量等式引理，直接与上述 tactic 搭配使用。常见的有：

  • Nat.add_0_r : forall n, n + 0 = n
  • Nat.add_comm : forall n m, n + m = m + n
  • Nat.add_assoc : forall n m p, n + (m + p) = n + m + p

rewrite Nat.add_comm 可直接将目标中第一处符合 ?n + ?m 的模式交换顺序。若需要指定重写的位置（避免无限循环或选择特定子表达式），可以用 rewrite Nat.add_comm at 2 或为引理提供显式参数：rewrite (Nat.add_comm n m)。

第 05 篇介绍的 Search 命令可以快速定位相关等式引理：Search (_ + 0) 会列出所有结论或假设中含 _ + 0 模式的引理。

循环重写陷阱

当等式两侧在对称变换后形式相同（如 Nat.add_comm : n + m = m + n），直接 rewrite Nat.add_comm 可能造成无限重写循环（实际上 Coq 不会真正无限循环，但会报 maximally inserted 或导致 rewrite 无法终止的变换）。处理方式是为引理提供具体参数：

1
2
3
(* 避免循环的写法 *)
rewrite (Nat.add_comm n m).
(* 而非 rewrite Nat.add_comm，后者可能反复交换同一对参数 *)

ring tactic（针对环结构的等式）在处理纯算术等式时完全避免了这个问题，因为它直接规范化两侧表达式而不依赖方向性重写。

练习一

证明以下引理，要求至少使用一次 f_equal 和一次 subst：

1
2
3
4
5
6
Lemma exercise_1 : forall (g : nat -> nat -> nat) (a b c : nat),
    a = b -> g a c = g b c.
Proof.
  (* 提示：f_equal 会把目标分解为两个子目标 *)
  (* 你的证明 *)
Admitted.

参考答案：

1
2
3
4
5
6
7
Lemma exercise_1_sol : forall (g : nat -> nat -> nat) (a b c : nat),
    a = b -> g a c = g b c.
Proof.
  intros g a b c H.
  subst a.
  reflexivity.
Qed.

练习二

以下证明有一个错误。找出错误所在，并给出正确证明：

1
2
3
4
5
6
7
(* 有误的证明 *)
Lemma exercise_2_buggy : forall (n m : nat),
    S n = S m -> n = m.
Proof.
  intros n m H.
  congruence.  (* 这里能成功吗？为什么？ *)
Qed.

分析：congruence 在此处确实能成功，因为它知道 S 是单射构造子。但若要展示推理细节，可以用 injection H as H' 将 S n = S m 转换为 n = m，再 exact H'。两种方式均正确，congruence 更简洁，injection 更显式。

练习三

证明以下引理，要求使用 replace ... with ... by ...，不得使用 ring 或 omega：

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

Lemma exercise_3 : forall (n : nat),
    (n + 1) + (n + 1) = 2 * n + 2.
Proof.
  intro n.
  (* 提示：可以先 replace (n + 1) with (S n) 或展开 2 * n 的定义 *)
  (* 你的证明 *)
Admitted.

参考答案：

1
2
3
4
5
6
7
8
Lemma exercise_3_sol : forall (n : nat),
    (n + 1) + (n + 1) = 2 * n + 2.
Proof.
  intro n.
  replace (2 * n + 2) with (n + 1 + (n + 1))
    by (rewrite Nat.mul_comm; simpl; rewrite Nat.add_assoc; reflexivity).
  reflexivity.
Qed.

参考资料