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: