面向软件工程师的 Lean 证明剖析：用 Lean 形式化验证 DFA 加法器识别二进制加法语言

我最近研究了一本计算理论教材中的一个问题，要求我使用有限状态自动机证明一个语言的性质。非正式的证明是一个简单的构造性证明，你建立一个自动机并展示它可以识别该语言。这有点类似于程序验证，所以我觉得把证明形式化看看需要什么会很有趣。Lean 是一个不错的选择，因为它的 Mathlib 包含了这个问题所需的所有定理。

在完成形式化证明后，我决定把它写出来，因为我认为这能为软件工程师提供有关形式化证明系统性质所需工作的良好见解。

我尽量让这篇文章易于理解。如果你熟悉现代静态类型编程语言（如 TypeScript 或 Rust）、二进制运算、基本的命题逻辑以及归纳证明，你应该能够跟上。

如果你对 DFA 和正规语言感到熟悉，可以直接跳到下一部分。

有限状态自动机提供了一个固定内存的理论计算模型。除了理论应用之外，有限状态自动机还有重要的实际应用。例如，有限状态自动机与解析器和正则表达式相关，其中一个错误曾导致互联网的很大一部分瘫痪。

确定性有限自动机（DFA）是一种具有固定、有限状态集的机器，它从左到右一次读取一个输入符号。每读一个符号，它通过确定性的状态转移函数更新其状态。在读取最后一个符号后，机器要么处于接受状态（输入被接受），要么不处于接受状态（输入被拒绝）。

如果你曾经写过一个简单的正则表达式，比如 -?[0-9]+，那么你已经构造了一个 DFA。这个正则表达式匹配像 12 和 -123 这样的整数字面值，对应的 DFA 看起来像这样（箭头上标注了引导到下一个状态的符号）：

机器的输入符号集由集合 Σ \Sigma Σ 定义。在我们的正则表达式示例中，Σ = { − , 0 , 1 , 2 , … , 9 } \Sigma = \left\{-, 0, 1, 2, \ldots, 9\right\} Σ = { − , 0 , 1 , 2 , … , 9 }。

语言只是一组字符串，也称为单词，如果某个DFA恰好接受其中的字符串，则称该语言为正规语言。识别正则语言是一类可以用不随输入增长的内存量来解决的决策问题。

正则语言具有有用的闭包性质：两个正规语言的并集和交集是正规的，补文也是正规的，且（对我们来说很重要）正则语言的反转也是正规的。

证明语言是正则语言的标准方法是构建一个DFA，并证明它完全接受该语言。

我们可以用集合构建符号描述语言 A A：

Σ ∗ \Sigma^{*} Σ ∗ 指由 Σ \Sigma Σ 和 P 中所有可能的符号串接所生成的字符串集合 （w ） P（w） P （w ） 是字符串 w w w 必须满足的条件，才能属于该语言。

让我们将这个符号应用到正则表达式示例：-？[0-9]+ .则 Σ ∗ \Sigma^{*} Σ ∗包含字符串如“” 、 “123” 、 “-111” 、 “2-625-” 等，而 P （ w ） P（w） P（w） P （w ） 可以定义为“w w w 不是空的，且无负号，除非其第一个字符可能是负号，且 w w 至少有两个字符。”

我们将要解决的问题来自Michael Sipser的《计算理论导论》第三版：

Σ 3 \Sigma_3 Σ 3 是所有高度为 3 的列 0 和 1 的集合，因此 Σ 3 \ Sigma_3 Σ 3 上的字符串决定了三行比特。将每行读作二进制数，定义

其中 P （ w ） P（w） P （w ） 是命题：w w 的底行等于顶两行之和。

证明 B B B 是正则的。（提示：使用 B R B^{\mathcal{R}} B R 更容易。）

该问题定义了一个不寻常的字母表。字母表由三位列组成，而不是像 [a-z] 这样的字符串。因此，语言由像“apple”、“banana”等字符串组成，而是由二维位字符串组成，如

其中第一列是第一个“字符”，依此类推。

判断字符串是否属于该语言的规则是将字符串的前两行相加，并检查它们是否与第三行匹配。

例如，以下字符串属于该语言：

但以下字符串不属于该语言：

虽然这样的语言乍一看可能很奇怪，但实际上很容易识别：我们只需要检查方程

以确定一个字符串是否属于该语言。挑战在于，我们需要用固定数量的内存处理任意长度的字符串。

技巧是记住你手动加数字的方式：你从最低有效位到最高有效位进行运算。唯一从一列传到下一列的东西是进位。

但 DFA 是从左到右读取，而问题给出的数字是最高有效位优先。因此，我们不能直接识别 B B B。相反，我们构建一个 DFA 来识别其倒序 B R B^{\mathcal{R}} B R，它由 B B B 倒写的字符串组成，所以机器首先看到最低有效列。

如果我们能够构建一个 DFA 来识别 B R B^{\mathcal{R}} B R，那么我们可以断定 B R B^{\mathcal{R}} B R 是正规语言。由于 B R B^{\mathcal{R}} B R 的倒序是 B B B，我们可以利用正规语言的倒序封闭性来断定 B B B 也是正规语言，从而完成解答。

在按列逐步进行算术运算时，我们在每一步使用加法器方程计算和位：

其中 x_i, y_i 是加数位，z_i 是和位，i 表示当前列的索引，而 c_{\mathrm{in}} 是前一步的输入进位。我们按如下方法计算下一步的输出进位，记作 c_{\mathrm{out}}：

这意味着只有当两个加数都是 1 或者存在输入进位且正好有一个加数为 1 时才会产生进位。注意，计算 c_{\mathrm{out}} 的更简单方法是检查 x_i, y_i 和 c_{\mathrm{in}} 中至少两个为 1（我们将在 Lean 证明中使用这一点）。

考虑到这一点，以下是识别 B R B^{\mathcal{R}} B R 的 DFA：

箭头标注了从输入状态到输出状态的列。如果图形一开始看起来让人困惑，以下示例希望能让它更清楚。

让我们通过 DFA 跟踪问题中的第一个示例：

DFA 识别 B R B^{\mathcal{R}} B R，因此它按列从后向前读取。展开运行得到一条直线，每步一个状态。

运行以进位 0（接受状态）结束，所以反向的单词在 B R B^{\mathcal{R}} B R 中。根据 B R B^{\mathcal{R}} B R 的定义，原始单词也在 B B B 中。

注意该机器两次经过非接受的进位 1 状态。如果单词在前两列中的任意一列后停止，它将被拒绝。1 + 1 = 0 \mathtt{1} + \mathtt{1} = \mathtt{0} 以及 11 + 01 = 00 \mathtt{11} + \mathtt{01} = \mathtt{00} 都是不正确的，因为没有地方放置进位。

现在看第二个示例，它应该被拒绝：

第一列本身是正确的（1 + 0 \mathtt{1} + \mathtt{0} 1 + 0 确实是 1 \mathtt{1} 1），所以机器暂时无法判断有什么错误。但是第二列失败了：由于没有待处理进位，0 + 0 \mathtt{0} + \mathtt{0} 0 + 0 必须产生 0 \mathtt{0} 0，但底行声称是 1 \mathtt{1} 1。运行在非接受状态结束，因此第二个示例被拒绝。

注意由于死状态是汇聚状态，即使在第二列之后有更多有效列，字符串也会被拒绝。

我们的目标是展示问题中的语言 B B B 是正则语言。如前所述，为了展示一个语言是正则的，我们需要构建 DFA 并展示它接受该语言。

Lean 证明将由三部分组成：

Lean 的 Mathlib 对形式语言和 DFA 提供了一流支持，因此我们只需要在库中的结构上构建规范和实现。

对于证明，我们需要做更多工作，但 Mathlib 在这里也会有帮助。它包含了正则语言在反转下封闭的定理，这将节省大量工作。证明中会包含一些不熟悉的语法，但在底层它只是一个程序。实际上，只要程序能编译，证明就被接受。

下面是一个展示程序组件的图。完整代码可以在 GitHub 上找到。

问题中的字母表由三位二进制列组成。我们可以用 Lean 中的三个布尔值元组来表示一列：

然后我们使用 Mathlib.Computability.Language 来定义 B B B：

Language 是形式语言的通用实现，带有标准操作和相关定理。我们用字母表 Sigma3 和 BBB 的成员谓词来构建它（记住语言是一组字符串）。

wBE 是一个候选单词，以大端模式读取，是一个 Sigma3 值的列表，即一个具有三行的二维二进制值列表。rowNBE 是一个函数，从上方选择二维列表的第 n 行，并使用大端解释将其转化为自然数。因此谓词就是

如果你使用过带集合推导的编程语言，集合构造语法可能看起来很熟悉，但我们这里并不是在构建一个集合。Language 在底层只是一个 Set，Lean 中的 Set 是一个测试元素是否属于集合的函数。因此我们对 BBB 的定义在底层会展开为一个函数定义：

该函数有一个类型为 List Sigma3 的参数，这是一个通用列表，用于保存 Sigma3 对象。这目前相当标准，但返回类型更有趣。在典型编程语言中，你会期望成员测试返回一个布尔值。但这里的返回类型是 Prop，它是 Lean 中所有命题的类型（命题是可能有证明也可能没有证明的东西）。

那么，成员测试是如何工作的呢？表达式 wBE ∈ B 将函数应用于 wBE，返回一个命题。在 Lean 中，命题本身就是一种类型，其值是命题的证明。因此，我们不是将 wBE ∈ B 计算为布尔值，而是证明它：为了显示一个单词属于某个语言，我们构造该命题类型的一个值。为了显示一个单词不属于该语言，我们构造一个被否定命题的值。通过这种方式，集合成员测试最终变成了类型检验，而不是在运行时进行计算。

我们首先将 DFA 的状态（进位 0、进位 1、死状态）定义为一个求和类型：

我们可以在 Rust 中使用枚举，或者在 TypeScript 中使用判别联合来定义相同的类型。然而，Lean 的归纳类型比这些语言中的递归求和类型多做了一些：它还生成一些脚手架，使得在证明中使用该类型变得容易。我们稍后会看到更多。

现在讨论 derives。DecidableEq 只是表示该类型支持完全的相等性检查（与 Rust 中的 Eq 相同），而 Fintype 是只有在证明助手中才有的东西。它表示该类型具有有限多个值，并创建一个包含这些值的列表以及该列表完整性的证明。派生 Fintype 让我们能够稍后断言该语言可以使用常量内存识别，因此它是正则语言。

接下来，我们定义 DFA 的转换函数：

该函数有两个参数：当前状态和下一个符号，并返回下一个状态。

正如我们之前看到的，死状态是一个汇点，因此它始终映射到自身。如果我们处于进位状态，并且加法器方程验证通过，那么下一个状态是持有进位值的进位状态。否则，我们进入死状态。

dfaStep 只是一个普通函数，我们可以执行，因此让我们做一个快速的正确性检查。

如果我们想确保这成立，我们可以将其转换为一个例子：

I recently worked through a problem from a theory of computation textbook that asked me to prove a property of a language using finite automata. The informal proof is a simple constructive proof where you build an automaton and show that it recognizes the language. This is kind of similar to program verification, so I thought it’d be interesting to see what it takes to formalize the proof. Lean is a good choice for this, because its Mathlib has all the theorems for the problem.

After finishing the formal proof, I decided to write it up, because I think it provides software engineers with good insight into what it takes to formally prove properties of a system.

I tried to make this post accessible. If you’re comfortable with a modern statically typed programming language (such as TypeScript or Rust), binary arithmetic, basic propositional logic, and inductive proofs, you should be able to follow along.

Feel free to skip to the next section if you’re comfortable with DFAs and regular languages.

Finite automata provide a theoretical model of computation with fixed memory. Besides theory, finite automata also have important practical applications. For example, finite automata are relevant for parsers and regular expressions, where a bug once took a significant portion of the internet down.

A deterministic finite automaton (DFA) is a machine with a fixed, finite set of states that reads its input one symbol at a time, left to right. With each symbol, it updates its state using a deterministic transition function. After the last symbol, the machine either sits in an accepting state (input is accepted) or not (input is rejected).

If you’ve ever written a simple regular expression like -?[0-9]+ , then you’ve constructed a DFA. This regex matches integer literals like 12 and -123 and the corresponding DFA looks like this (the arrows are annotated with the symbols that lead to the next state):

The set of input symbols to the machine is defined by the set Σ \Sigma Σ . In our regex example, Σ = { − , 0 , 1 , 2 , … , 9 } \Sigma = \left\{-, 0, 1, 2, \ldots, 9\right\} Σ = { − , 0 , 1 , 2 , … , 9 } .

A language is just a set of strings, also called words , and a language is called regular if some DFA accepts exactly the strings in it. Recognizing regular languages is the class of decision problems solvable with an amount of memory that does not grow with the input.

Regular languages have useful closure properties: the union and intersection of two regular languages are regular, and so are the complement and (important for us) the reversal of a regular language.

The standard way to prove that a language is regular is to build a DFA and show that it accepts exactly that language.

We can describe a language A A A with set-builder notation:

Σ ∗ \Sigma^{*} Σ ∗ means the set of strings that are created by all possible concatenations of symbols in Σ \Sigma Σ and P ( w ) P(w) P ( w ) is the condition that a string w w w must satisfy to be in the language.

Let’s apply this notation to our regex example: -?[0-9]+ . Then Σ ∗ \Sigma^{*} Σ ∗ contains strings like "" , "123" , "-111" , "2-625-" , etc. and P ( w ) P(w) P ( w ) can be defined as “ w w w is not empty and contains no negative sign, except that its first character may be a negative sign if w w w has at least two characters”.

The problem that we’re going to solve is from the Introduction to the Theory of Computation , 3rd ed. by Michael Sipser:

Σ 3 \Sigma_3 Σ 3 ​ is the set of all height-3 columns of 0s and 1s, so a string over Σ 3 \Sigma_3 Σ 3 ​ determines three rows of bits. Reading each row as a binary number, define

where P ( w ) P(w) P ( w ) is the proposition that the bottom row of w w w equals the sum of the top two rows.

Show that B B B is regular. (Hint: it is easier to work with B R B^{\mathcal{R}} B R .)

The problem defines an unusual alphabet. Instead of regular characters like [a-z] , the alphabet is made up of columns of three bits. So instead of a language that consists of strings like "apple" , "banana" , etc., the language consists of two-dimensional bit strings like

where the first column is the first “character” and so on.

The rule to decide whether a string is in the language is to add the first two rows of the string and check whether they match the third.

For example, the following string is in the language:

But the following string is not in the language:

While a language like this may look weird at first, it’s actually easy to recognize: we just need to check the equation

to determine whether a string is in the language. The challenge is that we need to do this with a fixed amount of memory for arbitrarily long strings.

The trick is to remember how you add numbers by hand: you work from the least significant digit to the most significant. The only thing you carry from one column to the next is the carry.

But a DFA reads left to right, and the problem presents the numbers most significant bit first. So we don’t recognize B B B directly. Instead we build a DFA to recognize its reversal B R B^{\mathcal{R}} B R , which consists of the strings of B B B written backwards, so the machine sees the least significant column first.

If we can build a DFA to recognize B R B^{\mathcal{R}} B R , then we can conclude that B R B^{\mathcal{R}} B R is a regular language. Since B R B^{\mathcal{R}} B R reversed is B B B , we can use the closure property of the reversal of regular languages to conclude that B B B is regular as well, which completes the solution.

When doing the arithmetic column-by-column, we compute the sum bit at each step with the adder equation :

where x i , y i x_i, y_i x i ​ , y i ​ are the addend bits, z i z_i z i ​ is the sum bit, i i i denotes the index of the current column, and c i n c_{\mathrm{in}} c in ​ is the input carry from the previous step. We compute the output carry, denoted c o u t c_{\mathrm{out}} c out ​ , for the next step as follows:

This means that there is a carry either if both addends are 1 \mathtt{1} 1 or there was an input carry and exactly one of the addends is 1 \mathtt{1} 1 . Note that a simpler way to compute c o u t c_{\mathrm{out}} c out ​ is to check if at least two of x i x_i x i ​ , y i y_i y i ​ and c i n c_{\mathrm{in}} c in ​ are 1 \mathtt{1} 1 (we’ll make use of this in the Lean proof).

With this in mind, here is the DFA that recognizes B R B^{\mathcal{R}} B R :

The arrows are annotated with the columns that lead from the input state to the output state. If the figure looks confusing at first, the following examples will hopefully make it clearer.

Let’s trace the first example from the problem through the DFA:

The DFA recognizes B R B^{\mathcal{R}} B R , so it reads the columns backwards. Unrolling the run gives a straight line with one state per step.

The run ends in carry 0 (the accepting state), so the reversed word is in B R B^{\mathcal{R}} B R . By the definition of B R B^{\mathcal{R}} B R , the original word is in B B B as well.

Note that the machine passes through the non-accepting carry 1 state twice. Had the word stopped after either of the first two columns, it would have been rejected. 1 + 1 = 0 \mathtt{1} + \mathtt{1} = \mathtt{0} 1 + 1 = 0 and 11 + 01 = 00 \mathtt{11} + \mathtt{01} = \mathtt{00} 11 + 01 = 00 are both wrong without somewhere to put the carry.

Now the second example, which should be rejected:

The first column is fine on its own ( 1 + 0 \mathtt{1} + \mathtt{0} 1 + 0 really is 1 \mathtt{1} 1 ) so the machine can’t tell anything is wrong yet. But the second column fails: with no carry pending, 0 + 0 \mathtt{0} + \mathtt{0} 0 + 0 must produce 0 \mathtt{0} 0 , but the bottom row claims 1 \mathtt{1} 1 . The run ends outside the accepting state, so the second example is rejected.

Note that since the dead state is a sink state, the string would get rejected even if there were more valid columns after the second column.

Our goal is to show that the language B B B from the problem is regular . As discussed earlier, in order to show that a language is regular, we need to build a DFA and show that it accepts the language.

The Lean proof will consist of three parts:

Lean’s Mathlib has first-class support for formal languages and DFAs, so we will just need to build on structures from the library for the specification and the implementation.

For the proof, we’ll have to do more work, but Mathlib will be helpful here as well. It contains the theorem that regular languages are closed under reversal, which will save a lot of work. The proof will contain some unfamiliar syntax, but under the hood it’s just a program. In fact, the proof is accepted if the program compiles.

Below is a figure laying out the components of the program. The full code can be found on GitHub .

The alphabet from the problem is made up of columns of three bits. We can represent one column with a tuple of three booleans in Lean:

Then we use Mathlib.Computability.Language to define B B B :

Language is a generic implementation of formal languages that comes with standard operations and associated theorems. We build it using our alphabet Sigma3 and the predicate for membership in B B B (recall that a language is a set of strings).

wBE is a candidate word, read big-endian, which is a list of Sigma3 values, i.e. a 2D list of binary values with three rows. rowNBE is a function that selects the nth row of the 2D list from the top and turns it into a natural number using a big-endian interpretation. 1 So the predicate is just

If you’ve used programming languages with set comprehensions, the set builder syntax might look familiar, but we’re not constructing a collection here. Language is just a Set under the hood and Set in Lean is a function that tests whether an element is in the set. 2 So our definition of B B B gets unrolled to a function definition under the hood:

The function has one argument of type List Sigma3 which is a generic list that holds Sigma3 objects. This is pretty standard so far, but the return type is more interesting. In a typical programming language, you’d expect a membership test to return a boolean. But the return type here is Prop which is the type of all propositions in Lean (a proposition is something that may or may not have a proof).

So how do membership tests work then? The expression wBE ∈ B applies the function to wBE , which gives back a proposition. In Lean a proposition is itself a type, and its values are proofs of the proposition. So instead of evaluating wBE ∈ B to a boolean, we prove it: to show that a word is in the language, we construct a value of the proposition’s type. And to show that a word isn’t in the language, we construct a value of the negated proposition. This way, a set membership test ends up being a type check, not a computation at runtime.

We first define the states of the DFA (carry 0, carry 1, dead) as a sum type:

We could define the same type using an enum in Rust or a discriminated union in TypeScript. Lean’s inductive type does a bit more than a recursive sum type in these languages, though: it also generates some scaffolding that makes it easy to use the type in proofs. We’ll see more of this later.

Now onto the derives. DecidableEq just says this type supports full equality checks (same as deriving Eq in Rust), but Fintype is something that’s only available in proof assistants. It says that the type has finitely many values and it creates a list of them plus a proof that the list is complete. Deriving Fintype lets us claim later on that the language can be recognized with constant memory, and therefore it’s regular.

Next, we define the transition function of the DFA:

The function has two arguments, the current state and the next symbol, and returns the next state.

As we saw earlier, the dead state is a sink, so it always maps to itself. If we’re in the carry state, and the adder equation checks out, then the next state is the carry state holding the value of the carry out. Otherwise we enter the dead state.

dfaStep is just a regular function that we can execute, so let’s run a quick sanity check.

If we want to make sure this holds, we can turn it into an example: