写 Isabelle/HOL 的时候最难受的往往不是第一遍证明而是半年后改了一个 datatype 定义、一个递归函数签名结果理论文件里几十条 lemma 集体标红。这种“代码还是原来的意图证明却全部失效”的情况在证明工程里有一个专门的名字Proof Repair。CAPRI 这条技术路线正是围绕 Isabelle 中的 Proof Repair 展开的。它的名字可以拆成两个关键词Contract-Aware意思是感知契约Proof Repair意思是证明修复。这篇文章不打算只堆概念而是把问题背景、CAPRI 的设计思路以及 Isabelle 中“契约感知式修复”的落地方案一起拆开来讲。如果你正在学习 Isabelle/HOL或者维护一个体量不断增长的.thy理论文件又或者对程序验证、证明自动化方向感兴趣这篇文章可以帮助你建立一条清晰的问题分析路径。读完你会知道Isabelle 中 Proof Repair 到底在修什么“契约感知”和普通修复有什么区别如何复现一个典型的证明失效场景手工完成一次 Contract-Aware 风格修复需要哪些步骤在真实工程里如何减少 proof breakage。1. 从一个常见的 Isabelle 维护场景说起1.1 什么是 Proof Repair先看一个非常常见的现象。你在一个理论文件里定义了一个表达式类型theory ExpExample imports Main begin datatype exp N nat | Plus exp exp fun val_of :: exp ⇒ nat where val_of (N n) n | val_of (Plus e1 e2) val_of e1 val_of e2 lemma val_of_nonneg: fixes e :: exp shows 0 ≤ val_of e proof (induction e) case (N n) then show ?case by simp next case (Plus e1 e2) then show ?case by (simp add: Plus.IH) qed end这个理论文件可以正常编译lemma 也证明完毕。后来需求变化表达式语言里要增加一个“减法”节点。你修改了定义datatype exp N nat | Plus exp exp | SubExp exp exp fun val_of :: exp ⇒ nat where val_of (N n) n | val_of (Plus e1 e2) val_of e1 val_of e2 | val_of (SubExp e1 e2) val_of e1 - val_of e2此时重新执行isabelle build原来的证明脚本就出问题了。这里的关键是val_of_nonneg这条 lemma 在新定义下依然成立因为自然数减法结果仍然是自然数。证明失效不是因为命题变了而是因为induction e生成的子目标从一个N分支、一个Plus分支变成了三个分支。手工写的 proof script 没有覆盖新的SubExp分支于是 Isabelle 在证明的第某个步骤开始报错。这种场景就是 Proof Repair当理论定义发生变化后原本可以编译通过的证明脚本无法继续通过需要自动或半自动地修复这些证明脚本使其与新定义保持一致。Proof Repair 不等同于“重新证明”。重新证明是完全丢弃旧 proof script从零开始Proof Repair 则希望尽可能保留原有证明的结构只做最小改动。1.2 为什么 Isabelle 的证明这么容易失效很多人第一次接触 Isabelle 时会觉得既然定理本身没有变为什么改一个函数定义就会导致一堆证明失效这背后的原因主要有三层。第一Isabelle 的证明脚本不只是“执行过程记录”它依赖于大量内部生成的规则例如exp.induct、val_of.simps、exp.distinct。一旦 datatype 增加构造器这些规则会全部重建。原来只针对两个构造器的 proof script自然难以处理三构造器的结构归纳。第二auto、simp、blast这类自动化方法虽然省力但它们的行为依赖当前理论文件里的 simp set 和默认规则集。定义变化后可用的 simp 规则变化了证明路径也会变化。也就是说即使定理保持正确自动化策略可能仍然走不通。第三一个大型.thy文件内部存在大量隐式依赖。lemma A使用了lemma B而lemma B的证明方式又依赖某个定义展开。修改底层定义之后依赖链上的任何一环发生改变都会向下传递。这就让 Proof Repair 不再是一个“要不要做”的问题而是一个“如何高效做”的问题。2. 什么是 CAPRIContract-Aware 到底在强调什么2.1 先理解“契约”在 Isabelle 里的含义Contract-Aware 中的 Contract指的并不是传统意义上的“软件接口文档”而是 Isabelle 理论中能被机器理解的约束关系。在 Isabelle/HOL 中契约至少可以体现在三个层面函数类型层面val_of :: exp ⇒ nat已经约束了输入和输出类型超过类型约束的表达式根本无法构造出来。定理假设层面locale里的assumes或者 lemma 中的assumes ... shows ...表达的是“只有在某些前置条件下某个结论才成立”。定义语义层面fun、function、inductive等命令本身会产生定义公理它们的定义内容是更深层的语义契约。举一个更具体的例子。假设你在验证一个小型解释器关于eval的定理通常会写成lemma eval_total: fixes e :: exp assumes well_typed e shows ∃ v. eval e Some v这里well_typed e就是前置契约∃ v. eval e Some v是输出契约。在维护证明的过程中这条定理其实就是一个完整的接口约定。任何人想重构eval的实现都必须保证这条约定不被破坏。CAPRI 的思路正是利用这些已有契约来指导证明修复。2.2 普通 Proof Repair 与 Contract-Aware Proof Repair 的区别普通的 Proof Repair 可以这样理解发现 proof script 失败尝试通过局部替换、增加方法参数、调用自动化证明策略把失败的地方修好。它更关注“怎么让 Isabelle 停止报错”。Contract-Aware Proof Repair 则会多问一层这个被破坏的 proof script 原本在证明什么契约修复后的证明是否仍然忠于这个契约这个区别在复杂重构中非常重要。假设一个定义从“总是成功”的求值函数改成了“返回option类型”的求值函数。旧定理是lemma eval_add: eval (Plus e1 e2) eval e1 eval e2新定义下旧定理的类型已经不匹配不可能直接修。此时简单的方法替换已经失效必须根据新函数的类型契约把旧定理改写为lemma eval_add_some: assumes eval e1 Some a assumes eval e2 Some b shows eval (Plus e1 e2) Some (a b)CAPRI 的修复不会只盯着 proof script 本身而是会把assumes、shows、函数签名、定义式内容作为约束确认“补丁是否满足契约”。一句话概括Contract-Aware 的 Proof Repair是在修复证明的同时始终把理论中的契约作为第一公民来检查。2.3 CAPRI 的输入与输出是什么从研究原型的角度CAPRI 这类系统通常以如下方式工作。输入部分包括一个修改后的 Isabelle 理论文件修改前的理论文件或者版本差异Isabelle 编译失败时的错误信息现有理论中可复用的定义、定理和契约。输出部分则包括一个新的 proof script 片段可以应用到原理论文件的 patch修复后的验证结果。需要注意的是CAPRI 并不是类似sledgehammer那样你在 Isabelle/jEdit 里点一个按钮就能直接使用的工具。它更像一条“方法路线”。公开资料中较少给出一个统一安装命令因此本文在讲解时会保留 CAPRI 的契约感知思想同时给出你可以在 Isabelle 中实际操作的修复流程。3. 环境准备与最小验证工程3.1 Isabelle 环境说明在继续后面的示例之前先确认你有可运行的 Isabelle 环境。如果你的电脑是 Linux 或 Windows可以到 Isabelle 官网下载对应安装包。macOS 也可以使用官方安装包。安装完成后命令行里一般会有isabelle命令或者你可以使用 Isabelle 自带图形界面的 jEdit。版本方面不需要和本文完全一致。Isabelle 的 datatype、fun、locale 等核心语法相对稳定但不同版本对某些策略和自动生成规则名称可能有差异。建议先在一个独立 session 中测试不要直接修改正在维护的大文件。你可以在终端执行isabelle version如果能看到版本号说明命令可以正常使用。3.2 创建一个最小 sessionIsabelle 项目通常通过 ROOT 文件描述 session 依赖。我们新建一个目录结构proof-repair-demo/ ├── ROOT └── BrokenProof.thyROOT 文件内容如下session ProofRepairDemo HOL theories BrokenProofBrokenProof.thy 可以先放一个最简单的理论theory BrokenProof imports Main begin datatype exp N nat | Plus exp exp fun val_of :: exp ⇒ nat where val_of (N n) n | val_of (Plus e1 e2) val_of e1 val_of e2 end在项目根目录执行isabelle build -D .如果没有报错说明工程建立成功。4. 契约感知的 Proof Repair 工作流在 Isabelle 中做一次契约感知的证明修复并不是直接无脑删掉旧证明然后让auto去猜。更建议按照下面的流程执行。4.1 阶段一定位失败点先让 Isabelle 编译整个理论文件得到失败位置。常见失败信息包括Failed to apply initial proof methodFailed to finish proofUndefined factWrong number of subgoals不要把错误信息当噪声第一件事是把失败点附近的定义变更、定理声明和证明脚本对照起来看。在这个阶段我们要问自己一个问题这个 lemma 的契约在新定义下还成立吗如果契约已经不再成立那么修复手段不是改证明而是改定理或改定义。如果契约仍然成立才进入下一步。4.2 阶段二抽取契约差异把失败证明对应的定理、以及它依赖的 definition 变化列出来。以最开始增加的SubExp构造器为例。需要检查的契约包括val_of的类型是否仍然能覆盖新构造器新增构造器是否改变induction e的归纳分支val_of_nonneg作为一条关于val_of输出的契约是否在SubExp分支下仍然成立。这一步的目标是从语义上判断是否存在“真命题但没有对应 proof”的情况。如果新分支下命题为假修复方向就不是补 proof而是修正定义或增加约束条件。4.3 阶段三生成候选补丁Isabelle 生态中已经有不少工具可以帮助生成候选证明try0自动尝试多种常用方法组合sledgehammer调用外部 ATP 搜索证明find_theorems查找可用定理手动补充分支 case。比如对于新增的SubExp分支可以在 jEdit 中先尝试lemma val_of_nonneg_fixed: fixes e :: exp shows 0 ≤ val_of e apply (induction e) apply auto done如果auto能直接跑通说明证明可以自动化完成如果还差一点就要手工补上缺失分支。4.4 阶段四用契约守卫补丁这是 CAPRI 和普通修复最大的差异点。找到一个候选 patch 之后不要立刻全部应用。要反向检查修复后的 lemma 是否保留了原定理的assumes和shows修复是否把原来的“全称成立”悄悄改成了“某些条件下成立”修复过程中是否引入了新的未定义函数或者放宽了某个类型约束这些检查听起来琐碎但在大型形式化工程里极其重要。很多时候快速修好一个 proof 后过几天才发现定理强度变弱了导致更上层的证明全部白做。5. 实战手工完成一次 Contract-Aware 修复5.1 原始理论文件我们先准备一个规范的原始文件。theory BrokenProof imports Main begin datatype exp N nat | Plus exp exp fun val_of :: exp ⇒ nat where val_of (N n) n | val_of (Plus e1 e2) val_of e1 val_of e2 lemma val_of_nonneg: fixes e :: exp shows 0 ≤ val_of e proof (induction e) case (N n) then show ?case by simp next case (Plus e1 e2) then show ?case by (simp add: Plus.IH) qed end这里的契约非常直白val_of总是产出非负自然数。证明采用结构归纳法两个构造器分别处理。5.2 修改定义并触发失败现在在datatype中增加SubExp构造器同时为val_of增加对应子句。datatype exp N nat | Plus exp exp | SubExp exp exp fun val_of :: exp ⇒ nat where val_of (N n) n | val_of (Plus e1 e2) val_of e1 val_of e2 | val_of (SubExp e1 e2) val_of e1 - val_of e2此时原来的证明文件没有改动。重新运行isabelle build -D .你会看到证明在qed附近失败。原因是归纳法现在产生三个子目标但证明脚本只覆盖了N和Plus两个分支。这不是一个逻辑错误而是 proof script 与新定义不同步。原来的契约“0 ≤ val_of e”在新定义下依然成立。5.3 分析契约与修复方向修复之前我们先做一个 Contract-Aware 检查。类型契约val_of :: exp ⇒ nat新增构造器没有改变函数输出类型。定义变更val_of (SubExp e1 e2) val_of e1 - val_of e2这里val_of e1和val_of e2都是自然数自然数减法的结果也永远是非负自然数。命题契约0 ≤ val_of e没有因为SubExp而失效。因此这是一个确定可以修复的场景。修复方式是在归纳中补充SubExp分支。修复后的证明如下lemma val_of_nonneg_repared: fixes e :: exp shows 0 ≤ val_of e proof (induction e) case (N n) then show ?case by simp next case (Plus e1 e2) then show ?case by (simp add: Plus.IH) next case (SubExp e1 e2) then show ?case by simp qed如果从 patch 的角度看改动可以理解为--- a/BrokenProof.thy b/BrokenProof.thy val_of 定义 val_of (Plus e1 e2) val_of e1 val_of e2 val_of (SubExp e1 e2) val_of e1 - val_of e2 val_of_nonneg 证明 next case (Plus e1 e2) then show ?case by (simp add: Plus.IH) next case (SubExp e1 e2) then show ?case by simp qed5.4 验证修复结果在 jEdit 中把光标放到 lemmas 上或者重新执行isabelle build -D .如果编译通过说明修复成功。这个示例虽然简单但已经很能说明 CAPRI 的核心思路修复时不是把证明全部推翻而是先判断契约是否仍然成立再针对失败的位置补充最小证明。真实的 Isabelle 理论文件会比这个复杂得多比如SubExp分支可能依赖额外的归纳假设可能需要对val_of e1、val_of e2做 case analysis可能还需要引入新的 lemma。但工作流是一致的定位失败 → 判断契约 → 生成候选证明 → 验证契约保持 → 应用最小补丁。5.5 更复杂的契约修改场景如果重构不只是“增加构造器”而是把函数的返回值改成option类型那契约本身就会变化。此时val_of_nonneg不再是一个可直接修复的 lemma因为它已经无法表达“Some v中的v满足0 ≤ v”。你需要做的其实是更新契约fun val_of_option :: exp ⇒ nat option where val_of_option (N n) Some n | val_of_option (Plus e1 e2) (case (val_of_option e1, val_of_option e2) of (Some a, Some b) ⇒ Some (a b) | _ ⇒ None) | val_of_option (SubExp e1 e2) (case (val_of_option e1, val_of_option e2) of (Some a, Some b) ⇒ Some (a - b) | _ ⇒ None)新定理变成lemma val_of_option_nonneg: fixes e :: exp assumes val_of_option e Some v shows 0 ≤ v using assms apply (induction e) apply (auto split: option.splits) done这种场景下CAPRI 的“契约感知”体现在它不会尝试把旧证明强行接到新函数上而是会先识别出“接口类型已经改变原契约需要被翻译成新契约”再来搜索证明。这也是为什么在实际工程里函数签名变化往往是最伤筋动骨的一类变更。6. 常见问题与排查思路6.1 证明脚本常见报错对照下面表格列出 Isabelle 维护中比较典型的报错问题现象常见原因解决思路Failed to apply initial proof methodinduction/cases 规则变化或定理引入了新条件查看 datatype/function 定义差异补充 case 或using条件Failed to finish proof某个子目标没有在当前方法下闭合用try0、sledgehammer生成候选证明或把大目标拆成多个中间 lemmaUndefined fact旧的simp定理被删除或改名检查定义变更后的定理名更新引用的 factWrong number of subgoals构造器数量增加旧证明脚本没有补齐 case按结构归纳增加新分支Type unification failed函数签名发生变化旧 lemma 无法匹配先修正 lemma 的契约再修证明过程6.2 排查顺序建议遇到证明失效不建议直接开着sledgehammer乱试。推荐按以下顺序排查。第一先看“失败证明所在的定义是否发生了语义变化”。如果定义变化导致原定理根本不可能成立任何策略都是浪费时间。第二再看“是否只是自动化规则变化”。把失败点之前的apply逐步执行观察剩余子目标。第三使用find_theorems检查当前环境是否有可用的新定理。例如想查找与minus相关的自然数不等式定理可以写find_theorems 0 ≤ _ - _如果有关键定理手动引入再试。第四如果单一 agent 策略无法解决把目标拆小。不要追求一个大auto解决所有问题增加一个中间 lemma 往往比硬调方法参数更稳定也更容易维护。第五修复后运行完整 session确认没有影响上层文件。6.3 为什么不建议使用sorry临时跳过在 proof repair 过程中有人会为了尽快看到整体编译结果而使用sorry占位。lemma val_of_nonneg: fixes e :: exp shows 0 ≤ val_of e sorrysorry会告诉 Isabelle 暂时接受这个证明但代价很大。因为它会绕过一致性检查把你当前理论变成一个可能存在逻辑漏洞的理论。在依赖链下面的所有证明都可能建立在一个未经验证的事实上后续排查问题会变得极其困难。如果确实需要临时标记未完成状态建议使用oops它表示“这个证明还没有完成”不会污染最终理论。7. Proof Repair 的工程化建议7.1 把定理声明当作 API 来维护在传统软件开发中我们不会随意修改对外接口而不通知调用方。Isabelle 理论也应该一样。每个有一定复杂度的 lemma都应该被视为当前理论层对外提供的 API。定义变更之前先列出受影响的 lemma 清单。这样可以显著减少“改了一处定义结果不知道哪里会挂”的焦虑。例如