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

系列脉络回顾

第 01-03 篇解决上手问题：opam switch 与 _CoqProject、目标窗口与 tactic 的状态机模型、Gallina 的核心语法。核心循环在这一阶段成型：写规约、观察目标状态、施加 tactic、关闭证明。

第 04-08 篇是 tactic 与自动化：六条基础 tactic 的语义、hint 数据库与 lia/ring/field、SSReflect 的栈式语法与 small-scale reflection、Ltac 的 match goal 元编程、Ltac2 的静态类型 tactic 语言。这一段把重复劳动交给机器。

第 09-12 篇是证明技术：结构归纳与良基递归、等式推理与重写策略、存在性证明与构造见证、类型类与 Canonical Structures 两套推断机制。

第 13-17 篇转向工程：常见卡住模式的诊断、程序提取、一个解释器的端到端验证、CompCert 源码走读、项目组织与 CI。

进阶方向

MathComp 代数层

第 06 篇覆盖了 SSReflect 的证明风格和 ssrbool 的布尔反射，第 12 篇讲了支撑 MathComp 层级的 Canonical Structures 机制。下一层是代数层级本身：zmodType（加法群）、ringType（环）、fieldType（域）、lalgType（代数）。这些类型为 mathcomp-algebra 和 mathcomp-field 中的多项式运算、矩阵理论和 Galois 理论提供统一接口。

入口建议：mathcomp-algebra 中的 poly 库。一个具体的起步项目是形式化域上一元多项式的除法算法，然后证明 Euclidean 算法产生最大公因子。这个项目会用到第 06 篇的 SSReflect 证明风格，以及第 12 篇讲的 Hierarchy Builder——mathcomp 2.0 起整个层次都由 HB.mixin / HB.structure / HB.instance 生成，1.x 时代手写 packed class 的构造子（EqMixin、EqType 等）已被删除。往代数层走之前先把这套机制摸熟，否则读 ssralg 的源码会寸步难行。

Iris 分离逻辑

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

典型的 Iris 证明同时操作资源（堆所有权、ghost state、不变量）和标准 Coq 逻辑。学习曲线陡峭，因为它组合了三个领域：Coq tactic（第 04-08 篇的内容）、分离逻辑连接词（∗、-∗、□、▷）、以及 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 中程序语言语义章节的典型练习，用到归纳法（第 09 篇）、等式重写（第 10 篇）、tactic 自动化（第 05、07、08 篇）。

参考资料