\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
key notion of ``proof.'' A \emph{formal proof} is a logical argument expressed
in a logical formalism. ``Formal'' is roughly synonymous with ``logical'' or
``logic-based.'' Logicians---the mathematicians of logics---carried out formal
proofs on papers decades before the advent of computers, but nowadays these
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 the 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, not only toy
examples or logic puzzles. Formal proofs also helps 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}

Formal proofs can help when we develop a new theory, to find out whether it
works and exactly which assumptions are needed. They are useful when
generalizing, refactoring, or otherwise modifying existing proof, in much the
same way as a compiler helps developing correct programs. They give a high
level of trustworthiness that makes it easier to review the proof. In
addition, formal proofs can form the basis of verified computational tools
(e.g., verified computer algebra).

\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 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}
and JinjaThreads \cite{lochbihler-2010}.

\paragraph{A Selection of Popular Proof Assistants}

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

\begin{itemize}
\item set theory: Isabelle/ZF, Metamath, Mizar;
\item simple type theory (also called higher-order logic): HOL4, HOL Light,
Isa\-belle\slash HOL;
\item dependent type theory: Agda, Coq, Lean, Matita, PVS.
\end{itemize}

ACL2 is hard to classify. It is based on a Lisp-like first-order logic.

\paragraph{Lean}

Lean is a new proof assistant developed primarily by Leonardo de Moura
(Microsoft Research) since 2012. Its mathematical library, \li{mathlib}, is
developed under the leadership of Jeremy Avigad (Carnegie Mellon University).

We will use version 3.4.2, which is likely to remain the last release before
Lean 4. We will use both Lean's basic libraries and \li{mathlib}.

Lean boasts the following strengths:

\begin{itemize}
\item It has a highly expressive logic based on the calculus of inductive
  constructions, a dependent type theory.
\item It is extended with classical axioms and quotient types.
\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}

Nonetheless, be aware that Lean is a research project, with some rough edges.

Lean's core library includes only basic algebraic definitions.
More setup and especially tactics are found in Lean's mathematical library,
\li{mathlib}.%
\footnote{\url{https://github.com/leanprover/mathlib/}}
It is more than a mathematical library; it provides a lot of basic automation
on top of bare-bones Lean.

%Link to installation instructions:
%
%  * Visual Studio Code (or Emacs?) \\
%  * elan (and Lean) \\
%  * \li{mathlib} \\
%  * LoVelib
%
%Get elan from \url{https://github.com/Kha/elan}.
%
%Investigate if obtaining binaries via "update-mathlib" works.

%\verb|leanpkg install https://github.com/leanprover-community/mathlib| and specify a branch
%Use elan/leanpkg also for LoVelib and the entire homework etc.

\paragraph{This Book}

This book is a companion to the course Logical Verification (LoVe) taught at
the Vrije Universiteit Amsterdam. Despite our attempts to make it
self-contained, unlikely to be suitable as a standalone Lean tutorial---we
recommend \emph{Theorem Proving in Lean} \cite{theorem-proving-in-lean}---nor
is it a substitute for attending class or doing the exercises. Ultimately,
theorem proving can only be learned by doing.

The Lean files accompanying this book can be found in a public repository.%
\footnote{\url{https://github.com/blanchette/logical_verification_2019}}
The files' naming scheme follows the book'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.

\paragraph{Special Symbols}

Lean lets us enter Unicode symbols such as \li{ℤ}, \li{ℚ}, and \li{→} using
\LaTeX-style macros. These symbols can be entered in Visual Studio Code by
typing \li{\Z}, \li{\Q}, or \li{\->} 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 book 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 can see the different ways in
which it can be entered.

\vskip3\smallskipamount

\begin{center}
\begin{tabular}{@{}l@{\quad}l@{\kern4em}l@{\quad}l@{\kern4em}l@{\quad}l@{\kern4em}l@{\quad}l@{}}
$\lnot$ & \verb|\not| &
$\land$ & \verb|\and| &
$\lor$ & \verb|\or| &
$\rightarrow$ & \verb|\->| \\
$\leftrightarrow$ & \verb|\<->| &
$\forall$ & \verb|\fo| &
$\exists$ & \verb|\ex| &
$\le$ & \verb|\<=| \\
$\ge$ & \verb|\>=| &
$\not=$ & \verb|\neq| &
$\lambda$ & \verb|\la| &
$\Pi$ & \verb|\Pi| \\
$\leftarrow$ & \verb|\<-| &
$\mapsto$ & \verb$\|->$ &
$\Rightarrow$ & \verb|\=>| &
$\Longrightarrow$ & \verb|\==>| \\
$\mathbb{N}$ & \verb|\N| &
$\mathbb{Z}$ & \verb|\Z| &
$\mathbb{Q}$ & \verb|\Q| &
$\mathbb{R}$ & \verb|\R| \\
$\alpha$ & \verb|\a| &
$\beta$ & \verb|\b| &
$\gamma$ & \verb|\g| &
$\delta$ & \verb|\de| \\
$_{\texttt 0}$ & \verb|\0| &
$_{\texttt 1}$ & \verb|\1| &
$_{\texttt 2}$ & \verb|\2| &
$_{\texttt 3}$ & \verb|\3| \\
\end{tabular}
\end{center}
