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

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

本篇代码片段统一假定已经 Require Import PeanoNat.——Nat.add_0_r、Nat.add_comm、Nat.add_shuffle1 这些引理都住在 PeanoNat.Nat 里（Require Import Arith. 也会连带把它们引进来）。

等式在 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
Lemma plus_comm_sym : forall (n m : nat), n + m = m + n.
Proof.
  intros n m.
  symmetry.
  (* 目标变为：m + n = n + m，正好是 Nat.add_comm 的形状 *)
  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（环论等式）或 lia（线性整数/自然数算术）。老代码里的 omega 在 8.14 已被移除，遇到就直接换 lia。

f_equal：函数应用的合同分解

对形如 f a1 ... an = g b1 ... bn 的目标，f_equal 生成 f = g 以及 n 个参数子目标 ai = bi。关键的一点写在参考手册里：能被 reflexivity 或 congruence 关掉的子目标会被自动消掉，只有剩下的才留给用户。

所以下面这两个例子都是一步收尾，后面不会有子目标可分：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Lemma f_equal_demo : forall (n m k : nat),
    n = m -> (n, k) = (m, k).
Proof.
  intros n m k H.
  f_equal.
  (* k = k 由 reflexivity 消掉，n = m 由 congruence 从 H 推出，目标全清 *)
Qed.

Lemma f_equal_unary : forall (n m : nat),
    n = m -> S n = S m.
Proof.
  intros n m H.
  f_equal.
  (* 唯一的子目标 n = m 同样被 congruence 就地关掉 *)
Qed.

想看到留下来的子目标，参数等式必须是这两条自动化都拿不下的。n + 0 = n 正好符合——前面刚验证过 congruence 不做算术：

1
2
3
4
5
6
7
8
Lemma f_equal_leftover : forall (n : nat),
    (n + 0, 1) = (n, 1).
Proof.
  intros n.
  f_equal.
  (* 1 = 1 被自动消掉；剩下 n + 0 = n 需要手动处理 *)
  apply Nat.add_0_r.
Qed.

f_equal 与 congruence 的关系因此不是"手动 vs 自动"的二选一：f_equal 先按参数位把目标劈开，再对每一片调用 congruence 收尾。congruence 单独用不动的场合（含算术、需要展开定义），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 与 rewrite 的分界

只要等式两侧的差异全部来自"同一个函数、不同的参数"，congruence 和 rewrite 都能收尾：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Lemma eq_double_rewrite :
  forall (n m : nat), n = m -> n + n = m + m.
Proof.
  intros n m H.
  rewrite H.        (* 目标里两处 n 一并换成 m，得到 m + m = m + m *)
  reflexivity.
Qed.

Lemma eq_double_congruence :
  forall (n m : nat), n = m -> n + n = m + m.
Proof.
  intros n m H.
  congruence.       (* 从 H 出发按合同性直接推出结论 *)
Qed.

分界线落在需不需要算术。n + n = m + m 只要求"把 n 换成 m"，+ 本身没有参与推理，所以 congruence 够用。一旦结论依赖 + 的代数性质，congruence 立刻失效：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Lemma needs_arith :
  forall (n m : nat), n = m -> n + m = m + n.
Proof.
  intros n m H.
  (* congruence. 这里也行，因为 H 让两侧变成同一个式子 *)
  (* 但去掉前提 H 之后就只能靠 Nat.add_comm 或 lia *)
  congruence.
Qed.

Lemma needs_arith_no_hyp :
  forall (n m : nat), n + m = m + n.
Proof.
  intros n m.
  (* 此时上下文空空，congruence 没有等式可用，只能走算术引理 *)
  apply Nat.add_comm.
Qed.

选 rewrite 还是 congruence，看后面还要不要接着推：rewrite 留下一个变形后的目标可以继续加工，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 不会循环——它只改写一批匹配就停。真正会打转的是加了重复修饰符或包在循环里的写法：repeat rewrite Nat.add_comm 会把同一对参数换过去再换回来，永不终止；rewrite !Nat.add_comm 同理。

单次 rewrite Nat.add_comm 的实际风险是换错位置：它匹配的是第一处符合 ?n + ?m 的子项，在 a + b + (c + d) 这种式子里，命中的往往不是要动的那一处。把参数钉死可以消除歧义：

1
2
rewrite (Nat.add_comm c d).   (* 明确只交换 c 和 d *)
rewrite Nat.add_comm at 2.    (* 或者按出现次序指定第 2 处 *)

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

练习一

下面这个目标用 f_equal、subst、congruence 都能一步关掉。三种都写一遍，然后用 Show Proof. 对比证明项：

1
2
3
4
5
Lemma exercise_1 : forall (g : nat -> nat -> nat) (a b c : nat),
    a = b -> g a c = g b c.
Proof.
  (* 你的证明 *)
Admitted.

参考答案：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Lemma exercise_1_feq : forall (g : nat -> nat -> nat) (a b c : nat),
    a = b -> g a c = g b c.
Proof.
  intros g a b c H.
  f_equal.        (* c = c 由 reflexivity 消掉，a = b 由 congruence 从 H 推出 *)
Qed.

Lemma exercise_1_subst : 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.

要点在于 subst 走的是 eq_ind——把 a 从整个目标里换成 b，换完两侧同形，reflexivity 收尾。f_equal 则沿参数位分解，再让 congruence 逐片收尾，证明项里留下的是合同引理的应用。两者体量差不多，但在参数多、只有一两个位置不同的目标上，f_equal 的分解更省事。

练习二

下面这个证明能通过。说明 congruence 凭什么能关掉它，然后写一个不依赖 congruence 的显式版本：

1
2
3
4
5
6
Lemma exercise_2 : forall (n m : nat),
    S n = S m -> n = m.
Proof.
  intros n m H.
  congruence.
Qed.

分析：congruence 的合同闭包算法内建了构造子的单射性，S n = S m 在它眼里直接蕴含 n = m，不需要额外提示。显式版本用 injection：

1
2
3
4
5
6
7
Lemma exercise_2_explicit : forall (n m : nat),
    S n = S m -> n = m.
Proof.
  intros n m H.
  injection H as H'.   (* H' : n = m *)
  exact H'.
Qed.

injection 只做构造子单射这一件事，边界清楚；congruence 把单射性、不相交性、传递闭包打包在一起，写起来短但失败时不好定位是哪一条没成立。

练习三

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

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.
  (* 提示：先把 2 * n 换成 n + n，剩下的是纯粹的重排 *)
  (* 你的证明 *)
Admitted.

参考答案：

1
2
3
4
5
6
7
8
9
10
11
12
Lemma exercise_3_sol : forall (n : nat),
    (n + 1) + (n + 1) = 2 * n + 2.
Proof.
  intro n.
  replace (2 * n) with (n + n)
    by (simpl; rewrite Nat.add_0_r; reflexivity).
  (* 目标：n + 1 + (n + 1) = n + n + 2 *)
  rewrite Nat.add_shuffle1.
  (* Nat.add_shuffle1 : n + m + (p + q) = n + p + (m + q)
     左侧 (n + 1) + (n + 1) 变成 (n + n) + (1 + 1) *)
  reflexivity.
Qed.

replace 产生的副目标是 n + n = 2 * n：simpl 把 2 * n 展开成 n + (n + 0)（Nat.mul 对第一个参数递归，2 是字面量所以能展开），rewrite Nat.add_0_r 消掉 + 0，两侧同形。主目标最后靠 reflexivity 收尾，因为 1 + 1 是闭项，归约到 2。

参考资料