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.

Background: DFAs & Regular Languages

Feel free to skip to thenext 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.

Deterministic Finite Automaton (DFA)

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):

This DFA has four states:

• Start: this is where we start before processing the first character. Since the start state is not an accepting state, we reject the empty string.
• Sign: we move to the sign state when we encounter the - character in the start state. We can skip the sign state and jump directly to digits from start, since the sign character is optional (-?). If we’re in this state at the end of the string, then we reject the string.
• Digits: we move from start or sign to digits when we encounter a digit character ([0-9]). If we’re in the digits state and encounter a digit character again, then we stay in the digits state. The digits state is the only accepting state of the DFA. If we’re in this state after we’ve processed the input string, then the DFA accepts the string.
• Dead: we get into this state if we encounter any other character than a digit (unless it’s a negative sign at the start). If we’re in the dead state at the end of the string, then the DFA rejects the string. Once we’re in the dead state, we stay in it, so the dead state in this DFA is a sink.

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}.

Regular Languages

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 AAA with set-builder notation:

A={ w∈Σ∗∣P(w) }A = \bigl\{\, w \in \Sigma^{*} \bigm| P(w) \,\bigr\}A={w∈Σ∗​P(w)}

Σ∗\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 www 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 “www is not empty and contains no negative sign, except that its first character may be a negative sign if www has at least two characters”.

The Problem

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

1.32 Let

Σ3={[000],[001],[010],…,[111]}.\Sigma_3 = \left\{ \begin{bmatrix}0\\0\\0\end{bmatrix}, \begin{bmatrix}0\\0\\1\end{bmatrix}, \begin{bmatrix}0\\1\\0\end{bmatrix}, \ldots, \begin{bmatrix}1\\1\\1\end{bmatrix} \right\}.Σ3​=⎩⎨⎧​​000​​,​001​​,​010​​,…,​111​​⎭⎬⎫​.

Σ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

B={ w∈Σ3∗∣P(w) }B = \bigl\{\, w \in \Sigma_3^{*} \bigm| P(w) \,\bigr\}B={w∈Σ3∗​​P(w)}

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

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

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

011
001
100

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:

011 # x row: first addend is 3 in decimal
001 # y row: second addend is 1 in decimal
100 # z row: sum is 4 which is equal to 3 + 1

But the following string is not in the language:

01 # x row: first addend is 1 in decimal
00 # y row: second addend is 0
11 # z row: sum is 3 which is not equal to 1 + 0

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

x+y=z x + y = zx+y=z

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 Solution

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 BBB directly. Instead we build a DFA to recognize its reversal BRB^{\mathcal{R}}BR, which consists of the strings of BBB written backwards, so the machine sees the least significant column first.

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

Adder Arithmetic

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

xi⊕yi⊕cin=zix_i \oplus y_i \oplus c_{\mathrm{in}} = z_ixi​⊕yi​⊕cin​=zi​

where xi,yix_i, y_ixi​,yi​ are the addend bits, ziz_izi​ is the sum bit, iii denotes the index of the current column, and cinc_{\mathrm{in}}cin​ is the input carry from the previous step. We compute the output carry, denoted coutc_{\mathrm{out}}cout​, for the next step as follows:

cout=(xi∧yi)∨(cin∧(xi⊕yi))c_{\mathrm{out}} = (x_i \wedge y_i) \vee \left( c_{\mathrm{in}} \wedge (x_i \oplus y_i) \right)cout​=(xi​∧yi​)∨(cin​∧(xi​⊕yi​))

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 coutc_{\mathrm{out}}cout​ is to check if at least two of xix_ixi​, yiy_iyi​ and cinc_{\mathrm{in}}cin​ are 1\mathtt{1}1 (we’ll make use of this in the Lean proof).

Adder DFA

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

The adder DFA has three states:

• Carry 0: We’re in this state if the carry is 0 before processing the next column. This is both the starting and the accepting state, since a leftover carry at the end would mean the sum overflowed the bottom row.
• Carry 1: We’re in this state if the carry is 1 before processing the next column. This state is non-accepting, since a word ending here has a carry left over, so the sum overflowed. But unlike the dead state we can still leave it, since a [001]\left[\begin{smallmatrix}\mathtt{0}\\\mathtt{0}\\\mathtt{1}\end{smallmatrix}\right][001​] column absorbs the pending carry and takes us back to carry 0.
• Dead: We end up in this state if the sum doesn’t match. This is a sink state, meaning we can never leave it.

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.

Example 1

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

011 # x row: 3 in decimal
001 # y row: 1 in decimal
100 # z row: 4 in decimal

The DFA recognizes BRB^{\mathcal{R}}BR, 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 BRB^{\mathcal{R}}BR. By the definition of BRB^{\mathcal{R}}BR, the original word is in BBB 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.

Example 2

Now the second example, which should be rejected:

01 # x row: 1 in decimal
00 # y row: 0 in decimal
11 # z row: 3 in decimal

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.

The Lean Proof

Our goal is to show that the language BBB 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:

1. A specification of the language BBB.
2. An executable implementation of the adder DFA.
3. A proof showing that the implementation matches the specification.

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 specification and the implementation meet in the proof

The Specification

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:

abbrev Sigma3 := Bool × Bool × Bool

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

def B : Language Sigma3 :=
  { wBE | row3BE wBE = row1BE wBE + row2BE wBE }

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 BBB (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

z=x+yz = x + yz=x+y

from our earlier examples.

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 BBB gets unrolled to a function definition under the hood:

def B : List Sigma3 → Prop :=
  fun wBE =>
      row3BE wBE = row1BE wBE + row2BE wBE

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.

The Implementation

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

inductive DFAState where
  | carry (c : Bool)
  | dead
  deriving DecidableEq, Fintype

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:

def dfaStep : DFAState → Sigma3 → DFAState
  | .dead, _ => .dead
  | .carry c, (x, y, z) =>
      if z = (x ^^ y ^^ c) then  -- ^^ is XOR
        .carry (Bool.atLeastTwo x y c)
      else
        .dead

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.

#eval dfaStep (.carry false) (true, true, false)
-- Prints: DFAState.carry true

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

example :
    dfaStep (.carry false) (true, true, false) = .carry true := by
  decide

The example : ... := by decide structure in Lean is kind of like a unit test, except it’s a proof that’s checked at compile time.

Finally, we use the generic Mathlib.Computability.DFA structure from Mathlib to complete the implementation. We give it the transition function and define the start and accept states:

def adderDFA : DFA Sigma3 DFAState where
  step := dfaStep
  start := .carry false
  accept := {.carry false}

DFA integrates with Mathlib.Computability.Language, which will make it easy to prove later on that our language is regular.

DFA also comes with evalFrom, which runs the machine step-by-step from a given starting state over a list of symbols. We can use it to evaluate Example 2 as a compile-time check:

example :
    adderDFA.evalFrom (.carry false)
      [(true, false, true), (false, false, true)] = .dead := by
  decide

The run starts from .carry false and ends in .dead as expected.

How Proofs Work

Before we dig into the proof of the solution in the next section, let’s review how proofs work in Lean using the dfaStep example:

example :
    dfaStep (.carry false) (true, true, false) = .carry true := by
  decide

The by keyword switches Lean into tactic mode which is an imperative way of generating proofs. decide is a tactic that proves a proposition by evaluating its decision procedure3 inside the type checker.4 It doesn’t actually run the compiled code, but for our purposes you can think of decide as proof by evaluation.

The proof generated by decide under the hood is equivalent to the following:5

abbrev StepEndsWithCarry : Prop :=
  dfaStep (.carry false) (true, true, false) = .carry true

example : StepEndsWithCarry :=
  (of_decide_eq_true (Eq.refl true))

Notice that there is no by after the := this time. This means that it’s a term mode proof where we have to construct a term whose type is the proposition to close the proof.

A term is a value of a type, just like 3 is a value of Nat which is the type of natural numbers. A proof of a proposition is a term whose type is that proposition, so writing the proof is like constructing a value of that type. In this view, a proposition is true when its type has at least one value, and false when it provably has none. A false proposition is like Rust’s empty enum or TypeScript’s never: since the type has no values, there is nothing you could write as a proof.

In the example above the proposition is StepEndsWithCarry and the term which serves as the proof is:

(of_decide_eq_true (Eq.refl true))

To understand the proof, we have to figure out why the type of this term is the proposition. of_decide_eq_true is a theorem from the standard library whose type is:

decide p = true → p

It states that if evaluating the decision procedure for proposition p returns true, then p holds. It’s a pretty nifty theorem that lets us prove a proposition by simply evaluating it (the proof of the theorem is beyond the scope of this post).

The arrow indicates that decide p = true → p is a function type with one argument of type decide p = true and the return type is p. So if we can pass an argument of type decide StepEndsWithCarry = true to of_decide_eq_true then we get ourselves a value of our proposition StepEndsWithCarry, which is a proof of the same proposition.

But how can we construct a term of type decide StepEndsWithCarry = true for of_decide_eq_true?

The answer is a bit convoluted. The argument we’re passing to of_decide_eq_true is Eq.refl true which has type true = true. At first glance, this has nothing to do with our proposition.

The magic happens when Lean checks true = true against decide StepEndsWithCarry = true. The type checker unfolds decide StepEndsWithCarry, which evaluates dfaStep and compares the result to .carry true, and this reduces to true.

Lean considers two types equal if they reduce to the same term, so decide StepEndsWithCarry = true and true = true are the same type, and Eq.refl true is accepted as a proof of both.

And now back to our regular programming.

The Proof

As discussed earlier, in order to prove that the language BBB is regular, we need to first show that the adder DFA accepts the reverse of the language, BRB^{\mathcal{R}}BR. We can then use the closure property of the reversal of regular languages to prove that BBB is regular. This is readily available as a theorem from Mathlib, but we’ll have to do some work to show that the adder DFA recognizes BRB^{\mathcal{R}}BR.

Mathlib’s definition of regular languages boils down to this:6

def IsRegular (L : Language T) : Prop :=
  ∃ σ [Fintype σ], ∃ M : DFA T σ, M.accepts = L

The (L : Language T) argument means that the language can have any type of symbols. The return type is again Prop.

∃ σ [Fintype σ] says that there is a finite number of states. The interesting part is ∃ M : DFA T σ, M.accepts = L, which says that L is regular if some DFA over those states accepts exactly L. So when does a DFA accept a language?

The language a DFA accepts in Mathlib is defined like this:7

def accepts : Language T :=
  { word | M.evalFrom M.start word ∈ M.accept }

This means that the language that the DFA accepts is the set of words for which evaluating the DFA from the starting state leads to an accepting state.

Our job is now to prove that adderDFA.accepts and B.reverse are the same set. This is formalized in our proof as follows:

theorem adderDFA_accepts_B_reverse : adderDFA.accepts = B.reverse := by
  ...

The way we’re going to prove this is by showing that the adder DFA computes the same equation that is the membership check for B.reverse which is defined as follows:

B.reverse = { w | w.reverse ∈ B }

B reads its rows most significant bit first with the rowNBE functions. Reading the reversed string big-endian is the same as reading the original string least significant bit first. In other words, while we interpret bit strings big-endian for B, we interpret them as little-endian for B.reverse. The membership test for B.reverse is therefore equivalent to:8

{ wLE | row1LE wLE + row2LE wLE = row3LE wLE }

The challenge in proving adderDFA_accepts_B_reverse is that the language definition states one equation about the whole word, while the adder DFA works one column at a time.

Run Invariant

The DFA has finitely many states, but it can process arbitrarily long strings. The natural way to prove properties of such a process is by induction.

In order to prove a proposition by induction we need an induction hypothesis that holds for all steps. One idea for the induction hypothesis could be to propose the following equivalence

adderDFA.evalFrom (.carry false) wLE = .carry false ↔
  row1LE wLE + row2LE wLE = row3LE wLE

which reads as

Running the adder DFA over a (little-endian) word www (wLE in the code) starting with carry 0 ends in state carry 0 if and only if

row1(w)+row2(w)=row3(w)\mathrm{row}_1(w) + \mathrm{row}_2(w) = \mathrm{row}_3(w)row1​(w)+row2​(w)=row3​(w)

where the rows are read as little-endian binary numbers.

This is what we need ultimately. We always start from carry 0 and the only accepting state is also carry 0, and the right-hand side of the equivalence matches the membership test for B.reverse. But as we saw earlier, carry 1 can be a valid intermediate state as well, so this statement is too weak to serve as an induction hypothesis.

We cannot restrict our induction hypothesis to a certain carry value, but we still need to establish a connection between carry in and carry out. We can accomplish this by extending the right-hand side of the equivalence to include cinc_{\mathrm{in}}cin​ and coutc_{\mathrm{out}}cout​ terms:

row1LE wLE + row2LE wLE + carryIn =
  row3LE wLE + carryOut * 2 ^ wLE.length

Or with mathematical notation to make it easy to see that it’s just the definition of binary addition:

∑i=0n−1xi2i+∑i=0n−1yi2i+cin=∑i=0n−1zi2i+cout⋅2n\sum_{i=0}^{n-1} x_i 2^i + \sum_{i=0}^{n-1} y_i 2^i + c_{\mathrm{in}} = \sum_{i=0}^{n-1} z_i 2^i + c_{\mathrm{out}} \cdot 2^ni=0∑n−1​xi​2i+i=0∑n−1​yi​2i+cin​=i=0∑n−1​zi​2i+cout​⋅2n

The full equivalence now becomes

adderDFA.evalFrom (.carry carryIn) wLE = .carry carryOut ↔
  row1LE wLE + row2LE wLE + carryIn =
    row3LE wLE + carryOut * 2 ^ wLE.length

which reads as

Running the adder DFA over a (little-endian) word www (wLE in the code) starting with carry cinc_{\mathrm{in}}cin​ ends in state coutc_{\mathrm{out}}cout​ if and only if

row1(w)+row2(w)+cin=row3(w)+cout⋅2∣w∣\mathrm{row}_1(w) + \mathrm{row}2(w) + c{\mathrm{in}} = \mathrm{row}3(w) + c{\mathrm{out}} \cdot 2^{|w|}row1​(w)+row2​(w)+cin​=row3​(w)+cout​⋅2∣w∣

where the rows are read as little-endian binary numbers.

With both carries set to 0, this is equivalent to our first attempt. But it holds for intermediate steps as well, where both carry in and carry out may be non-zero.

Run Invariant Proof

Here is the run invariant as a theorem, with the proof left out for now:

def RunEndsWithCarry (carryIn : Bool) (wLE : List Sigma3)
    (carryOut : Bool) : Prop :=
  adderDFA.evalFrom (.carry carryIn) wLE = .carry carryOut

def WordAddsWithCarry (carryIn : Bool) (wLE : List Sigma3)
    (carryOut : Bool) : Prop :=
  row1LE wLE + row2LE wLE + carryIn.toNat
    = row3LE wLE + carryOut.toNat * 2 ^ wLE.length

lemma run_invariant (wLE : List Sigma3) (carryIn carryOut : Bool) :
    RunEndsWithCarry carryIn wLE carryOut ↔
      WordAddsWithCarry carryIn wLE carryOut := by
  ...

Both sides of the equivalence get their own name, so that the lemma reads as “the run from carryIn ends in carryOut if and only if the word adds up with these carries”. RunEndsWithCarry and WordAddsWithCarry are definitions whose type is Prop, so they’re statements rather than values. RunEndsWithCarry is the left-hand side of the equivalence from the previous section, and WordAddsWithCarry is the right-hand side. The only difference from that equation is .toNat, which converts a boolean into 0 or 1 so that the carries can take part in the arithmetic (.toNat will be omitted in the following code blocks for brevity).

Notice that the theorem has arguments like a function. In fact, a theorem is essentially a function: its arguments are the variables the statement talks about, its type is the proposition, and its body is the proof. So we have a parameterized theorem that we’ll have to prove for all possible values of its arguments. But we will only use it later on in the proof of adderDFA_accepts_B_reverse with both carries set to false, which corresponds to the membership test for B.reverse:

run_invariant (carryIn := false) wLE (carryOut := false)

The proof is by induction on the word wLE which has type List Sigma3. Induction on a list requires proving the statement for the empty list, and then proving that if it holds for some list, it also holds for that list with one more element added to the front. Since every list can be built from the empty list by adding elements to the front, these two steps cover all lists.

  induction wLE generalizing carryIn with
  | nil => ...
  | cons column columnsLE induction_hypothesis => ...

Lean in tactic mode works by creating goals that need to be proved. A goal is a statement that Lean still needs a proof of. Each tactic transforms or closes the current goal.

The initial goal is the theorem that we’re trying to prove, but we cannot prove it directly, so we use the induction tactic which gives us a goal to prove for each constructor of the list. nil is the constructor for the empty list, and cons is the constructor that prepends an element to an existing list. In the cons case we get to name the first column, the remaining columns, and the induction hypothesis, which is the run invariant assumed to be true for the remaining columns.

The generalizing carryIn part is important. Without it, the induction hypothesis would only talk about runs that start with the same carryIn as the run we are looking at. But in the inductive step we peel off the first column. The run over the remaining columns then starts with the carry that the first column produced, which is not necessarily the same value that carryIn had. generalizing makes the induction hypothesis hold for every starting carry. The ending carry is the same for the whole run, so carryOut can stay fixed.

Base Case

Let’s have a look at the proof of the base case (when the DFA is running over an empty word). Recall the run invariant:

RunEndsWithCarry carryIn wLE carryOut ↔
  WordAddsWithCarry carryIn wLE carryOut

Let’s focus on what happens on the left-hand side of the equivalence first. Unfolding RunEndsWithCarry gives:

adderDFA.evalFrom (.carry carryIn) wLE = .carry carryOut

DFA.evalFrom is defined in Mathlib as follows:

def evalFrom (s : σ) : List T → σ :=
  List.foldl M.step s

List.foldl just returns the initial value if the input list is empty, and the initial value we provide to DFA.evalFrom is .carry carryIn, so in the base case we have

.carry carryIn = .carry carryOut

on the left-hand side of the equivalence.

Next, let’s see what happens on the right-hand side in the base case. Unfolding WordAddsWithCarry gives the equation:

row1LE wLE + row2LE wLE + carryIn =
  row3LE wLE + carryOut * 2 ^ wLE.length

rowNLE returns 0 for the empty list, so we have

0 + 0 + carryIn = 0 + carryOut * 2 ^ 0

or simply

carryIn = carryOut

So in the base case we need to prove that

.carry carryIn = .carry carryOut ↔
  carryIn = carryOut

Since there are only four cases, we can prove this by exhaustion. The equivalence holds if both sides have the same truth value in every row of the table:

carryIn| carryOut| .carry carryIn =

The same argument in Lean:

lemma run_invariant (wLE : List Sigma3) (carryIn carryOut : Bool) :
    RunEndsWithCarry carryIn wLE carryOut ↔
      WordAddsWithCarry carryIn wLE carryOut := by
  induction wLE generalizing carryIn with
  -- base case
  | nil =>
    unfold RunEndsWithCarry WordAddsWithCarry
    revert carryIn carryOut
    decide
  -- inductive step
  | cons column columnsLE induction_hypothesis => ...

We let decide check the four rows of the table, like it checked the single dfaStep step in How Proofs Work, but it needs two things set up first.

decide cannot see through a definition on its own, so unfold RunEndsWithCarry WordAddsWithCarry replaces the two names with their definitions. decide also needs a proposition without free variables, but carryIn and carryOut are arguments of the lemma. revert carryIn carryOut moves them back into the goal, which is now a statement about all values of both carries:

∀ carryOut carryIn : Bool,
  adderDFA.evalFrom (.carry carryIn) [] = .carry carryOut ↔
    row1LE [] + row2LE [] + carryIn =
      row3LE [] + carryOut * 2 ^ [].length

A statement about all values of finitely many booleans is decidable, so decide evaluates both sides of the equivalence for each of the four rows and closes the goal because they always agree.

Inductive Step

Recall that in the inductive step we need to prove that, if the invariant holds for some list, then it also holds for that list with one more element added to the front.

In the inductive step, the word is cons column columnsLE which is the list created by prepending column to columnsLE. Lean has an infix operator :: for prepending to a list, so we can write column :: columnsLE.

The induction hypothesis holds by assumption for columnsLE, but we need to prove the invariant for the whole word. We’ll do this by introducing an intermediate carry after the first step of the DFA that runs on the first column (which is the least significant column of the word). Then we rearrange the equation from WordAddsWithCarry to show that the arithmetic checks out.

These are the high-level steps:

1. On the DFA side, split the run into its first step and the run over the remaining columns and join them with an intermediate carry.
2. Turn the first step of the DFA into arithmetic. This is the adder equation for a single column.
3. Turn the run over the remaining columns into arithmetic using the induction hypothesis.
4. On the arithmetic side, show that the equation for the whole word splits into the equation for the least significant bit and the equation for the remaining bits.

The DFA side and the arithmetic side meet in the inductive step

After these steps the two sides of the equivalence say the same thing, which closes the goal. Steps 1, 2 and 4 each get their own helper lemma, so let’s look at those first.

Splitting the Run

lemma split_run (column : Sigma3) (columnsLE : List Sigma3)
    (carryIn carryOut : Bool) :
    RunEndsWithCarry carryIn (column :: columnsLE) carryOut ↔
      ∃ carryMid,
        dfaStep (.carry carryIn) column = .carry carryMid ∧
        RunEndsWithCarry carryMid columnsLE carryOut := by
    ...

This is step 1 of the plan. The lemma says that a run over the word in the inductive step (column :: columnsLE) ends in carryOut if and only if there is an intermediate carry carryMid with two properties. The first column takes the DFA to carryMid, and the rest of the run from carryMid ends in carryOut.

As a reminder, the definition of RunEndsWithCarry is:

def RunEndsWithCarry (carryIn : Bool) (wLE : List Sigma3)
    (carryOut : Bool) : Prop :=
  adderDFA.evalFrom (.carry carryIn) wLE = .carry carryOut

so unfolding RunEndsWithCarry leaves us with the following goal:

adderDFA.evalFrom (.carry carryIn) (column :: columnsLE) =
    .carry carryOut ↔
  ∃ carryMid,
    dfaStep (.carry carryIn) column = .carry carryMid ∧
    adderDFA.evalFrom (.carry carryMid) columnsLE = .carry carryOut

We’re going to prove this by rewriting both sides to be the same statement. We’ll run through the informal argument first and then we’ll have a look at how it’s formalized in Lean.

First, we split the left-hand side into a single step on the first column followed by a run over columnsLE from the state that the step lands in:

adderDFA.evalFrom (dfaStep (.carry carryIn) column) columnsLE =
    .carry carryOut ↔
  ∃ carryMid,
    dfaStep (.carry carryIn) column = .carry carryMid ∧
    adderDFA.evalFrom (.carry carryMid) columnsLE = .carry carryOut

Below is a visual representation of the split:

The run over the whole word is a single step on the first column followed by a run over the rest

We now have dfaStep (.carry carryIn) column on both sides of the equivalence. Next, let’s assume that the first step on column ends in a carry state c. Then we have

adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut ↔
  ∃ carryMid,
    .carry c = .carry carryMid ∧
    adderDFA.evalFrom (.carry carryMid) columnsLE = .carry carryOut

The right-hand side of the equivalence is only true if c = carryMid, therefore we can drop the existential and the first conjunct and rewrite it as

adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut ↔
    adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut

which matches the left-hand side exactly.

So far we have assumed that dfaStep (.carry carryIn) column ends up in a carry state c, but the step on the column can also end up in a dead state. The right-hand side is explicitly only true if the first step ends in a carry state, but the left-hand side could potentially allow a dead state on the first step. Except we know that the dead state is a sink (a run starting in a dead state ends in a dead state) which makes the left-hand side false too. Both sides are false, so the equivalence holds, which concludes the proof.

Now let’s review what the proof looks like in Lean:

lemma split_run (column : Sigma3) (columnsLE : List Sigma3)
    (carryIn carryOut : Bool) :
    RunEndsWithCarry carryIn (column :: columnsLE) carryOut ↔
      ∃ carryMid,
        dfaStep (.carry carryIn) column = .carry carryMid ∧
        RunEndsWithCarry carryMid columnsLE carryOut := by
  simp only [RunEndsWithCarry, DFA.evalFrom_cons, adderDFA_step]
  cases dfaStep (.carry carryIn) column with
  | dead =>
    rw [dead_state_is_sink]
    simp
  | carry c =>
    simp only [DFAState.carry.injEq, exists_eq_left']

simp is one of the most commonly used tactics in Lean. It rewrites the goal using a database of simplification rules plus the definitions and lemmas that we pass to it in the square brackets. It closes the goal if the goal ends up as something trivially true. simp only restricts simp to the listed lemmas instead of its whole default set, which keeps the goal predictable.

The first simp only line rewrites the lemma to a form with dfaStep on both sides of the equivalence:

adderDFA.evalFrom (dfaStep (.carry carryIn) column) columnsLE =
    .carry carryOut ↔
  ∃ carryMid,
    dfaStep (.carry carryIn) column = .carry carryMid ∧
    adderDFA.evalFrom (.carry carryMid) columnsLE = .carry carryOut

The cases tactic splits a goal into one goal per constructor of a type. Here cases dfaStep (.carry carryIn) column introduces two new goals: one where the first step on the column ends up in the dead state and one where it ends up in a carry state.

The dead state case is proved with a helper lemma that we’re going to skip over here as it follows directly from our definition of dfaStep.

In the carry case c is introduced as the carry value from the first step on the column:

cases dfaStep (.carry carryIn) column with
| dead => ...
| carry c =>
  simp only [DFAState.carry.injEq, exists_eq_left']

Which leaves us with the following goal:

adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut ↔
  ∃ carryMid,
    .carry c = .carry carryMid ∧
    adderDFA.evalFrom (.carry carryMid) columnsLE = .carry carryOut

Earlier we took it for granted that .carry c = .carry carryMid implies c = carryMid, but we need a formal argument for this now. Luckily constructors like DFAState.carry are injective in Lean, meaning that if two values built with the same constructor are equal, then their arguments are equal. This useful fact is provided by the automatically generated DFAState.carry.injEq theorem which simp uses to pull c and carryMid out of the .carry constructor:

adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut ↔
  ∃ carryMid,
    c = carryMid ∧
    adderDFA.evalFrom (.carry carryMid) columnsLE = .carry carryOut

Then we use the theorem exists_eq_left' from the standard library to close the goal. The theorem states (∃ a, a' = a ∧ p a) ↔ p a' which lets us substitute carryMid with c and drop the existential and the first conjunct:

adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut ↔
    adderDFA.evalFrom (.carry c) columnsLE = .carry carryOut

Both sides of the equivalence are the same now, so simp closes this goal by itself, which concludes the proof.

First Step Adds

lemma first_step_adds (x y z carryIn carryOut : Bool) :
    dfaStep (.carry carryIn) (x, y, z) = .carry carryOut ↔
      x + y + carryIn = z + 2 * carryOut := by
  ...

This is step 2 of the plan. The lemma says that a single step of the DFA on the column (x, y, z) takes the state carryIn to the state carryOut if and only if

x+y+cin=z+2⋅coutx + y + c_{\mathrm{in}} = z + 2 \cdot c_{\mathrm{out}}x+y+cin​=z+2⋅cout​

which is just the adder arithmetic from earlier in a single equation.9

We need this lemma to turn the first step of the run, which split_run separated from the rest, from a statement about the DFA into arithmetic. We’re going to prove it by unfolding the definition of dfaStep and then checking every combination of values for the five booleans.

As a reminder, the definition of dfaStep is:

def dfaStep : DFAState → Sigma3 → DFAState
  | .dead, _ => .dead
  | .carry c, (x, y, z) =>
      if z = (x ^^ y ^^ c) then  -- ^^ is XOR
        .carry (Bool.atLeastTwo x y c)
      else
        .dead

The state that we start from is a carry state, so the second branch applies and unfolding dfaStep leaves us with the following goal:

(if z = (x ^^ y ^^ carryIn) then
    .carry (Bool.atLeastTwo x y carryIn)
 else
    .dead) = .carry carryOut ↔
  x + y + carryIn = z + 2 * carryOut

The left-hand side of the equivalence says that the sum bit checks out and that the carry out is true exactly when at least two of x, y and carryIn are true. The right-hand side says the same thing with arithmetic on natural numbers.

Both sides are fixed formulas over five booleans which yields only 32 combinations, so we can check all of them by exhaustion like we did in the base case. The equivalence holds if both sides have the same truth value in every row of the truth table.

Let’s review two of the 32 cases before we look at the Lean proof. Take the row where x, y and carryOut are true and z and carryIn are false. This is the same as our dfaStep example from earlier:

Substituting the values gives:

(if false = (true ^^ true ^^ false) then
    .carry (Bool.atLeastTwo true true false)
 else
    .dead) = .carry true ↔
  1 + 1 + 0 = 0 + 2 * 1

true ^^ true ^^ false evaluates to false, so the condition holds and the step takes the first branch. Two of x, y and carryIn are true, so the step lands in .carry true:

.carry true = .carry true ↔
  1 + 1 + 0 = 0 + 2 * 1

Both sides are true, so this row holds.

Now take a row where the column doesn’t add up: x, y, z and carryOut are true and carryIn is false.

This time the condition is true = (true ^^ true ^^ false), which is true = false, so the step takes the second branch and lands in the dead state:

.dead = .carry true ↔
  1 + 1 + 0 = 1 + 2 * 1

The left-hand side is false because .dead and .carry true are different states. The right-hand side is false because 2 is not 3. Both sides are false, so this row holds too.

The remaining 30 rows go the same way: either the column adds up and both sides are true, or it doesn’t and both sides are false. This concludes the proof.

Now let’s review what the proof looks like in Lean:

lemma first_step_adds (x y z carryIn carryOut : Bool) :
    dfaStep (.carry carryIn) (x, y, z) = .carry carryOut ↔
      x + y + carryIn = z + 2 * carryOut := by
  revert x y z carryIn carryOut
  decide

This is the same recipe as the base case of the run invariant. revert moves the five boolean arguments back into the goal, so the goal becomes:

∀ x y z carryIn carryOut : Bool,
  dfaStep (.carry carryIn) (x, y, z) = .carry carryOut ↔
    x + y + carryIn = z + 2 * carryOut

decide then evaluates both sides of the equivalence for each of the 32 combinations.

Least Significant Bit Split

def WholeRunAddition (x y z carryIn : Bool) (a b d k : Nat) : Prop :=
  (x + 2 * a) + (y + 2 * b) + carryIn
    = (z + 2 * d) + 2 * k

def SplitRunAddition (x y z carryIn : Bool) (a b d k : Nat) : Prop :=
  ∃ carryMid : Bool,
    x + y + carryIn = z + 2 * carryMid ∧
    a + b + carryMid = d + k

lemma least_significant_bit_split
    (x y z carryIn : Bool) (a b d k : Nat) :
    WholeRunAddition x y z carryIn a b d k ↔
      SplitRunAddition x y z carryIn a b d k := by
  ...

This is step 4 of the plan. As with the run invariant, both sides of the equivalence get their own name to make it easier to read. WholeRunAddition is the addition equation for the whole word, and SplitRunAddition is the same equation split in two.

The lemma says that the addition equation for the whole word holds if and only if there is an intermediate carry carryMid such that the adder equation holds for the least significant bits and the addition equation holds for the remaining bits.10 The shape of this lemma mirrors split_run, but it’s just arithmetic, the DFA doesn’t appear in it.

We need this lemma to connect the two sides of the run invariant: split_run, first_step_adds and the induction hypothesis turn the DFA into an equation for the first column and an equation for the remaining columns. This lemma shows that together they say the same thing as the equation for the whole word.

We’re going to use mathematical notation as we break down this lemma, because the arithmetic is easier to follow this way. Unfolding WholeRunAddition and SplitRunAddition leaves us with the following goal:

(x+2⋅a)+(y+2⋅b)+cin=(z+2⋅d)+2⋅k ⟺ ∃ cmid: x+y+cin=z+2⋅cmid ∧∃ cmid: a+b+cmid=d+k\begin{aligned} &(x + 2 \cdot a) + (y + 2 \cdot b) + c_{\mathrm{in}} = (z + 2 \cdot d) + 2 \cdot k \iff \\ &\qquad \exists\, c_{\mathrm{mid}} :\; x + y + c_{\mathrm{in}} = z + 2 \cdot c_{\mathrm{mid}} \;\land \\ &\qquad \phantom{\exists\, c_{\mathrm{mid}} :\;} a + b + c_{\mathrm{mid}} = d + k \end{aligned}​(x+2⋅a)+(y+2⋅b)+cin​=(z+2⋅d)+2⋅k⟺∃cmid​:x+y+cin​=z+2⋅cmid​∧∃cmid​:a+b+cmid​=d+k​

xxx, yyy and zzz are the least significant bits of the three rows, aaa, bbb and ddd are the values of the remaining bits, and kkk stands for the carry out term of the remaining bits.

The equations of the lemma laid out as a run, least significant bits first

As a reminder, the addition equation from the run invariant is:

∑i=0n−1xi2i+∑i=0n−1yi2i+cin=∑i=0n−1zi2i+cout⋅2n\sum_{i=0}^{n-1} x_i 2^i + \sum_{i=0}^{n-1} y_i 2^i + c_{\mathrm{in}} = \sum_{i=0}^{n-1} z_i 2^i + c_{\mathrm{out}} \cdot 2^ni=0∑n−1​xi​2i+i=0∑n−1​yi​2i+cin​=i=0∑n−1​zi​2i+cout​⋅2n

The x+2⋅ax + 2 \cdot ax+2⋅a term comes from splitting

∑i=0n−1xi2i=x0+2⋅∑i=1n−1xi2i−1\sum_{i=0}^{n-1} x_i 2^i = x_0 + 2 \cdot \sum_{i=1}^{n-1} x_i 2^{i-1}i=0∑n−1​xi​2i=x0​+2⋅i=1∑n−1​xi​2i−1

so x+2⋅ax + 2 \cdot ax+2⋅a is the value of a row whose first bit is xxx and whose remaining bits have value aaa (the same applies to terms with yyy and zzz).

kkk stands for the carry out term of the remaining bits, which is cout⋅2n−1c_{\mathrm{out}} \cdot 2^{n-1}cout​⋅2n−1, so the carry out term of the whole word, cout⋅2nc_{\mathrm{out}} \cdot 2^ncout​⋅2n, is 2⋅k2 \cdot k2⋅k. Notice how WholeRunAddition has a 2⋅k2 \cdot k2⋅k term in it while SplitRunAddition has just kkk in the equation for the remaining bits. This is because the word in WholeRunAddition is one bit longer than the remaining bits in SplitRunAddition.

Circling back to our goal, we need to show that WholeRunAddition and SplitRunAddition are saying the same thing. WholeRunAddition is a simple linear equation, but SplitRunAddition has an existential and a conjunction. If we can turn SplitRunAddition into a linear equation, then we can close the goal by showing that the two linear equations are equivalent which is easy.

We’re going to use the same trick that we used when splitting the run. If the first part of the conjunction is only true for a single value of cmidc_{\mathrm{mid}}cmid​, we can substitute that value in the second conjunct. Then we can drop the existential and the first conjunct. As a reminder, this is the first conjunct:

∃ cmid: x+y+cin=z+2⋅cmid\exists\, c_{\mathrm{mid}} :\; x + y + c_{\mathrm{in}} = z + 2 \cdot c_{\mathrm{mid}}∃cmid​:x+y+cin​=z+2⋅cmid​

The equation involves the four boolean arguments of the lemma and cmidc_{\mathrm{mid}}cmid​ which means that once we fix the four booleans, cmidc_{\mathrm{mid}}cmid​ is the only unknown left in it. So we’re going to check every combination of the four booleans like we did in the base case, which gives 16 cases, and solve the equation for cmidc_{\mathrm{mid}}cmid​ in each of them.

If there is a solution, SplitRunAddition turns into a linear equation, and we’ll rearrange it to show that it’s the same equation as WholeRunAddition. If there is no solution, SplitRunAddition is false, and we’ll show that WholeRunAddition is false too.

Let’s work through an example of each kind before we look at the Lean proof.

First, consider the case where xxx and yyy are 111 and zzz and cinc_{\mathrm{in}}cin​ are 000. This is again the column where 1+1=01 + 1 = 01+1=0 with cout=1c_{\mathrm{out}} = 1cout​=1.

The equation for the whole word is an equation for the least significant bits followed by an equation for the rest

Substituting the values gives:

(1+2⋅a)+(1+2⋅b)+0=(0+2⋅d)+2⋅k ⟺ ∃ cmid: 1+1+0=0+2⋅cmid ∧∃ cmid: a+b+cmid=d+k\begin{aligned} &(\colorbox{#fff2a8}{$\displaystyle 1$} + 2 \cdot a) + (\colorbox{#fff2a8}{$\displaystyle 1$} + 2 \cdot b) + \colorbox{#fff2a8}{$\displaystyle 0$} = (\colorbox{#fff2a8}{$\displaystyle 0$} + 2 \cdot d) + 2 \cdot k \iff \\ &\qquad \exists\, c_{\mathrm{mid}} :\; \colorbox{#fff2a8}{$\displaystyle 1 + 1 + 0$} = \colorbox{#fff2a8}{$\displaystyle 0$} + 2 \cdot c_{\mathrm{mid}} \;\land \\ &\qquad \phantom{\exists\, c_{\mathrm{mid}} :\;} a + b + c_{\mathrm{mid}} = d + k \end{aligned}​(1​+2⋅a)+(1​+2⋅b)+0​=(0​+2⋅d)+2⋅k⟺∃cmid​:1+1+0​=0​+2⋅cmid​∧∃cmid​:a+b+cmid​=d+k​

On the right-hand side, the least significant bit equation is now 2=2⋅cmid2 = 2 \cdot c_{\mathrm{mid}}2=2⋅cmid​. The only value that satisfies it is cmid=1c_{\mathrm{mid}} = 1cmid​=1, so we can drop the existential and substitute 111 for cmidc_{\mathrm{mid}}cmid​:

(1+2⋅a)+(1+2⋅b)+0=(0+2⋅d)+2⋅k ⟺ a+b+1=d+k\begin{aligned} &(1 + 2 \cdot a) + (1 + 2 \cdot b) + 0 = (0 + 2 \cdot d) + 2 \cdot k \iff \\ &\qquad a + b + \colorbox{#fff2a8}{$\displaystyle 1$} = d + k \end{aligned}​(1+2⋅a)+(1+2⋅b)+0=(0+2⋅d)+2⋅k⟺a+b+1​=d+k​

On the left-hand side, every term is now even. Collecting the constants gives 2+2⋅a+2⋅b=2⋅d+2⋅k2 + 2 \cdot a + 2 \cdot b = 2 \cdot d + 2 \cdot k2+2⋅a+2⋅b=2⋅d+2⋅k, and dividing both sides by two gives:

1+a+b=d+k ⟺ a+b+1=d+k\begin{aligned} &\colorbox{#fff2a8}{$\displaystyle 1 + a + b = d + k$} \iff \\ &\qquad a + b + 1 = d + k \end{aligned}​1+a+b=d+k​⟺a+b+1=d+k​

Both sides say the same thing, so the case holds.

Now take a case where the column doesn’t add up: xxx is 111 and yyy, zzz and cinc_{\mathrm{in}}cin​ are 000.

The same split in a case where the column doesn't add up

Substituting the values gives:

(1+2⋅a)+(0+2⋅b)+0=(0+2⋅d)+2⋅k ⟺ ∃ cmid: 1+0+0=0+2⋅cmid ∧∃ cmid: a+b+cmid=d+k\begin{aligned} &(\colorbox{#fff2a8}{$\displaystyle 1$} + 2 \cdot a) + (\colorbox{#fff2a8}{$\displaystyle 0$} + 2 \cdot b) + \colorbox{#fff2a8}{$\displaystyle 0$} = (\colorbox{#fff2a8}{$\displaystyle 0$} + 2 \cdot d) + 2 \cdot k \iff \\ &\qquad \exists\, c_{\mathrm{mid}} :\; \colorbox{#fff2a8}{$\displaystyle 1 + 0 + 0$} = \colorbox{#fff2a8}{$\displaystyle 0$} + 2 \cdot c_{\mathrm{mid}} \;\land \\ &\qquad \phantom{\exists\, c_{\mathrm{mid}} :\;} a + b + c_{\mathrm{mid}} = d + k \end{aligned}​(1​+2⋅a)+(0​+2⋅b)+0​=(0​+2⋅d)+2⋅k⟺∃cmid​:1+0+0​=0​+2⋅cmid​∧∃cmid​:a+b+cmid​=d+k​

This time the least significant bit equation is 1=2⋅cmid1 = 2 \cdot c_{\mathrm{mid}}1=2⋅cmid​. No value of cmidc_{\mathrm{mid}}cmid​ satisfies it since the left-hand side is odd and the right-hand side is even, so the right-hand side of the equivalence is false. The left-hand side of the equivalence is

1+2⋅a+2⋅b=2⋅d+2⋅k1 + 2 \cdot a + 2 \cdot b = 2 \cdot d + 2 \cdot k1+2⋅a+2⋅b=2⋅d+2⋅k

which is also odd on one side and even on the other, so it’s false as well. Both sides are false, so the case holds.

Each of the remaining 14 cases is of one of these two kinds. If the sum of xxx, yyy and cinc_{\mathrm{in}}cin​ has the same parity as zzz, exactly one cmidc_{\mathrm{mid}}cmid​ satisfies the least significant bit equation and the rest of the equation matches once we divide by two. If the parities differ, both sides are false. This concludes the proof.

The second kind of case is how the dead state shows up on the arithmetic side. On the DFA side, a column with the wrong parity sends the run into the dead state, so it never ends in a carry state. On the arithmetic side, the same column makes both sides of the equivalence false, so we don’t need a separate case for it.

Now let’s review what the proof looks like in Lean:

lemma least_significant_bit_split
    (x y z carryIn : Bool) (a b d k : Nat) :
    WholeRunAddition x y z carryIn a b d k ↔
      SplitRunAddition x y z carryIn a b d k := by
  cases x <;> cases y <;> cases z <;> cases carryIn <;>
    simp [WholeRunAddition, SplitRunAddition] <;>
    omega

The <;> combinator runs the tactic on its right on every goal produced by the tactic on its left. So cases x <;> cases y splits the goal on x and then splits each of the two resulting goals on y, and the chain of four cases gives 16 goals, one per combination of the four bits. simp then runs on each of them, and omega runs on whatever simp leaves behind.

We won’t go through the steps simp performs here, since we’ve seen it in action before. simp leaves one goal behind in each of the 16 cases. Each of these cases takes the shape of one of the two examples that we worked through.

If there is a solution for carryMid, simp leaves an equivalence of two linear equations. This is the goal for the first example from above:

1+2⋅a+(1+2⋅b)=2⋅d+2⋅k ⟺ a+b+1=d+k\begin{aligned} 1 + 2 \cdot a + (1 + 2 \cdot b) &= 2 \cdot d + 2 \cdot k \iff \\ a + b + 1 &= d + k \end{aligned}1+2⋅a+(1+2⋅b)a+b+1​=2⋅d+2⋅k⟺=d+k​

If there is no solution for carryMid, SplitRunAddition is false, and p ↔ False is the same as ¬p, so simp leaves the negation of WholeRunAddition. This is the goal for the second example from above:

¬ (1+2⋅a+2⋅b=2⋅d+2⋅k)\neg\,(1 + 2 \cdot a + 2 \cdot b = 2 \cdot d + 2 \cdot k)¬(1+2⋅a+2⋅b=2⋅d+2⋅k)

simp can’t go further, because it is a rewriting engine, not an arithmetic solver. It won’t notice that one equation is the other multiplied by two, or that an odd number can’t equal an even one. This is where omega comes in, which is a decision procedure for linear arithmetic over natural numbers and integers.

omega proves a goal by contradiction: it assumes that the goal is false, and shows that no values of the variables can satisfy the equations and inequalities that follow from this. In the first goal, the first equation is the second multiplied by two, so no values of a, b, d and k can make one side true and the other false. In the second goal, the equation has an odd number on one side and an even number on the other, so no values can make it true. omega closes the remaining 14 goals the same way, which concludes the proof of least_significant_bit_split.

Putting It Together

lemma run_invariant (wLE : List Sigma3) (carryIn carryOut : Bool) :
    RunEndsWithCarry carryIn wLE carryOut ↔
      WordAddsWithCarry carryIn wLE carryOut := by
  induction wLE generalizing carryIn with
  -- base case
  | nil => ...
  -- inductive step
  | cons column columnsLE induction_hypothesis => ...

With the helper lemmas in place, we can return to the inductive step of the run invariant. We’re going to prove it by following the four steps of the plan. The first three turn the DFA on the left-hand side of the equivalence into arithmetic, and the fourth shows that the arithmetic on the two sides says the same thing. We’ll run through the informal argument first and then we’ll have a look at how it’s formalized in Lean.

In the inductive step the word is column :: columnsLE, so the goal is the run invariant for this word:

RunEndsWithCarry carryIn (column :: columnsLE) carryOut ↔
  WordAddsWithCarry carryIn (column :: columnsLE) carryOut

We also get to use the induction hypothesis, which is the run invariant for the remaining columns:

∀ carryIn,
  RunEndsWithCarry carryIn columnsLE carryOut ↔
    WordAddsWithCarry carryIn columnsLE carryOut

The ∀ carryIn is there because of generalizing carryIn. It means that the induction hypothesis holds for every starting carry, and not just for the carryIn of the goal.

Step 1 is to split the run. The left-hand side of the goal is the left-hand side of split_run, so we can replace it with the right-hand side of the lemma:

(∃ carryMid,
  dfaStep (.carry carryIn) column = .carry carryMid ∧
  RunEndsWithCarry carryMid columnsLE carryOut) ↔
    WordAddsWithCarry carryIn (column :: columnsLE) carryOut

Step 2 is to turn the first step of the run into arithmetic. Let x, y and z be the three bits of column. The first part of the conjunction is then the left-hand side of first_step_adds, so we can replace it with the adder equation:

(∃ carryMid,
  x + y + carryIn = z + 2 * carryMid ∧
  RunEndsWithCarry carryMid columnsLE carryOut) ↔
    WordAddsWithCarry carryIn (column :: columnsLE) carryOut

Step 3 is to turn the run over the remaining columns into arithmetic. The second part of the conjunction is the left-hand side of the induction hypothesis with carryMid as the starting carry, so we can replace it with the right-hand side:

(∃ carryMid,
  x + y + carryIn = z + 2 * carryMid ∧
  WordAddsWithCarry carryMid columnsLE carryOut) ↔
    WordAddsWithCarry carryIn (column :: columnsLE) carryOut

This is why we needed generalizing carryIn: the run over the remaining columns starts from carryMid, which is not necessarily the same as carryIn.

The DFA is now gone from the goal and we only have arithmetic on both sides, so we’re going to switch to mathematical notation again. Let www stand for the whole word ((x, y, z) :: columnsLE in the code) and w′w'w′ for the remaining columns (columnsLE). Unfolding WordAddsWithCarry on both sides gives:

(∃ cmid: x+y+cin=z+2⋅cmid ∧(∃ cmid: row1(w′)+row2(w′)+cmid=row3(w′)+cout⋅2∣w′∣) ⟺ row1(w)+row2(w)+cin=row3(w)+cout⋅2∣w∣\begin{aligned} &\bigl(\exists\, c_{\mathrm{mid}} :\; x + y + c_{\mathrm{in}} = z + 2 \cdot c_{\mathrm{mid}} \;\land \\ &\phantom{\bigl(\exists\, c_{\mathrm{mid}} :\;} \colorbox{#fff2a8}{$\displaystyle \mathrm{row}_1(w') + \mathrm{row}2(w') + c{\mathrm{mid}} = \mathrm{row}3(w') + c{\mathrm{out}} \cdot 2^{|w'|}$}\bigr) \iff \\ &\qquad \colorbox{#fff2a8}{$\displaystyle \mathrm{row}_1(w) + \mathrm{row}2(w) + c{\mathrm{in}} = \mathrm{row}3(w) + c{\mathrm{out}} \cdot 2^{|w|}$} \end{aligned}​(∃cmid​:x+y+cin​=z+2⋅cmid​∧(∃cmid​:row1​(w′)+row2​(w′)+cmid​=row3​(w′)+cout​⋅2∣w′∣​)⟺row1​(w)+row2​(w)+cin​=row3​(w)+cout​⋅2∣w∣​​

The whole word is one column longer than the remaining columns. So the value of each of its rows is the first bit plus twice the value of the remaining bits. Its carry out term is twice the carry out term of the remaining columns:

row1(w)=x+2⋅row1(w′)row2(w)=y+2⋅row2(w′)row3(w)=z+2⋅row3(w′)cout⋅2∣w∣=2⋅(cout⋅2∣w′∣)\begin{aligned} \mathrm{row}_1(w) &= x + 2 \cdot \mathrm{row}_1(w') \\ \mathrm{row}_2(w) &= y + 2 \cdot \mathrm{row}_2(w') \\ \mathrm{row}_3(w) &= z + 2 \cdot \mathrm{row}3(w') \\ c{\mathrm{out}} \cdot 2^{|w|} &= 2 \cdot \bigl(c_{\mathrm{out}} \cdot 2^{|w'|}\bigr) \end{aligned}row1​(w)row2​(w)row3​(w)cout​⋅2∣w∣​=x+2⋅row1​(w′)=y+2⋅row2​(w′)=z+2⋅row3​(w′)=2⋅(cout​⋅2∣w′∣)​

If we write aaa, bbb and ddd for the values of the rows of the remaining columns and kkk for their carry out term cout⋅2∣w′∣c_{\mathrm{out}} \cdot 2^{|w'|}cout​⋅2∣w′∣, the goal becomes:

(∃ cmid: x+y+cin=z+2⋅cmid ∧(∃ cmid: a+b+cmid=d+k) ⟺ (x+2⋅a)+(y+2⋅b)+cin=(z+2⋅d)+2⋅k\begin{aligned} &\bigl(\exists\, c_{\mathrm{mid}} :\; x + y + c_{\mathrm{in}} = z + 2 \cdot c_{\mathrm{mid}} \;\land \\ &\phantom{\bigl(\exists\, c_{\mathrm{mid}} :\;} \colorbox{#fff2a8}{$\displaystyle a + b + c_{\mathrm{mid}} = d + k$}\bigr) \iff \\ &\qquad \colorbox{#fff2a8}{$\displaystyle (x + 2 \cdot a) + (y + 2 \cdot b) + c_{\mathrm{in}} = (z + 2 \cdot d) + 2 \cdot k$} \end{aligned}​(∃cmid​:x+y+cin​=z+2⋅cmid​∧(∃cmid​:a+b+cmid​=d+k​)⟺(x+2⋅a)+(y+2⋅b)+cin​=(z+2⋅d)+2⋅k​​

This brings us to step 4 of the plan. The goal is least_significant_bit_split with the two sides of the equivalence swapped. An equivalence holds in both directions, so the lemma closes the goal. This concludes the proof of the inductive step, and with it the proof of the run invariant.

Next let’s review what the proof of the inductive step looks like in Lean:

lemma run_invariant (wLE : List Sigma3) (carryIn carryOut : Bool) :
    RunEndsWithCarry carryIn wLE carryOut ↔
      WordAddsWithCarry carryIn wLE carryOut := by
  induction wLE generalizing carryIn with
  -- base case
  | nil => ...
  -- inductive step
  | cons column columnsLE induction_hypothesis =>
    obtain ⟨x, y, z⟩ := column
    rw [split_run]
    simp_rw [first_step_adds, induction_hypothesis]
    simp only [
      WordAddsWithCarry,
      row1LE_cons, row2LE_cons, row3LE_cons,
      List.length_cons, pow_succ'
    ]
    rw [Nat.mul_left_comm]
    exact
      Iff.symm
        (least_significant_bit_split
          x y z carryIn
          (row1LE columnsLE)
          (row2LE columnsLE)
          (row3LE columnsLE)
          (carryOut * 2 ^ columnsLE.length))

obtain ⟨x, y, z⟩ := column destructures the column into its three bits, like let (x, y, z) = column would in a regular program.

rw [split_run] is step 1 of the plan. rw looks for the left-hand side of a lemma in the goal and replaces it with the right-hand side.

simp_rw [first_step_adds, induction_hypothesis] is steps 2 and 3. simp_rw is like rw, but it can also rewrite under the ∃, which rw can’t do.

At this point the DFA is gone from the goal and we’re working with arithmetic only. The only thing left is to get the equations into a shape that matches least_significant_bit_split.

The goal is now:

(∃ carryMid,
  x + y + carryIn = z + 2 * carryMid ∧
  WordAddsWithCarry carryMid columnsLE carryOut) ↔
    WordAddsWithCarry carryIn ((x, y, z) :: columnsLE) carryOut

The simp only line first unfolds WordAddsWithCarry on both sides of the goal, but we’ll just focus on the right-hand side of the equivalence, as the goal gets too large to follow otherwise. So simp only first rewrites

WordAddsWithCarry carryIn ((x, y, z) :: columnsLE) carryOut

as

row1LE ((x, y, z) :: columnsLE) +
    row2LE ((x, y, z) :: columnsLE) + carryIn =
  row3LE ((x, y, z) :: columnsLE) +
    carryOut * 2 ^ ((x, y, z) :: columnsLE).length

Then it splits the first column off from the whole word on the right-hand side using the rowNLE_cons lemmas:

x + 2 * row1LE columnsLE + (y + 2 * row2LE columnsLE) + carryIn =
  z + 2 * row3LE columnsLE +
    carryOut * 2 ^ ((x, y, z) :: columnsLE).length

The rowNLE_cons lemmas say that the value of a row of column :: columnsLE is the column’s bit plus twice the value of the same row of columnsLE.

Finally, it does the same for the carry out term using List.length_cons and pow_succ':

x + 2 * row1LE columnsLE + (y + 2 * row2LE columnsLE) + carryIn =
  z + 2 * row3LE columnsLE + carryOut * (2 * 2 ^ columnsLE.length)

List.length_cons says that column :: columnsLE is one longer than columnsLE, and pow_succ' rewrites 2n+12^{n+1}2n+1 as 2⋅2n2 \cdot 2^n2⋅2n.

At this point there is just one small thing that we need to fix before we can conclude the proof using least_significant_bit_split. The lemma has a 2⋅k2 \cdot k2⋅k term, where kkk stands for the carry out term of the remaining columns. So it expects 2 * (carryOut * 2 ^ columnsLE.length), but we have carryOut * (2 * 2 ^ columnsLE.length).

rw [Nat.mul_left_comm] fixes this. Nat.mul_left_comm states a * (b * c) = b * (a * c), so rewriting with it swaps carryOut and 2 on the right-hand side of the equivalence:

x + 2 * row1LE columnsLE + (y + 2 * row2LE columnsLE) + carryIn =
  z + 2 * row3LE columnsLE + 2 * (carryOut * 2 ^ columnsLE.length)

The goal is now in the shape of least_significant_bit_split (with the sides of the equivalence reversed).

As the final step of the proof we switch into term mode using the exact tactic. This means that in order to conclude the proof, we need to construct a term that matches the type of the goal. The full goal including the left-hand side of the equivalence is quite a mouthful, so I’ll only show it for completeness:

(∃ carryMid,
  x + y + carryIn = z + 2 * carryMid ∧
  row1LE columnsLE + row2LE columnsLE + carryMid =
    row3LE columnsLE + carryOut * 2 ^ columnsLE.length) ↔
    x + 2 * row1LE columnsLE + (y + 2 * row2LE columnsLE) + carryIn =
      z + 2 * row3LE columnsLE + 2 * (carryOut * 2 ^ columnsLE.length)

We construct the necessary term by calling least_significant_bit_split with the three bits of the column, carryIn, and the row values and carry out term of columnsLE, and wrapping the result in Iff.symm to flip the sides of the equivalence:

Iff.symm
  (least_significant_bit_split
    x y z carryIn
    (row1LE columnsLE)
    (row2LE columnsLE)
    (row3LE columnsLE)
    (carryOut * 2 ^ columnsLE.length))

You don’t have to convince yourself that this term has the type of the goal, you can trust Lean with this.

BRB^{\mathcal{R}}BR Is Regular

Now that we have proven the run_invariant theorem, we can use it to prove that BRB^{\mathcal{R}}BR is regular. We do this in two steps: first we show that the adder DFA accepts BRB^{\mathcal{R}}BR, and then that this makes BRB^{\mathcal{R}}BR regular.

Adder DFA Accepts BRB^{\mathcal{R}}BR

The first step is the following theorem:

theorem adderDFA_accepts_B_reverse : adderDFA.accepts = B.reverse := by
  ...

As we’ve seen before, both adderDFA.accepts and B.reverse are sets. Two sets are equal when they have the same members, so the equation in the theorem is equivalent to the following for every word wLE:

wLE ∈ adderDFA.accepts ↔ wLE ∈ B.reverse

Since adderDFA.start is .carry false and .carry false is the only accepting state, the membership rule for adderDFA.accepts is

{ wLE | RunEndsWithCarry (carryIn := false) wLE (carryOut := false) }

Therefore,

wLE ∈ adderDFA.accepts ↔
  RunEndsWithCarry (carryIn := false) wLE (carryOut := false)

And the membership rule for B.reverse is equivalent to:8

{ wLE | WordAddsWithCarry (carryIn := false) wLE (carryOut := false) }

Therefore,

wLE ∈ B.reverse ↔
  WordAddsWithCarry (carryIn := false) wLE (carryOut := false)

So we need to prove that

RunEndsWithCarry (carryIn := false) wLE (carryOut := false) ↔
  WordAddsWithCarry (carryIn := false) wLE (carryOut := false)

But this is just the run_invariant theorem instantiated with false for both carries which we’ve already proven:

run_invariant (carryIn := false) wLE (carryOut := false)

This concludes the proof of the adderDFA_accepts_B_reverse theorem.

The Lean proof takes roughly the same steps, but it’s about a dozen lines long, so we will not go through it in detail here. However, it’s a good idea at this point to check out the code and step through it yourself, so you can see the proof unfold interactively.

From Acceptance to Regularity

With the adderDFA_accepts_B_reverse theorem in hand, we can show that BRB^{\mathcal{R}}BR is regular. The theorem is just the statement that IsRegular holds for B.reverse:

theorem B_reverse_isRegular : B.reverse.IsRegular :=
  ...

There is no by after the :=, so this is a term mode proof, which means that we write the term of the theorem’s type directly instead of having tactics build it for us. As we saw earlier, IsRegular says that there exists a finite type of states and a DFA over those states that accepts the language:

def IsRegular (L : Language T) : Prop :=
  ∃ σ [Fintype σ], ∃ M : DFA T σ, M.accepts = L

So we need to show that there is a finite type of states, a DFA over those states, and that the DFA accepts B.reverse, which we do by listing them between angle brackets:

theorem B_reverse_isRegular : B.reverse.IsRegular :=
  ⟨DFAState, inferInstance, adderDFA, adderDFA_accepts_B_reverse⟩

DFAState is the type of states, and adderDFA is the DFA. inferInstance asks Lean to find the Fintype instance for DFAState, which was generated when we derived Fintype for it. The instance is a list of all the values of the type, together with a proof that the list is complete. The last part is the proof that the DFA accepts B.reverse, which is the theorem we’ve just proven.

BBB Is Regular

We set out to prove that the language BBB is regular and we’re finally in a position to do so. All we need is the closure of regular languages under reversal. Mathlib provides this as Language.isRegular_reverse_iff, and its type is

L.reverse.IsRegular ↔ L.IsRegular

where L is a generic Mathlib.Computability.Language.

An equivalence holds in both directions and we have a proof that B.reverse.IsRegular, so we can use the implication

L.reverse.IsRegular → L.IsRegular

to prove that BBB is regular.

The formalization in Lean is written as follows:

theorem B_isRegular : B.IsRegular :=
  Language.isRegular_reverse_iff.mp B_reverse_isRegular

mp is short for modus ponens. We use the mp field here to turn the theorem which has type L.reverse.IsRegular ↔ L.IsRegular into a function with type L.reverse.IsRegular → L.IsRegular.

We pass this function B_reverse_isRegular, and we get back a term with type B.IsRegular which is the proof that B is regular.

Outro

We set out to show that the language BBB is regular, and we now have a proof that Lean accepts. You can verify this yourself by checking out the code and compiling it.

Along with our proof, we’ve also created a formally verified implementation of a DFA. The implementation is in Lean, which is pretty fast, as it compiles to C, but we could also implement the DFA in another language such as Rust and keep only the spec and the proofs in Lean.11

As we’ve seen, the formal proof needed a lot of detail that we’d normally skip. It is a lot of work to write proofs like this even though we had it relatively easy with the adder DFA. We could turn its behavior into arithmetic until we were left with some simple linear equations to solve.

Formal proofs of real-world systems are much harder to write. For example, distributed systems often call for temporal logic, which reasons about how a system changes over time, and cryptographic primitives often need their own styles of proof.12

Fortunately, in 2026 machines can write proofs for us. State-of-the-art coding agents can one-shot proofs like ours, and they’re rapidly getting better at tackling more complex ones as well. At the same time, Lean is improving to make complex proofs more efficient to write.13 Together, these are quickly driving down the cost of formal verification.

It’s tempting to think that with coding agents, humans can just focus on making sure the spec is correct and then the machine-generated implementation and proof can be treated as black boxes. I’m a bit skeptical about this, because, in my experience, the interface between specification and proof is not so clear, as one often has to look at the proof to understand the spec. And if we see something weird in the proof, that’s a good indication that something is off.

Our proof has a small example of this: the run invariant introduced a carry out term that the definition of BBB never mentioned. That was not a bug in the spec, but it did surface a hidden requirement: all three rows of a word have the same length, so BBB rules out sums that would overflow.

My feeling is that while we can probably start treating formally verified implementations as black boxes, it’s important going forward that we can understand machine-generated proofs. This is a challenge, because proofs generated by coding agents can be convoluted.

In any case, I think the future of software engineering is super exciting, because formal methods let us work at a higher level of abstraction and make us more productive as they unlock more automation.

• * *
  1. Instead of using the LE/BE convention to distinguish between interpretations of lists of bits, we could introduce separate types for little- and big-endian lists of bits to prevent mixing them up. However, this would require re-deriving many of the theorems that are already available for native lists, so it’s not worth it for a project of this scope. ↩︎
  2. Set as a collection is available as Std.HashSet and Std.TreeSet. ↩︎
  3. A decision procedure is a function that evaluates a proposition and returns true if it holds and false if it doesn’t. We have this automatically for the dfaStep example, because the proposition is an equation between two DFAState values and we’ve derived DecidableEq for DFAState earlier. ↩︎
  4. The evaluation in the type checker is guaranteed to terminate, because Lean rejects functions unless termination is proven (automatically or by the author). A definition can opt out explicitly, but then the type checker cannot unfold it, so it cannot be evaluated in a proof. ↩︎
  5. The actual term is of_decide_eq_true (id (Eq.refl true)). The id is a type ascription that decide needs because it builds the argument before it applies of_decide_eq_true, so it has to record that Eq.refl true is meant as a proof of decide p = true rather than true = true. When the proof is written by hand, the expected type is known from the example signature, so the id can be omitted. ↩︎
  6. Simplified version of Mathlib’s definition. The actual definition spells out the universe of T and writes the finiteness as ∃ σ : Type, ∃ _ : Fintype σ. ↩︎
  7. The actual Mathlib definition is a bit more verbose, so I’m not quoting it here. ↩︎
  8. The informal argument about the equivalence of the little-endian interpretation of a word and the big-endian interpretation of its reversal (rowNBE w.reverse = rowNLE w) is formalized in the specification file, but it’s basically just bookkeeping, so I didn’t include it in the post. ↩︎ ↩︎
  9. As before, we’ve dropped .toNat from the booleans in the lemma statement for brevity. ↩︎
  10. Dropped .toNat for brevity. ↩︎
  11. For example, Aeneas translates Rust programs into Lean so that their behavior can be verified there. ↩︎
  12. E.g. game-based or simulation-based proofs are difficult to formalize. Game-based proofs rewrite an attack on a protocol as a sequence of small steps, each of which changes the attacker’s odds only slightly; see Shoup’s Sequences of Games. Simulation-based proofs show that anything an attacker learns from the real protocol could have been produced without it; see Lindell’s How to Simulate It. ↩︎
  13. For more on this, see Leonardo de Moura’s blog posts Proof Assistants in the Age of AI and Signal Shot: The Platform Is Ready. ↩︎