SSReflect 是 Coq 的一个 tactic 语言扩展，由 Georges Gonthier 等人在形式化四色定理期间开发，后来成为 Mathematical Components（MathComp）库的基础 tactic 层。Coq 8.7 起，SSReflect 被收入标准发行版，无需额外安装。本篇在前序文章（01 开发环境、02 目标窗口、04 基础 tactic、05 搜索与自动化）的基础上，系统介绍 SSReflect 的设计哲学与核心 tactic。

MathComp 选择 SSReflect 的原因

原生 Coq tactic（intro、destruct、induction 等）在小规模证明中已经够用，但在大型数学库的维护场景下暴露出几个结构性问题。

第一，上下文管理成本高。intro 引入假设后，名字由用户手动管理；destruct 和 induction 在分支众多时很容易导致名字污染，同一个局部变量在不同分支有不同含义，证明脚本难以阅读。

第二，命题（Prop）和布尔函数（bool）之间缺乏统一的转换机制。Coq 标准库里存在大量 Prop 形式的谓词，而计算可判定性（bool 函数）的引理分散在不同位置，在两者之间来回转化需要大量胶水代码。

第三，原生 rewrite 的方向控制和匹配控制较弱，在复杂等式链中需要频繁用 symmetry、rewrite <- 切换方向，视觉噪声大。

SSReflect 的解决方案是引入三个机制：统一的 move/case/elim 栈式语法减少名字管理开销；reflect 类型桥接 bool 和 Prop；以及视图（view）机制在 tactic 内部进行局部转换。

环境设置

本篇所有代码需要以下 Require 声明：

1
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.

对于只需要 SSReflect tactic 语法而不用 MathComp 数学内容的场景，最小依赖是：

1
From Coq Require Import ssreflect.

验证环境：Coq 8.19，MathComp 2.2.x。

move、case、elim 的栈式语法

SSReflect 把目标和假设看作一个隐式栈。: 将上下文中的假设压入目标顶部，=> 将目标顶部的量词或假设弹出到上下文并命名。

move 的基本形式

1
2
3
4
5
6
Lemma add_comm_ssr (m n : nat) : m + n = n + m.
Proof.
  move: m.         (* 将 m 压回目标 *)
  move=> m.        (* 重新引入 m，等价于 intro m *)
  (* 目标：m + n = n + m *)
Abort.

move: h 和 move=> h 可以链式组合。以下将假设 H : P 从上下文移入目标再立即析构：

1
move: H => [h1 h2].   (* 等价于 destruct H as [h1 h2] *)

case 与 elim 的引入模式

case 对目标顶部的归纳类型执行模式匹配（不产生归纳假设），elim 产生归纳假设。两者均支持紧跟引入模式：

1
2
3
4
5
6
Lemma nat_cases (n : nat) : n = 0 \/ exists m, n = m.+1.
Proof.
  case: n => [| m].
  - left. reflexivity.
  - right. exists m. reflexivity.
Qed.

[| m] 是引入模式：第一个分支（n = 0）不引入变量，第二个分支（n = S m）引入 m。对比原生写法需要单独的 intro n; destruct n as [| m]，SSReflect 将析构和命名压缩到同一行。

elim 的用法类似，但第二个分支多出归纳假设：

1
2
3
4
5
6
Lemma add_0_r (n : nat) : n + 0 = n.
Proof.
  elim: n => [| k IHk].
  - reflexivity.
  - simpl. rewrite IHk. reflexivity.
Qed.

[| k IHk] 中 IHk 是归纳假设，命名由用户显式控制，避免了原生 induction 自动生成的名字（如 IHn）在批量重构时带来的脆弱性。

have 与 suffices

have：局部引理

have 在当前证明内引入一个子目标，证完后将结论加入上下文：

1
2
3
4
5
6
Lemma example_have (n : nat) : n + 1 > n.
Proof.
  have H : 1 > 0 by exact: lt0n.
  (* 上下文现在有 H : 1 > 0 *)
  exact: ltnSn.
Qed.

by 后面跟一个 tactic 表达式，尝试立即关闭 have 产生的子目标。若需要多步证明，可以用 have H : P. 不带 by，然后在新子目标里证 P，再继续原目标。

suffices：反向充分条件

suffices H : P 的逻辑是：若能证明 P → 当前目标，且能证明 P，则目标成立。它先让用户证明"P 足够了"，再证 P 本身：

1
2
3
4
5
Lemma example_suffices (n : nat) : n * 2 = n + n.
Proof.
  suffices H : forall k, k * 2 = k + k by exact: H n.
  intro k. ring.
Qed.

suffices 在证明归纳步骤时特别有用——先把"只需更强命题成立"的论证写清楚，再回头证更强命题。

apply 与 rewrite 的 SSReflect 增强

apply 的精确目标控制

SSReflect 的 apply: 与原生 apply 的区别在于对目标形状的匹配更严格，出错信息更精确：

1
2
apply: some_lemma.       (* SSReflect 风格 *)
apply some_lemma.        (* 原生风格 *)

两者语义相近，但 SSReflect 版本在引理类型与目标不匹配时会更快报错，而不是进入 unification 黑洞。

rewrite 的方向与重复控制

SSReflect 的 rewrite 扩展了几个常用修饰符：

1
2
3
4
rewrite -lemma.          (* 从右向左改写，等价于原生 rewrite <- lemma *)
rewrite [pattern]lemma.  (* 只改写匹配 pattern 的子项 *)
rewrite !lemma.          (* 重复改写直到失败 *)
rewrite ?lemma.          (* 尝试改写，失败不报错 *)

示例：

1
2
3
4
5
Lemma rewrite_demo (a b c : nat) : a + b + c = c + (a + b).
Proof.
  rewrite -addnA.    (* addnA : m + n + p = m + (n + p)，从右向左 *)
  rewrite addnC.     (* 完成 *)
Qed.

small-scale reflection 哲学

SSReflect 的核心设计思想称为"small-scale reflection"，指在证明中频繁地在 bool 计算和 Prop 逻辑之间切换，利用布尔函数的可计算性简化证明。

reflect 类型

标准库中 reflect 的定义如下：

1
2
3
Inductive reflect (P : Prop) : bool -> Type :=
  | ReflectT :  P -> reflect P true
  | ReflectF : ~P -> reflect P false.

reflect P b 表示：当 b = true 时，P 成立；当 b = false 时，P 不成立。这个类型将命题 P 与它的布尔决策函数 b 绑定在一起。

iffP、idP、eqP

MathComp 提供了一批 reflect 相关的引理，用于在证明中快速切换视角。

idP 是最基础的：

1
idP : reflect b b

它说明任何布尔值 b 都可以被当作命题 b = true 来处理（当 b = true 时成立，b = false 时不成立）。

iffP 用于从已知的 reflect P b 构造新的反射引理：

1
iffP : reflect P b -> (P <-> Q) -> reflect Q b

eqP 是 MathComp 中相等性反射的核心：

1
eqP : reflect (x = y) (x == y)

其中 x == y 是 MathComp 中可判定相等的布尔版本（eqb），x = y 是 Coq 原生的命题相等。有了 eqP，在 x == y = true 和 x = y 之间转换无需手写 apply Nat.eqb_eq 之类的引理。

布尔命题的使用示例

1
2
3
4
5
6
7
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype.

Lemma reflect_example (n m : nat) : n == m -> n = m.
Proof.
  move/eqP.    (* 用 eqP 视图将 n == m 转为 n = m *)
  exact: id.
Qed.

move/eqP 是视图语法，详见下节。

视图机制与 move/view

视图（view）机制允许在 move、case、apply 等 tactic 中内嵌一次 reflect 转换，避免单独调用 apply。

语法是 /lemma，放在 move、case 的后面：

1
2
3
move/eqP => H.     (* 将栈顶的 n == m 通过 eqP 转为 n = m，命名为 H *)
case/eqP.          (* 对 n == m 做 case，分析 n = m 的情形 *)
apply/eqP.         (* 将目标 n = m 转为 n == m，再用后续 tactic 证明 *)

完整示例：

1
2
3
4
5
6
Lemma view_example (n : nat) : n == 0 -> 0 == n.
Proof.
  move/eqP => H.    (* H : n = 0 *)
  apply/eqP.        (* 目标转为 0 = n *)
  exact: esym H.
Qed.

视图机制的好处在于把"先转换表示，再证明"这两步合并，减少中间名字的引入。

SSReflect 与原生 tactic 的风格对比

以同一个定理为例：∀ n m : nat, n = m → m = n（等式对称性，可以直接用 eq_sym，这里为演示目的手动证明）。

原生 tactic 写法

1
2
3
4
5
Lemma sym_vanilla (n m : nat) (H : n = m) : m = n.
Proof.
  destruct H.
  reflexivity.
Qed.

或者：

1
2
3
4
5
6
Lemma sym_vanilla2 (n m : nat) : n = m -> m = n.
Proof.
  intro H.
  symmetry.
  exact H.
Qed.

SSReflect 写法

1
2
3
4
5
Lemma sym_ssr (n m : nat) : n = m -> m = n.
Proof.
  move=> H.
  exact: esym H.
Qed.

更紧凑的版本直接用 move 链：

1
2
3
4
Lemma sym_ssr2 (n m : nat) : n = m -> m = n.
Proof.
  by move=> ->.    (* -> 是引入模式：引入 H : n = m 并立即改写目标 *)
Qed.

-> 在引入模式中的含义：将等式 H : a = b 引入并立即执行 rewrite H，然后丢弃 H。目标从 m = n 变为 n = n，由 by 调用 reflexivity 关闭。

失败尝试与正确做法

在使用视图时，常见错误是把视图方向弄反。

1
2
3
4
5
6
(* 失败尝试：目标是 n == m，错误地用 apply/eqP 期望直接关闭 *)
Lemma wrong_direction (n m : nat) (H : n = m) : n == m.
Proof.
  apply/eqP.   (* 正确：目标从 n == m 转为 n = m *)
  exact H.     (* 现在目标是 n = m，可以用 H 关闭 *)
Qed.

上面实际上是正确的。以下是真正的失败案例：

1
2
3
4
5
6
7
8
9
(* 失败尝试：混淆 move/ 和 apply/ 的方向 *)
Lemma failed_attempt (n m : nat) : n == m -> n = m.
Proof.
  (* 错误写法：apply/eqP 在这里期望目标是 n == m，但目标是 n == m -> n = m *)
  (* apply/eqP.  <- 这会报错：无法匹配 *)
  (* 正确写法：用 move/eqP 处理前提 *)
  move/eqP => H.
  exact H.
Qed.

规则：move/v 将栈顶（前提或目标量词）通过视图 v 转换后引入；apply/v 将当前目标通过视图 v 转换后再试图证明。两者的方向刚好相反，混用是初学者最常见的错误。

在一个证明完成后，可以用 Print Assumptions 检查证明是否依赖了公理（axiom）或未闭合的假设：

1
2
3
4
5
6
7
8
9
Lemma add_comm_check (m n : nat) : m + n = n + m.
Proof.
  elim: m => [| k IHk].
  - by rewrite add0n addn0.
  - by rewrite addSn IHk addnS.
Qed.

Print Assumptions add_comm_check.
(* 输出：Closed under the global context *)

“Closed under the global context” 意味着证明不依赖任何额外公理，是完全构造性的证明。

如果证明链中某处用了 Classical（排中律）或 FunctionalExtensionality，Print Assumptions 会把它们列出来。

布尔逻辑的反射引理汇总

MathComp 的 ssrbool 模块提供了系统性的布尔反射引理，以下是常用的几个：

引理 类型 含义
idP reflect b b 布尔值自反射
andP reflect (P /\ Q) (b && c) 合取反射
orP reflect (P \/ Q) (b || c) 析取反射
negP reflect (~P) (~~ b) 否定反射
eqP reflect (x = y) (x == y) 相等性反射
implyP reflect (P -> Q) (b ==> c) 蕴含反射

有了这些引理，case/andP、move/orP 之类的 tactic 组合可以直接在布尔语义和命题语义之间切换，无需手写转换引理。

小结与前后参照

SSReflect 的设计不是替换原生 tactic，而是在特定场景下提供更结构化的证明语言。move/case/elim 的栈式语法适合需要精确控制引入顺序的证明；have/suffices 适合分解复杂证明目标；reflect 类型和视图机制适合需要频繁在 bool 和 Prop 之间转换的算法性质证明。

原生 tactic（04 篇覆盖）在交互式探索阶段仍然有价值，SSReflect 更适合工业级证明脚本的书写和维护。

下篇（07 Ltac 编程）处理自定义 tactic 的元编程。

习题

习题一：基础 move 语法

不使用 intro 和 destruct，只用 SSReflect 的 move、case、exact，证明以下引理：

1
Lemma ex1 (P Q : Prop) : P /\ Q -> Q /\ P.

提示：move=> [h1 h2] 可以在一步内析构合取。

习题二：布尔反射

使用 andP、orP 或 eqP 的视图机制证明以下引理（禁止使用 simpl 或 rewrite）：

1
2
3
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype.

Lemma ex2 (b1 b2 : bool) : b1 && b2 -> b2 && b1.

提示：case/andP 可以把 b1 && b2 分解为两个命题。

习题三：have 与 suffices 的组合

证明以下定理，要求：

  • 用 have 引入至少一个中间引理；
  • 用 suffices 将原目标规约为更弱的条件；
  • 在证明结束后添加 Print Assumptions，确认无额外公理依赖。
1
2
3
From mathcomp Require Import ssreflect ssrnat.

Lemma ex3 (n : nat) : n + n = 2 * n.

提示：2 * n 在 MathComp 中展开为 n + (n + 0)，addn0 可消去右侧的 + 0。

参考资料