深入 Lean 01：Lake 项目结构与依赖管理
Lake 是 Lean 4 的官方构建系统与包管理器，随 lean 工具链一同分发。形式化方法系列的第 07-08 篇已覆盖 elan 安装与 lake new 起手骨架；本篇从那个骨架向前推进，聚焦生产级项目需要的部分：toolchain 锁定、Mathlib4 依赖引入、lake-manifest.json 版本固定、多目标 lakefile 设计，以及可直接套用的 GitHub Actions CI 配置。 lean-toolchain：锁定工具链版本 项目根目录的 lean-toolchain 是一行纯文本文件，内容就是 toolchain 字符串： 1leanprover/lean4:v4.12.0 elan 读取该文件，自动下载并激活对应版本的 lean 与 lake。项目目录内的所有 lake 命令都在该 toolchain 下执行，与机器全局版本无关。 版本字符串的两种合法格式： 格式 示例 说明 正式 release leanprover/lean4:v4.12.0 推荐生产项目使用 nightly leanprover/lean4:nigh...
Coding Agent 领域的 Graph Engineering——当图工程遇上智能体编排
图工程有两重含义。《深入图工程》讨论的是以图数据为中心的系统工程——图数据库、图计算引擎、知识图谱。本文讨论第二重：当 Coding Agent 系统本身成为一个图结构的工程制品时，传统图工程的哪些原理可以复用，哪些问题是全新的。 2024-2026 年间，Agent 系统从"一个 LLM 调用 + 几个工具"扩展到多步骤、多角色和可恢复执行。LangGraph 直接使用状态图；CrewAI 以 agents、tasks、crews 和 flows 为主要抽象；AutoGen 同时提供 conversation、team 与实验性的 GraphFlow。图适合作为统一分析视角，但不能把不同框架都改写成同一种图调度器。 Agent 系统中的三类图结构 Agent 系统至少包含三类不同性质的图，它们在生命周期、变化频率和工程约束上各不相同： 执行图（Execution Graph）：Agent 单次任务执行的控制流。每个节点是一个计算步骤（LLM 调用、工具执行、条件判断），边表示控制转移。LangGraph 的 StateGraph 是这一类的典型代表。执行图在...
深入 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...
