深入 Coq 08：Ltac2 与现代 tactic 编程
Ltac 解决了"把 tactic 序列抽象成可复用脚本"的问题，但它是一门无类型的动态语言——变量绑定在运行时才解析，错误在 backtracking 时悄悄吞掉，定义期不做任何静态检查。Ltac2 是 Coq 8.11 起随发行版分发的替代方案（此前是独立插件），把 tactic 编程从"解释型脚本"升级为"有类型的函数式语言"。本篇是系列第 08 篇，前置阅读建议先过一遍《深入 Coq 02：目标窗口与 tactic 交互模型》和第 07 篇（Ltac 编程：match goal/repeat/try/first/solve）。 Ltac 的动态类型问题 Ltac 的 match goal 子句在运行时匹配当前目标，成功的子句继续执行，失败的子句触发 backtracking 退到上一个选择点。这套设计对于简单的"try 一批 tactic，哪个行用哪个"场景相当便利，但有几类问题在复杂 tactic 里难以调试。 变量绑定完全动态是其中一个根本问题。Ltac 里的 ?x 是 pattern ...
深入 Coq 07：Ltac 编程
Ltac 是 Coq 内置的 tactic 脚本语言，负责将零散的交互式证明步骤组合成可复用的自动化脚本。与 Gallina 的静态类型系统不同，Ltac 是动态类型的：tactic 表达式在运行时对当前证明状态求值，失败时会触发回溯，而非编译期报错。这一特性既带来了灵活性，也引入了难以诊断的错误行为。本篇覆盖 match goal、repeat、try、first、solve、idtac、fail 的语义，以及如何用 Ltac 关键字定义可复用的 tactic 组合子。前置阅读：本系列《基础 tactic 全景》和《搜索与自动化》；理论背景见形式化方法系列《依值类型——从命题逻辑到一阶逻辑》。 Ltac 的位置与定位 Coq 的证明引擎分三层：内核（kernel）验证证明项（proof term）的类型正确性；精化引擎（elaboration engine）把 tactic 序列翻译成证明项；Ltac 是在精化引擎之上运行的元语言，负责描述"如何生成 tactic 序列"。 Ltac 表达式的求值结果是一个 tactic 或一段证明片段。因为 Ltac 不...
深入 Coq 06：SSReflect 风格
SSReflect 是 Coq 的一个 tactic 语言扩展，由 Georges Gonthier 等人在形式化四色定理期间开发，后来成为 Mathematical Components（MathComp）库的基础 tactic 层。Coq 8.7 起，SSReflect 被收入标准发行版，无需额外安装。本篇在前序文章（01 开发环境、02 目标窗口、04 基础 tactic、05 搜索与自动化）的基础上，系统介绍 SSReflect 的设计哲学与核心 tactic。 MathComp 选择 SSReflect 的原因 原生 Coq tactic（intro、destruct、induction 等）在小规模证明中已经够用，但在大型数学库的维护场景下暴露出几个结构性问题。 第一，上下文管理成本高。intro 引入假设后，名字由用户手动管理；destruct 和 induction 在分支众多时很容易导致名字污染，同一个局部变量在不同分支有不同含义，证明脚本难以阅读。 第二，命题（Prop）和布尔函数（bool）之间缺乏统一的转换机制。Coq 标准库里存在大量 Prop 形式的...
深入 Coq 05：搜索与自动化
Coq 的自动化 tactic 不是万能的黑盒，而是针对特定目标形状设计的搜索算法。auto 和 eauto 在 hint 数据库上做反向链推导；lia 在线性整数/自然数算术上调用决策程序；ring 和 field 把多项式等式规约到规范形式再比较。了解每个 tactic 的适用边界，才能在恰当的地方放手让机器搜，而不是在它注定失败的地方反复重试。前置阅读：《深入 Coq 02：目标窗口与 tactic 交互模型》和《深入 Coq 03：Gallina 核心语法速查》。 auto 与 hint 数据库 auto 的核心机制是反向链推导（backward chaining）：从当前 goal 出发，匹配 hint 数据库中的引理头部，将 goal 替换为引理的前提，递归直到所有 subgoal 都被 assumption 或 reflexivity 关闭，或达到搜索深度上限（默认 5）。 1234Goal forall (P Q R : Prop), P -> (P -> Q) -> (Q -> R) -> R.Proof. auto.Qed. ...
深入 Coq 04：基础 tactic 全景
本系列前三篇分别处理了开发环境（01）、目标窗口与证明状态机（02）、Gallina 核心语法（03）。有了这些基础，证明编写的核心工具就是 tactic。Coq 的 tactic 语言（称为 Ltac）本质上是一套操作证明状态的指令集，每条 tactic 执行后，目标列表发生确定性的转移。本篇覆盖最常用的六条 tactic：intro、apply、exact、rewrite、destruct、induction。 tactic 的语义模型 在 Coq 的 Curry-Howard 对应下，每个证明目标 ⊢ T 等价于构造一个类型为 T 的项。tactic 是"构造证明项"这个任务的分解策略：intro 对应 λ 抽象，apply 对应函数应用，exact 对应直接给出项，rewrite 对应等式替换，destruct 对应模式匹配，induction 对应递归定义。 理解这个对应关系有助于预判 tactic 的行为。每条 tactic 执行后，目标要么减少（一个目标被完成或被拆分），要么上下文增加新的假设。若想看 tactic 序列最终构造出了什么样的证明...
深入 Coq 03：Gallina 核心语法速查
Gallina 是 Coq 的规范语言（specification language），负责定义类型、函数和命题；tactic 语言（Ltac/Ltac2）只是证明搜索的外壳，最终生成的证明项本质上仍是 Gallina 表达式。本篇是一张速查表，覆盖 Definition、Fixpoint、Inductive、Record、Section、Module 六个核心构造，以及模式匹配、匿名函数、隐式参数的基本用法，目标是让读者能独立写出完整的 .v 文件并通过 coqc 零 warning 编译。前置阅读：形式化方法系列《归纳类型与递归——把数据嵌入证明》和《依值类型——从命题逻辑到一阶逻辑》。 Definition Definition 引入一个全局名称，绑定到一个 Gallina 表达式。类型标注可选；省略时 Coq 从右侧推断。 12345678(* 带类型标注 *)Definition double : nat -> nat := fun n => n + n.(* 省略类型标注，Coq 推断 *)Definition triple n := n + n + n...
深入 Coq 02：目标窗口与 tactic 交互模型
Coq 的证明过程不是一次性写出完整的证明项，而是通过 tactic 序列逐步缩减待完成的工作。每执行一条 tactic，Coq 会更新"当前需要证明的内容"，直到不再有任何待证目标，Qed 才能通过。这个状态驱动的交互过程有一个专用的视图——目标窗口（goal window）。 证明状态机 每个 Proof. 之后，Coq 内部维护一个证明状态（proof state），其结构是一个目标列表，每个目标由两部分组成： 123context (上下文 / 假设区)━━━━━━━━━━━━━━━━━━━━━━━━━━goal (当前要证明的命题) 在 CoqIDE 或 VS Code vscoq2 插件里，这个结构对应右侧的 Goals 面板。在 Proof General (Emacs) 里，它出现在 *goals* 缓冲区。在命令行 coqtop 里，每执行完一条 tactic 后，Coq 打印出更新后的状态。 分隔符 ============================ 是可视化的 ⊢ 符号。分隔符上方是已知假设，下方是当前目标。 一个典型的中间状态（...
深入 Coq 01：开发环境与项目结构
「形式化方法」系列的 14 篇文章建立了 Curry-Howard 同构、依值类型、归纳类型与 Lean 4 入门的理论底座。本系列从工具链入手，目标是让读者能独立用 Coq 完成 200 行以内的证明项目。本篇处理的问题只有一个：从零搭建一套可重复、可在 CI 上运行的 Coq 开发环境。 opam switch 管理 Coq 的工具链通过 opam 管理，opam 是 OCaml 生态的包管理器。Coq 8.20 要求 OCaml ≥ 4.09（coq-core.opam 里写的是 "ocaml" {>= "4.09.0"}），4.x 系列官方测试到 4.14.1，OCaml 5.x 支持仍标注为实验性——所以下面固定用 4.14.2。不同项目可能需要不同的 Coq 版本，因此每个项目建议使用独立的 opam switch。 本系列锚定 Coq 8.20，因为它是存量项目的公共分母。但要先说清一件事：Coq 在 8.20 之后更名为 Rocq，现在 opam install coq 装到的可能是 9.x 的兼容层。9.0 起标准...
图工程综述——大规模图计算引擎与框架全览
大规模图计算是互联网基础设施的重要组成部分。社交网络中的好友关系、金融风控中的资金流转链路、供应链中的货品追溯，本质上都是图结构问题。本文专注计算范式、批量与增量引擎、规模化算法和基准测试；图数据库、知识图谱与 GNN 的全链路地图见《深入图工程》，Agent 编排中的图模型则由《Coding Agent 领域的 Graph Engineering》展开。 图计算范式 Pregel 与 BSP 模型 2010 年，Google 在 SIGMOD 发表 Pregel 论文，确立了大规模图计算中影响深远的"以顶点为中心"（vertex-centric）编程抽象。开发者实现单个顶点的计算逻辑，系统负责分区、消息传递和全局协调。 执行单元是超步（superstep）：所有活跃顶点先并行执行用户定义的 compute() 函数，顶点通过消息向邻居传递结果，消息在超步间缓冲；当前超步内所有顶点计算完毕后进行全局屏障同步，再进入下一超步。 这是 Leslie G. Valiant 在 1990 年提出的 BSP（Bulk Synchronous Parallel）模型在图...
深入图工程
图（Graph）作为数据结构，在计算机科学里存在了半个多世纪。“图工程”（Graph Engineering）并不是边界明确的正式学科名称，本文把它作为一个工作定义：围绕图的建模、存储、查询、计算、学习、运维与验证形成的系统工程。图规模、消费者和时效性要求扩大之后，这些原本分散的工作需要放进同一套方法中讨论。 图工程的学科定位 图工程在本文中承载两层含义。第一层是以图数据为中心的系统工程，涵盖建模、存储、查询、计算和学习全链路。第二层来自 AI Agent 领域：有些框架直接采用有向状态图，有些采用 crew、conversation、handoff 或普通工作流抽象；"图"是分析这些编排关系的统一视角，但并非每个框架的字面核心。两层含义的交叉点是 Agent 以知识图谱或代码图作为上下文源。计算引擎的细节见《图工程综述》，Agent 编排的边界见《Coding Agent 领域的 Graph Engineering》。 与传统数据工程的关键分野在于： 分区目标通常难以精确求解。关系型数据常按主键 hash 或 range 分片；图分区需要同时考虑负载、割边...
