企业官网建设流程全解析

在 Isabelle 工程项目里待过一段时间的人，大概都经历过这样的时刻：昨天还能顺利done的证明，今天因为某个函数定义增加了一个分支、某个递归结构变了，重新跑一次却红掉大片。此时我们要面对的不是“这个证明怎么从零开始写”，而是“一个已经过期的证明，还有没有机会抢救回来”。这个问题在定理证明领域里有一个专门的名字：Proof Repair。当它前面再加上 Contract-Aware，也就是“基于合约感知的证明修复”，理解角度又会不一样。CAPRI 这个名字本身，其实把 Isabelle 开发中的一个长期痛点给点了出来：证明不是写完就结束，它会在代码与规范不断演进的过程中持续损坏，而真正昂贵的不是第一次书写证明，而是后续没完没了的修补。

这不是一篇 CAPRI 的官方使用手册，更多是基于主题本身的工程化拆解。如果你正在用 Isabelle、Coq 或其他交互式定理证明器，又经常被“代码一改、证明全红”折磨，这篇内容也许能给你一个更结构化的应对思路。

1. Proof Repair 要回答的，不是“证明怎么写”，而是“证明坏了以后怎么救”

1.1 为什么 Isabelle 里的证明会随代码变更一起“过期”

Isabelle 对正确性的验证是机器检查的。你的定理、引理、证明脚本，只要通过内核检查，就说明在当前的定义和逻辑环境下它是成立的。问题在于，这个“当前环境”不是静止的。

真实项目里，函数定义会变，数据类型会加构造子，引理签名会调整，前置条件会收紧或放宽。每一次这样的变化，都意味着所有依赖旧版本的证明，都需要重新经过内核检查。许多证明脚本看着像一段文本，但里面大量步骤其实建立在对某个递归定义具体形态的假设之上。比如auto能不能自动闭合目标，取决于函数定义的等式形状；induct能不能顺利推进，取决于归纳原则是否还覆盖新增的分支。定义一改，这些隐性依赖全部落空。

更麻烦的是，定理证明器的报错不像普通程序那样会告诉你“这里空指针了”。很多证明脚本的失败，误差来自几十行之前某个策略的展开结果。你要同时理解原来的证明在说什么，又得知道新定义和目标状态之间发生了什么冲突。这不是简单的 debug 思维能解决的问题。

1.2 传统调试思维的三个坑

我刚接触 Isabelle 时，总喜欢拿运行时 debug 的经验去处理证明失败，结果连续踩了三个坑。

第一个坑是“看到失败就删证据”。很多开发者的第一反应是删掉中间的引理或步骤，但一个引理往往不是孤立存在的，它可能被后续七八个证明共同依赖。删除之后，失败点会像多米诺骨牌一样蔓延。

第二个坑是“只盯着出错的那一行”。证明脚本是状态依赖的，目标能不能闭合，取决于前面每一步是否生成出正确形态的子目标。真正的问题常常在出错位置之前的函数定义变体或归纳策略上。

第三个坑是“试图在一个过期的上下文里做局部修补”。旧证明之所以失败，通常不是因为某一个策略用错了，而是证明所依赖的语义环境已经变了。这种情况下，盲目用try、sledgehammer或手动堆策略，也许能碰巧通过，但你可能并不理解自己为什么通过。

这也正是 Proof Repair 和普通证明补丁最大的区别。前者关心的不是“这一条引理怎么补”，而是如何识别哪些证明步骤已经失去效力，哪些可以复用，哪些需要调整为新的合约形态。

1.3 Promise: 把修复问题提上议程

所以，当我看到 CAPRI 强调 Contract-Aware 时，我的第一反应是：它尝试把“证明修复”从一件完全依赖个人经验的事，变成一种可以被描述、被定位、被自动化辅助的工程流程。虽然名字里的 “Repair” 听起来像是事后补救，但它真正解决的问题，其实是 Isabelle 开发过程中长期被忽略的“证明维护成本”。

2. Contract-Aware 究竟感知了什么：变更合约才是修复地图

2.1 合约在定理证明里的三层含义

Contract 这个词，很多读者可能更熟悉来自 JML、Dafny 或者设计契约理论，它通常指前置条件、后置条件和对象不变量。但在 Isabelle/HOL 的语境里，合约还可以有更宽泛的理解。

一层是“定义层合约”。函数定义里每一个分支、每一条递归方程，都可以理解成这个函数和外界之间的契约。调用者得明白它处理哪些输入，也会大致猜到它产生什么输出。新增一个分支，相当于修改了这条契约。

第二层是“定理层合约”。一个lemma的陈述本身是一份合约，它描述了什么条件下什么性质成立，函数的输入输出约束都在这里体现。证明只是用来证明这份合约确实被当前代码满足。

第三层是“证明脚本内部的局部合约”。一些中间引理承担着局部推导桥梁的作用，它们通常不像主定理那样被文档化，却常常是自动化证明能继续推进的关键。代码一改，很多这类隐式中间引理最先失效。

2.2 先看合约差异，再谈修证明

如果契约没有被显式表达，修复旧证明就像是让维修师在不看图纸的情况下处理一台机器。他只能从报错和证明脚本反推原来的设计意图，工作量大且容易出错。

Contract-Aware 的核心思路，是先把“变更前和变更后的合约差异”当成最重要输入。例如旧函数对某个输入返回完整列表，新函数则增加了一个过滤条件。接下来要考虑的不是怎么让旧引理继续通过，而是识别旧引理的结论在新合约下是否还成立。如果不再成立，任何局部的策略修补都只是自欺欺人。

真正的修复路径应该是：先承认旧引理失效，分析失效是因为新合约引入了新的边界情况，还是因为旧合约的某些假设已被修改。接着再决定是否需要引入新引理，或者是否可以把旧引理泛化成一个更一般的形式。

2.3 CAPRI 的方法论启示：给自动化修复补上“上下文”

从名称和方向上看，CAPRI 这类工作的一个重要价值，是尝试把“合约差异”纳入自动修复的搜索过程。如果“修复程序”只学习语法层面的补丁，很容易错过真正的语义变化。但如果它能先感知到哪里变了、变化边界是什么，它就可以更有针对性地生成修复方案。

这里需要区分事实与推测。至少从概念上，“Contract-Aware Proof Repair”这个定义给 Isabelle 开发者提供了一个很好的提醒：在你动手修复之前，先给当前证明重新建立一份和代码对齐的上下文地图。地图不是证明本身，但决定了修复从哪里开始。

一个实用的经验是：当新代码导致多个证明失败时，不要立刻去改失败文件，而是先整理一份从旧合约到新合约的差异清单，哪怕它只是几行注释，也能减少大量无效尝试。

3. 一个最小可理解的证明损伤链：过滤函数加了分支之后

3.1 一次从可证明到不可证明的转折

为了让“证明修复”更具体，我举一个 Isabelle/HOL 里很常见的例子。先看一个简单的列表函数，它保留列表里的全部元素：

fun collect_all :: "nat list ⇒ nat list" where "collect_all [] = []" | "collect_all (x # xs) = x # collect_all xs" lemma collect_all_len: "length (collect_all xs) = length xs" by (induction xs) simp_all

这个引理很容易证明。收集完所有元素，列表长度当然不变。现在需求变化了：我们不想要0，新函数collect_nonzero会把所有值为0的元素过滤掉。

fun collect_nonzero :: "nat list ⇒ nat list" where "collect_nonzero [] = []" | "collect_nonzero (x # xs) = (if x = 0 then collect_nonzero xs else x # collect_nonzero xs)"

这时候，原来的collect_all_len已经无法直接迁移。因为collect_nonzero [0, 1]返回的是[1]，长度显然不等于原始列表长度。如果你继续尝试用induction xs加上auto去证明同样的引理，会失败在最根本的结论上。

这里就是 Proof Repair 真正要处理的问题。旧证明之所以会失败，不是因为哪一个证明策略写错了，而是因为合约发生了变化：新定义引入了“过滤语义”。

3.2 自动化修复通常要经历的四步动作

从工程角度看，一个 Contract-Aware 的修复流程大致可以拆成下面四步，这也比较接近我在理解 CAPRI 方向时的模型。

第一步是“合约对比”。找出旧函数和新函数定义之间的差异。这里能看到if x = 0这个新条件，因此旧引理中“长度不变”的合约不再成立。这个动作看起来简单，却是整个修复中最重要的一步。没有它，后面的搜索都像蒙着眼睛打靶。

第二步是“失效定位”。找到证明脚本中真正依赖旧合约的点。对于collect_nonzero，失效点并不一定是最终的by命令，而是归纳过程中对递归方程形态的依赖。定义多了分支，自动化简规则就不再能覆盖所有情况。

第三步是“修复决策”。判断旧引理应该被替换、泛化，还是只能删除。在这里，与其继续尝试一个错误命题，不如把旧引理泛化成一个更精确的关系：length (collect_nonzero xs) = length (filter (λx. x ≠ 0) xs)。这个新引理不仅描述了新函数的行为，也弥补了旧引理无法继续成立的空缺。

第四步是“生成补丁并重新验证”。把新引理接入证明文件，运行 Isabelle 内核检查。如果补丁通过，才算修复完成。自动化工具在此过程中需要不断尝试不同的引理形态，所以成本并不低。

3.3 这里最难的其实不是语法补丁，而是语义决策

很多人会把 Proof Repair 想象成“找一条能通过的证明脚本”。但如果只是追求“能通过”，Sledgehammer 加上随机策略也能碰出一些结果。真正困难的是判断结论是否与开发意图一致。

继续用上面的例子。原目标length (collect_nonzero xs) = length xs在函数增加过滤后本来就不应该成立，任何让这条错误引理通过的修复都意味着问题的隐藏或误诊。Contract-Aware 的价值，在于它能提前识别出这种语义冲突，而不是让你浪费时间去寻找一个永远不会成立的证明。

这个点也解释了为什么人工经验在 Isabelle 开发中仍然如此重要。工具的职责是帮助定位失效点、生成候选引理、压缩搜索空间，但“这条性质是否仍然应该是代码的不变量”这个判断，暂时仍然需要人来完成。

4. 把 Proof Repair 变成日常工程能力的四条建议

4.1 维护一份“合约变更日志”

大多数 Isabelle 项目都有注释说明函数和定理，却很少维护一份专门的“合约变更日志”。它不需要很长，只需要记录每次关键定义变化时，哪些函数签名、递归分支或定理陈述被修改，哪些下游引理可能受影响。

这份日志最大的意义是帮你建立增量修复顺序。如果函数 A 的改变会影响引理 B 和 C，而 B 又是 C 的依赖，那么先修 B、再修 C，通常比随机修文件要快得多。它也能让后续加入项目的人知道，为什么某些引理会呈现出奇怪的前提条件。

4.2 每次批量修证明时，按依赖顺序分诊

真实项目里，一次改动往往会让十几个证明文件变红。此时最忌讳的是“哪个先报错就先修哪个”。你需要先把所有失败任务按依赖关系排个序：底层定义优先，其次是直接依赖底层性质的中间引理，最后才是靠这些引理撑起来的高层应用。

这个过程很像系统故障排查：不要先打表面补丁，而是先定位哪一层坏了。如果基础定义层的变化导致大量后续引理需要重新表述，那么顶层修复就要晚一点再做，否则你很可能白修一遍。

一个可以复用的排查顺序是：

1. 确认代码变更是否真的被 Isabelle 正确加载。
2. 比较旧定义和新定义中函数签名的变化。
3. 找出失败引理中是否直接使用了旧的函数名、构造子或递归谓词。
4. 检查是否存在已经被用户删除或改名的中间引理。
5. 小规模运行单个失败证明，观察当前目标和错误信息。
6. 判断是因为结论本身不再成立，还是定义形态变化导致现有策略无法闭合目标。

4.3 把修复后的证明提交成回归样本

很多开发者在手工把证明修好后，就当作任务结束。但这类问题几乎一定会再次出现。如果每修一次都只留下一个“现在能通过”的状态，下一次问题复现时，你还是得重新经历完整的定位过程。

更稳妥的做法是，在修复完成之后，提交一个最小化的失败样例并让它进入回归集合。以后只要再有类似定义变化，你就能通过回归测试第一时间发现哪条性质又被破坏，而不是等到部署前才集中爆发。

不要急着删掉那些曾经失败的引理痕迹。它们是后续修复最重要的参照样本。真正漂亮的 Isabelle 工程不是永不失败，而是每次失败都能被快速归类、快速定位、快速修复。

5. 适用边界：什么项目适合 Contract-Aware Proof Repair

5.1 真正适合它的是“长生命周期、规范频繁演进”的项目

CAPRI 这类工作最有价值的地方，可能不是帮你从零开始证明第一个定理，而是减少“后续每改一次规范，就得陪着一个历史证明文件打地鼠”的痛苦。

如果一个项目满足以下条件，那么引入 Contract-Aware 的修复思路会很有收益：

• 需要长期维护大量已经通过的证明，例如操作系统模型、编译器形式化验证、协议安全证明。
• 规范本身还在演进，经常有性质调整、边界条件增加或函数结构变化。
• 对证明的可追溯性有要求，不只是“能通过”，还希望知道每个证明在为什么契约负责。
• 多个开发者协作维护 Isabelle 代码，彼此对旧证明的意图不熟悉。

在这种场景下，自动修复能帮你快速定位“新合约和旧证明之间冲突在哪里”，再配合人的判断来完成决策。

5.2 需要谨慎的场景与两个前置条件

也有很多场景不适合追求自动化 Proof Repair。

第一类是不稳定探索阶段。如果你还在快速尝试各种定义，证明本身就处于随时可能推翻的状态，这时候投入精力维护可复用的修复流程有点为时过早。先跑通最小样例，确认方向和目标后，再开始沉淀证明资产。

第二类是合约表达不清晰的历史项目。如果一个库里的函数和引理之间没有任何文档或结构化的合约说明，自动化修复很难判断哪些差异是用户有意的，哪些只是草稿遗留。

使用 CAPRI 或类似工具前，至少要确认两个前置条件：当前 Isabelle 版本与工具版本兼容，能在一个小仓库跑通最小修复样例；并且你有能力判断工具生成的“通过补丁”是否包含不合理的删证或削弱结论行为。即使工具声称是自动化，你仍然需要理解它为什么这样修。

6. 从 CAPRI 看定理证明工具链的下一个方向：证明也需要维修经济

6.1 证明资产的复用，取决于你对失败原因是否有可解释的诊断

Isabelle 的项目经验积累得越久，越会发现证明资产的价值不在于单个工具能跑通，而在于它可以被后续维护者理解和修改。如果失败时只能看到满屏红色，而没有任何诊断信息说明“这条性质曾经对应哪份契约、为什么现在开始失效”，那项目会越来越难维护。

Contract-Aware Proof Repair 的更大意义，是它把失败原因和合约差异联系起来了。它对“为什么这个证明需要修复”给出了一种可解释的回答，而不是只给一个修复补丁。这种可解释性，也是后续自动化工具真正的护城河。

6.2 合约会成为人与自动修复工具之间最自然的对齐边界

未来定理证明器的自动修复方式，大概率不会越来越像一个神秘黑盒。相反，人类开发者、AI 辅助工具和证明器之间会形成一个三角：开发者维护契约，工具在契约约束下搜索证明路径，证明器负责最终检查。合约，就成了人和机器之间最自然的接口。

从这个角度理解 CAPRI，你就不会只把它当成一个单纯为了“省几分钟修证明”的研究。它代表的是下一阶段交互式证明工具的开发方式：让机器去承担那些可以被合约描述的重复修复工作，让人去处理语义意图和性质取舍。

6.3 最后的建议：先从最小失败样例开始，不要急于全自动

如果你想让自己的 Isabelle 项目也获得类似收益，我建议不要急着把希望寄托在某个全能修复工具上。先把一次失败的最小样例跑通，记录从合约变化到证明失败之间发生了什么，再尝试手工或半自动地完成一轮修复。这个最小闭环跑通之后，再慢慢扩大范围。

真正成熟的工作流，不是给你一把能把所有红证变绿的神奇钥匙，而是让你在代码演进的同时，能快速知道每个证明和契约之间还有没有保持一致性。当你开始把证明当成需要随合约一起演化的代码资产，而不是一次性通过的“字数兑换结果”，CAPRI 这个方向才算真正用对了地方。