\chapter{Preface}

Formal proof assistants are software tools designed to help their users carry
out computer-checked proofs in a logical calculus. We usually call them
\emph{proof assistants}, or \emph{interactive theorem provers}, but a
mischievous student coined the phase ``proof-preventing beasts,'' and dictation
software occasionally misunderstands ``theorem prover'' as ``fear improver.''
Consider yourself warned.

\paragraph{Rigorous and Formal Proofs}

Interactive theorem proving has its own terminology, already starting with the
notion of ``proof.'' A \emph{formal proof} is a logical argument expressed
in a logical formalism. In this context, ``formal'' means ``logical'' or
``logic-based.'' Logicians---the mathematicians of logics---carried out formal
proofs on papers decades before the advent of computers, but nowadays formal
proofs are almost always carried out using a proof assistant.

In contrast, an \emph{informal proof} is what a mathematician would normally
call a proof. These are often carried out in \LaTeX{} or on a blackboard,
and are also called ``pen-and-paper proofs.'' The level of detail can vary a
lot, and phrases such as ``it is obvious that,'' ``clearly,'' and ``without
loss of generality'' move some of the proof burden onto the reader. A
\emph{rigorous proof} is a very detailed informal proof.

The main strength of proof assistants is that they help develop highly
trustworthy, unambiguous proofs of mathematical statements, using a precise
logic. They can be used to prove arbitrarily advanced results, and not only toy
examples or logic puzzles. Formal proofs also help students understand what
constitutes a valid definition or a valid proof. To quote
Scott Aaronson:%
\footnote{\url{https://www.scottaaronson.com/teaching.pdf}}
%
\begin{quote}
I still remember having to grade hundreds of exams where the students started
out by assuming what had to be proved, or filled page after page with
gibberish in the hope that, somewhere in the mess, they \emph{might}
accidentally have said something correct.
\end{quote}

When we develop a new theory, formal proofs can help us explore it. They are
useful when we generalize, refactor, or otherwise modify an existing proof, in
much the same way as a compiler helps us develop correct programs. They give a
high level of trustworthiness that makes it easier for others to review the
proof. In addition, formal proofs can form the basis of verified computational
tools (e.g., verified computer algebra systems).

\paragraph{Success Stories}

There have been a number of success stories in mathematics and computer
science. Three landmark results in the formalization of mathematics have
been the proof of the four-color theorem by Gonthier et
al.~\cite{gonthier-2008}, the proof of the odd-order theorem by Gonthier et
al.~\cite{gonthier-et-al-2013}, and the proof of the Kepler conjecture by Hales
et al.~\cite{hales-et-al-2015}. The earliest work in this area was carried out
by Nicolaas de Bruijn and his colleagues starting in the 1960s in a system
called AUTOMATH.%
\footnote{\url{https://www.win.tue.nl/automath/}}

Today, few mathematicians use proof assistants, but this is slowly changing.
For example, 29~participants of the Lean Together 2019 meeting in Amsterdam,%
\footnote{\url{https://lean-forward.github.io/lean-together/2019/index.html}}
about formalization of mathematics, self-identified as mathematicians.

Most users of proof assistants today are computer scientists.
A few companies, including AMD \cite{russinoff-1999} and Intel
\cite{harrison-2003}, have been using proof assistants to verify their designs.
In academia, some of the milestones are the verifications of the operating
system kernels seL4 \cite{klein-et-al-2010} and CertiKOS \cite{gu-et-al-2016}
and the development of the verified compilers CompCert \cite{leroy-2009-jar},
JinjaThreads \cite{lochbihler-2010}, and CakeML \cite{kumar-et-al-2014}.

\paragraph{Proof Assistants}

There are dozens of proof assistants in development or use across the world. A
list of the main ones follows, classified by logical foundations:

\begin{itemize}
\item set theory: Isabelle/ZF, Metamath, Mizar;
\item simple type theory: HOL4, HOL Light, Isa\-belle\slash HOL;
\item dependent type theory: Agda, Coq, Lean, Matita, PVS;
\item Lisp-like first-order logic: ACL2.
\end{itemize}

For a history of proof assistants and interactive theorem proving, we refer to
Harrison, Urban, and Wiedijk's highly informative chapter
\cite{harrison-et-al-2014}.

\paragraph{Lean}

Lean is a new proof assistant developed primarily by Leo\-nardo de Moura
(Microsoft Research) since 2012. Its mathematical library, \li{mathlib}, was
originally developed under the leadership of Jeremy Avigad (Carnegie Mellon
University) but is now maintained and further extended by the users' community
\cite{mathlib-mathlib-2020}.%
\footnote{\url{https://github.com/leanprover-community/mathlib}}

We will use Lean community version 3.20.0,
\li{mathlib} revision \li{d33341c90c18}, and a few extensions collected in a
small library called \li{LoVelib}.%
\footnote{\url{https://github.com/blanchette/logical_verification_2020/raw/master/lean/lovelib.lean}}
Although it is still a research project, with some rough edges, there are
several reasons why Lean is a suitable vehicle to teach interactive theorem
proving:

\begin{itemize}
\item It has a highly expressive, and highly interesting, logic based on the
    calculus of inductive constructions, a dependent type theory.

\item It is extended with classical axioms and quotient types, making it
  convenient to verify mathematics.

\item It includes a convenient metaprogramming framework, which can be used
  to program custom proof automation.

\item It includes a modern user interface via a Visual Studio Code plugin.

\item It has highly readable, fairly complete documentation.

\item It is open source.
\end{itemize}

Lean's core library includes only basic algebraic definitions. More setup and
proof automation are found in \li{mathlib}. It is more than a mathematical
library; it provides a lot of basic automation on top of Lean's core library
that one would expect from a modern proof assistant.

\paragraph{This Guide}

This guide is a companion to the MSc-level course Logical Verification (LoVe)
taught at the Vrije Universiteit Amsterdam. Our primary aim is to teach
interactive theorem proving. Lean is the vehicle, not an end of itself. As
such, this guide is not designed to be a comprehensive Lean tutorial---for
this, we recommend \emph{Theorem Proving in Lean}
\cite{theorem-proving-in-lean}. The guide is also no substitute for attending
class or doing the exercises and homework. Theorem proving is not for
spectators; it can only be learned by doing.

Specifically, our goal is that you
%
\begin{itemize}
\item learn fundamental theory and techniques in interactive theorem
  proving;

\item learn how to use logic as a precise language for modeling systems and
  stating properties about them;

\item familiarize yourselves with some areas in which proof assistants are
  successfully applied, such as functional programming, the semantics of
  imperative programming languages, and mathematics;

\item develop some practical skills you can apply on a larger project (as
  a hobby, for an MSc or PhD, or in industry);

\item reach a point where you feel ready to move to another proof assistant and
  apply what you have learned;

\item get to understand the domain well enough to start reading relevant
  scientific papers published at international conferences such as Certified
  Programs and Proofs (CPP) and Interactive Theorem Proving (ITP) or in journals
  such as the \emph{Journal of Automated Reasoning} (JAR).
\end{itemize}

Equipped with a good knowledge of Lean, you will find it easy to move to
another proof assistant based on dependent type theory, such as Agda or Coq, or
to a system based on simple type theory, such as HOL4 or Isa\-belle\slash HOL.

We assume that you are familiar with typed functional programming, as embodied
in the languages Haskell, OCaml, and Standard ML. If you do not see that
the term \li{g (f a b)} applies the (curried) function \li{f} to two arguments
\li{a} and \li{b} and passes the result to the function \li{g}, or that
\li{λn, n + 1} is the function that maps \li{n} to \li{n + 1}, we strongly
recommend that you start by studying a tutorial, such as the first chapters
of the online tutorial \emph{Learn You a Haskell for Great Good!}
\cite{lipovaca-2011}. You can stop reading once you have reached the end of the
section titled ``Lambdas.''

An important characteristic of this guide, which it shares with Knuth's
\emph{\TeX{}book} \cite{knuth-1986}, is that it does not always tell the truth.
To simplify the exposition, simple but false claims are made about Lean. Some
of these statements are rectified in later chapters. Like Knuth, we feel that
``this technique of deliberate lying will actually make it easier for you to
learn the ideas. Once you understand a simple but false rule, it will not be
hard to supplement that rule with its exceptions.''

The Lean files accompanying this guide can be found in a public repository.%
\footnote{\url{https://github.com/blanchette/logical_verification_2020}}
The files' naming scheme follows this guide's chapters; thus,
\verb|love06_|\allowbreak\verb|monads_|\allowbreak\verb|demo.|\allowbreak\verb|lean|
is the main file associated with Chapter~6 (``Monads''), which is demonstrated
in class,
\verb|love06_|\allowbreak\verb|monads_|\allowbreak\verb|exercise_|\allowbreak\verb|sheet.|\allowbreak\verb|lean|
is the exercise sheet, and
\verb|love06_|\allowbreak\verb|monads_|\allowbreak\verb|homework_|\allowbreak\verb|sheet.|\allowbreak\verb|lean|
is the homework sheet.

We have a huge debt to the authors of \emph{Theorem Proving in Lean}
\cite{theorem-proving-in-lean} and \emph{Concrete Semantics:\ With
Isabelle\slash HOL}~\cite{nipkow-klein-2014}, who have taught us Lean and
programming language semantics. Many of their ideas appear in this guide.

We thank Robert Lewis and Assia Mahboubi for their useful comments on this
guide's organization and focus. We thank Kiran Gopinathan and Ilya Sergey for
sharing the anecdote reported in footnote \ref{foot:false-anecdote} of
Chapter~\ref{chap:definitions-and-statements} and letting us share it further.
We thank Daniel Fabian for designing the first tablet-optimized version of this
guide. Finally, we thank Chris Bailey, Kevin Buzzard, Wan Fok\-kink, Antonius
Danny Reyes, Robert Sch\"utz, Patrick Thomas, Huub Vromen, and Wijnand van
Woerkom for reporting typos and some more serious errors they found in earlier
editions of this guide. Should \emph{you} find some mistakes in this text,
please let us know.

\paragraph{Special Symbols}

Visual Studio Code lets us enter Unicode symbols by entering backslash \li{\}
followed by an ASCII identifier. For example, \li{→}, \li{ℤ}, or \li{ℚ} can be
entered by typing \li{\->}, \li{\Z}, or \li{\Q} and pressing the tab key or the
space bar. We will freely use these notations. For reference, we provide a list
of the main non-ASCII symbols that are used in the guide and, for each, one of
its ASCII representations. By hovering over a symbol in Visual Studio Code
while holding the control or command key pressed, you will see the different
ways in which it can be entered.

\vskip3\smallskipamount

\begin{center}
\tabletsmall
\begin{tabular}{@{}l@{\quad}p{8.5em}l@{\quad}p{8.5em}l@{\quad}p{8.5em}@{}}
\li|¬| & \verb|\not| &
\li|∧| & \verb|\and| &
\li|∨| & \verb|\or| \\
\li|→| & \verb|\->| &
\li|↔| & \verb|\<->| &
\li|∀| & \verb|\fo| \\
\li|∃| & \verb|\ex| &
\li|≤| & \verb|\<=| &
\li|≥| & \verb|\>=| \\
\li|≠| & \verb|\neq| &
\li|≈| & \verb|\~~| &
\li|×| & \verb|\x| \\
\li|∘| & \verb|\circ| &
\li|∅| & \verb|\empty| &
\li|∪| & \verb|\union| \\
\li|∩| & \verb|\intersect| &
\li|∈| & \verb|\in| &
\li|⇃| & \verb|\downleftharpoon| \\
\li|◯| & \verb|\bigcirc| &
\li|←| & \verb|\<-| &
\li|↦| & \verb|\mapsto| \\
\li|⇒| & \verb|\=>| &
\li|⟹| & \verb|\==>| &
\li|⟦| & \verb|\[[| \\
\li|⟧| & \verb|\]]| &
\li|𝒜| & \verb|\McA| &
\li|ℕ| & \verb|\N| \\
\li|ℤ| & \verb|\Z| &
\li|ℚ| & \verb|\Q| &
\li|ℝ| & \verb|\R| \\
\li|α| & \verb|\a| &
\li|β| & \verb|\b| &
\li|γ| & \verb|\g| \\
\li|δ| & \verb|\de| &
\li|ε| & \verb|\e| &
\li|λ| & \verb|\la| \\
\li|σ| & \verb|\s| &
\li|₀| & \verb|\0| &
\li|₁| & \verb|\1| \\
\li|₂| & \verb|\2| &
\li|₃| & \verb|\3| &
\li|₄| & \verb|\4| \\
\li|₅| & \verb|\5| &
\li|₆| & \verb|\6| &
\li|₇| & \verb|\7| \\
\li|₈| & \verb|\8| &
\li|₉| & \verb|\9|
\end{tabular}
\end{center}

\vskip3\smallskipamount
