Anatomy of a Lean Proof for Software Engineers

[Contents]IntroBackground: DFAs & Regular LanguagesDeterministic Finite Automaton (DFA)Regular LanguagesThe ProblemThe SolutionAdder ArithmeticAdder DFAExample 1Example 2The Lean ProofThe SpecificationThe ImplementationHow Proofs WorkThe ProofRun InvariantRun Invariant ProofBase CaseInductive StepSplitting the RunFirst Step AddsLeast Significant Bit SplitPutting It TogetherBRB^{\mathcal{R}} Is RegularAdder DFA Accepts BRB^{\mathcal{R}}From Acceptance to RegularityBB Is RegularOutroIntroI 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 LanguagesFeel 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):DFA for a decimal integer literal, including the dead statestartsigndigitsdead-0-90-90-9otherotherotheranyThis 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\}.Regular LanguagesA 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 AA with set-builder notation:A={ w∈Σ∗∣P(w) }A = \bigl\{\, w \in \Sigma^{*} \bigm| P(w) \,\bigr\}Σ∗\Sigma^{*} means the set of strings that are created by all possible concatenations of symbols in Σ\Sigma and P(w)P(w) is the condition that a string ww 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) can be defined as “ww is not empty and contains no negative sign, except that its first character may be a negative sign if ww has at least two characters”.The ProblemThe 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\Sigma_3 is the set of all height-3 columns of 0s and 1s, so a string over Σ3\Sigma_3 determines three rows of bits. Reading each row as a binary number, defineB={ w∈Σ3∗∣P(w) }B = \bigl\{\, w \in \Sigma_3^{*} \bigm| P(w) \,\bigr\}where P(w)P(w) is the proposition that the bottom row of ww equals the sum of the top two rows.Show that BB is regular. (Hint: it is easier to work with BRB^{\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 like011 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 equationx+y=z x + y = zto 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 SolutionThe 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 BB directly. Instead we build a DFA to recognize its reversal BRB^{\mathcal{R}}, which consists of the strings of BB written backwards, so the machine sees the least significant column first.If we can build a DFA to recognize BRB^{\mathcal{R}}, then we can conclude that BRB^{\mathcal{R}} is a regular language. Since BRB^{\mathcal{R}} reversed is BB, we can use the closure property of the reversal of regular languages to conclude that BB is regular as well, which completes the solution.Adder ArithmeticWhen 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_iwhere xi,yix_i, y_i are the addend bits, ziz_i is the sum bit, ii denotes the index of the current column, and cinc_{\mathrm{in}} is the input carry from the previous step. We compute the output carry, denoted coutc_{\mathrm{out}}, 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)This means that there is a carry either if both addends are 1\mathtt{1} or there was an input carry and exactly one of the addends is 1\mathtt{1}. Note that a simpler way to compute coutc_{\mathrm{out}} is to check if at least two of xix_i, yiy_i and cinc_{\mathrm{in}} are 1\mathtt{1} (we’ll make use of this in the Lean proof).Adder DFAWith this in mind, here is the DFA that recognizes BRB^{\mathcal{R}}:DFA recognizing B reversed: a full adder whose state is the pending carry, plus a dead state. Each transition is labelled with the three-bit column symbols that take it: solid arrows are the columns whose sum bit checks out, dashed red arrows the columns whose sum bit does not match.carry 0carry 1deadstartany columnxi⊕ yi⊕ cin= zi✓xi⊕ yi⊕ cin≠ zi✗000,011,101010,100,111110001001,010,100,111000,011,101,110The 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] 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