深入 Lean 04：核心 tactic 精讲
Lean 4 的 tactic mode 把证明分解成一系列目标变换步骤。每条 tactic 接收当前的目标状态（一组待证的 ⊢ 句），修改它，产生零个或多个新目标。当所有目标消除完毕，证明关闭。七条核心 tactic——intro、apply、exact、constructor、cases、induction、simp——覆盖了命题逻辑和结构归纳证明的绝大部分场景，各自有精确的语义模型和目标变换规则。 前置阅读：本系列 01 Lake 项目结构与依赖管理、02 Term-mode 与 Tactic-mode 切换心法、03 Universe 与类型层级实战；形式化方法系列 在 Lean 4 中证明经典命题。 intro 语义模型 intro h 处理目标形如 ⊢ A → B 或 ⊢ ∀ x, P x 的情形。它把 goal 的前件或全称绑定变量从目标中移走，引入上下文成为假设，同时把目标替换为后件或实例化的命题。 123456引入前：⊢ A → B执行 intro h 后：h : A⊢ B ∀ 的情形： 123456引入前：⊢ ∀ (n : Nat), n + 0 = n执行...
深入 Lean 03：Universe 与类型层级实战
Lean 4 的类型系统里有一个经常被初学者忽视的维度：每个类型本身也有类型，类型的类型称为 universe（宇宙）。忽视这一维度，往往导致一类难以直觉理解的报错——类型不匹配、universe 不一致、无法做大消除。本篇聚焦 universe 层级的实际操作，包括 Prop 与 Type u 的区别、universe 多态定义、以及常见 universe 错误的诊断方法。 前置阅读：本系列 01 Lake 项目结构与依赖管理 和 02 Term-mode 与 Tactic-mode 的切换心法；形式化方法系列 准备 Lean 4 实验环境。 Universe 层级 Lean 4 的类型层级是一个无穷塔（infinite tower），用 Sort 统一表示： 1Sort 0 : Sort 1 : Sort 2 : Sort 3 : ... Prop 是 Sort 0 的别名，Type 是 Type 0 = Sort 1 的别名，Type 1 是 Sort 2，以此类推。 12345#check Prop -- Prop : Type#check Type ...
深入 Lean 02：Term-mode 与 Tactic-mode 切换心法
Lean 4 提供两种写证明的语法面：term mode 直接给出构造该类型的项；tactic mode 通过一系列指令逐步缩减未完成的目标。两者在语义上等价——任何 tactic 证明最终都被 elaboration 翻译成一个 term，类型检查器只检查 term 层。选择哪种写法是风格决策，但这个决策在实践中有明确的倾向规则。 本篇是"深入 Lean"系列第 02 篇。系列前置知识见《在 Lean 4 中证明经典命题》，该篇已展示了两种模式的基本对照；本篇专注于切换判断本身：什么情况下 term mode 更短、更清晰，什么情况下 tactic mode 更易读、更可维护，以及两种模式如何在同一个证明里混合使用。 Term mode 基础 Term mode 把证明写成一个表达式，该表达式的类型就是命题。Lean 4 的类型论里，命题是类型，证明是居民（inhabitant），“证明成立"等价于"该类型有居民”。 fun、⟨⟩、点投影 12345678-- 蕴含：函数抽象theorem impl_intro (A B : Prop)...
深入 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 项翻译成目...
