深入 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...
深入 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 序列最终构造出了什么样的证明...
