% For a single index; for multiple indexes, see the manual
% "Instructions for preparation of papers and monographs:
% AMS-LaTeX" (instr-l.pdf in the AMS-LaTeX distribution).
\makeindex
\begin{document}
\frontmatter
\title{Formal Reasoning About Programs}
% Remove any unused author tags.
% author one information
\author{Adam Chlipala}
\address{MIT, Cambridge, MA, USA}
\email{adamc@csail.mit.edu}
\begin{abstract}
\emph{Briefly}, this book is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected.
\emph{More specifically}: Introductions to two intertangled subjects: the Coq proof assistant, a tool for machine-checked mathematical theorem proving; and formal logical reasoning about the correctness of programs.
The classic engineering disciplines all have their standard mathematical techniques that are applied to the design of any artifact, before it is deployed, to gain confidence abouts its safety, suitability for some purpose, and so on.
The engineers in a discipline more or less agree on what are ``the rules'' to be followed in vetting a design.
Those rules are specified with a high degree of rigor, so that it isn't a matter of opinion whether a design is safe.
Why doesn't software engineering have a corresponding agreed-upon standard, whereby programmers convince themselves that their systems are safe, secure, and correct?
The concepts and tools may not quite be ready yet for broad adoption, but they have been under deveopment for decades.
This book introduces one particular tool and a body of ideas for how to apply it to different tasks in program proof.
As this document is in a very early draft stage, no more will be said here, in favor of jumping right into the technical material.
Eventually, there will no doubt be some sort of historical overview here, as part of a general placing-in-context of the particular approach that will come next.
There will also be plenty of scholarly citations (here and throughout the book).
In this early version, you get to take the author's word for it that we are about to learn a promising approach!
However, one overarching element of our strategy is important enough to deserve to be called out here.
We will study a variety of different approaches for formalizing what a program should do and for proving that a program does what it should.
At every step, we will pay close attention to the \emph{common foundation} that underlies everything.
For one thing, we will be proving all of our theorems with the Coq proof assistant, a powerful framework for writing and machine-checking proofs.
Coq itself is based on a relatively small set of core features, much like a well-designed programming language, and in both we build up increasingly sophisticated abstractions as libraries.
Those features can be thought of as the core of all mathematical reasoning.
We will also apply a recipe specific to program proof.
When we encounter a new challenge, to prove a new kind of property about a new kind of program, we will generally be considering four broad elements that appear in nearly all techniques.
\begin{itemize}
\item\index{encoding}\textbf{Encoding.}
Every programming language has both \index{syntax}\emph{syntax}, which defines what programs look like, and \index{semantics}\emph{semantics}, which defines how programs behave when run.
Even when these elements seem obvious intuitively, we often find that there are surprisingly subtle choices to be made in defining syntax and semantics at the highest level of rigor.
Seemingly minor decisions can have big impacts on how smoothly our proofs go.
\item\textbf{Invariants.}
Nearly every theorem about a program is stated in terms of a \index{transition system}\emph{transition system}, with some set of states and a relation for stepping from one state to the next, moving forward in time.
Nearly every program proof also works by finding an \index{invariant}\emph{invariant} of a transition system, or a property that always holds of every state reachable from some starting state.
The concept of invariant is very close to being a direct reinterpretation of mathematical induction, that glue of every serious mathematical development, known and loved by all.
\item\index{abstraction}\textbf{Abstraction.}
Often a transition system is too complex to analyze directly.
Instead, we \emph{abstract} it with another transition system that is somehow more tractable, proving that the new system preserves all relevant properties of the original.
\item\index{modularity}\textbf{Modularity.}
Similarly, when a transition system is too complex, we often break it into separate \emph{modules} and use some well-behaved composition operators to reassemble them into the whole.
Often abstraction and modularity go together, as we decompose a system both \index{horizontal decomposition}\emph{horizontally} (i.e., with modularity), splitting it into more manageable parts, and \index{vertical decomposition}\emph{vertically} (i.e., with abstraction), simplifying parts in ways that preserve key properties.
We can even alternate between strategies, breaking a system into parts, abstracting one as a simpler part, further decomposing that part into pieces, and so on.
In the course of the book, we will never quite define any of these meta-techniques in complete formality.
Instead, we'll meet many examples of each, called out by eye-catching margin notes.
Generalizing from the examples should help the reader start developing an intuition for when to use each element and for the common design patterns that apply.
The core subject matter of the book is often grouped under traditional disciplinary headers like \index{semantics}\emph{semantics}, \index{programming-languages theory}\emph{programming-languages theory}, \index{formal methods}\emph{formal methods}, and \index{verification}\emph{verification}.
Often these different traditions have their own competing terminology for shared concepts.
We'll follow one particular set of unified terminology and notation, cherry-picked from the conventions of different communities.
There really is a huge amount of commonality across everything that we'll study, so we don't want to distract by constantly translating between notations.
It is quite important to be literate in the standard notational conventions, which are almost always implemented with \index{\LaTeX{}}\LaTeX{}, and we stick entirely to that kind of notation in this book.
However, we follow another, much less usual convention: while we give theorem and lemma statements, we rarely give their proofs.
The reason is that the author and many other researchers today feel that proofs on paper have outlived their usefulness.
Instead, the proofs are all found in the parallel world of the accompanying Coq source code.
That is, each chapter of this book has a corresponding Coq source file, distributed with the general book source code.
The Coq sources are heavily commented and may even, in many cases, be feasible to read without also reading the book chapters.
More importantly, the Coq sources aren't just meant to be \emph{read}.
They are meant to be \emph{executed}.
We suggest stepping through them interactively, seeing intermediate states of proofs as appropriate.
The book proper can be read without the Coq sources, to learn the standard background material of program proof; and the Coq sources can be read without the book proper, to learn a particular concrete realization of those ideas.
The definition of a program starts with the definition of a programming language, and the definition of a programming language starts with its \emph{syntax}\index{syntax}, which covers which sorts of phrases are basically well-formed.
In the next chapter, we turn to \emph{semantics}\index{semantics}, which, in the course of saying what programs \emph{mean}, may impose further validity conditions.
Turning to examples, let's start with \emph{concrete syntax}\index{concrete syntax}, which decrees which sequences of characters are acceptable.
For a simple language of arithmetic expressions, we might accept the following strings as valid.
$$\begin{array}{l}
3 \\
x \\
3 + x \\
y * (3 + x)
\end{array}$$
Plenty of other strings might be invalid, like these.
$$\begin{array}{l}
1 + + \; 2 \\
x \; y \; z
\end{array}$$
Rather than appeal to our intuition about grade-school arithmetic, we prefer to formalize concrete syntax with a \emph{grammar}\index{grammar}, following a style known as \emph{Backus-Naur Form (BNF)}\index{Backus-Naur Form}\index{BNF}.
We have a set of \emph{nonterminals}\index{nonterminal} (e.g., $e$ below), standing for sets of allowable strings.
Some are defined by appeal to existing sets, as below, when we define constants $n$ in terms of the well-known set $\mathbb N$\index{N@$\mathbb N$} of natural numbers\index{natural numbers} (nonnegative integers).
\textrm{Expressions}& e &::=& n \mid x \mid e + e \mid e \times e
\end{array}$$
To interpret the grammar in plain English: we assume sets of constants and variables, based on well-known sets of natural numbers and strings, respectively.
We then define expressions to include constants, variables, addition, and multiplication.
Crucially, the last two cases are specified \emph{recursively}: we show how to build bigger expressions out of smaller ones.
Incidentally, we're already seeing how many different formal notations creep into the discussion of formal program proofs.
All of this content is typeset in \LaTeX{}\index{\LaTeX{}}, and it may be helpful to consult the book sources, to see how it's all done.
Throughout the subject, one of our most crucial tools will be \emph{inductive definitions}\index{inductive definition}, explaining how to build up bigger sets from smaller ones.
The recursive nature of the grammar above is implicitly giving an inductive definition.
A more general notation for inductive definitions provides a series of \emph{inference rules}\index{inference rules} that define a set.
Formally, the set is defined to be \emph{the smallest one that satisfies all the rules}.
Each rule has \emph{premises}\index{premise} and a \emph{conclusion}\index{conclusion}.
We illustrate with four rules that together are equivalent to the BNF grammar above, for defining a set $\mathsf{Exp}$ of expressions.
The general reading of an inference rule is: \textbf{if} all the facts above the horizontal line are true, \textbf{then} the fact below the line is true, too.
The rule implicitly needs to hold for \emph{all} values of the \emph{metavariables}\index{metavariable} (like $n$ and $e_1$) that appear within it; we can model them more explicitly with a sort of top-level universal quantification.
Newcomers to semantics often react negatively to seeing this style of definition, but very quickly it becomes apparent as a remarkably compact notation for expressing many concepts.
Think of it as a domain-specific programming language for mathematical definitions, an analogy that becomes quite concrete in the associated Coq code!
\section{Abstract Syntax}
After that brief interlude with concrete syntax, we now drop all formal treatment of it, for the rest of the book!
Instead, we concern ourselves with \emph{abstract syntax}\index{abstract syntax}, the real heart of language definitions.
Now programs are \emph{abstract syntax trees}\index{abstract syntax tree} (\emph{ASTs}\index{AST}), corresponding to inductive type definitions in Coq or algebraic datatype\index{algebraic datatype} definitions in Haskell\index{Haskell}.
Such types can be defined by enumerating their \emph{constructor}\index{constructor} functions with types.
Actually, semanticists get tired of writing such verbose descriptions, so proofs on paper tend to use exactly the sort of notation that we associated with concrete syntax.
The trick is mental desugaring of the concrete-syntax notation into abstract syntax!
We will generally not dwell on the particularities of that process.
Instead, we repeatedly illustrate it by example, using Coq code that starts with abstract syntax, accompanied by \LaTeX{}-based ``code'' in this book that applies concrete syntax freely.
Abstract syntax is handy for writing \emph{recursive definitions}\index{recursive definition} of functions.
Here is one in the clausal\index{clausal function definition} style of Haskell\index{Haskell}.
It is important that we include \emph{one clause per constructor of the inductive type}.
Otherwise, the function would not be \emph{total}\index{total function}.
We also need to be careful to ensure \emph{termination}\index{termination of recursive definitions}, by making recursive calls only on the arguments of the constructors.
This termination criterion, adopted by Coq, is called \emph{primitive recursion}\index{primitive recursion}.
Let's continue to exercise our creative license and write $\depth{e}$ for the \emph{depth} of $e$, that is, the length of the longest downward path from the syntax-tree root to any leaf.
The main reason to prefer abstract syntax is that, while strings of text \emph{seem} natural and simple to our human brains, they are really a lot of trouble to treat in complete formality.
Inductive trees are much nicer to manipulate.
Considering the name, it's probably not surprising that the main thing we want to do on them is \emph{induction}\index{induction}, an activity most familiar in the form of \emph{mathematical induction}\index{mathematical induction} over the natural numbers.
In this book, we will not dwell on many proofs about natural numbers, instead presenting the more general and powerful idea of \emph{structural induction}\index{structural induction} that subsumes mathematical induction in a formal sense, based on viewing the natural numbers as one simple inductively defined set.
There is a general recipe to go from an inductive definition to its associated induction principle.
When we define set $S$ inductively, we gain an induction principle for proving that some predicate $P$ holds for all elements of $S$.
To make this conclusion, we must discharge one proof obligation per rule of the inductive definition.
Recall our last rule-based definition above, for the abstract syntax of $\mathsf{Exp}$.
To derive an $\mathsf{Exp}$ structural induction principle, we produce a new set of rules, cloning each rule with two key modifications:
\begin{enumerate}
\item Replace each conclusion, of the form $E \in S$, with a conclusion $P(E)$. That is, the obligations involve \emph{showing} that $P$ holds of certain terms.
\item For each premise $E \in S$, add a companion premise $P(E)$. That is, the obligation allows \emph{assuming} that $P$ holds of certain terms. Each such assumption is called an \emph{inductive hypothesis}\index{inductive hypothesis} (\emph{IH}\index{IH}).
\end{enumerate}
That mechanical procedure derives the following four proof obligations, associated with an inductive proof that $\forall x \in\mathsf{X}. \; P(x)$.
$$\infer{P(\mathsf{Const}(n))}{
n \in\mathbb N
}
\quad\infer{P(\mathsf{Var}(x))}{
x \in\mathsf{Strings}
}$$
$$\quad\infer{P(\mathsf{Plus}(e_1, e_2))}{
e_1 \in\mathsf{Exp}
& P(e_1)
& e_2 \in\mathsf{Exp}
& P(e_2)
}
\quad\infer{P(\mathsf{Times}(e_1, e_2))}{
e_1 \in\mathsf{Exp}
& P(e_1)
& e_2 \in\mathsf{Exp}
& P(e_2)
}$$
In other words, to establish $\forall x \in\mathsf{X}. \; P(x)$, we need to prove that each of these inference rules is valid.
To see induction in action, we prove a theorem giving a sanity check on our two recursive definitions from earlier: depth can never exceed size.
\begin{theorem}
For all $e \in\mathsf{Exp}$, $\depth{e}\leq\size{e}$.
\end{theorem}
\begin{proof}
By induction on the structure of $e$.
\end{proof}
That sort of minimalist proof often surprises and frustrates newcomers.
Our position here is that proof checking is an activity fit for machines, not people, so we will leave out gory details, which are to be found in the accompanying Coq code, for this theorem and many others associated with this chapter.
Actually, even published proofs on paper tend to use ``proofs'' as brief as the one above, relying on the reader's experience to ``fill in the blanks''!
Unsurprisingly, fairly often there are logical errors in such arguments, leading to acceptance of bogus theorems.
For that reason, we stick to machine-checked proofs here, using the book chapters to introduce concepts, reasoning principles, and statements of key theorems and lemmas.
We do, however, need to get all the proof details filled in somehow.
One of the most convenient cases is when a proof goal fits into some \emph{decidable theory}\index{decidable theory}.
We follow the sense from computability theory\index{computability theory}, where we consider some \emph{decision problem}\index{decision problem}, as a (usually infinite) set $F$ of formulas and some subset $T \subseteq F$ of \emph{true} formulas, possibly considering only those provable using some limited set of inference rules.
The decision problem is \emph{decidable} if and only if there exists some always-terminating program that, when passed some $f \in F$ as input, returns ``true'' if and only if $f \in T$.
Decidability of theories is handy because, whenever our goal belongs to the $F$ set of a decidable theory, we can discharge the goal automatically by running the deciding program that must exist.
One common decidable theory is \emph{linear arithmetic}\index{linear arithmetic}, whose $F$ set is generated by the following grammar as $\phi$.
$$\begin{array}{rrcl}
\textrm{Constants}& n &\in&\mathbb Z \\
\textrm{Variables}& x &\in&\mathsf{Strings}\\
\textrm{Terms}& e &::=& x \mid n \mid e + e \mid e - e \\
\textrm{Propositions}&\phi&::=& e = e \mid e < e \mid\neg\phi\mid\phi\land\phi
\end{array}$$
The arithmetic terms used here are \emph{linear} in the same sense as \emph{linear algebra}\index{linear algebra}: we never multiply together two terms containing variables.
Actually, multiplication is prohibited outright, but we allow multiplication by a constant as an abbreviation (logically speaking) for repeated addition.
Propositions are formed out of equality and less-than tests on terms, and we also have the Boolean negation (``not'') operator $\neg$ and conjunction (``and'') operator $\land$.
This set of propositional\index{propositional logic} operators is enough to encode the other usual inequality and propositional operators, so we allow them, too, as convenient shorthands.
Using decidable theories in a proof assistant like Coq, it is important to understand how a theory may apply to formulas that don't actually satisfy its grammar literally.
As one more example of a decidable theory, consider the algebraic structure of \emph{semirings}\index{semirings}, which may profitably be remembered as ``types that act like natural numbers.''
A semiring is any set containing two elements notated 0 and 1, closed under two binary operators notated $+$ and $\times$.
The notations are suggestive, but in fact we have free reign in choosing the set, elements, and operators, so long as the following axioms\footnote{The equations are taken almost literally from \url{https://en.wikipedia.org/wiki/Semiring}.} are satisfied:
\begin{eqnarray*}
(a + b) + c &=& a + (b + c) \\
0 + a &=& a \\
a + 0 &=& a \\
a + b &=& b + a \\
(a \times b) \times c &=& a \times (b \times c) \\
1 \times a &=& a \\
a \times 1 &=& a \\
a \times (b + c) &=& (a \times b) + (a \times c) \\
(a + b) \times c &=& (a \times c) + (b \times c) \\
While we leave most proof details to the accompanying Coq code, it does seem important to introduce two key principles that are often implicit in proofs on paper.
The first is \emph{algebraic simplification}\index{algebraic simplification}, where we apply the defining equations of a recursive definition to simplify a goal.
For example, recall that our definition of expression size included this clause.
We may apply the defining equation to rewrite into a different formula, where we have essential pushed the definition of $\size{\cdot}$ through the $\mathsf{Plus}$.
We may use already-proved theorems via a more general \emph{rewriting}\index{rewriting} mechanism, applying whenever we know some quantified equality.
Within a new goal we are proving, we find some subterm that matches the lefthand side of that equality, after we choose the proper values of the quantified variables.
The process of finding those values automatically is called \emph{unification}\index{unification}.
Rewriting enables us to take the subterm we found and replace it with the righthand side of the equation.
As an example, assume that, for some $P$, we know $P(2+\size{\mathsf{Var}(x)})$ and are trying to prove $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$.
We may use our earlier fact to rewrite the argument of $P$ in what we are trying to show, so that it now matches the argument from what we already know, at which point the proof is trivial to finish.
Here, unification found the assignment $e =\mathsf{Var}(x)$.
We close the chapter with an important note on terminology.
A formula like $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$ combines several levels of notation.
We consider that we are doing our mathematical reasoning in some \emph{metalanguage}\index{metalanguage}, which is often applicable to a wide variety of proof tasks.
We also happen to be applying it here to reason about some \emph{object language}\index{object language}, a programming language whose syntax is defined formally, here the language of arithmetic expressions.
We have $x$ as a variable of the metalanguage, while $\mathsf{Var}(x)$ is a variable expression of the object language.
It is difficult to use English to explain the distinction between the two in complete formality, but be on the lookout for places where formulas mix concepts of the metalanguage and object language!
The general patterns should soon become clear, as they are somehow already familiar to us from natural-language sentences like:
\begin{quote}
The wise man said ``it is time to prove some theorems.''
\end{quote}
The quoted remark could just as well be in Spanish instead of English, in which case we have two languages nested in a nontrivial way.
We start at the top left, with a given expresson $e$ and valuation $v$.
The diagram shows the equivalence of \emph{two different paths} to the bottom right.
Each individual arrow is labeled with some description of the transformation it performs, to get from the term at its source to the term at its destination.
The right-then-down path is based on substituting and then interpreting, while the down-then-right path is based on extending the valuation and then interpreting.
Since both paths wind up at the same spot, the diagram indicates an equality between the corresponding terms.
It's a matter of taste whether the theorem statement or the diagram expresses the property more clearly!
As an example of a very different language, consider a \emph{stack machine}\index{stack machine}, similar at some level to, for instance, the Forth\index{Forth} programming language, or to various postfix\index{postfix} calculators.
Though here we defined an explicit grammar for programs, which are just sequences of instructions, in general we'll use the notation $\overline{X}$ to stand for sequences of $X$'s, and the associated concrete syntax won't be so important.
We also freely use single instructions to stand for programs, writing just $i$ in place of $i; \cdot$.
\newcommand{\push}[2]{#1 \rhd #2}
Each instruction of this language transforms a \emph{stack}\index{stack}, a last-in-first-out list of numbers.
Rather than spend more words on it, here is an interpreter that makes everythig precise.
Here and elsewhere, we overload the Oxford brackets $\denote{\ldots}$ shamelessly, where context makes clear which language or interpreter we are dealing with.
We write $s$ for stacks, and we write $\push{n}{s}$ for pushing number $n$ onto the top of stack $s$.
The last two cases require the stack have at least a certain height.
Here we'll ignore what happens when the stack is too short, though it suffices, for our purposes, to add pretty much any default behavior for the missing cases.
We overload $\denote{\overline{i}}$ to refer to the \emph{composition} of the interpretations of the different instructions within $\overline{i}$, in order.
Next, we give our first example of what might be called a \emph{compiler}\index{compiler}, or a translation from one language to another.
Let's compile arithmetic expressions into stack programs, which then become easy to map onto the instructions of common assembly languages.
In that sense, with this translation, we make progress toward efficient implementation on commodity hardware.
Throughout this book, we will use notation $\compile{\ldots}$ for compilation, where the floor-based notation suggests \emph{moving downward} to a lower abstraction level.
We strengthen the statement by considering both an arbitrary initial stack $s$ and a sequence of extra instructions $\overline{i}$ to be run after $e$.
The interpreter approach to semantics is usually the most convenient one, when it applies.
Coq requires that all programs terminate, and that requirement is effectively also present in informal math, though it is seldom called out with the same terms.
Instead, with math, we worry about whether recursive systems of equations are well-founded, in appropriate senses.
From either perspective, extra encoding tricks are required to write a well-formed interpreter for a Turing-complete\index{Turing-completeness} language.
We will dodge those complexities for now by defining a simple imperative language with bounded loops, where termination is easy to prove.
\textrm{Command}& c &::=&\mathsf{skip}\mid x \leftarrow e \mid c; c \mid\repet{e}{c}
\end{array}$$
Now the implicit state, read and written by a command, is a variable valuation, as we used in the interpreter for expressions.
A $\mathsf{skip}$ command does nothing, while $x \leftarrow e$ extends the valuation to map $x$ to the value of expression $e$.
We have simple command sequencing $c_1; c_2$, in addition to the bounded loop $\repet{e}{c}$, which executes $c$ a number of times equal to the value of $e$.
\newcommand{\id}[0]{\mathsf{id}}
To give the semantics, we need a few commonplace notations that are worth reviewing.
We write $\id$ for the identity function\index{identity function}, where $\id(x)= x$; and we write $f \circ g$ for composition of functions\index{composition of functions}$f$ and $g$, where $(f \circ g)(x)= f(g(x))$.
We also have iterated self-composition\index{self-composition}, written like \emph{exponentiation} of functions\index{exponentiation of functions}$f^n$, defined as follows.
\begin{eqnarray*}
f^0 &=&\id\\
f^{n+1}&=& f^n \circ f
\end{eqnarray*}
From here, $\denote{\ldots}$ is easy to define yet again, as a transformer over variable valuations.
To put this semantics through a workout, let's consider a simple \emph{optimization}\index{optimization}, a transformation whose input and output programs are in the same language.
There's an additional, fuzzier criterion for an optimization, which is that it should improve the program somehow, usually in terms of running time, memory usage, etc.
The optimization we choose here may be a bit dubious in that respect, though it is related to an optimization found in every serious C\index{C programming language} compiler.
In particular, let's tackle \emph{loop unrolling}\index{loop unrolling}.
When the iteration count of a loop is a constant $n$, we can replace the loop with $n$ sequenced copies of its body.
C compilers need to work harder to find the iteration count of a loop, but luckily our language includes loops with very explicit iteration counts!
To define the transformation, we'll want a recursive function and notation for sequencing of $n$ copies of a command $c$, written $^nc$.
\begin{eqnarray*}
^0c &=&\mathsf{skip}\\
^{n+1}c &=& c; {^nc}
\end{eqnarray*}
\newcommand{\opt}[1]{{\left | #1 \right |}}
Now the optimization itself is easy to define.
We'll write $\opt{\ldots}$ for this and other optimizations, which move neither down nor up a tower of program abstraction levels.
Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches.
Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics preserving}\index{semantics preservation}.
\begin{theorem}\label{unroll}
$\denote{\opt{c}}v =\denote{c}v$.
\end{theorem}
It all looks so straightforward from that statement, doesn't it?
Indeed, there actually isn't so much work to do to prove this theorem.
We can also present it as a commuting diagram much like the prior one.
\[
\begin{tikzcd}
c \arrow{r}{\opt{\ldots}}\arrow{dr}{\denote{\ldots}}&\opt{c}\arrow{d}{\denote{\ldots}}\\
&\denote{c}
\end{tikzcd}
\]
The statement of Theorem \ref{unroll} happens to already be in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.
\begin{lemma}
$\denote{^nc}=\denote{c}^n$.
\end{lemma}
Let us end the chapter with the commuting-diagram version of the lemma statement.
\[
\begin{tikzcd}
c \arrow{r}{^n\ldots}\arrow{d}{\denote{\ldots}}&^nc \arrow{d}{\denote{\ldots}}\\
For simple programming languages where programs always terminate, it is often most convenient to formalize them using interpreters, as in the last chapter.
However, many important languages don't fall into that category, and for them we need different techniques.
Nontermination isn't always a bug; for instance, we expect a network server to run indefinitely.
We still need to be able to talk about the correct behavior of programs that run forever, by design.
For that reason, in this chapter and in most of the rest of the book, we model programs using relations, in much the same way that may be familiar from automata theory\index{automata theory}.
An important difference, though, is that, while undergraduate automata-theory classes generally study \emph{finite-state machines}\index{finite-state machines}, for general program reasoning we want to allow infinite sets of states, otherwise referred to as \emph{infinite-state systems}\index{infnite-state systems}.
Let's start with an example that almost seems too mundane to be associated with such terms.
\section{Factorial as a State Machine}
We're familiar with the factorial operation, implemented as an imperative program with a loop.
\begin{verbatim}
factorial(n) {
a = 1;
while (n > 0) {
a = a * n;
n = n - 1;
}
return a;
}
\end{verbatim}
In the analysis to follow, consider some value $n_0\in\mathbb N$ fixed, as the input passed to this operation.
A state machine is lurking within the surface syntax of the program.
In fact, we have a variety of choices in modeling it as a state machine.
Here is the set of states that we choose to use here:
$$\begin{array}{rrcl}
\textrm{Natural numbers}& n &\in&\mathbb N \\
\textrm{States}& s &::=&\mathsf{AnswerIs}(n) \mid\mathsf{WithAccumulator}(n, n)
For consistency with the notation we will be using later, we define the set $\mathcal F_0$ using an inference rule.
Equivalently, we could just write $\mathcal F_0=\{\mathsf{WithAccumulator}(n_0, 1)\}$, essentially reading off the initial variable values from the first lines of the code above.
Similarly, we also define a set of \emph{final states}\index{final state}.
Note that this definition only captures when the program is \emph{done}, not when it \emph{returns the right answer}.
It follows from the last line of the code.
The last and most important ingredient of our state machine is its \emph{transition relation}, where we write $s \to s'$ to indicate that state $s$ advances to state $s'$ in one step, following the semantics of the program.
Here inference rules are more obviously a good fit.
$$\infer{\mathsf{WithAccumulator}(n+1, a)\to\mathsf{WithAccumulator}(n, a \times(n+1))}{}$$
The first rule corresponds to the case where the program ends, because the loop test has failed and we now know the final answer.
The second rule corresponds to going once around the loop, following directly from the code in the loop body.
We can fit these ingredients into the general concept of a \emph{transition system}\index{transition system}, the term we will use throughout this book for this sort of state machine.
Actually, the words ``state machine'' suggest to many people that the state set must be finite, hence our preference for ``transition system,'' which is also used fairly frequently in semantics.
A \emph{transition system} is a triple $\angled{S, S_0, \to}$, with $S$ a set of states, $S_0\subseteq S$ a set of initial states, and $\to\;\subseteq S \times S$ a transition relation.
\end{definition}
For an arbitrary transition relation $\to$, not just the one defined above for factorial, we define its \emph{transitive-reflexive closure}\index{transitive-reflexive closure}$\to^*$ with two inference rules:
$$\infer{s \to^* s}{}
\quad\infer{s \to^* s''}{
s \to s'
& s' \to^* s''
}$$
That is, a formal claim $s \to^* s'$ corresponds exactly to the informal claim that ``starting from state $s$, we can reach state $s'$.''
\begin{definition}
For transition system $\angled{S, S_0, \to}$, we say that a state $s$ is \emph{reachable} if and only if there exists $s_0\in S_0$ such that $s_0\to^* s$.
\end{definition}
Building on these notations, here is one way to state the correctness of our factorial program, which, defining $S$ according to the state grammar above, we model as $\mathcal F =\angled{S, \mathcal F_0, \to}$.
The concept of ``invariant'' may be familiar from such relatively informal notions as ``loop invariant''\index{loop invariant} in introductory programming classes.
Intuitively, an invariant is a property of program state that \emph{starts true and stays true}, but let's make that idea a bit more formal, as applied to our transition-system formalism.
\begin{definition}
An \emph{invariant} of a transition system is a property that is always true, in all reachable states of a transition system. That is, for transition system $\angled{S, S_0, \to}$, where $R$ is the set of all its reachable states, some $I \subseteq S$ is an invariant iff $R \subseteq I$.
\end{definition}
At first look, the definition may appear a bit silly.
Why not always just take the reachable states $R$ as the invariant, instead of scrambling to invent something new?
The reason is the same as for strengthening induction hypotheses to make proofs easier.
Often it is easier to characterize an invariant that isn't fully precise, admitting some states that the system can never actually reach.
Additionally, it can be easier to prove existence of an approximate invariant by induction, by the method that this key theorem formalizes.
\begin{theorem}\label{invariant_induction}
Consider a transition system $\angled{S, S_0, \to}$ and its candidate invariant $I$. The candidate is truly an invariant if (1) $S_0\subseteq I$ and (2) for every $s \in I$ where $s \to s'$, we also have $s' \in I$.
\end{theorem}
That's enough generalities for now.
Let's define a suitable invariant for factorial.
\begin{eqnarray*}
I(\mathsf{AnswerIs}(a)) &=& n_0! = a \\
I(\mathsf{WithAccumulator}(n, a)) &=& n_0! = n! \times a
\end{eqnarray*}
It is an almost-routine exercise to prove that $I$ really is an invariant, using Theorem \ref{invariant_induction}.
The key new ingredient we need is \emph{inversion}, a principle for deducing which inference rules may have been used to prove a fact.
For instance, at one point in the proof, we need to draw a conclusion from a premise $s \in\mathcal F_0$, meaning that $s$ is an initial state.
By inversion, because set $\mathcal F_0$ is defined by a single inference rule, that rule must have been used to conclude the premise, so it must be that $s =\mathsf{WithAccumulator}(n_0, 1)$.
Similarly, at another point in the proof, we must reason from a premise $s \to s$'.
The relation $\to$ is defined by two inference rules, so inversion leads us to two cases to consider.
In the first case, corresponding to the first rule, $s =\mathsf{WithAccumulator}(0, a)$ and $s' =\mathsf{AnswerIs}(a)$.
In the second case, corresponding to the second rule, $s =\mathsf{WithAccumulator}(n+1, a)$ and $s' =\mathsf{WithAccumulator}(n, a \times(n+1))$.
It's worth checking that these values of $s$ and $s'$ are read off directly from the rules.
Though a completely formal and exhaustive treatment of inversion is beyond the scope of this text, generally it follows standard intuitions about ``reverse-engineering'' a set of rules that could have been used to derive some premise.
Another important property of invariants formalizes the connection with weakening an induction hypothesis.
\begin{theorem}\label{invariant_weaken}
If $I$ is an invariant of a transition system, then $I' \supseteq I$ (a superset of the original) is also an invariant of the same system.
\end{theorem}
Note that the larger $I'$ above may not be suitable to use in an inductive proof by Theorem \ref{invariant_induction}!
For instance, for factorial, we might define $I' =\mathcal\{\mathsf{AnswerIs}(n_0)\}\cup\{\mathsf{WithAccumulator}(n, a)\mid n, a \in\mathbb N\}$, clearly a superset of $I$.
However, by forgetting everything that we know about intermediate $\mathsf{WithAccumulator}$ states, we will get stuck on the inductive step of the proof.
Thus, what we call invariants here needn't also be \emph{inductive invariants}\index{inductive invariants}, and there may be slight terminology mismatches with other sources.
Combining Theorems \ref{invariant_induction} and \ref{invariant_weaken}, it is now easy to prove Theorem \ref{factorial_ok}, establishing the correctness of our particular factorial system $\mathcal F$.
First, we use Theorem \ref{invariant_induction} to deduce that $I$ is an invariant of $\mathcal F$.
Then, we choose the very same $I'$ that we warned above is not an inductive invariant, but which is fairly easily shown to be a superset of $I$.
Therefore, by Theorem \ref{invariant_weaken}, $I'$ is also an invariant of $\mathcal F$, and Theorem \ref{factorial_ok} follows quite directly from that fact, as $I'$ is essentially a restatement of Theorem \ref{factorial_ok}.
Coq\index{Coq} is a proof-assistant software package developed as open source, primarily by Inria\index{Inria}, the French national computer-science lab.
\section{Installation and Basic Use}
The project home page is:
\begin{center}
\url{https://coq.inria.fr/}
\end{center}
The code associated with this book is designed to work with Coq versions 8.4 and higher.
The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common.
We assume that readers have installed Coq by one of those means or another.
It will also be almost essential to use some graphical interface for Coq editing.
The author prefers Proof General\index{Proof General}, an Emacs\index{Emacs} mode:
\begin{center}
\url{http://proofgeneral.inf.ed.ac.uk/}
\end{center}
It should be possible to follow along using CoqIDE\index{CoqIDE}, a standalone tool distributed with Coq itself, but we will not give any CoqIDE-specific instructions.
The Proof General instructions are simple: after installing, within a regular Emacs session, open a file with the Coq extension \texttt{.v}.
Move the point (cursor) to a position where you would like to examine the current state of a proof, etc.
Then press C-C C-RET (``control-C, control-enter'') to run Coq up to that point.
Several display panes will open, showing different aspects of Coq's state, any error messages it wants to report, etc.
This feature is the main workhorse of Proof General.
It can be used both to move \emph{forward}, checking that Coq accepts a command; and to move \emph{backward}, to undo commands processed previously.
Proof General has plenty of other bells and whistles, but we won't go into them here.
\section{Tactic Reference}
\emph{Tactics} are the commands run in Coq to advance the state of a proof, corresponding to deduction steps at different granularities.
Here we collect all of the short explanations of tactics that appear in Coq source files associated with the chapters included in this document.
Note that many of these are specific to the \texttt{Frap} library distributed with this book, where built-in tactics often do quite similar things, but in a way that the author judges to be more of a hassle for beginners.
\begin{description}
\item[\texttt{apply} $H$] For $H$ a hypothesis or previously proved theorem, establishing some fact that matches the structure of the current conclusion, switch to proving $H$'s own hypotheses. This is \emph{backwards reasoning} via a known fact.
\item[\texttt{cases} $e$] Break the proof into one case for each constructor that might have been used to build the value of expression $e$. In the special case where $e$ essentially has a Boolean type, we consider whether $e$ is true or false.
\item[\texttt{equality}] A complete decision procedure for the theory of equality and uninterpreted functions. That is, the goal must follow from only reflexivity, symmetry, transitivity, and congruence of equality, including that functions really do behave as functions. See Section \ref{decidable}.
\item[\texttt{f\_equal}] When the goal is an equality between two applications of the same function, switch to proving that the function arguments are pairwise equal.
\item[\texttt{induct} $x$] Where $x$ is a variable in the theorem statement, structure the proof by induction on the structure of $x$. You will get one generated subgoal per constructor in the inductive definition of $x$. (Indeed, it is required that $x$'s type was introduced with \texttt{Inductive}.)
\item[\texttt{invert} $H$] Replace hypothesis $H$ with other facts that can be deduced from the structure of $H$'s statement. More detail to be added here soon!
\item[\texttt{linear\_arithmetic}] A complete decision procedure for linear arithmetic. Relevant formulas are essentially those built up from variables and constant natural numbers and integers using only addition and subtraction, with equality and inequality comparisons on top. (Multiplication by constants is supported, as a shorthand for repeated addition.) See Section \ref{decidable}.
\item[\texttt{rewrite} $H$] Where $H$ is a hypothesis or previously proved theorem, establishing \texttt{forall x1 .. xN, e1 = e2}, find a subterm of the goal that equals \texttt{e1}, given the right choices of \texttt{xi} values, and replace that subterm with \texttt{e2}.
\item[\texttt{ring}] Prove goals that are equalities over some registered ring or semiring, in the sense of algebra, where the goal follows solely from the axioms of that algebraic structure. See Section \ref{decidable}.
\item[\texttt{simplify}] Simplify throughout the goal, applying the definitions of recursive functions directly. That is, when a subterm matches one of the \texttt{match} cases in a defining \texttt{Fixpoint}, replace with the body of that case, then repeat.
\item[\texttt{symmetry}] When proving $X = Y$, switch to proving $Y = X$.
\item[\texttt{transitivity} $X$] When proving $Y = Z$, switch to proving $Y = X$ and $X = Z$.
\item[\texttt{trivial}] Coq maintains a database of simple proof steps, such as proving a fact by direct appeal to a matching hypothesis. \texttt{trivial} asks to try all such simple steps.
\item[\texttt{unfold} $X$] Replace $X$ by its definition.
\end{description}
\section{Proof-Automation Basics}
Coming soon!
\section{Further Reading}
For more Coq information, we recommend a few books (beyond the Coq reference manual). Some focus purely on introducing Coq:
\begin{itemize}
\item Adam Chlipala, \emph{Certified Programming with Dependent Types}, MIT Press, \url{http://adam.chlipala.net/cpdt/}
\item Yves Bertot and Pierre Cast\'eran, \emph{Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions}, Springer, \url{https://www.labri.fr/perso/casteran/CoqArt/}
\end{itemize}
The first of these two, especially, goes in-depth on the automated proof-scripting principles showcased from time to time in the Coq example code associated with the present book.
There are also other sources that introduce program-reasoning principles at the same time, including:
\begin{itemize}
\item Benjamin C. Pierce et al., \emph{Software Foundations}, \url{http://www.cis.upenn.edu/~bcpierce/sf/}
\end{itemize}
\emph{Software Foundations} generally proceeds at a slower pace than this book does.
