在 Isabelle/HOL 里维护形式化项目，真正的分水岭往往不是第一次把这个定理证完，而是几周之后你修改了一个函数定义或一条规范约束，然后启动构建的那一瞬间。
旧证明可能不是“逻辑错了”，而是它依赖的规范变了。比如你原来约定了mset (sort xs) = mset xs，后来想把接口改成去重语义mset (sort xs) ≤# mset xs，那么所有依赖“排序后长度不变”的定理都会变红。Isabelle 只会诚实地告诉你 proof failed，却不会告诉你这条旧证明应该怎么修，哪些结论还可以保留，哪些必须重写。
CAPRI 的全称是 Contract-Aware Proof Repair for Isabelle，也就是“契约感知的 Isabelle 证明修复”。从命名和同类工作路线看，它要解决的不是“从零开始写证明”，而是“当规范发生变化之后，如何让旧证明尽量复用、局部修补、最小化返工”。这篇文章想把 CAPRI 这类证明修复思路背后的概念讲清楚，并且用 Isabelle/HOL 的最小工程示例，带你在本地复现一次从“规范变更引发证明失效”到“基于契约差异完成修复”的完整过程。
无论你是在研究证明修复工具，还是只是在 Isabelle 里维护一个几千行 theory 的验证项目，下面的内容都有可操作的参考价值。
1. 这篇文章真正要解决的问题
先说说读者可能经历过的痛感。
假设你维护一个排序算法的验证项目。函数本身不复杂，但关于它的引理可能有几十条。某一天产品需求变了：原来接口保持“排序结果与输入是同一个多重集合”，现在允许排序后自动去重。这个改动从头到尾只改了核心定义的一行，但接下来你会看到一串连锁失败。
这背后的原因在于，形式化证明不是写的“一次性结论”，而是长在规范和定义上的“依赖网络”。你改了上层接口的契约，却没有同步更新下游引理，证明自然就断裂了。
CAPRI 这类系统瞄准的正是这个场景：从旧契约和新契约之间的差异入手，判断哪些 proof step 仍然成立，哪些需要换引理，哪些应该删掉重来。它并不是要替代 Isabelle 内核去证明任意命题，而是让“proof repair”这件事有更强的语义指引。
关于 CAPRI 本身，目前公开材料并不算多。因此这篇文章不会假装它是一个开箱即用的 CLI，而是更侧重讲清楚它背后那套可复用的方法论。读完你应该能回答三个问题：
- Isabelle 的 proof repair 为什么难？
- Contract-aware 与传统“拿 Sledgehammer 重新试一遍”有什么本质区别？
- 如果不用 CAPRI 这个具体工具，你在自己的 Isabelle 项目里能怎么应用这套思路？
2. Isabelle/HOL 基础概念与核心原理
2.1 Isabelle/HOL：定理证明器与形式化项目的“编译环境”
Isabelle/HOL 是 Isabelle 之上最常用的对象逻辑，属于交互式定理证明器（proof assistant）。你写的.thy文件由 Isabelle 内核校验，而不是像普通程序那样交给操作系统执行。
一个典型的 theory 文件通常由三部分组成：
- 导入依赖，例如
Main、HOL-Library.Multiset。 - 类型、函数和归纳定义。
- lemma/theorem/corollary，以及对应的证明脚本。
Isabelle 的校验模式可以理解成一种更严格的“类型检查”：如果证明脚本无法让内核确认命题为真，构建就会失败。这就使得形式化项目的修改成本很高，但也让结果可信度远超普通测试。
2.2 证明修复（Proof Repair）到底在修什么
Proof repair 并不是一个新的概念。在软件工程领域，测试用例坏了你去改测试；在形式化验证领域，证明脚本坏了你去改证明。但 Isabelle 的 proof repair 有一个特殊性：旧证明的对错，取决于它所在的 theory 上下文。
比如下面这种变化就很典型：
- 函数返回值从保持所有元素，变成允许过滤元素。
- lemma 结论本身还写着
length (sort xs) = length xs。 - 旧证明中的
simp、auto、sledgehammer无法继续找到路径。
这种情况下，仅仅说“重新跑一下自动证明”通常解决不了问题。因为命题本身在新规范下不再为真，你要做的不是修补证明，而是调整命题。CAPRI 思路的关键点就在这里：它把规范中的约束看成 contract，用 contract 的差异来判断一个旧证明的结论是否仍然语义可导。
2.3 Isabelle 里如何表达 contract
Contract 在程序语言里通常指接口的前置条件、后置条件、数据不变量。在 Isabelle/HOL 中，并没有一个强制叫 “contract” 的语言构造，但我们常用locale把一组假设集中表达出来。
看下面这个最小例子：
theory SpecChangeDemo imports Main begin locale length_preserving_contract = fixes f :: "'a list ⇒ 'a list" assumes length_eq: "length (f xs) = length xs" begin lemma nonempty_image: assumes "xs ≠ []" shows "f xs ≠ []" using length_eq[of xs] assms by (metis length_0_conv) end end在这个locale中：
f是一个抽象函数，不指定实现，只声明它满足某个契约。length_eq说明f不会改变列表长度。nonempty_image是从这个契约推导出的一个定理。
写实际项目时，我们会把复杂的算法定义成一个具体函数，然后把它的关键性质写成一组 lemma 集合。但对于 CAPRI 这类证明修复工具来说，真正重要的是“函数应该满足什么”，而不是“函数怎么实现”。所以用locale隔离契约，反而能更清晰地表达修复目标。
2.4 规范变更为什么会引发证明失败
变化类型不同，修复难度完全不同。下面这张表可以帮助判断你到底遇到了哪一类失败：
| 变化类型 | 典型描述 | 对证明的影响 |
|---|---|---|
| 函数签名变化 | 类型从'a list ⇒ 'a list变成nat list ⇒ nat list | 类型错误先暴露，修复相对机械 |
| 前置约束加强 | 要求输入更严格 | 函数调用点和新契约会冲突，依赖旧结论的证明可能失效 |
| 后置约束放宽 | 输出的保证变弱 | 下游引理不能再依赖旧结论，需要降低目标或补充分支 |
| 定义语义重写 | 同一接口但内部实现不同 | 旧证明可能在归纳或展开时卡住，需要重新理解递归结构 |
| 类型结构变化 | 递归数据类型加了构造子 | 几乎所有归纳证明都要处理新的构造子分支 |
CAPRI 的“契约感知”，本质上就是先回答“这次变更属于哪一类、哪些原子约束发生了增减、量化结构怎么变”，然后再决定 proof repair 的策略。
3. 契约感知修复的核心理念
3.1 Contract-Aware 不只是“看到报错再修”
传统做法通常是：某个 lemma 红了，你光标移上去，先apply auto试一试，不行就sledgehammer，再不行就打开 PDF 或打印 proof state 慢慢猜。这种方式在小项目里够用，但在大型验证项目里效率很低，因为你看不到失败证明与旧契约之间的结构关系。
CAPRI 的命名里出现了 Contract-Aware，说明它的核心判断依据不是证明脚本本身，而是契约。
可以把旧规范看成一份“接口文档”，新规范是它的修订版。旧证明之所以会坏，不是因为它不符合 Isabelle 语法，而是因为它依赖了已被修改或删除的契约条款。因此，修复时必须先回答：
- 旧证明依赖了哪些前提或结论？
- 新契约保留了哪一部分？
- 新契约是否新增了可以支撑原目标的条件？
- 原目标是被弱化、加强，还是与新契约冲突？
当你把这些问题结构化之后，修复就从“对着红色 error 试策略”变成了“先对比 contract diff，再选择局部补丁”。
3.2 一个直观示例：从“长度不变”到“长度可能变小”
再看第二节的locale。现在假设你决定把f的契约从“保持长度”改成“长度不超过输入”。这听起来只是放宽了约束，但原来的定理nonempty_image就失效了。
我用下面这段示意代码表达：在新契约shrinking_contract中，同样想证明非空输入的输出非空，已经无法从length_le推出。
locale shrinking_contract = fixes f :: "'a list ⇒ 'a list" assumes length_le: "length (f xs) ≤ length xs" begin (* 旧定理的结论在新契约下不一定成立 *) lemma nonempty_image_not_provable: assumes "xs ≠ []" shows "f xs ≠ []" oops end这里的oops表示“放弃当前证明尝试”。上面的引理并不是不能被自动证明，而是在当前这个契约下，它的结论本来就不成立。如果f可以丢弃元素，那么即使输入非空，输出也可能为空。
这正是很多开发者在 Isabelle 项目里会遇到的情况：你以为是“证明技术不够”，实际上问题是“命题目标已经超过了新契约能给出的保证”。如果不懂这个道理，你会想用更强的证明策略去硬证一个在语义上为假的命题，注定浪费时间。
继续往下想，新的契约下你要么改写结论，比如：
locale bounded_shrinking_contract = fixes f :: "'a list ⇒ 'a list" assumes length_le: "length (f xs) ≤ length xs" and keep_nonempty: "xs ≠ [] ⟹ f xs ≠ []" begin lemma nonempty_image_repaired: assumes "xs ≠ []" shows "f xs ≠ []" using assms keep_nonempty by blast end这个例子说明 contract-aware 修复会给你两条路线：
- 如果你仍然需要
f xs ≠ []，那就应该把这条约束加强到新契约中。 2
