\chapter{Programs and Theorems}
\label{chap:programs-and-theorems}

We continue our study of the basics of Lean, focusing on programs and theorems,
without carrying out any proofs yet. We review how to define new types and
functions and how to state their intended properties as theorems.

\section{Type Definitions}
\label{sec:type-definitions}

A distinguishing feature of Lean's calculus of inductive constructions is its
built-in support for inductive types. An \emph{inductive type} is a type whose
values are built by applying special constants called \emph{constructors}.
Inductive types are a concise way of representing acyclic data in a program.
You may know them under some other, largely synonymous names, including
algebraic data types, inductive data types, freely generated data types,
recursive data types, and data types.

\subsection{Definition of Natural Numbers}
\label{ssec:definition-of-natural-numbers}

The ``Hello, World!''\ example of inductive types is the type \li{Nat} (\li{= ℕ})
of natural numbers. In Lean, it can be defined as follows:

\lstinputlisting[linerange=nat_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

The first line announces to the world that we are introducing a new type
called \li{Nat}, intended to represent the natural numbers.
The second and third line declare two new constructors, \li{Nat.zero} \li{:} \li{Nat}
and \li{Nat.succ : Nat → Nat}, that can be used to build values of type
\li{Nat}. Following an established convention in computer science and logic,
counting starts at zero. The second constructor is what makes this inductive
definition interesting---it requires an argument of type \li{Nat} to produce a
value of type \li{Nat}. The terms
%
\begin{center}
\li{Nat.zero} \\
\li{Nat.succ Nat.zero} \\
\li{Nat.succ (Nat.succ Nat.zero)} \\
$\vdots$
\end{center}
%
denote the different values of type \li{Nat}---zero, its successor,
its successor's successor, and so on. This notation is called \emph{unary}---or
\emph{Peano}, after the logician Giuseppe Peano. For an alternative explanation
of Peano numbers in Lean (and some groovy video game graphics),
see Kevin Buzzard's article ``Can computers prove theorems?''%
\footnote{\url{http://chalkdustmagazine.com/features/can-computers-prove-theorems/}}

The general format of type declarations is
%
\begin{quote}
\lic{inductive} \,{\color{procnamecolor}\ttvar{type-name}}
\,\tabletbreak{\qquad}
  \lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
  \lic{(}\ttvar{params}$_{\ttvar{k}}$ \lic{:} \ttvar{type}$_{\ttvar{k}}$\lic{)}%
\rlap{~\,\lic{:} \lic{Type}} \\
\noindent\hbox{}\phantom{\li{xx}}\lic{where} \\
\noindent\hbox{}\phantom{\li{xx}}\lic{|}\, \ttvar{constructor-name}$_\texttt{1}$ \,\lic{:}\, \ttvar{constructor-type}$_\texttt{1}$ \\[-0.5\jot]
\noindent\hbox{}\noindent\hbox{}\phantom{\li{xx}}\phantom{\lic{|}\, \textit{co}}$\vdots$ \\
\noindent\hbox{}\phantom{\li{xx}}\lic{|}\, \ttvar{constructor-name}$_\ttvar{n}$ \,\lic{:}\, \ttvar{constructor-type}$_\ttvar{n}$
\end{quote}

For the natural numbers, it is possible to convince Lean to use the familiar
names \li{0}, \li{1}, \li{2}, \ldots, and indeed the predefined \li{ℕ}
type offers such syntactic sugar. But using the lengthier notations sheds more
light on Lean's type definitions. (Besides, syntactic sugar is known to cause
cancer of the semicolon \cite{perlis-1982}.)

In the Lean file accompanying this chapter, the definition of \li{Nat} is
located in a namespace, delimited by \hbox{\li{namespace}} \hbox{\li{MyNat}} and
\li{end} \li{MyNat}, to keep its effects contained to a portion of the file. After
\li{end} \li{MyNat}, any occurrence of \hbox{\li{Nat},} \li{Nat.zero}, or \li{Nat.}\allowbreak\li{succ}
will refer to Lean's predefined type of natural numbers. Similarly, the entire
file is put in the \li{LoVe} namespace to prevent name clashes with
existing Lean libraries.

We can inspect an earlier definition at any point in Lean by using the
\hbox{\li{#print}} command. For example, \li{#print Nat} within the \li{MyNat}
namespace displays the following information:
%
\begin{lstlisting}[language=leanxbw]
inductive LoVe.MyNat.Nat : Type
number of parameters: 0
constructors:
LoVe.MyNat.Nat.zero : Nat
LoVe.MyNat.Nat.succ : Nat → Nat
\end{lstlisting}

The focus on natural numbers is one of the many features of this guide that
reveal a bias towards computer science. Number theorists would be more
interested in the integers \li{ℤ} and the rational numbers \li{ℚ}; analysts
would want to work with the real numbers \li{ℝ} and the complex numbers
\li{ℂ}. But the natural numbers are ubiquitous in computer science and enjoy a
very simple definition as an inductive type. They can also be used to build
other types, as we will see in
Chapter~\ref{chap:logical-foundations-of-mathematics}.

\subsection{Definition of Arithmetic Expressions}
\label{ssec:definition-of-arithmetic-expressions}

If we were to specify a calculator program or a programming language, we would
likely need to define a type to represent arithmetic expressions as an abstract
syntax tree. The next example shows how this could be done in Lean:

\lstinputlisting[linerange=aexp_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
Mathematically, this definition is equivalent to defining the type \li{AExp}
inductively by the following formation rules:
%
\begin{itemize}
\item[1.] For every integer \li{i}, the term \li{AExp.num i} is an \li{AExp}
  value. (Intuitively, the constructor \li{AExp.num} ``boxes'' an integer
  into an arithmetic expression.)

\item[2.] For every character string \li{x}, the term \li{AExp.var x} is an
  \li{AExp} value.

\item[3.] If \li{e₁} and \li{e₂} are \li{AExp} values, then so are
  \li{AExp.add e₁ e₂}, \li{AExp.sub e₁ e₂}, \li{AExp.mul e₁ e₂}, and
  \li{AExp.div e₁ e₂}.
\end{itemize}
%
The above definition is exhaustive. The only possible values for \li{AExp} are
those built using formation rules 1~to~3. Moreover, \hbox{\li{AExp}} values
built using different formation rules are distinct. These two properties of
inductive types are captured by the motto ``No junk, no confusion'' due to
Joseph Goguen.

%\subsection{Comparison with Java}
%\label{ssec:comparison-with-java}

It may be instructive to compare the concise Lean specification of \li{AExp}
above with a Java program that achieves the same. The program
consists of one interface and six classes that implement it, corresponding to
the \li{AExp} type and its six constructors:

\begin{lstlisting}[language=minijavaandc]
public interface AExp { }

public class Num implements AExp {
    public int num;

    public Num(int num) { this.num = num; }
}

public class Var implements AExp {
    public String var;

    public Var(String var) { this.var = var; }
}

public class Add implements AExp {
    public AExp left;
    public AExp right;

    public Add(AExp left, AExp right)
    { this.left = left; this.right = right; }
}

public class Sub implements AExp {
    public AExp left;
    public AExp right;

    public Sub(AExp left, AExp right)
    { this.left = left; this.right = right; }
}

public class Mul implements AExp {
    public AExp left;
    public AExp right;

    public Mul(AExp left, AExp right)
    { this.left = left; this.right = right; }
}

public class Div implements AExp {
    public AExp left;
    public AExp right;

    public Div(AExp left, AExp right)
    { this.left = left; this.right = right; }
}
\end{lstlisting}

%(Arguably the Java version is more flexible, because users can add new
%``constructors'' simply by providing new classes. But this flexibility comes at
%a price, especially when we want to reason logically about a program.
%Extensibility is possible in Lean as well if desired.)

%\subsection{Comparison with C}
%\label{ssec:comparison-with-c}

In C, the natural counterpart of an inductive type is a tagged union. The type
declarations would be as follows:
%
\begin{lstlisting}[language=minijavaandc,emph={AExpKind,aexp_num,aexp_var,aexp_binop},emphstyle={\color{procnamecolor}}]
#include <stddef.h>
#include <stdlib.h>

enum AExpKind {
    AEK_NUM, AEK_VAR, AEK_ADD, AEK_SUB, AEK_MUL, AEK_DIV
};

struct aexp;

struct aexp_num {
    int num;
};

struct aexp_var {
    char var[1024];
};

struct aexp_binop {
    struct aexp *left;
    struct aexp *right;
};
\end{lstlisting}
\betweenlistings
\begin{lstlisting}[language=minijavaandc,emph={aexp},emphstyle={\color{procnamecolor}}]
struct aexp {
    enum AExpKind kind;
    union {
        struct aexp_num anum;
        struct aexp_var avar;
        struct aexp_binop abinop;
    } data;
};
\end{lstlisting}

Corresponding to each constructor in Lean, we would need to write a function
to allocate an \li{aexp} object of the right size in memory. Here is the
definition of the function corresponding to the first constructor,
\li{AExp.num}:
%
\begin{lstlisting}[language=minijavaandc,emph={create_num},emphstyle={\color{procnamecolor}}]
struct aexp *create_num(int num)
{
    struct aexp *res = malloc(offsetof(struct aexp, data) +
            sizeof(struct aexp_num));

    res->kind = AEK_NUM;
    res->data.anum.num = num;
    return res;
}
\end{lstlisting}
%
The subtle pointer arithmetic for the \li{malloc} call is needed to allocate
exactly the right amount of memory.

\subsection{Definition of Lists}
\label{ssec:definition-of-lists}

The next type we consider is that of finite lists:

\lstinputlisting[linerange=list_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The type is \emph{polymorphic}: It is parameterized by a type \li{α}, which we
can instantiate with concrete types. For example, \li{List ℤ} is the type of
lists over integers, and \li{List} \li{(List ℝ)} is the type of lists of lists of
real numbers. The type constructor \li{List} takes a type as argument and
returns a type. Like generics in Java and templates in C++, polymorphism is a
mechanism that provides parameterized types.

The following commands display the constructors' types:

\lstinputlisting[linerange=check_list-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The output looks different from what we might expect:
%
\begin{lstlisting}[language=]
List.nil : List ?m.2396
List.cons : ?m.2397 → List ?m.2397 → List ?m.2397
\end{lstlisting}
%
Even if we try to restrict ourselves to a fragment of Lean's language, Lean
often exposes us to more advanced constructs in the output, such as \li{?m.2396}
and \hbox{\li{?m.2397}} above. Our advice is to adopt a \emph{sporty attitude}:
Do not worry if you do not always understand everything the first time. Use your
common sense and your imagination. And, above all, do not hesitate to ask.

Lean's built-in lists offer syntactic sugar for writing lists:
%
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\li|[]| & for & \li|List.nil| \\
\li|x :: xs| & for & \li|List.cons x xs| \\
\li|[x₁, …, x|$_\ttvar{n}$\li|]| & for & \li|x₁ :: … :: x|$_\ttvar{n}$\li| :: []| \\
\end{tabular}
\end{center}

The \li|::| operator, like all other binary operators, binds less tightly than
function application. Thus, \hbox{\li{f x}} \hbox{\li{::}} \hbox{\li{List.reverse ys}} is parsed as
\li{(f x) :: (List.reverse} \li{ys)}. It is good practice to avoid needless
parentheses. They can quickly impair readability. In addition, it is important
to put spaces around infix operators, to suggest the right precedence.

Functional programmers often use names such as \li{xs}, \hbox{\li{ys},} \li{zs}
for lists, although \li{l} is also common in Lean. A list contains many
elements, so a plural form is natural. A list of cats might be called
\li{cats}; a list of lists of cats, \li{catss}. When a nonempty list is
presented as a head and a tail, we usually write, say, \li|x :: xs| or
\li|cat :: cats|.

\section{Function Definitions}
\label{sec:function-definitions}

If all we want is to declare a function, we can use the \hbox{\li{opaque}} command
(Section~\ref{sec:terms}). But usually, we want to
\emph{define} the function's behavior, and for this we can use the
\li{def} command. Because Lean's roots are in functional programming, functions
are defined as mathematical expressions evaluating to a value, not as an
imperative program modifying some state. Accordingly, recursion, rather than
iteration with \li{while} or \li{for}, is the primary mechanism for traversing
data.

\subsection{Recursion on Natural Numbers}
\label{ssec:recursion-on-natural-numbers}

Let us see on a simple example how recursion works.
The Lean definition of Fibonacci numbers is as follows:
%
\lstinputlisting[linerange=fib_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The patterns on the left correspond to the argument of the function. Here,
\li{fib} is declared with a single argument of type \li{ℕ}, so we
\emph{pattern-match} on a single natural number. A pattern is triggered when the
input has the given form. For example, if the input is \li{1}, then the pattern
\li{1} matches it, and the corresponding right-hand side is evaluated. If the
input is \li{5}, then the pattern \li{n + 2} is triggered, with \li{n := 3}.
Then the right-hand side is evaluated with \li{n} set to \li{3}, yielding
\li{fib 4 + fib 3}.

The general format of recursive definitions is
%
\begin{quote}
\lic{def} {\color{procnamecolor}\,\ttvar{name}}
  \,\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
  \lic{(}\ttvar{params}$_\ttvar{m}$ \lic{:} \ttvar{type}$_\ttvar{m}$\lic{)}
  \,\lic{:}\, \ttvar{type} \\
\noindent\hbox{}\phantom{\li{xx}}\lic{|}\, \ttvar{patterns}$_\texttt{1}$ \,\lic{=>}\, \ttvar{result}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\li{xx}}\phantom{\lic{|}\, \ttvar{pa}}$\vdots$ \\
\noindent\hbox{}\phantom{\li{xx}}\lic{|}\, \ttvar{patterns}$_\ttvar{n}$ \,\lic{=>}\, \ttvar{result}$_\ttvar{n}$
\end{quote}
% 
The parameters \ttvar{params}$_\texttt{1}$ to \ttvar{params}$_\ttvar{m}$ cannot
be subjected to pattern matching, only the remaining arguments declared in
\ttvar{type}. If multiple patterns are provided on one line, they are separated
by commas.
%
Patterns may contain variables, which are then visible in the corresponding
right-hand side, as well as constructors.

The basic arithmetic operations on natural numbers, such as addition, multiplication,
and exponentiation, can be
defined by recursion. Of course, they are already defined in Lean (as \li{+},
\li{*}, and \li|^|), but they are useful exercises. We start with addition:

\lstinputlisting[linerange=add_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
We pattern-match on two arguments at the same time, distinguishing the case
where the second argument is zero and the case where it is nonzero. Each
recursive call to \li{add} peels off one \li{Nat.succ} constructor from the
second argument. Instead of \li{Nat.}\allowbreak\li{zero} and
\li{Nat.}\allowbreak\li{succ n}, Lean also allows us to write \li{0} and
\li{n + 1} as syntactic sugar.

We can evaluate the result of applying \li{add} to numbers using \li{#eval} or
\li{#reduce}:

\lstinputlisting[linerange=eval_reduce_add-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
Both commands print \li{9}, as expected (at least in Visual Studio Code).
\li{#eval} employs an optimized interpreter, whereas \li{#reduce} uses Lean's
inference kernel, which is less efficient.

It is good practice to provide a few tests each time we define a
function, to ensure that it behaves as expected. You can even leave the
\li{#eval} or \li{#reduce} calls in your Lean files as documentation.

The definition of multiplication is similar to that of addition:

\lstinputlisting[linerange=mul_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The underscore (\li{_}) stands for an unused variable. We could have
put a name (e.g., \li{m}), but \li{_} documents our intentions better.

The \li{#eval} command below prints \li{14}, as expected:

\lstinputlisting[linerange=eval_mul-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

Exponentiation (``\textit{m} to the power of \textit{n}'') can be defined
in various ways. Our first proposal is structurally identical to the definition of
multiplication:

\lstinputlisting[linerange=power_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
Since the first argument, \li{m}, remains unchanged in the recursive call,
\li{power m n}, we can factor it out and put it next to the function's name, as
a \emph{parameter}, before the colon introducing the type of the function
(excluding the parameter \li{m}):

\lstinputlisting[linerange=power_param_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
From the outside, there is no difference between the two definitions. In fact,
we already saw this syntax for the type argument \li{α} of the \li{List}
constructor (Section~\ref{sec:type-definitions}).

Yet another definition is possible by first introducing a general-purpose
iterator and then using it with the right arguments:

\lstinputlisting[linerange=iter_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=power_iter_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

The \li{iter} function takes a type \li{α}, a ``zero'' value \li{z}, a unary function \li{f}, and
a natural number \li{n}, and computes
%
\[\underbrace{\hbox{\li{f (f (⋯ (f}}}_{\text{\li{n}~times}}\,\hbox{\li{z) ⋯))}}\]
%
It is an example of a higher-order function:\ a function that takes another
function (here, \li{f}) as argument. In functional programming, functions are
treated like any other objects and can be used as arguments or as the result of
a function. Here, we use \li{iter} to compute \li{m} to the power of \li{n} as
%
\[\underbrace{\hbox{\li{mul m (mul m (⋯ (mul m}}}_{\text{\li{n}~times}}\,\hbox{\li{1) ⋯))}}\]

Finally, notice that the definition of \li{powerIter} is not recursive. For
nonrecursive functions without pattern matching, the syntax is simply
%
\begin{quote}
\lic{def} \,{\color{procnamecolor}\ttvar{name}}
\,\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
\lic{(}\ttvar{params}$_\ttvar{m}$ \lic{:} {\ttvar{type}}$_\ttvar{m}$\lic{)} \lic{:}
\ttvar{type}\,~\lic{:=} \\
\noindent\hbox{}\phantom{\li{xx}}\ttvar{result}
\end{quote}

\subsection{Recursion on Arithmetic Expressions}
\label{ssec:recursion-on-arithmetic-expressions}

Going back to the type of arithmetic expressions, if we wanted to implement an
\li{eval} function in Java, we would probably add it as part of \li{AExp}'s
interface and implement it in each subclass. For \li{Add}, \li{Sub}, \li{Mul},
and \li{Div}, we would recursively call \li{eval} on the \li{left} and
\li{right} objects.

In Lean, the syntax is very compact. We define a single function and use
pattern matching to distinguish the six cases:

\lstinputlisting[linerange=eval_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
Notice that this function is higher-order: It takes a function, \li{env}, that
represents an ``environment'' assigning values to the variables. The
environment is used in the \li{AExp.var} case to evaluate a variable and is
threaded through in the recursive cases (\li{AExp.add}, \li{AExp.sub},
\li{AExp.mul}, and \li{AExp.div}).

Perhaps you are worried about division by zero in the
\li{AExp.}\allowbreak\li{div} case. Let us see what \li{#eval} has to say about
it, using some environment that assigns 7 to all variables:

\lstinputlisting[linerange=eval_eval-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The output is \li{0}. In Lean, division is conveniently defined as a total
function that returns zero when the denominator is zero. For a lucid explanation
of why this is not dangerous, see Buzzard's blog.%
\footnote{\url{https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/}}

\subsection{Recursion on Lists}
\label{ssec:recursion-on-lists}

Recursive functions on lists can be defined in a similar way:

\lstinputlisting[linerange=append_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The \li{append} function takes three arguments:\ a type \li{α} and two lists
of type \li{List α}.

\lstinputlisting[linerange=append_eval-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
By passing the placeholder \li{_}, we leave it to Lean to
infer the type \li{ℕ} from the type of the other two arguments.

To make the type argument~\li{α} implicit, we can put it in curly braces
\li${ }$:

\lstinputlisting[linerange=append_implicit_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
The at sign (\li{@}) can be used to make the implicit arguments explicit.
This is occasionally necessary to guide Lean's parser.

\lstinputlisting[linerange=append_implicit_eval-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

We can use syntactic sugar in the definition, both in the patterns on the
left-hand sides of \li{=>} and in the right-hand sides:

\lstinputlisting[linerange=append_pretty_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

In Lean's standard library, the append function is an infix operator called
\li{++}. We can use it to define a function that reverses a list:

\lstinputlisting[linerange=reverse_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

\section{Theorem Statements}
\label{sec:theorem-statements}

What makes Lean a proof assistant and not only a programming language is that we
can state theorems about the types and constants we define and prove that they
hold. In interactive theorem proving, the terms theorem, lemma, corollary, fact,
property, and true statement are used more or less interchangeably. Similarly,
propositions, logical formulas, and statements will all mean the same.

In Lean, propositions are simply terms of type \li{Prop}. This stands in
contrast with first-order logic, where terms and formulas are traditionally
distinguished in the syntax. A proposition that can be proved is called a
theorem (or lemma, corollary, etc.); otherwise it is a nontheorem or false
statement. Mathematicians sometimes use the term ``proposition'' as a synonym
for theorem (e.g., ``Proposition~3.14''), but in formal logic propositions can
also be false.

Here are examples of true statements that can be made about the addition,
multiplication, and list reversal operations defined in
Section~\ref{sec:function-definitions}:

\lstinputlisting[linerange=add_theorems-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=mul_theorems-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=reverse_reverse-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}

The general format is
%
\begin{quote}
\lic{theorem} \,{\color{procnamecolor}\ttvar{name}}
  \,\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
  \lic{(}\ttvar{params}$_\ttvar{m}$ \lic{:} \ttvar{type}$_\ttvar{m}$\lic{) :} \\
\noindent\hbox{}\phantom{\li{xx}}\ttvar{statement}\, \lic{:=} \\
\noindent\hbox{}\phantom{\li{xx}}\ttvar{proof}
\end{quote}
%
The \li{:=} symbol separates the theorem's statement and its proof. The syntax of
\li{theorem} is very similar to that of a \li{def} command without pattern
matching, with \ttvar{statement} instead of \ttvar{type}
and \ttvar{proof} instead of \ttvar{result}. In the examples above, we put the
marker \li{sorry} as a placeholder for the actual proof. The marker is quite
literally an apology to future readers and to Lean for the absence of a
proof. It is also a reason to \emph{worry}, until we manage to eliminate it.
In Chapters \ref{chap:backward-proofs}~and~\ref{chap:forward-proofs}, we will
see how to achieve this.

The intuitive semantic of a \li{theorem} command with a \li{sorry} proof is,
``This proposition should be provable, but I have not carried out the proof
yet---sorry.'' Sometimes, we want to express a related idea, namely, ``Let us
assume this proposition holds.'' Lean provides the \li{axiom} command for this,
which is often used in conjunction with \li{opaque}. For example:

\lstinputlisting[linerange=ab_def-q,emph={b},emphstyle={\color{procnamecolor}}]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=a_less_b-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
After the \li{opaque} commands, we have no information about \li{a}
and~\hbox{\li{b}} beyond their type. The axiom specifies the desired property
about them. The general format of the command is
%
\begin{quote}
\lic{axiom} \,{\color{procnamecolor}\ttvar{name}}
  \,\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
  \lic{(}\ttvar{params}$_\ttvar{m}$ \lic{:} \ttvar{type}$_\ttvar{m}$\lic{) :} \\
\noindent\phantom{\lic{xx}}\ttvar{statement}
\end{quote}

Axioms are dangerous, because they can lead to an inconsistent logic,
in which we can derive \li{False}. For example, if we added a second axiom
stating that \li{a >} \hbox{\li{b},} we could easily derive
\li{False}. The history of interactive theorem proving is
paved with inconsistent axioms. One anecdote among many: At the 2020 edition of
the Certified Programs and Proofs conference, a submitted paper was rejected
due to a flawed axiom, from which one of the peer reviewers derived \li{False}.%
\footnote{\label{foot:false-anecdote}One of the authors of that submission
reported that the axiom has now been revised and derived as a theorem. The
entire formal development is now axiom-free. The revised paper has been accepted
at the conference Computer Aided Verification 2020
\cite{gopinathan-sergey-2020}.}
Therefore, we will generally avoid axioms.

From Lean's point of view, a theorem with a \li{sorry} proof is effectively an
axiom and can be used to play havoc with the logic's consistency. To prevent
misunderstandings, it is better to use \li{sorry} only as a temporary measure,
while developing a proof, and not as an alternative to the more explicit, and
honest, \li{axiom}.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Diagnosis Commands}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|#eval| & executes a term using an optimized interpreter \\
\lic|#print| & prints the definition of a constant \\
\lic|#reduce| & executes a term using Lean's inference kernel \\
\end{xltabular}

\subsection*{Declarations}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|axiom| & states an axiom \\
\lic|def| & defines a new constant \\
\lic|inductive| & introduces a type and its constructors \\
\lic|namespace … end| & collects declarations in a named scope \\
\lic|theorem| & states a theorem and its proof \\
\end{xltabular}

\subsection*{Proof Commands}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|sorry| & stands for a missing proof or definition \\
\end{xltabular}

\endgroup
