企业官网建设流程全解析

开一场代码评审会时，有人把一个 PR 丢进仓库：改动只有几行，把 Isabelle/HOL 里的一个递归函数边界条件改了，意图是“让 0 不再被视为一个合法特例”。你下意识觉得，这种改动最多影响一两处调用。结果 CI 跑完，屏幕上出现了一排红色 lemma：原本能通过的证明全部失守。更麻烦的是，它们并不是语义写错，只是原来依赖的证明路径断了。

在形式化验证项目里，这可能是我见过最真实的痛点：修改规范和定理证明的“维护成本”并不和代码行数成正比。哪怕只改了一个 case，可能在另一条证明链上引起连锁反应。这就是所谓 Proof Repair（证明修复）问题。今天想借“CAPRI: Contract-Aware Proof Repair for Isabelle”这个题目，聊清楚一个关键判断：自动证明修复要想走出玩具阶段，不能只靠搜索策略，还必须理解“契约”。

这篇文章不会教你背 CAPRI 的命令行接口，也不保证它已经公开了开箱即用版本。因为 CAPRI 这个方向的真正价值是“设计思路”，它可以被复用到任何 Isabelle/HOL 项目里。我会先讲清楚 Proof Repair 解决什么问题，再用一个能直接跑的最小 Isabelle 例子，演示契约变化导致证明破裂的全过程，最后梳理 Contract-Aware 为什么比传统修复方法更本质。

1. Isabelle 的 Proof Repair，到底在解决哪种痛苦

很多 CSDN 读者第一次接触 Isabelle，是在论文里看到类似theorem add_commute这样的花哨证明。于是会形成一种错觉：定理证明器就是把定理输进去自动出新定理？其实真实工程不是这样的。

Isabelle/HOL 里的理论文件（.thy）更像一份“可验证的代码库”。你既写fun、definition、datatype，也用lemma和theorem表达你想证明的性质。每次运行isabelle build，这些证明都会被重新检查一遍。问题在于：数学函数定义一旦变化，原先的证明脚本不一定还能工作。

这类问题的本质是软件演化。在普通程序中，重构之后有类型系统检查和单测兜底；在定理证明项目中，类型系统能抓类型错误，但不能自动修复定理证明。一个 lemma 之所以成立，往往依赖函数定义的递归结构、case分支顺序、某个simp规则是否可用。你改的不只是代码，还是证明的“证据链”。

Proof Repair 要做的事情，可以定义得很朴素：

给定原理论 T、原证明 P，以及变更后的理论 T’，当 P 无法在 T’ 中证明原目标时，自动生成一个能够在 T’ 中通过的新证明 P’。

但朴素定义背后是一个高难度问题。普通程序修复可以只看语法和类型；证明修复必须保证生成结果仍然是一个“合法证明”。这比普通代码修复多了一个不可协商的限制：正确性是形式化的。

所以 Isabelle 社区对这个方向非常感兴趣，但成熟工具很少。早期做法很大程度依赖人工：打开红了的 lemma，观察报错，尝试sledgehammer、try0、blast…… CAPRI 这个标题里的关键词，就是在给“修复”加约束。它不打算盲目猜证明，而是先找出“这次变更影响了哪些契约”，再有目的地修复。

2. 基础概念：契约、Isabelle/HOL 与 Proof Repair

要理解 CAPRI，先要把这几个词拆开。

2.1 Isabelle/HOL，不只是证明编辑器

Isabelle 是一个交互式定理证明框架，最常用的对象逻辑是 HOL（高阶逻辑）。它采用 LCF 架构：所有定理必须经过一个小核心检查。这意味着你不能“骗”过证明器，就算用自动策略生成了证明脚本，最终通过的定理依然是被核心验证过的。

这带来一个工程后果：一旦 lemma 失败，失败原因不是“程序运行崩溃”，而是“该证明策略无法在给定目标上构造出合法证明”。Isabelle 给出的错误信息通常比较底层，经常需要从证明脚本一层层往前查。

2.2 什么是“契约”

软件工程里的契约，通常指接口双方都要遵守的约定。把函数看成一个组件：

• 前置条件：调用方必须满足什么条件，例如x > 0。
• 后置条件：函数保证返回什么性质，例如result > x。
• 类型约束：输入输出必须是什么类型。
• 不变式：在对象生命周期内始终成立的性质。

在 Isabelle/HOL 里，这些契约并不是某个专门的魔法字段，它们由assumes、shows、definition、locale、class、fun方程共同表达。举个例子：

definition add_positive :: "int ⇒ int ⇒ int" where "add_positive x y = x + y" lemma add_positive_post: assumes "0 < x" and "0 < y" shows "0 < add_positive x y" unfolding add_positive_def using assms by auto

这里assumes "0 < x" and "0 < y"是前置条件，shows "0 < add_positive x y"是后置条件。

有趣的是，Isabelle 中一个 lemma 既是对源码规格的陈述，也构成模块对外承诺的契约。当函数实现变化，这条 lemma 能不能继续成立，直接决定这个“承诺”有没有被打破。

2.3 Proof Repair 与传统代码修复的差异

传统代码修复面对的行为对象是“运行结果不符合测试预期”，修复目标是让代码跑对。Proof Repair 面对的是“证明脚本和新的理论不一致”，修复目标可能出现在多处：

• 函数定义写错了，应该修代码。
• lemma 的后置条件太强，新实现根本不能满足，需要削弱结论或加强前置条件。
• lemma 的证明策略过期了，目标其实成立，但原本的auto/induct路径已经无法覆盖新的 case。

第三种情况里，如果 CAPRI 只是换一个更强的证明策略，那它和sledgehammer没本质区别。它真正出彩的地方，应该是识别出“这次契约变了，所以你要判断到底是改代码、改规范，还是改证明过程”。

CAPRI 这个题目里的 Contract-Aware，准确表达了这种判断能力。它不是把修复当成纯语法匹配，而是把修复放到“契约变更”这个解释框架内。

3. 一个“改了几行就让证明失效”的最小例子

我们直接来做一个能跑通的实验。它会清晰展示，一个看起来很小、甚至更加“合理”的函数修改，如何让旧证明直接崩溃。

3.1 原始理论

先定义一个函数nextNat：输入自然数 n，输出 n+1。

theory CapriDemo_Original imports Main begin fun nextNat :: "nat ⇒ nat" where "nextNat n = n + 1" lemma nextNat_atLeast_1: "1 ≤ nextNat n" by simp end

这很自然：自然数加 1，肯定大于等于 1。在这个版本里，by simp可以轻松证明。

假设我们的业务契约是：nextNat的输出总是至少为 1。这条 lemma 就是该契约的抽象表达。

3.2 一次“优化”

现在产品经理说，0 不是一个有意义的输入，希望程序在输入 0 时返回一个“默认错误值”，并对其它正常输入保持原来的行为。开发者随手把它改成：输入 0 时返回 0，输入Suc n时返回n + 2。

theory CapriDemo_V2 imports Main begin fun nextNat :: "nat ⇒ nat" where "nextNat 0 = 0" | "nextNat (Suc m) = m + 2"

看这个定义，对于 n≥1，它依然能保证输出≥1。你可能会觉得，这条改动非常“局部”。但原来的 lemma 现在变成了什么？它要求对所有自然数 n 都成立1 ≤ nextNat n，而当n = 0时，nextNat 0 = 0，结论显然不成立。

所以在 V2 里，原证明写进理论文件会直接失败：

lemma nextNat_atLeast_1: "1 ≤ nextNat n" by simp

即使simp能自动处理很多情况，它也无法证明一条在新实现下为假的命题。这是形式化证明真正残酷的地方：它不会像测试那样给你一个“反例警告”之后继续跑，而是会把构建直接停在失败点。

4. 修复该怎么做：先判断契约，而不是急着换 tactic

如果你只是在编辑器里看到红，第一反应可能是：把simp换成auto，或者上sledgehammer。但对这个案例来说，换任何自动策略都没用，因为命题为假。

更理性的修复路径是问：新实现是否仍然承诺“输出至少为 1”？如果不是，那么原来的契约就要更新。

4.1 修复方向一：加强前置条件

如果产品语义允许n > 0作为合法输入，那我们可以把原 lemma 更新为如下形式：

lemma nextNat_atLeast_1_v2: assumes "0 < n" shows "1 ≤ nextNat n" using assms by (cases n) simp_all

这里的关键变化不是证明方法从simp换成了cases n，而是我们在逻辑上新增了一条假设。也就是说，契约从“对所有 n 输出 ≥1”变成了“当输入合法时输出 ≥1”。

这个例子里，cases n实际上只是在告诉 Isabelle：考虑n = 0和n = Suc m两种情形。assumption排除掉n = 0后，剩下的情形交给simp_all自动处理。

这种修复使得 lemma 依然成立，但它其实是“约束调用方”。如果你不知道这是契约变化，只把simp换成更强的sledgehammer，是永远得不到通过结果的。

4.2 修复方向二：承认实现违反原契约

如果合法输入包括 0，那就不是证明的问题，而是函数实现本身违反契约。此时正确的产出应该是反例，而不是一个强行凑出来的证明。

我们可以清楚地展示反例：

lemma counterexample_when_input_is_zero: "nextNat 0 = 0" by simp text ‹因此，在 `n = 0` 时，原契约 `1 ≤ nextNat n` 为假。›

一个 Contract-Aware 的 Proof Repair 系统，最该做的事就是在上面两种方向里做判断。如果修复候选给出一堆虽然能通过、但严重改变 original lemma 语义的证明，反而会埋下更大的坑。

这才是 CAPRI 标题中 “Contract-Aware” 的分量。普通程序修复系统可以只关心“能不能跑绿”，定理证明修复系统必须关心“这个修复是否违背了原本的模块契约”。

5. CAPRI 这类系统的一般处理流程

因为 CAPRI 是一个研究型题目，我不会假设你已经拿到了可执行包。下面这套流程，是从论文标题和 Isabelle 工程实践里能提炼出的最合理抽象。CAPRI 如果按这个思路实现，那么它的输入输出大致会是：

输入：

• 变更前的理论文件或提交版本。
• 变更后的理论文件。
• 一个或多个失败的 lemma 标识。
• 契约信息，通常由assumes、shows、函数定义、locale等结构提供。

输出：

• 针对失败 lemma 的可执行修复建议，对应一个能通过 Isabelle 核心检查的新证明脚本。
• 如果实现违反了契约，则输出反例或“契约冲突”提示，而不是强行修复。

处理过程大概可以拆成下面几步。

5.1 第一步：失败定位

理论上，Isabelle 可以一次性告诉你哪些 lemma 失败，但失败原因往往没有精确到“哪一行定义变化导致”。第一层要做的是把失败目标、失败前已应用的 proof method、以及当前使用的定义和前置条件完整收集起来。

5.2 第二步：契约差异分析

这一步是 Contract-Aware 的核心。

对比变更前后，函数定义如果从“无递归分支”变成“有特殊 case”，那么旧证明中所有依赖“全称输入”的结论都可能被破坏。对比nextNat n = n+1与nextNat 0 = 0 | nextNat (Suc m) = m+2，会发现：

• 新实现给 0 单独开了一个异常 case。
• 后置条件在异常 case 下不再被满足。
• 函数结果的“最低值”下限变了。

系统如果把这种语义变化抽象出来，就不会盲目尝试对所有目标应用auto，而会先把受影响的范围缩小到与 0 case 相关的 branch。这就把搜索空间砍掉一大块。

5.3 第三步：生成候选修复

修复不只是生成一个 tatic，而是生成一个“语义可解释的补丁”：

• 如果原有 lemma 是新实现下的假命题，返回“不建议在证明层修复”。
• 如果加前置条件后成立，则建议用户更新assumes。
• 如果证明策略过时，则重放证明脚本，逐个策略段替换失效步骤。
• 如果函数定义有多个构造 case，考虑是否需要调整induct/cases策略。

5.4 第四步：核心验证与信息回滚

候选修复最终仍要送进 Isabelle 核心做严格校验。只有通过验证的补丁才能作为最终输出。这个回滚机制很重要：自动修复系统不能“几乎正确”，一旦通过，就必须是真正可以在理论文件里工作的证明。

从这套流程也可以看出，CAPRI 并不是要替代 Isabelle 现有自动策略。它是更高一层“修复调度器”。它决定要不要修、修代码还是修契约、用哪种策略修。而最终底层证明还是离不开 Isabelle 的策略引擎。

6. 为什么 Contract-Aware 比通用“证明搜索”更关键

有读者可能会问：sledgehammer现在不是已经很能打了吗？为什么还需要 CAPRI？

sledgehammer的原理，是把当前目标发给多个外部自动证明器，搜索后把结果翻译回 Isabelle 可验证的 tactic。它擅长“在目标已明确且成立的情况下，找到一条可行证明路径”。但它的定位是“我帮你把证完的最后一公里跑完”，它不会回答“这个 lemma 应不应该存在”。

Proof Repair 真正难的一点，是语义歧义。目标变红时，可能有两类原因：

1. 目标在新理论下其实成立，只是没找到证明。
2. 目标本身在新理论下已不成立，因为某个前置/后置条件被悄悄破坏了。

前者是策略问题，后者是契约问题。如果一个修复工具只处理前者，它会浪费大量算力去尝试验证一个根本不成立的命题，直到穷尽所有自动策略。如果一个修复工具能感知契约，它能很快把你引到正确的元问题上。

打个不严谨但容易记的比方：普通程序测试挂了，可能是测试代码写错，也可能是被测代码写错。一个合格的工具不会只知道“重新跑测试”。

对一个 Isabelle 项目而言，auto、simp、blast、sledgehammer都像执行测试的 worker；但 project 级别的 Proof Repair 需要的是一个能理解“合约是否被打破”的指挥者。CAPRI 的价值主张，正是把它放到第一优先级。

7. 工程建议：把 Isabelle 证明维护纳入持续验证

如果你看到这里，说明你已经在把 Isabelle 当成严肃工程来使用。这时候最好的状态是：不要等问题爆发再手工打开编辑器红色一片，而是把证明维护纳入日常验证。

一个最小目录结构可以是这样：

capri-demo/ ├── CapriDemo_Original.thy ├── CapriDemo_V2.thy └── ROOT

其中ROOT文件定义一个 session，把两个理论都放进去：

session CapriDemo = HOL + theories CapriDemo_Original CapriDemo_V2

在本地，可以用下面命令在 jEdit 里打开单个理论：

isabelle jedit -l HOL CapriDemo_V2.thy

要跑整个 session，可以执行：

isabelle build -d . CapriDemo

这是把定理证明放进 CI/commit 前检查的基础。你可以建一个很小的脚本：

#!/usr/bin/env bash set -euo pipefail isabelle build -d . CapriDemo || { echo "Isabelle proof check failed" exit 1 }

这只是最基本的“证明回归”检查。除了把构建跑绿，还有几个实战建议。

7.1 把契约集中表达，方便 diff

在代码中，不要把所有约束都藏在by auto的实现细节里。尽量用assumes/shows把它们显式化。这样每次改动后，git diff能显示契约变化的位置，也让未来的自动修复系统更容易定位。

7.2 优先写结构化 Isar 证明

直接用apply (auto)堆策略，前期很爽，后期很难维护。结构化 Isar 证明虽然写起来长一点，但每一个 proof step 都对应清晰的逻辑关系。

举例，同样是修复 V2 中的 lemma，如果写成 Isar 风格，会更容易看出“我加了前置条件，排除了 n=0 分支”：

lemma nextNat_atLeast_1_isar: assumes "n ≠ 0" shows "1 ≤ nextNat n" proof - obtain m where "n = Suc m" using assms by (cases n) auto then show ?thesis by simp qed

这样的证明即使以后函数再变，人也能快速看出：为什么需要n ≠ 0？因为只有非 0 输入能保证后置条件。

7.3 使用 Quickcheck/Nitpick 做反例检测

当某个 lemma 在新实现下失败，不一定马上冲去改证明。先用反例工具验证它本身是否还成立。

lemma nextNat_atLeast_1_false: "1 ≤ nextNat n" nitpick oops

nitpick会为n = 0生成反例。看到反例，你就能明白：这不是证明技巧不够，而是陈述本身在新实现下已经不成立。这种前置判断，能省下大量无效尝试。

8. 常见问题与排查思路

下面整理几个在实际使用 Isabelle 和维护证明时最容易遇到的问题：

排查 Proof Repair 问题时，最高效的口诀是：先判断陈述的真假，再判断策略是否有效，最后才是改证明脚本。顺序一旦反了，很容易在假命题上浪费几个小时。

9. 总结与后续学习方向

CAPRI 这个工具虽然名字里带 Isabelle，但它真正值得学习的地方是方法论：自动修复证明时，系统必须感知契约变化，并据此决定是改代码、改契约、还是改证明策略。这是从“搜索证明”上升到“理解软件演化”的一步。

如果你手头没有现成 CAPRI release，也别急着写“求安装包”。更好的实践路径是：

• 先熟悉 Isabelle/HOL 的基本理论文件结构和lemma/fun/definition写法。
• 把一个实际项目中的函数定义改动和 lemma 失败记录下来，观察失败模式。
• 用nitpick先排除假命题。
• 再尝试sledgehammer和结构化 Isar 修复。
• 最后把这些经验抽象成自己的 Proof Repair 检查清单。

形式化验证一旦进入长期维护阶段，“证明修复”就是一个无法回避的工程成本问题。CAPRI 开了一个好头：它让我们重新思考，自动修复不能只看 strategy，更要看 contract。后续值得继续关注 Isabelle 社区在这一块的演变，也要警惕“工具能自动修证明”这句话的另一面：如果一条证明在新实现下已经不再为真，最该修的不一定是证明，而是那段悄悄改变了世界的新代码。