软件工程师眼中的 Lean 证明剖析

# 面向软件工程师的 Lean 证明解析 来源：https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/ \[目录\] - 引言 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#intro) - 背景：DFA 与正则语言 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#background-dfas--regular-languages) - 确定性有限自动机 \(DFA\) (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#deterministic-finite-automaton-dfa) - 正则语言 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#regular-languages) - 问题 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-problem) - 解决方案 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-solution) - 加法运算 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#adder-arithmetic) - 加法器 DFA (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#adder-dfa) - 示例 1 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#example-1) - 示例 2 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#example-2) - Lean 证明 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-lean-proof) - 规约 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-specification) - 实现 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-implementation) - 证明的工作原理 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#how-proofs-work) - 证明 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-proof) - 运行不变量 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#run-invariant) - 运行不变量证明 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#run-invariant-proof) - 基础情况 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#base-case) - 归纳步骤 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#inductive-step) - 拆分运行 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#splitting-the-run) - 第一步的加法 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#first-step-adds) - 最低位拆分 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#least-significant-bit-split) - 综合起来 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#putting-it-together) - \(B^{\mathcal{R}}\) 是正则的 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#b-reverse-is-regular) - 加法器 DFA 接受 \(B^{\mathcal{R}}\) (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#adder-dfa-accepts) - 从接受性到正则性 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#from-acceptance-to-regularity) - \(B\) 是正则的 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#b-is-regular) - 结语 (https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#outro) ## 引言 最近我做了一道计算理论教材上的题目，要求用有限自动机证明某种语言的一个性质。非形式化的证明是一个简单的构造性证明——构建一个自动机，并证明它能识别该语言。这和程序验证有几分相似，所以我想看看把证明形式化需要做哪些工作。Lean 很适合这项任务，因为它的 [Mathlib](https://lean-lang.org/use-cases/mathlib/) 包含了该问题所需的全部定理。 完成形式化证明之后，我决定把它写下来，因为我相信它能让软件工程师很好地了解，形式化证明系统性质到底需要什么。 我尽量让这篇文章易于阅读。如果你熟悉现代静态类型编程语言（如 TypeScript 或 Rust）、二进制算术、基本的命题逻辑和归纳证明，你应该能跟上。 ## 背景：DFA 与正则语言 *如果你对 DFA 和正则语言已经熟悉，可以跳到[下一节](https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-problem)。* 有限自动机为计算提供了一种具有固定内存的理论模型。除了理论价值，有限自动机还有重要的实际应用。例如，解析器和正则表达式领域就与有限自动机息息相关——曾有一个[缺陷](https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/)导致互联网的大面积瘫痪。 ### 确定性有限自动机（DFA） **确定性有限自动机**（DFA）是一种具有固定、有限状态集合的机器，它从左到右逐个读取输入符号。每读取一个符号，它就通过确定性的转移函数更新自身状态。读完最后一个符号后，机器要么处于*接受*状态（输入被接受），要么不处于接受状态（输入被拒绝）。 如果你写过 `\-?\[0\-9\]\+` 这样的简单正则表达式，那你实际上就已经构造了一个 DFA。该正则表达式匹配像 `12` 和 `\-123` 这样的整数字面量，对应的 DFA 如下所示（箭头上标注了导向下一个状态的符号）： 十进制整数字面量的 DFA（含死状态）：start（起点）→ sign（符号）→ digits（数字）→ dead（死状态）；dead 为汇点状态，自环标注 "other"，digits 读到 `0-9` 保持在 digits，遇到 other 进入 dead；sign 读到 `\-` 进入 sign，读到 digits 进入 digits，读到 other 进入 dead；start 读到 `\-` 进入 sign，读到 digits 进入 digits，读到 other 进入 dead。 该 DFA 有四个状态： - **start（起点）：** 这是处理第一个字符之前的起始位置。由于起始状态不是接受状态，我们拒绝空字符串。 - **sign（符号）：** 当在 start 状态遇到 `\-` 字符时，我们转移到 sign 状态。由于符号是可选的（`\-?`），我们可以跳过 sign 状态，从 start 直接跳转到 digits。如果字符串结束时处于该状态，则拒绝该字符串。 - **digits（数字）：** 当遇到数字字符（`\[0\-9\]`）时，我们从 start 或 sign 转移到 digits。如果处于 digits 状态时再次遇到数字字符，则保持在 digits 状态。digits 状态是该 DFA 中唯一的接受状态。处理完输入字符串后如果处于该状态，则 DFA 接受该字符串。 - **dead（死状态）：** 如果遇到数字以外的任何字符（除非是开头的负号），就会进入该状态。如果字符串结束时处于 dead 状态，则 DFA 拒绝该字符串。一旦进入 dead 状态，就会一直停留在那里，因此该 DFA 中的 dead 状态是一个*汇点*。 机器的输入**符号**集合由 Σ 定义。在我们的正则表达式示例中，Σ = \{−, 0, 1, 2, …, 9\}。 ### 正则语言 **语言**就是字符串（也称为**词**）的集合。如果某个 DFA 恰好接受该集合中的字符串，则称该语言是**正则**的。识别正则语言是这样一类判定问题：其求解所需内存量不随输入增长。 正则语言具有一些有用的封闭性：两个正则语言的并集和交集仍然是正则语言，它们的补集（以及对本文至关重要的**反转**）也是正则的。 证明某个语言是正则的标准方法是构建一个 DFA，并证明它恰好接受该语言。 我们可以用集合构造法来描述语言 A： A = \{ w ∈ Σ\* ∣ P(w) \} Σ\* 表示由 Σ 中符号的所有可能拼接所构成的字符串集合，P(w) 是字符串 w 要属于该语言必须满足的条件。 把这套记法应用到我们的正则表达式示例：`\-?\[0\-9\]\+`。那么 Σ\* 包含像 `""`、`"123"`、`"\-111"`、`"2\-625\-"` 这样的字符串，P(w) 可以定义为"w 不为空且不含负号，唯一的例外是当 w 至少有两个字符时，其第一个字符可以是负号"。 ## 问题 我们要解决的问题出自 Michael Sipser 所著的 [Introduction to the Theory of Computation](https://math.mit.edu/~sipser/book.html)（《计算理论导论》）第三版： > **1.32** 设 Σ₃ = \{ \[\[000\], \[\[001\], \[\[010\], …, \[\[111\]\}。Σ₃ 是所有高度为 3、由 0 和 1 组成的列的集合，因此 Σ₃ 上的一个字符串决定了三行比特位。将每一行按二进制数读取，定义 B = \{ w ∈ Σ₃\* ∣ P(w) \}，其中 P(w) 是命题"w 的底行等于上两行之和"。证明 B 是正则语言。（提示：研究 B 的反转 B^{\mathcal{R}} 更容易。） 题目定义了一个不寻常的字母表。字母表不是由 `\[a\-z\]` 这样的常规字符组成，而是由三位比特构成的列组成。所以，这个语言不是由 `"apple"`、`"banana"` 这样的字符串组成，而是由二维比特串组成，例如： ``` 011 001 100 ``` 其中第一列是第一个"字符"，以此类推。 判断某个字符串是否属于该语言的规则是：将字符串的前两行相加，检查结果是否与第三行匹配。 例如，下面这个字符串属于该语言： ``` 011 # x 行：第一个加数在十进制下为 3 001 # y 行：第二个加数在十进制下为 1 100 # z 行：和为 4，等于 3 + 1 ``` 但下面这个字符串不属于该语言： ``` 01 # x 行：第一个加数在十进制下为 1 00 # y 行：第二个加数为 0 11 # z 行：和为 3，不等于 1 + 0 ``` 虽然这样的语言起初看起来很奇怪，但识别它其实很容易：我们只需检查等式 x + y = z 来判断字符串是否属于该语言。挑战在于：我们需要用固定数量的内存来处理任意长的字符串。 ## 解决方案 诀窍在于回忆你如何手工做加法：从最低有效位到最高有效位列计算。你从一列带到下一列的唯一信息就是进位。 但 DFA 是从左到右读取的，而题目中的数字是以最高位在前的方式呈现的。所以我们不能直接识别 B。相反，我们构建一个 DFA 来识别它的反转 B^{\mathcal{R}}——即把 B 中的字符串倒过来写，这样机器看到的最先是最低位的列。 如果我们能构建一个 DFA 来识别 B^{\mathcal{R}}，就可以得出 B^{\mathcal{R}} 是正则语言的结论。由于 B^{\mathcal{R}} 再反转就是 B，我们可以利用"正则语言的反转也是正则的"这一封闭性，得出 B 也是正则语言，这就完成了整个解答。 ### 加法运算 逐列做算术时，我们用*加法器方程*来计算每一步的和位： x_i ⊕ y_i ⊕ c_in = z_i 其中 x_i、y_i 是加数的比特位，z_i 是和的比特位，i 表示当前列的索引，c_in 是上一步的输入进位。我们按如下方式计算下一步的输出进位 c_out： c_out = (x_i ∧ y_i) ∨ (c_in ∧ (x_i ⊕ y_i)) 这意味着：当两个加数都是 1 时会产生进位；或者当存在输入进位且两个加数中恰好有一个是 1 时也会产生进位。注意，计算 c_out 有一个更简单的方法：检查 x_i、y_i 和 c_in 中至少有两个是 1（我们将在 Lean 证明中用到这一点）。 ### 加法器 DFA 考虑到这一点，下面是识别 B^{\mathcal{R}} 的 DFA： 识别 B 反转的 DFA：一个全加器，其状态就是待处理的进位，外加一个死状态。每条转移都标注了导致该转移的三位列符号：实线箭头表示和位校验通过的列，红色虚线箭头表示和位不匹配的列。 进位 0 →（经 `000`、`011`、`101`）进位 0；进位 0 →（经 `010`、`100`、`111`）进位 1；进位 0 →（经 `001`）进位 1？—— 详见下文各列的转移标注。 进位 1 →（经 `001`）进位 0；进位 1 →（经 `010`、`100`、`111`）进位 1；进位 1 →（经 `000`、`011`、`101`、`110`）dead。 该加法器 DFA 有三个状态： - **进位 0（Carry 0）：** 处理下一列之前进位为 0 时，我们处于该状态。这既是起始状态也是接受状态，因为如果最后还留有进位，说明和溢出了底行。 - **进位 1（Carry 1）：** 处理下一列之前进位为 1 时，我们处于该状态。该状态是非接受状态，因为以它结尾的词留有进位，说明和发生了溢出。但与 dead 状态不同，我们仍可以离开它，因为一列 `[[001]]`（即 `0/0/1`）可以吸收待处理的进位，把我们带回进位 0。 - **Dead：** 当和不匹配时，我们会进入该状态。这是一个汇点状态，意味着我们永远无法离开。 箭头上标注了从输入状态导向输出状态的列。如果一开始觉得这张图很困惑，下面的例子应该能帮助你理解。 ### 示例 1 让我们把题目中的第一个示例在 DFA 上跟踪一遍： ``` 011 # x 行：十进制下为 3 001 # y 行：十进制下为 1 100 # z 行：十进制下为 4 ``` 该 DFA 识别的是 B^{\mathcal{R}}，所以它从后向前读取列。将运行展开后得到一条直线，每一步对应一个状态。 进位自动机在接受词上的运行，展开后：从进位 0 开始，机器依次读取列 (1,1,0)、(1,0,0)、(0,0,1)，途经进位 1、进位 1、进位 0，最终结束于接受状态。 开始 → 读取 `110`（即列 (1,1,0)）→ 1 ⊕ 1 ⊕ 0 = 0 ✓，输出进位 = 1 → 读取 `100`（即列 (1,0,0)）→ 1 ⊕ 0 ⊕ 1 = 0 ✓，输出进位 = 0 → 读取 `001`（即列 (0,0,1)）→ 0 ⊕ 0 ⊕ 1 = 1 ✓，输出进位 = 0 → 结束于进位 0。 运行结束于进位 0（即接受状态），因此反转后的词属于 B^{\mathcal{R}}。根据 B^{\mathcal{R}} 的定义，原始词也属于 B。 注意，机器两次*穿过*了非接受的进位 1 状态。如果这个词在前两列中的任一列之后就结束，它就会被拒绝。1 + 1 = 0 和 11 + 01 = 00 在没有地方存放进位的情况下都是错误的。 ### 示例 2 现在看第二个示例，它应该被拒绝： ``` 01 # x 行：十进制下为 1 00 # y 行：十进制下为 0 11 # z 行：十进制下为 3 ``` 进位自动机在被拒绝词上的运行，展开后：从进位 0 开始，列 (1,0,1) 让机器保持在进位 0，然后列 (0,0,1) 未通过和位校验，将机器送往 dead 汇点状态。 开始 → 读取 `101`（即列 (1,0,1)）→ 1 ⊕ 0 ⊕ 0 = 1 ✓，输出进位 = 0 → 读取 `001`（即列 (0,0,1)）→ 0 ⊕ 0 ⊕ 0 ≠ 1 ✗，和位不匹配 → 进入 dead 状态。 第一列单独看是没问题的（1 + 0 确实等于 1），所以机器还看不出哪里有问题。但第二列失败了：在没有待处理进位的情况下，0 + 0 必须产生 0，但底行声称是 1。运行结束于接受状态之外，因此第二个示例被拒绝。 注意，由于 dead 状态是汇点状态，即使第二列之后还有更多合法的列，该字符串仍会被拒绝。 ## Lean 证明 我们的目标是证明[问题](https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#the-problem)中定义的语言 B 是[正则的](https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#regular-languages)。如前所述，为了证明一个语言是正则的，我们需要构建一个 [DFA](https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#deterministic-finite-automaton-dfa)，并证明它接受该语言。 Lean 证明将由三部分组成： 1. 语言 B 的**规约**（specification）。 2. [加法器 DFA](https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/#adder-dfa) 的可执行**实现**。