\chapter{Definitions and Statements}
\label{chap:definitions-and-statements}

We start our journey by studying the basics of Lean, without carrying out any
proofs yet. We review how to define new types and functions and how to state
their expected properties as lemmas.

Lean's logical foundation is a rich formalism called the \emph{calculus of
inductive constructions}, which supports \emph{dependent types}. In this
chapter, we restrict our attention to its simply (i.e., nondependently) typed
fragment. It is inspired by the \li{λ}-calculus and resembles typed
functional programming languages such as Haskell, OCaml, and Standard ML. Even
if you have not been exposed to these languages, you will recognize many of the
concepts from modern languages (e.g., Python, C++11, Java 8). In a first
approximation:
%
\[\text{Lean \texttt{=} functional programming \texttt{+} logic}\]

If your background is in mathematics, you probably already know most of the
key concepts underlying functional programming, sometimes under different
names. For example, the Haskell program
%
\begin{lstlisting}[language=]
fib 0 = 0
fib 1 = 1
fib n = fib (n - 2) + fib (n - 1)
\end{lstlisting}
%
closely matches the mathematical definition
%
\[\text{\textit{fib}(\textit{n})} = \begin{cases}
  \text{0} & \text{if~}\textit{n} = \text{0} \\[-\jot]
  \text{1} & \text{if~}\textit{n} = \text{1} \\[-\jot]
  \textit{fib}\text{(}\textit{n} - \text{2)} + \textit{fib}\text{(}\textit{n} - \text{1)} & \text{if~\textit{n}} \ge \text{2}
\end{cases}\]

\section{Types and Terms}
\label{sec:types-and-terms}

\emph{Simple type theory} (also called \emph{higher-order logic}) corresponds
roughly to the simply typed \li{λ}-calculus \cite{barendregt-et-al-2013}
extended with an equality operator (\li{=}). It is an abstract, extremely
simplified version of a programming language with a function-calling mechanism
that prefigures functional programming. It can also be viewed as a
generalization of first-order logic (also called predicate logic).

\subsection{Types}
\label{ssec:types}

\emph{Types} are either basic types such as \li{ℤ}, \li{ℚ}, and \li{bool} or
total functions \hbox{\li{σ → τ}}, where \li{σ} and \li{τ} are themselves
types. Types indicate which values an expression may evaluate to. They
introduce a discipline that is followed somewhat implicitly in mathematics. In
principle, nothing prevents a mathematician from stating \li{1 ∈ 2}, but a
typing discipline would mark this as the error it likely is.

Semantically, types can be viewed as sets. We would normally define the
types \li{ℤ}, \li{ℚ}, and \li{bool} so that they faithfully capture
the mathematicians' \li{ℤ} and \li{ℚ} and the computer scientists' Booleans,
and similarly for the function arrow (\li{→}). But despite their similarities,
Lean and mathematics are distinct languages. Lean's types may be
\emph{interpreted as} sets, but they \emph{are not} sets.

\emph{Higher-order types} are types containing left-nested \li{→} arrows.
Values of such types are functions that take other functions as arguments.
Accordingly, the type \li{(ℤ → ℤ) → ℚ} is the type of unary functions that
take a function of type \li{ℤ → ℤ} as argument and that return a value of type
\li{ℚ}.

\subsection{Terms}
\label{ssec:terms}

The \emph{terms}, or expressions, of simple type theory consist of
\begin{itemize}
\item \emph{constants}~\li{c};
\item \emph{variables} \li{x};
\item \emph{applications} \li{t u};
\item \li{λ}\emph{-expressions} \li{λx, t}.
\end{itemize}
%
Above, \li{t} and \li{u} denote arbitrary terms. We can also write
\li{t : σ} to indicate that the term \li{t} has the type \li{σ}.

A \relax{constant} \li{c : σ} is a symbol of type \li{σ} whose meaning is
fixed in the current global context. For example, an arithmetic theory
might contain constants such as \li{0 : ℤ}, \li{1 : ℤ},
\li{abs : ℤ → ℕ}, \li{square} \li{: ℕ → ℕ}, and \li{prime} {\li{:}} \li{ℕ → bool}.
Constants include functions (e.g., \li{abs}) and predicates (e.g., \li{prime}).

A \relax{variable} \li{x : σ} is either \emph{bound} or \emph{free}. A bound
variable refers back to the input of a \li{λ}-expression \li{λx : σ, t}
enclosing it. In \li{λx :} \hbox{\li{ℤ, square (abs x)}} the second \li{x}
is a variable that refers back to the \li{λ}~binder's input \li{x}.
By contrast, a free variable is declared in the local context---a concept that
will be explained below.

An \relax{application} \li{t u}, where \li{t : σ → τ} and \li{u : σ}, is a term
of type \li{τ} denoting the result of applying the function \li{t} to the
argument \li{u}---e.g., \li{abs 0}. No parentheses are needed around the
argument, unless it is a complex term---e.g., \li{prime (abs 0)}.

Given a term \li{t : τ}, a \li{λ}\relax{-expression} \li{λx : σ, t} denotes the
total function of type \li{σ} \li{→} \li{τ} that maps each input value \li{x}
of type \li{σ} to the function body \li{t}, where \li{t} may
contain \li{x}\nobreak. For example, \hbox{\li{λx : ℤ,}} \li{square (abs x)} denotes the
function that maps (the value denoted by) \li{0} to (the value denoted by)
\li{square} \hbox{\li{(abs 0)},} that maps \li{1} to \li{square (abs 1)}, and
so on. A more intuitive syntax would have been \li{x ↦ square} \li{(abs x)}, but
this is not supported by Lean.

Applications and \li{λ}-expressions mirror each other: A
\li{λ}-expres\-sion ``builds'' a function; an application ``destructs''
a function. Although our functions are unary (i.e., they take one argument),
we can build \textit{n}-ary functions by nesting \li{λ}s, using an ingenious
technique called \emph{currying}. For example, \li{λx : σ, (λy : τ, x)} denotes
the function of type \li{σ → (τ → σ)} that takes two arguments and returns the
first one. Strictly speaking, \li{σ → (τ → σ)} takes a single argument and
returns a function, which in turn takes an argument. Applications work
in the same way: If \li{K := (λx : ℤ, (λy : ℤ, x))}, then
\li{K 1 = (λy : ℤ, 1)} and \li{(K 1) 0 = 1}. The function \li{K} in \li{K 1},
which is applied to a single argument, is said to be \emph{partially applied}.

Currying is so useful a concept that we will omit most parentheses, writing
%
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\li|σ → τ → υ| & for & \li|σ → (τ → υ)| \\
\li|t u v| & for & \li|(t u) v| \\
\hphantom{\li|()|}\li|λx : σ, λy : τ, t| & for & \li|λx : σ, (λy : τ, t)|\hphantom{\li|,|} \\
\end{tabular}
\end{center}
%
and also
%
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\hphantom{\li|,|}\li|λ(x : σ) (y : τ), t| & for & \li|λx : σ, λy : τ, t| \\
\li|λx y : σ, t| & for & \li|λ(x : σ) (y : σ), t|\hphantom{\li|,,|} \\
\end{tabular}
\end{center}

In mathematics, it is customary to write binary operators in infix
syntax---e.g., \li{x + y}. Such notations are also possible in Lean, as
syntactic sugar for \li{(+) x y}. The parentheses around the \li{+} sign are
necessary to disable the parsing of \li{+} as an infix operator. Partial
application is possible with this syntax. For example, \li{(+) 1} denotes the
unary function that adds one to its argument. Other ways to write this function
are \li{λx, (+) 1 x} and \li{λx, 1 + x}.

One way to work with Lean is to declare the types and constants we need using
the \li{constant}(\li{s}) command. Consider the following declarations:

\lstinputlisting[linerange=abfg_def-q,emph={b},emphstyle={\color{procnamecolor}}]{../lean/love01_definitions_and_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=abfg_check-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
The first three lines declare four constants (\li{a}, \li{b}, \li{f},
\li{g}), which can be used to form terms. The last two lines use the
\li{#check} command to type-check some terms and show their types.
The \li{#} prefix identifies diagnosis commands:\ commands that are useful for
debugging but that we would normally not keep in our Lean files.

The \li{constant}(\li{s}) command can even be used to declare types. In Lean,
types are terms like any other. The next example introduces a type of
``Trooleans'' and three constants of that type:

\lstinputlisting[linerange=trool-q,emph={trool.false,trool.maybe},emphstyle={\color{procnamecolor}}]{../lean/love01_definitions_and_statements_demo_master.lean}
%
The constants thus introduced have no definition. They are fully unspecified.
We cannot tell whether \li{trool.true}, \li{trool.false}, and
\li{trool.maybe} are equal or not, and we know nothing about \li{trool} except
that it has at least one value (e.g., \li{trool.true}).

\subsection{Type Checking and Type Inference}
\label{ssec:type-checking-and-type-inference}

When Lean parses a term, it checks whether the term is well typed. In the
process, it tries to infer the types of bound variables if those are
omitted---e.g., the type of \li{x} in \li{λx, 1 + x}. Type inference lightens
notations and saves some typing.

For simple type theory, type checking and type inference are decidable
problems. Advanced features such as overloading (the possibility to reuse the
same name for several constants---e.g., \li{0 : ℕ} and \li{0 : ℝ}) can lead to
undecidability \cite{pierce-2002}. Lean takes a pragmatic,
computer-science-oriented approach and assumes that numerals \li{0}, \li{1},
\li{2}, \ldots{} are of type \li{ℕ} if several types are possible.

Lean's type system can be expressed as a formal system. A \emph{formal system}
consists of \emph{judgments} and of (\emph{derivation}) \emph{rules} for
producing judgments. A typing judgment has the form \li{C ⊢ t : σ}, meaning
that term \li{t} has type \li{σ} in local context~\hbox{\li{C}.} The local context
gives the types of the variables in \li{t} that are not bound by a~\li{λ}.
The local context is used to keep track of the variables bound by \li{λ}'s
\emph{outside}~\li{t}. For a function definition, it will consist of the
function's parameters. For example, in Lean, the right-hand side of the last
equation of \li{fib}'s above would be type-checked in a local context consisting
of \li{n : ℕ}.

For simple type theory, there are four typing rules, one per kind of term:

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Cst}\quad if \lic{c} is declared with type~\lic|\σ|}
  {\strut\text{\lic{C ⊢ c : σ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Var}\quad if \lic{x : σ} is the last occurrence of \lic{x} in \lic{C}}
  {\strut\text{\lic{C ⊢ x : σ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{App}}
  {\strut\text{\lic{C ⊢ t : σ → τ}}}
  {\strut\text{\lic{C ⊢ u : σ}}}
  {\strut\text{\lic{C ⊢ t u : τ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Lam}}
  {\strut\text{\lic|C, x : σ ⊢ t : τ|}}
  {\strut\text{\lic|C ⊢ (λx : σ, t) : σ → τ|}}}

\vskip\belowdisplayskip

Each rule has zero or more premises (above the horizontal bar), a conclusion
(below the bar), and possibly a side condition. The premises are typing
judgments, whereas the side conditions are arbitrary mathematical conditions on
the mathematical variables occurring in the rule. To discharge the premises, we
need to continue performing a derivation upward, as we will see in a moment. As
for the side conditions, we can use the entire arsenal of mathematics to show
that they are true.

The first two rules, labeled \textsc{Cst} and \textsc{Var}, have no premises,
but they have side conditions
that must be satisfied for the rules to apply. The last two rules take one or
two judgments as premises and produce a new judgment. \textsc{Lam} is the only
rule that modifies the local context: As we enter the body~\li{t} of a
\li{λ}-expression, we need to record the existence of the bound variable~\li{x}
and its type to be ready when we meet \li{x} in~\li{t}.

We can use this rule system to prove that a given term is well typed by
working our way backwards (i.e., upwards) and applying the rules, building a
\emph{formal derivation} of a typing judgment. Like natural trees, derivation
trees are drawn with the root at the bottom. The derived judgment appears at
the root, and each branch ends with the application of a premise-less rule.
Rule applications are indicated by a horizontal bar and a label. The following
typing derivation establishes that the term \li{λx : ℤ, abs x} has type
\li{ℤ → ℕ} in an arbitrary local context \li{C}:
%
\begin{gather*}
\prftree[r]{\textsc{Lam}}
  {\prftree[r]{\textsc{App}}
    {\prftree[r]{\textsc{Cst}}
      {\strut\text{\lic{C, x : ℤ ⊢ abs : ℤ → ℕ}}}}
    {\prftree[r]{\textsc{Var}}
      {\strut\text{\lic{C, x : ℤ ⊢ x : ℤ}}}}
    {\strut\text{\lic{C, x : ℤ ⊢ abs x : ℕ}}}}
  {\strut\text{\lic{C ⊢ (λx : ℤ, abs x) : ℤ → ℕ}}}
\end{gather*}
%
Reading the proof from the root upwards, notice how the local context is
threaded through and how it is extended by the \textsc{Lam} rule. The rule
moves the variable bound by the \li{λ}-expression to the local context, making
an application of \textsc{Var} possible further up the tree. If the
variable~\li{x} is already declared in \li{C}, it becomes shadowed by
\li{x : ℤ} after entering the \li{λ}-expression.

The above type system only checks that terms are well typed. It does not check
that types are well formed. For example, \hbox{\li{list ℤ}} is well formed, whereas
\hbox{\li{ℤ list}} and \li{list list} are ill-formed. For simple type theory,
well-formedness is easy to check: Only declared type constructors should be
used, and each \textit{n}-ary type constructor should be passed exactly
\textit{n}~type arguments.

As a side note, type inference is a generalization of type checking where the
types on the right-hand side of the colon (\li{:}) in judgments may be replaced
by placeholders. Lean's type inference is based on an algorithm due to Hindley
\cite{hindley-1969} and Milner \cite{milner-1978}, which also forms the basis of
Haskell, OCaml, and Standard ML. The algorithm generates type constraints
involving type variables \li{?α}, \li{?β}, \li{?γ}, \dots, and attempts to solve
them using a type unification procedure. For example, when inferring the type
\li{?α} of \li{λx, abs x}, Lean would perform the following schematic type
derivation:
%
\begin{gather*}
\prftree[r]{\textsc{Lam}}
  {\prftree[r]{\textsc{App}}
    {\prftree[r]{\textsc{Cst}}
      {\strut\text{\lic{x : ?β ⊢ abs : ?β → ?γ}}}}
    {\prftree[r]{\textsc{Var}}
      {\strut\text{\lic{x : ?β ⊢ x : ?β}}}}
    {\strut\text{\lic{x : ?β ⊢ abs x : ?γ}}}}
  {\strut\text{\lic{\⊢ (λx, abs x) : ?α}}}
\end{gather*}
%
In addition, Lean would generate the following constraints to ensure that all
the rule applications are legal:
%
\begin{itemize}
\item[1.] For the application of \textsc{Lam}, the type of \li{λx, abs x} must be of
  the form \li{?β →} \hbox{\li{?γ}}, for some types \li{?β} and \li{?γ}. Thus,
  Lean would generate the constraint \li{?α =} \li{?β → ?γ}.

\item[2.] For the application of \textsc{Cst}, the type of \li{abs} must correspond
  to the declaration as \li{ℤ → ℕ}. Thus, Lean would generate the constraint
  \li{?β → ?γ = ℤ → ℕ}.
\end{itemize}
%
Solving the two constraints yields \li{?α := ℤ → ℕ}, which is indeed the type
that Lean infers for \li{λx, abs x}.

\subsection{Type Inhabitation}
\label{ssec:type-inhabitation}

Given a type~\li{σ}, the type inhabitation problem consists of finding an
``inhabitant'' of that type---a term of type~\li{σ}---within the empty
local context. It may seem like a pointless exercise, but as we will see in
Chapter~\ref{chap:forward-proofs}, this problem is closely related to that
of finding a proof of a proposition. Seemingly silly exercises of the form
``find a term of type \li{σ}'' are good practice towards mastery of theorem
proving.

To create a term of a given type, start with the placeholder \li{_} and
recursively apply a combination of the following two steps:
%
\begin{itemize}
\item[1.] If the type is of the form \li{σ → τ}, a possible inhabitant is an
  anonymous function, of the form \li{λx : σ, _}, where \li{_} is a placeholder
  for a missing term of type \li{τ}. Lean will mark \li{_} as an error; if you hover over it
  in Visual Studio Code, a tooltip will show the missing term's type as well as
  any variables declared in the local context.

\item[2.] Given a type \li{σ} (which may be a function type), you can use any
  constant~\li{c} or variable \li{x :} \li{τ}$_\texttt{1}$ \li{→} \li{⋯} \li{→}
  \li{τ}$_\ttvar{n}$ \li{→} \li{σ} to build a term of that type.
  For each argument, you need to put a placeholder, yielding \li{c} \li{_}
  \li{…} \li{_} or \li{x} \li{_} \li{…} \li{_}.
\end{itemize}
%
The placeholders can be eliminated recursively using the same procedure.

As an example, we will apply the procedure to find a term of type
%
\[\hbox{\li{(α → β → γ) → ((β → α) → β) → α → γ}}\]
%
Initially, only step~1 is applicable, with \li{σ := α → β → γ} and
\hbox{\li{τ :=}} \hbox{\li{((β → α) → β)}} \li{→ α → γ}. (Recall that \li{→} is
right-associative:\ \li|σ → τ → υ| stands for \li|σ → (τ → υ)|.)
This results in the term
\li{λf, _}, which has the right type but has a placeholder left. Since the
argument \li{f} has type~\li{σ}, a function type, it makes sense to use the
name \li{f} for it. Then we continue recursively with the placeholder, of
type~\li{τ}. Again, only step~1 is possible, so we end up with the term
\li{λf, λg, _}, where \li{g} has type \li{(β → α) → β} and the placeholder has
type \li{α → γ}. A third application of step~1 yields \hbox{\li{λf, λg, λa, _},}
where \li{a} has type~\li{α} and the placeholder has type~\hbox{\li{γ}.}

At this point, step~1 is no longer possible. Let us see if step~2 is
applicable. The context surrounding the placeholder contains the following
variables:
%
\[\hbox{\ctxt{f} \lic|: α → β → γ,| \,\ctxt{g} \lic|: (β → α) → β,| \,\ctxt{a} \lic|: α|}\]
%
Recall that we are trying to build a term of type \li{γ}. The only variable we
can use to achieve this is \li{f}: It takes two arguments and returns a value
of type~\li{γ}. So we replace the placeholder with the term \li{f _ _}, where
the two new placeholders stand for the two missing arguments. Putting
everything together, we now have the term \li{λf, λg, λa, f _ _}.

Following \li{f}'s type, the placeholders are of type \li{α} and \li{β},
respectively. The first placeholder is easy to fill, using step~2 again, by
simply supplying \li{a}, of type \li{α}, with no arguments. For the
second placeholder, we apply step~2 with the variable~\hbox{\li{g},}
which is the only source of \li{β}s. Since \li{g} takes an argument, we must
supply a placeholder. This means our current term is \li{λf, λg, λa, f a (g _)}.

We are almost done. The only placeholder left has type \hbox{\li{β →}}
\li{α}, which is \li{g}'s argument type. Applying step~1, we replace the
placeholder with \li{λb, _}, where \li{_} has type \li{α}. Here, we can
simply supply \li{a}. Our final term is \li{λf, λg, λa, f a (g (λb, a))}---i.e.,
\li{λf g a, f a (g (λb, a))}.

The above derivation was tedious but deterministic: At each point, either step
1~or~2 was applicable, but not both. In general, this will not always be the
case. For some other types, we might encounter dead ends and need to backtrack.
We might also fail altogether, with nowhere to backtrack to. Notably, with an
empty local context, it is impossible to supply a witness for \li{α}.

\thekeyidea{term}

\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{Natural Numbers}
\label{ssec:natural-numbers}

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

\lstinputlisting[linerange=nat_def-q]{../lean/love01_definitions_and_statements_demo_master.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}} \\
\lic{|}\, \ttvar{constructor-name}$_\texttt{1}$ \,\lic{:}\, \ttvar{constructor-type}$_\texttt{1}$ \\[-0.5\jot]
\noindent\hbox{}\phantom{\lic{|}\, \textit{co}}$\vdots$ \\
\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{ℕ}, \li{0}, \li{1}, \li{2}, \ldots, and indeed the predefined \li{nat}
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{my_nat}} and
\li{end} \li{my_nat}, to keep its effects contained to a portion of the file. After
\li{end} \li{my_nat}, 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 located 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
\li{#print} command. For example, \li{#print nat} within the \li{my_nat}
namespace displays the following information:
%
\begin{lstlisting}[language=leanxbw]
inductive my_nat.nat : Type
constructors:
my_nat.nat.zero : nat
my_nat.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:rational-and-real-numbers}.

\subsection{Arithmetic Expressions}
\label{ssec: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. The next
example shows how this could be done in Lean:

\lstinputlisting[linerange=aexp_def-q]{../lean/love01_definitions_and_statements_demo_master.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}, we have that \li{aexp.num i} is an \li{aexp}
  value.

\item[2.] For every character string \li{x}, we have that \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.
%xtensibility 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 {
    AET_NUM, AET_VAR, AET_ADD, AET_SUB, AET_MUL, AET_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 = AET_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{Lists}
\label{ssec:lists}

The next type we consider is that of finite lists:

\lstinputlisting[linerange=list_def-q]{../lean/love01_definitions_and_statements_demo_master.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 (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. Inside the definition, since \hbox{\li{α}} is fixed as a
\emph{parameter} on the left-hand side of the colon, it is sufficient to write
\li{list} to get \li{list α}. Polymorphism is related to generics (in Java) and
templates (in C++). The general idea in all cases is to have parameterized
types.

The following commands display the constructors' types:

\lstinputlisting[linerange=check_list-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
The output is
%
\begin{lstlisting}[language=]
list.nil : Π(α : Type), list α
list.cons : ?M_1 → list ?M_1 → list ?M_1
\end{lstlisting}
%
Informally:
%
\begin{itemize}
\item The \li{nil} constructor takes a type \li{α} as argument and produces a
  result of type \li{list α}. The $\Pi$ syntax for the type argument will
  be explained in Chapter~\ref{chap:forward-proofs}.

\item The \li{cons} constructor takes an element (the \emph{head}) of some
  arbitrary type \hbox{\li{?M_1}} as argument and a list over \li{?M_1} (the
  \emph{tail}) and produces a result of type \li{list ?M_1}. Unlike for
  \li{nil}, there is no need to pass a type argument to \li{cons}---the type
  is inferred from the first argument. If we want to pass the type argument
  explicitly, we need to write an at sign (\li{@}) in front of the constant:
  \li{@list.cons}. We then have the type
  \li{Πα : Type, α → list α → list α}.
\end{itemize}

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{Π}
above, \li{Sort u}, or \li{Type 1}. 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, \li{f x :: reverse ys} is parsed as
\li{(f x) :: (reverse 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; it is all too
easy to misread \li{f x::reverse ys} as \li{f (x::reverse) ys}.

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 list 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{constant}} command
described above (Section~\ref{ssec:terms}). But usually, we want to
\emph{define} the function's behavior, and for this we would use \li{def}.

Going back to the arithmetic expression example
(Section~\ref{sec:type-definitions}), 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 \emph{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
\emph{pattern matching} to distinguish the six cases:

\lstinputlisting[linerange=eval_def-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
The keyword \li{def} introduces the definition. The general format of definitions
by pattern matching is
%
\begin{quotecode}
\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{|}\, \ttvar{patterns}$_\texttt{1}$ \,\lic{:=}\, \ttvar{result}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\lic{|}\, \ttvar{pa}}$\vdots$ \\
\lic{|}\, \ttvar{patterns}$_\ttvar{n}$ \,\lic{:=}\, \ttvar{result}$_\ttvar{n}$
\end{quotecode}
%
The parentheses \li{( )} around the parameters can also be curly braces \li${ }$
if we want to make them implicit arguments. The parameters cannot be subjected
to pattern matching, only the remaining arguments (e.g., the \li{aexp} argument
of \li{eval}).

Patterns may contain variables, which are then visible in the corresponding
right-hand side, as well as constructors. For example, in the second case in
\hbox{\li{eval}'s} definition, the variable \li{x} can be used in the right-hand
side \li{env x}.

Some definitions do not need pattern matching. For these, the syntax is
simply
%
\begin{quotecode}
\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{:=} \\
\ttvar{result}
\end{quotecode}
%
We can have pattern matching without recursion (e.g., in the
\li{aexp.}\allowbreak\li{num} and \li{aexp.}\allowbreak\li{var} cases above),
and we can have recursion without pattern matching.

The basic arithmetic operations on natural numbers, such as addition, can be
defined by recursion:

\lstinputlisting[linerange=add_def-q]{../lean/love01_definitions_and_statements_demo_master.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/love01_definitions_and_statements_demo_master.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.

Perhaps you are worried about division by zero in the definition of \li{eval}
above. Let us see what \li{#eval} has to say about it:

\lstinputlisting[linerange=eval_eval-q]{../lean/love01_definitions_and_statements_demo_master.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/}}

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/love01_definitions_and_statements_demo_master.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/love01_definitions_and_statements_demo_master.lean}

The power operation (``\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/love01_definitions_and_statements_demo_master.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₂_def-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
Notice that the recursive call to \li{power₂} does \emph{not} take \li{m} as
argument. In the entire \li{def} block introducing \li{power₂}, \li{m} is fixed
as the first argument. Outside the block, \li{power₂} is a (curried) binary
function, just like \li{power}. 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/love01_definitions_and_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=power₃_def-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
Notice that the second definition is not recursive.

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

\lstinputlisting[linerange=append_def-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
The \li{append} function takes three arguments:\ a type \li{α} and two lists
of type \li{list α}. 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₂_def-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
The at sign (\li{@}) can be used to make the implicit arguments explicit.
This is occasionally necessary to guide Lean's parser.

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₃_def-q]{../lean/love01_definitions_and_statements_demo_master.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/love01_definitions_and_statements_demo_master.lean}

\section{Lemma Statements}
\label{sec:lemma-statements}

What makes Lean a proof assistant and not only a programming language is that we
can state lemmas about the types and constants we define and prove that they
hold. We will use the terms lemma, theorem, corollary, fact, property, and true
statement 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 most descriptions of first-order logic, where terms and formulas
are separate syntactic entities. 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_lemmas-q]{../lean/love01_definitions_and_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=mul_lemmas-q]{../lean/love01_definitions_and_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=reverse_reverse-q]{../lean/love01_definitions_and_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=shuffle_shuffle_shuffle-q]{../lean/love01_definitions_and_statements_demo_master.lean}

The general format is
%
\begin{quote}
\lic{lemma} \,{\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{) :} \\
\phantom{\lic{xx}}\ttvar{statement}\, \lic{:=} \\
\ttvar{proof}
\end{quote}
%
The \li{:=} symbol separates the lemma's statement and its proof. The syntax of
\li{lemma} 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{lemma} 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{constant}(\li{s}). For example:

\lstinputlisting[linerange=ab_def-q,emph={b},emphstyle={\color{procnamecolor}}]{../lean/love01_definitions_and_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=a_less_b-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
After the \li{constants} command, 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{) :} \\
\phantom{\lic{xx}}\ttvar{statement}
\end{quote}

Axioms are dangerous, because they rapidly 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 = b}, we could easily derive \li{b} \li{<} \li{b}, from
which we could derive \li{false}. The history of interactive theorem proving is
paved with inconsistent axioms. An anecdote among many: At the 2020 edition of
the Certified Programs and Proofs (CPP) 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 (CAV) 2020
\cite{gopinathan-sergey-2020}.}
Therefore, we will generally avoid axioms, preferring the benign
combination of \li{def} and \li{lemma} to the dangerous combination of
\li{constant}(\li{s}) and \li{axiom}.

From Lean's point of view, a lemma 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}

At the end of this and most other chapters, we include a brief summary of the
constructs introduced in the chapter. Some syntaxes have multiple meanings,
which will be introduced gradually. We refer to \emph{The Lean Reference
Manual} \cite{lean-reference-manual}, the \emph{Theorem Proving in Lean}
\cite{theorem-proving-in-lean} tutorial, and the \li{mathlib} documentation%
\footnote{\url{https://leanprover-community.github.io/mathlib_docs/}}
for details.

\begingroup
\summarysize

\subsection*{Diagnosis Commands}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|#check| & checks and prints type of a term \\
\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|constant|({\color{keywordcolor}\li|s|}) & declares unspecified new constants or types \\
\lic|def| & defines a new constant \\
\lic|inductive| & introduces a type and its constructors \\
\lic|lemma| & states a lemma and its proof \\
\lic|namespace … end| & collects declarations in a named scope \\
\end{xltabular}

\subsection*{Proof Commands}

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

\endgroup
