深入 Coq 18：Coq 证明工程总结与路线图
本篇回顾系列的整体脉络，指出从当前知识基线出发的几条进阶路线，并以一个综合验证项目作为系列收束。 系列脉络回顾 第 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 代数层 第...
深入 Coq 17：项目组织与持续集成
单文件脚本足够应付练习，但 MathComp、Iris、CompCert 这类真实库管理数百个 .v 文件。本篇覆盖两套主流构建系统（coq_makefile 与 dune）、opam 包发布流程、CI 管道配置和 Coq 版本管理策略。 _CoqProject 与 coq_makefile _CoqProject 是 Coq 内置构建工具的项目描述文件。一个最小示例： 1234567-Q theories MyLib-Q tests MyLib.Teststheories/Basics.vtheories/Induction.vtheories/Lists.vtests/TestBasics.v -Q theories MyLib 把 theories/ 目录映射到逻辑路径 MyLib，使得 Require Import MyLib.Basics 解析到 theories/Basics.v。另一个标志 -R 做的是同一件事，只是额外允许调用方省略前缀直接写 Require Import Basics.。新项目建议用 -Q：多打几个字，换来的是调用方不会因为两个库都有 Basic...
深入 Coq 16：读 CompCert 源码
CompCert 是经过机器检验的优化 C 编译器，也是规模最大的 Coq 工程之一。以 3.17 版实测：自有 Coq 代码约 17.1 万行，加上 vendored 的 flocq（浮点）与 MenhirLib（解析器验证库）共约 20.6 万行；OCaml 侧（.ml/.mli/.mll/.mly）约 4.1 万行。本篇不试图覆盖 CompCert 全貌，而是以 Constprop（常量传播）pass 为切入点，解剖一个工业级 Coq 项目在模块组织、证明策略、仿真关系、提取边界上的工程选择。 本篇的行号与路径基于 CompCert 3.17（2026-02 发布）。CompCert 的目录结构相对稳定，但具体行号会随版本漂移，读源码时以自己 clone 的那份为准。 在动手 clone 之前先看一眼许可：CompCert 版权归 INRIA 与 AbsInt Angewandte Informatik GmbH，默认走 INRIA Non-Commercial License Agreement——这是一份非自由许可，只授予教学、研究、评估用途，明确禁止商业使用；商业使用...
深入 Coq 15：验证一个小型解释器
本篇用一个端到端的案例把前 14 篇的技术串起来：定义一门带类型的小语言，给它写解释器，证明类型安全定理（progress + preservation），最后用 Extraction 把经过验证的解释器导出为可执行的 OCaml 代码。整个流程对应 Programming Language Foundations (PLF) 中 STLC 章节的精简版本，但更侧重工程实操。 语言定义：MiniLang MiniLang 只有两种类型、五种表达式，足够展示类型安全证明的完整结构，又不至于让证明淹没在 case analysis 中。 类型与语法 12345678910Inductive ty : Type := | TBool : ty | TNat : ty.Inductive expr : Type := | ETrue : expr | EFalse : expr | ENat : nat -> expr | EPlus : expr -> expr -> expr | EIf : expr -> expr -> ...
深入 Coq 14：程序提取
Coq 不仅是证明助手，也是一门带有计算语义的函数式语言。通过 Extraction 机制，Gallina 程序可以被翻译成 OCaml、Haskell 或 Scheme 的可运行代码，同时抹去所有停留在 Prop 宇宙中的证明项。本文覆盖 Extraction 的核心命令、类型映射指令、内联控制、性能陷阱，以及一个从证明到编译运行的完整示例。 前置阅读：本系列前三篇（01 开发环境与项目结构、02 目标窗口与 tactic 交互模型、03 Gallina 核心语法速查）以及第 09 篇（归纳证明）提供了本文所需的 Gallina 和 tactic 基础。 Extraction 机制概览 Extraction 的基础是 Curry-Howard 同构的计算部分：类型为 A : Type 或 A : Set 的项携带运行时数据，而类型为 P : Prop 的项纯粹是逻辑断言，不携带可观察的计算内容。提取器（extractor）遍历 Gallina 的 proof term，遇到 Prop 宇宙中的构造子时直接擦除，只保留 Type/Set 宇宙的骨架，再将剩余的 CIC 项翻译成目...
深入 Coq 13：证明红绿灯：常见卡住模式与诊断
证明中断不是随机的。Coq 报错信息有规律，每种卡住模式都有对应的诊断手段和修复路径。本文整理六类高频卡住模式，逐一给出错误现场、根因和处理方法，附诊断工具用法。 诊断工具速览 下列诊断命令不参与证明，只用于观察状态，本文各节均会用到。 1234567Set Printing All. (* 显示所有隐式参数、强制转换、记号展开 *)Set Printing Universes. (* 在类型中显示宇宙层级标注 *)Check @term. (* 显示 term 的完整类型，含所有显式参数 *)About ident. (* 显示 ident 的来源、类型、透明度等元信息 *)Print ident. (* 显示 ident 的定义或公理 *)Show Proof. (* 在证明过程中打印当前 proof term 的骨架 *)Print Assumptions thm. (* 列出 thm 依赖的全部公理和假设 *) Set Printing All 是最常用的...
深入 Coq 12：类型类与 Canonical Structures
Coq 提供两套独立的"重载"机制：类型类（Type Classes）和典范结构（Canonical Structures）。两者表面都是让用户向一个通用接口注册实现，但底层驱动方式截然不同：类型类依赖 unification 变量加实例搜索，典范结构依赖投影展开后的合一。MathComp 库选择典范结构作为代数层次的支柱，这一设计决策影响了整套库的证明风格。本篇覆盖两套机制的语义、调试手段、权衡比较，以及 MathComp 如何用典范结构把 eqType、choiceType、zmodType、ringType、fieldType 串成一条可继承的层次链。前置阅读：《深入 Coq 03：Gallina 核心语法速查》和《深入 Coq 07：Ltac 编程》；代数基础见《依值类型——从命题逻辑到一阶逻辑》。 类型类的核心机制 Class 与 Instance 声明 Coq 的 Class 关键字声明一个带有命名字段的 record，附带一个隐式实例参数占位符。Instance 声明将某个具体类型注册为该 class 的实现。 1234567891011121...
深入 Coq 11：存在性证明与构造见证
存在性命题断言某个满足特定性质的对象存在。在 Coq 的命题即类型对应中，证明 ∃ x, P x 等价于构造一个依值对 ⟨w, p⟩，其中 w 是具体见证项，p : P w 是该见证满足性质的证明。这种"构造即证明"的机制直接决定了存在性证明的操作方式。 存在性命题的底层结构 Coq 标准库中 ex 的定义如下： 12Inductive ex (A : Type) (P : A -> Prop) : Prop := | ex_intro : forall x : A, P x -> ex A P. 语法糖 ∃ x : A, P x 展开为 ex A (fun x => P x)。构造证明的唯一方式是应用 ex_intro，给出见证 x 和 P x 的证明。tactic 层面的 exists w 等价于 apply ex_intro with (x := w)，然后留下 P w 作为子目标。 123456(* 最基础的存在性证明 *)Lemma ex_basic : exists n : nat, n + 2 = 5.Proof. exis...
深入 Coq 10：等式推理与重写策略
等式推理是 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，通常...
深入 Coq 09：归纳证明：自然数、列表、树
归纳证明是 Coq 中最核心的推理手段。无论是对自然数的算术性质、对列表的结构性质，还是对树的递归性质，归纳原理都以同一套框架给出严格证明。本文系统覆盖三类归纳：标准结构归纳、完全归纳（强归纳），以及依赖 Acc 和 Fix 的 well-founded 递归。 前置阅读：本系列 01（环境与项目结构）、02（目标窗口与 tactic 交互）、03（Gallina 核心语法）、04（基础 tactic 全景）提供了必要的语法和 tactic 背景。本文中出现的 induction、simpl、rewrite、auto 等 tactic 在 04 中均有详细说明。 自然数上的结构归纳 归纳原理的来源 nat 在 Coq 标准库中定义为： 123Inductive nat : Set := | O : nat | S : nat -> nat. Inductive 指令自动生成归纳原理 nat_ind，其类型为： 1234nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P...
