Anatomy of a Lean Proof for Software Engineers

Intro

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.

Background: DFAs & Regular Languages

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.

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, $\Sigma = \left\{-, 0, 1, 2, \ldots, 9\right\}$.

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 $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)$ is the condition that a string $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)$ can be defined as “$w$ is not empty and contains no negative sign, except that its first character may be a negative sign if $w$ 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

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

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

$$B = \bigl\{\, w \in \Sigma_3^{*} \bigm| P(w) \,\bigr\}$$

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

Show that $B$ is regular. (Hint: it is easier to work with $B^{\mathcal{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

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

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

If we can build a DFA to recognize $B^{\mathcal{R}}$, then we can conclude that $B^{\mathcal{R}}$ is a regular language. Since $B^{\mathcal{R}}$ reversed is $B$, we can use the closure property of the reversal of regular languages to conclude that $B$ 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:

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

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

Adder DFA

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

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 $\left[\begin{smallmatrix}\mathtt{0}\\\mathtt{0}\\\mathtt{1}\end{smallmatrix}\right]$ 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 $B^{\mathcal{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^{\mathcal{R}}$. By the definition of $B^{\mathcal{R}}$, the original word is in $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. $\mathtt{1} + \mathtt{1} = \mathtt{0}$ and $\mathtt{11} + \mathtt{01} = \mathtt{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 ($\mathtt{1} + \mathtt{0}$ really is $\mathtt{1}$) so the machine can’t tell anything is wrong yet. But the second column fails: with no carry pending, $\mathtt{0} + \mathtt{0}$ must produce $\mathtt{0}$, but the bottom row claims $\mathtt{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 $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:

1. A specification of the language $B$.
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

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 $B$:

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 $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.¹ So the predicate is just

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.² So our definition of $B$ 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 procedure³ inside the type checker.⁴ 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:⁵

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 $B$ is regular, we need to first show that the adder DFA accepts the reverse of the language, $B^{\mathcal{R}}$. We can then use the closure property of the reversal of regular languages to prove that $B$ 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 $B^{\mathcal{R}}$.

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

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

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

{ 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 $w$ (wLE in the code) starting with carry 0 ends in state carry 0 if and only if

$$\mathrm{row}_1(w) + \mathrm{row}_2(w) = \mathrm{row}_3(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 $c_{\mathrm{in}}$ and $c_{\mathrm{out}}$ 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:

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

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:

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.

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:

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

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

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.¹⁰ 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$, $y$ and $z$ are the least significant bits of the three rows, $a$, $b$ and $d$ are the values of the remaining bits, and $k$ stands for the carry out term of the remaining bits.

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

The $x + 2 \cdot a$ term comes from splitting

so $x + 2 \cdot a$ is the value of a row whose first bit is $x$ and whose remaining bits have value $a$ (the same applies to terms with $y$ and $z$).

$k$ stands for the carry out term of the remaining bits, which is $c_{\mathrm{out}} \cdot 2^{n-1}$, so the carry out term of the whole word, $c_{\mathrm{out}} \cdot 2^n$, is $2 \cdot k$. Notice how WholeRunAddition has a $2 \cdot k$ term in it while SplitRunAddition has just $k$ 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 $c_{\mathrm{mid}}$, 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:

The equation involves the four boolean arguments of the lemma and $c_{\mathrm{mid}}$ which means that once we fix the four booleans, $c_{\mathrm{mid}}$ 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 $c_{\mathrm{mid}}$ 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 $x$ and $y$ are $1$ and $z$ and $c_{\mathrm{in}}$ are $0$. This is again the column where $1 + 1 = 0$ with $c_{\mathrm{out}} = 1$.

Substituting the values gives:

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

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

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

Now take a case where the column doesn’t add up: $x$ is $1$ and $y$, $z$ and $c_{\mathrm{in}}$ are $0$.

Substituting the values gives:

This time the least significant bit equation is $1 = 2 \cdot c_{\mathrm{mid}}$. No value of $c_{\mathrm{mid}}$ 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

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 $x$, $y$ and $c_{\mathrm{in}}$ has the same parity as $z$, exactly one $c_{\mathrm{mid}}$ 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:

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:

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 $w$ stand for the whole word ((x, y, z) :: columnsLE in the code) and $w'$ for the remaining columns (columnsLE). Unfolding WordAddsWithCarry on both sides gives: