本篇回顾系列的整体脉络，指出从当前知识基线出发的几条进阶路线，并以一个综合验证项目作为系列收束。

系列脉络回顾

第 01-06 篇建立基础：从 opam 安装和目标窗口交互（01-02），到 Gallina 语法（03）、tactic 工作流（04）、SSReflect 方言（05）、MathComp 数据结构（06）。核心循环在这一阶段成型——写规约、观察目标状态、施加 tactic、关闭证明。

第 07-12 篇引入工程工具：Ltac 自动化（07）、Ltac2 类型化元编程（08）、Hierarchy Builder 代数层级构建（09）、Canonical Structure 实例解析（10）、universe 多态（11）、程序提取（12）。这些工具使证明开发能够超越玩具级别的规模。

第 13-17 篇将工具连接到实际问题：SSReflect 模算术（13）、setoid 重写与自定义等价关系（14）、可判定性与布尔反射（15）、CompCert 已验证编译器源码阅读（16）、项目组织与 CI（17）。

进阶方向

MathComp 代数层

第 05-06 篇和第 13 篇覆盖了 MathComp 的 ssrnat、seq、fintype 家族。下一层是代数层级：zmodType（加法群）、ringType（环）、fieldType（域）、lalgType（代数）。这些类型为 mathcomp-algebra 和 mathcomp-field 中的多项式运算、矩阵理论和 Galois 理论提供统一接口。

入口建议：mathcomp-algebra 中的 poly 库。一个具体的起步项目是形式化域上一元多项式的除法算法，然后证明 Euclidean 算法产生最大公因子。这个项目会用到 Hierarchy Builder（第 09 篇）构建的层级和 SSReflect（第 05 篇）的证明风格。

Iris 分离逻辑

Iris 是一个构建在 Coq 之上的高阶并发分离逻辑框架。它提供 iProp 类型的分离逻辑命题和一套证明模式（iProofMode），在 Coq 的 tactic 语言基础上扩展出空间上下文和持久上下文。

典型的 Iris 证明同时操作资源（堆所有权、ghost state、不变量）和标准 Coq 逻辑。学习曲线陡峭，因为它组合了三个领域：Coq tactic（第 04-07 篇的内容）、分离逻辑连接词（∗、-∗、□、▷）、以及 Iris 特有概念（ghost name、view shift、最弱前条件）。

入口建议：iris-project.org 上的教程。一个具体的起步项目是使用 Iris 的不变量机制验证一个自旋锁实现。

VST 与 C 程序验证

VST（Verified Software Toolchain）将分离逻辑应用于 C 程序验证，目标程序以 CompCert 的 Clight AST（第 16 篇介绍的 CompCert 前端中间表示）为载体。VST 在 CompCert 的语义之上提供了一套 C 语言的 Hoare 逻辑。

一个 VST 证明的典型流程：从 .c 文件出发，通过 CompCert 的解析器获得 Clight AST，然后用 DECLARE ... WITH ... PRE ... POST ... 语法陈述函数规约，最后通过 forward（符号执行）和 entailer!（分离逻辑蕴涵）tactic 组合完成证明。

入口建议：Software Foundations 第 5 卷。一个具体的起步项目是验证一个链表反转函数。

CompCert 源码贡献

第 16 篇走读了 CompCert 的 pass 结构。向 CompCert 贡献代码需要掌握其中描述的证明方法论：simulation diagram、match_states 不变量、forward_simulation / backward_simulation 框架。

可行的贡献方向包括：在后端添加新的优化 pass（LTL 或 Mach 层的 peephole 优化）、扩展前端以处理更多 C 特性、改进目标架构语义的形式规约。

工具链资源

资源 用途
Coq Zulip 社区问答，核心开发者活跃
coq-community 维护库集合、CI 模板、文档
Coq Platform 一键安装 Coq + 常用库
Software Foundations 形式化教材，覆盖逻辑→PLT→验证
MathComp Book SSReflect + MathComp 系统教程
CPDT 自动化证明策略进阶

综合验证项目

作为系列收束，下面是一个综合项目规格，覆盖系列中多个主题。

实现并验证一个简单的表达式求值器。定义 AST 类型：

1
2
3
4
5
6
7
8
9
10
11
Inductive expr : Type :=
  | Const : nat -> expr
  | Plus  : expr -> expr -> expr
  | Times : expr -> expr -> expr.

Fixpoint eval (e : expr) : nat :=
  match e with
  | Const n     => n
  | Plus e1 e2  => eval e1 + eval e2
  | Times e1 e2 => eval e1 * eval e2
  end.

定义栈机指令集和编译器：

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
Inductive instr : Type :=
  | Push : nat -> instr
  | Add  : instr
  | Mul  : instr.

Definition prog := list instr.

Fixpoint run (p : prog) (stack : list nat) : option (list nat) :=
  match p with
  | []            => Some stack
  | Push n :: p'  => run p' (n :: stack)
  | Add :: p'     =>
      match stack with
      | b :: a :: s => run p' ((a + b) :: s)
      | _           => None
      end
  | Mul :: p'     =>
      match stack with
      | b :: a :: s => run p' ((a * b) :: s)
      | _           => None
      end
  end.

Fixpoint compile (e : expr) : prog :=
  match e with
  | Const n     => [Push n]
  | Plus e1 e2  => compile e1 ++ compile e2 ++ [Add]
  | Times e1 e2 => compile e1 ++ compile e2 ++ [Mul]
  end.

目标定理：

1
2
Theorem compile_correct : forall e,
  run (compile e) [] = Some [eval e].

直接对 e 做归纳会卡在 Plus 情况：归纳假设只谈空栈 []，而递归调用 compile e2 执行时栈上已有 eval e1。修复方式是证明一个对任意栈和后续程序泛化的辅助引理：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
Lemma compile_correct_gen : forall e p s,
  run (compile e ++ p) s = run p (eval e :: s).
Proof.
  induction e; intros p s; simpl.
  - (* Const *) reflexivity.
  - (* Plus *)
    rewrite app_assoc_reverse.
    rewrite IHe1. rewrite app_assoc_reverse.
    rewrite IHe2. simpl. reflexivity.
  - (* Times *)
    rewrite app_assoc_reverse.
    rewrite IHe1. rewrite app_assoc_reverse.
    rewrite IHe2. simpl. reflexivity.
Qed.

Theorem compile_correct : forall e,
  run (compile e) [] = Some [eval e].
Proof.
  intros e.
  rewrite <- app_nil_r with (l := compile e).
  rewrite compile_correct_gen. reflexivity.
Qed.

完成后验证公理依赖：

1
2
Print Assumptions compile_correct.
(* 预期: Closed under the global context *)

如果证明过程中不慎使用了 admit，Print Assumptions 会暴露出 Axioms: compile_correct_gen_subproof : ... 之类的残留。

扩展方向：添加变量绑定（Let x = e1 in e2）和条件分支（IfZero e1 then e2 else e3）。变量绑定需要引入环境（变量到值的映射），条件分支需要在栈机中增加跳转指令。重新证明编译正确性时，泛化引理的形式需要同时携带环境参数。这是 Software Foundations 中程序语言语义章节的典型练习，用到归纳法（第 04 篇）、列表操作（第 05-06 篇）、tactic 自动化（第 07-08 篇）。

参考资料