深入 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...
深入 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 起标准...
