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

We start by the basics of Lean, without carrying out actual proofs yet. We
review how to define types and functions and how to state their intended
properties as lemmas.

Lean's logical foundation is a rich formalism called the \emph{calculus of
inductive constructions}, whose defining feature is its support for
\emph{dependent types}. In this chapter, we restrict our attention to its
simply (i.e., nondependently) typed fragment, which 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 programming
languages (e.g., Python, C++11, Java 8). In a first approximation:
%
\[\text{Lean \li{=} typed functional programming \li{+} 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 corresponds to 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}\]
%
If you are not familiar with typed functional programming, we recommend that you
study a tutorial, such as the first six chapters of \emph{Learn You a Haskell
for Great Good!}%
\footnote{\url{http://learnyouahaskell.com/}}

\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{DBLP:books/daglib/0032840}
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.

\paragraph{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 regarded as sets. We would normally define the
types \li{ℤ}, \li{ℚ}, and \li{bool} in such a way 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; when studying them, it is
important to keep them apart. Lean's types may be \emph{interpreted} as
mathematical 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{ℤ}.

\paragraph{Terms}

The \emph{terms}, or expressions, of simple type theory consist of
constants~\hbox{\li{c},} applications \li{t u}, \li{λ}-expressions \li{λx, t},
and variables \li{x}, where \li{t} and \li{u} denote terms. We write
\li{t : σ} to indicate that term \li{t} has type \li{σ}.
%
\begin{itemize}
\item A \emph{constant} \li{c : σ} is a symbol of type \li{σ} whose meaning is
  fixed in the current logical context. For example, an arithmetic theory
  might be expected to contain constants such as \li{0 : ℤ}, \li{1 : ℤ},
  \li{abs : ℤ → ℕ}, \li{square : ℕ → ℕ}, and \li{prime} {\li{:}} \li{ℕ → bool}.
  Note that functions (e.g., \li{abs}, \li{square}) and predicates (e.g.,
  \li{prime}) are considered constants.

\item An \emph{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{prime 0}. No parentheses are necessary
  around the argument, unless it is a complex term---e.g., \li{prime (abs 0)}.

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

\item A \emph{variable} \li{x : σ} refers back to the input of a
  \li{λ}-expression \li{λx : σ, t} enclosing it. In the expression
  \li{λx : ℤ, square (abs x)}, the second \li{x} is a variable that refers
  back to the \li{λ}~binder's input \li{x}.
\end{itemize}

Applications and \li{λ}-expressions mirror each other: A
\li{λ}-expression ``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 a technique
called \emph{currying}. For example, \li{λx : σ, (λy : τ, x)} denotes the
function of type \li{σ → (τ → σ)} that takes two arguments and that returns the
first one. Strictly speaking, \li{σ → (τ → σ)} takes a single argument
and returns a function, which in turn takes an argument. Applications work
analogously: If \li{K} denotes the term \li{λ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 only to one 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} or \li{constants} command. Consider the following declarations:

\lstinputlisting[linerange=abfg-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
The first three lines introduce four constants (\li{a}, \li{b}, \li{f},
\li{g}), which can be used to form terms. The last two lines invoke the
\li{#check} diagnosis command to type-check some terms and print their types.

The \li{constant}(\li{s}) command can be used even to declare types. The next example
introduces a type of ``trooleans'' and three values of that type:

\lstinputlisting[linerange=trool-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
The constants thus introduced have no definition. They are fully unspecified.
For example, we cannot tell whether \li{ttrue}, \li{tfalse}, and \li{tmaybe}
are equal or not, and we know nothing about \li{trool} except that it has at
least one value (e.g., \li{ttrue}).

\paragraph{Type Checking and Type Inference}

When Lean parses a term, it checks whether the term is well typed. In the
process, Lean will try 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 helps keep
notations lighter and saves some keystrokes.

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{DBLP:books/daglib/0005958}. Lean takes a pragmatic
approach, by assuming that numerals \li{0}, \li{1}, \li{2}, etc., 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{Γ ⊢ t : σ}, meaning
that term \li{t} has type \li{σ} in context \li{Γ}. The context gives the
types of the variables in \li{t} that are not bound by any \li{λ}. There are
four typing rules, corresponding to the four kinds of terms:
%
\begin{gather*}
\prftree[r]{\textsc{Cst}\quad if \li{c} is declared with type~$\sigma$}
  {\strut\Gamma~\vdash~\text{\li{c : σ}}}
\\[2\jot]
\prftree[r]{\textsc{App}}
  {\strut\Gamma~\vdash~\text{\li{t : σ → τ}}}
  {\strut\Gamma~\vdash~\text{\li{u : σ}}}
  {\strut\Gamma~\vdash~\text{\li{t u : τ}}}
\\[2\jot]
\prftree[r]{\textsc{Lam}}
  {\strut\Gamma\text{\li{, x : σ}}~\vdash~\text{\li{t : τ}}}
  {\strut\Gamma~\vdash~\text{\li{(λx : σ, t) : σ → τ}}}
\\[2\jot]
\prftree[r]{\textsc{Var}\quad if \li{x : σ} occurs in $\Gamma$}
  {\strut\Gamma~\vdash~\text{\li{x : σ}}}
\end{gather*}

The first and last 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 other two rules take one or two judgments as premises and
produce a new judgment.

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, forming a
\emph{formal derivation} of a typing judgment. Like natural trees, derivation
trees are drawn with their 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 the empty variable context:
%
\begin{gather*}
\prftree[r]{\textsc{Lam}}
  {\prftree[r]{\textsc{App}}
    {\prftree[r]{\textsc{Cst}}
      {\strut\text{\li{x : ℤ}}\,~{\vdash}~\text{\li{abs : ℤ → ℕ}}}}
    {\prftree[r]{\textsc{Var}}
      {\strut\text{\li{x : ℤ}}\,~{\vdash}~\text{\li{x : ℤ}}}}
    {\strut\text{\li{x : ℤ}}\,~{\vdash}~\text{\li{abs x : ℕ}}}}
  {\strut{\vdash}~\text{\li{(λx : ℤ, abs x) : ℤ → ℕ}}}
\end{gather*}
%
Reading the proof from the root upwards, notice how \textsc{Lam} moves the
variable bound by the \li{λ}-expression to the context, making an application
of \textsc{Var} possible further up the tree.

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 J. Roger
Hindley \cite{LoVe:hindley-1969} and Robin Milner
\cite{DBLP:journals/jcss/Milner78}, which also forms the basis of Haskell,
OCaml, and Standard ML. The algorithm generates type constraints involving
placeholders \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{\li{x : β}}\,~{\vdash}~\text{\li{abs : β → γ}}}}
    {\prftree[r]{\textsc{Var}}
      {\strut\text{\li{x : β}}\,~{\vdash}~\text{\li{x : β}}}}
    {\strut\text{\li{x : β}}\,~{\vdash}~\text{\li{abs x : γ}}}}
  {\strut{\vdash}~\text{\li{(λx, abs x) : α}}}
\end{gather*}
%
In addition, Lean would generate constraints to ensure that all the rule
applications are legal:
%
\begin{enumerate}
\item For the \textsc{Lam} application, the type of \li{λx, abs x} must have
  the form \li{β → γ}, for some types \li{β} and \li{γ}. Thus, Lean would
  generate the constraint \li{α = β → γ}.

\item For the \textsc{Cst} application, the type of \li{abs} must correspond
  to the declaration as \li{ℤ → ℕ}. Thus, Lean would generate the constraint
  \li{β → γ = ℤ → ℕ}.
\end{enumerate}
%
By putting the two constraints together, we obtain the solution
\li{α = ℤ → ℕ}, which is indeed the type that Lean infers for \li{λx, abs x}.

\paragraph{Type Inhabitation}

Given a type~\li{σ}, the type inhabitation problem consists of finding an
``inhabitant'' of that type---i.e., a term of type~\li{σ}. It may seem like a
pointless exercise, but as we will see in
Chapter~\ref{chap:structured-proofs-and-proof-terms}, there is a close
connection between this problem and the problem of finding a proof of a
proposition. In other words, seemingly silly exercises of the form ``specify
a term of type \li{σ}'' are good practice towards mastery of theorem proving.

To create a term of a given type, you can recursively apply a combination of
the following two steps:
%
\begin{enumerate}
\item 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. Lean will mark \li{_} as an error; if you hover over it
  in Visual Studio Code, a tooltip will appear, specifying the type of the
  missing term (here, \li{τ}) as well as any constants declared in the
  context.

\item Given a type \li{σ} (which may be a function type), you can use any
  constant \li{c :} \li{τ}$_\texttt{1}$ \li{→} \li{⋯} \li{→}
  \li{τ}$_\texttt{\itshape n}$ \li{→} \li{σ} to build a term of that type.
  For each of the \texttt{\itshape n} arguments to \li{c}, you need to
  pass a placeholder, yielding \li{c} \li{_} \li{…} \li{_}.
\end{enumerate}
%
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 possible, with \li{σ := α → β → γ} and
\hbox{\li{τ := ((β → α) → β) →}} \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{α → β →} \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 the placeholder has
type \li{α → γ}. A third application of step~1 yields the term
\li{λf, λg, λa, _}, where the placeholder has type \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
local constants:
%
\begin{center}
\begin{tabular}{@{}r@{}c@{}l@{}}
\texttt{f} & ${}:{}$ & \li|α → β → γ| \\
\texttt{g} & ${}:{}$ & \li|(β → α) → β| \\
\texttt{a} & ${}:{}$ & \li|α| \\
\end{tabular}
\end{center}
%
Recall that we are trying to build a term of type \li{γ}. The only constant 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}, which has type \li{α}, with no arguments. For the
second placeholder, we apply step~2 with the constant~\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 now close to our goal. The remaining placeholder has type \li{β → α},
corresponding to \li{g}'s argument type. Applying step~1, we replace the
placeholder with \li{λb, _}, where the new placeholder has type \li{α}. Like
above, we can 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 never both. This will not always be the case. We
might encounter deadends and need to backtrack. We may also fail altogether,
with no possiblity to backtrack; for example, in the empty context, it is
impossible to supply a witness for \li{α}.

\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 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 equivalent names, including
algebraic data types, inductive data types, freely generated data types, or
simply ``data types'' or ``datatypes.''

\paragraph{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_lemma_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 : 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{align*}
  & \text{\li{nat.zero}}
& & \text{\li{nat.succ nat.zero}}
& & \text{\li{nat.succ (nat.succ nat.zero)}}
\end{align*}
%
and so on denote the different values of type \li{nat}---zero, its successor,
its successor's successor, etc. This notation is called \emph{unary}, or
\emph{Peano}, after the logician Giuseppe Peano.

The general format of all type declarations presented in this chapter is
%
\begin{quote}
\li{inductive} \,\texttt{\itshape type-name} \,\li{:} \li{Type} \\
\li{|}\, \texttt{\itshape constructor-name}$_\texttt{1}$ \,\li{:}\, \texttt{\itshape type}$_\texttt{1}$ \\[-0.5\jot]
\noindent\hbox{}\phantom{\li{|}\, \textit{co}}$\vdots$ \\
\li{|}\, \texttt{\itshape constructor-name}$_\texttt{\itshape n}$ \,\li{:}\, \texttt{\itshape type}$_\texttt{\itshape n}$
\end{quote}

For the naturals, it is possible to convince Lean to use the familiar
names \li{ℕ}, \li{0}, \li{1}, \li{2}, etc., and indeed the built-in \li{nat}
type offers such syntactic sugar. But using the lengthier notations sheds more
light on the syntax of Lean's type definitions, and anyway syntactic sugar is
known to cause cancer of the semicolon \cite{DBLP:journals/sigplan/Perlis82}.

In the Lean file accompanying this chapter, the definition of \li{nat} is
enclosed by a namespace, delimited by the commands \li{namespace my_nat} and
\li{end my_nat}, to keep its effects contained to a portion of the file. After
\li{end my_nat}, any occurrence of \li{nat}, \li{nat.zero}, or \li{nat.succ}
refers to Lean's predefined type of natural numbers. Similarly, the entire
file is enclosed 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}
namespaces displays the following information:
%
\begin{lstlisting}
inductive LoVe.my_nat.nat : Type
constructors:
LoVe.my_nat.nat.zero : nat
LoVe.my_nat.nat.succ : nat → nat
\end{lstlisting}

The focus on natural numbers is one of the many features of this book 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}.

\paragraph{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_lemma_statements_demo_master.lean}
%
Mathematically, this definition is equivalent to defining the type \li{aexp}
inductively by the following formation rules:
%
\begin{enumerate}
\item For every integer \li{i}, we have that \li{num i} is an \li{aexp} value.

\item For every character string \li{x}, we have that \li{var x} is an
  \li{aexp} value.

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

\paragraph{Comparison with Java}

At this point, it may be instructive to compare the concise Lean specification
of \li{aexp} above with the canonical 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=]
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}

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

\paragraph{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=]
#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;
};

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{num}:
%
\begin{lstlisting}[language=]
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 if we want to
allocate exactly the right amount of memory.

\paragraph{Lists}

The next type we consider is that of finite lists:

\lstinputlisting[linerange=list_def-q]{../lean/love01_definitions_and_lemma_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, because \li{α} is fixed on the
left-hand side of the column, it is sufficient to write \li{list} to obtain
\li{list α}.

The following commands allow us to inspect the constructors' types:

\lstinputlisting[linerange=check_list-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
The output is
%
\begin{lstlisting}
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 of arguments will
  be explained in Chapter~\ref{chap:structured-proofs-and-proof-terms}.)

\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
  \hbox{\li{@list.cons : Π(α : Type), α →}} \hbox{\li{list α → list α}}.
\end{itemize}

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|h :: t| & for & \li|list.cons h t| \\
\li|[x₁, …, x|$_\texttt{\itshape n}$\li|]| & for & \li|x₁ :: … :: x|$_\texttt{\itshape 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 precedences; it is all too
easy to misread \li{f x::reverse ys} as \li{f (x::reverse) ys}.

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

If all we want is to declare a function, we can use the \li{constant} command
described above (Section~\ref{sec:types-and-terms}). But usually, we want
to \emph{define} the function's behavior, and for this we can use the \li{def}
command.

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_lemma_statements_demo_master.lean}
%
The keyword \li{def} introduces the definition. The general format of pattern
matching is
%
\begin{quote}
\li{def} \,\texttt{\itshape name} \,\texttt{(\itshape vars}$_\texttt{1}$ : \texttt{\itshape type}$_\texttt{1}$\texttt{)} $\ldots$ \texttt{(\itshape vars}$_\texttt{\itshape m}$ : \texttt{{\itshape type}$_\texttt{\itshape m}$)}
  \,\li{:}\, \texttt{\itshape type} \\
\li{|}\, \texttt{\itshape patterns}$_\texttt{1}$ \,\li{:=}\, \texttt{\itshape result}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\li{|}\, \texttt{\itshape pa}}$\vdots$ \\
\li{|}\, \texttt{\itshape patterns}$_\texttt{\itshape n}$ \,\li{:=}\, \texttt{\itshape result}$_\texttt{\itshape n}$
\end{quote}
%
Patterns may contain variables, whose scope is the corresponding right-hand
side, as well as constructors. For example, in the second case of \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{quote}
\li{def} \,\texttt{\itshape name} \,\texttt{(\itshape vars}$_\texttt{1}$ : \texttt{\itshape type}$_\texttt{1}$\texttt{)} $\ldots$ \texttt{(\itshape vars}$_\texttt{\itshape m}$ : \texttt{{\itshape type}$_\texttt{\itshape m}$)}
\texttt{\itshape type}\, \li{:=}\, \\
\texttt{\itshape result}
\end{quote}
%
We can have pattern matching without recursion (e.g., in the \li{num} and
\li{var} cases above), and we can have recursion without pattern matching.

\emph{Structural recursion} is a form of recursion that allows us to peel off
one or more constructors from the value on which we recurse. The \li{eval}
function above is structurally recursive. Such functions are guaranteed to call
themselves only finitely many times before the recursion stops. This is a
prerequisite for establish that the function terminates, an important property
to ensure logical consistency and termination of evaluation.

For structurally recursive functions, Lean can automatically prove termination.
For more general recursive schemes, the termination check may fail. Sometimes it
does so for a good reason, as in the following example:

\lstinputlisting[linerange=evil_def-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
If Lean were to accept this definition, we could exploit it to prove that
\li{0 = 1}, by subtracting \li{evil n} on each side of the equation
\li{evil n = nat.succ (evil n)}.

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

\lstinputlisting[linerange=add_def-q]{../lean/love01_definitions_and_lemma_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{succ} constructor from the second
argument. (Given that addition is symmetric, there is no deep reason for
choosing to recurse on the second argument.)

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

\lstinputlisting[linerange=reduce_eval_add-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
Both commands print \li{9}, as expected.

It is generally 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{#reduce} or \li{#eval} 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_lemma_statements_demo_master.lean}
%
This time, \li{#reduce} prints \li{14}:

\lstinputlisting[linerange=reduce_mul-q]{../lean/love01_definitions_and_lemma_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 analogous to the definition of
multiplication:

\lstinputlisting[linerange=power_def-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
Since the first argument does not change in the recursive calls, we can factor
it out and put it next to the function's name, before the colon introducing
the function's type:

\lstinputlisting[linerange=power₂_def-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
In fact, we already saw a similar 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_lemma_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=power₃_def-q]{../lean/love01_definitions_and_lemma_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_lemma_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 implicit by default, we can put it in curly braces
\verb|{|\,\verb|}|:

\lstinputlisting[linerange=append₂_def-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
The at sign (\li{@}) can be used to make the implicit arguments explicit.

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_lemma_statements_demo_master.lean}

In Lean's standard library, \li{++} is provided as syntactic sugar for the
append function. We can use it to define a function that reverses a list:

\lstinputlisting[linerange=reverse_def-q]{../lean/love01_definitions_and_lemma_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, logical formulas,
propositions, and true/false statements will all mean the same.

In Lean, propositions are simply terms of type \li{Prop}. A proposition that
can be proved is a theorem (or lemma, corollary, etc.); otherwise it is a
nontheorem or false statement. Mathematicians sometimes use ``proposition'' as
a synonym for theorem (e.g., ``Proposition~3.14''), but in formal logic it is
customary to let it encompass false statements.

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_lemma_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=mul_lemmas-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=reverse_reverse-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=shuffle_shuffle_shuffle-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}

The general format is
%
\begin{quote}
\li{lemma} \,\texttt{\itshape name} \,\texttt{(\itshape vars}$_\texttt{1}$ : \texttt{\itshape type}$_\texttt{1}$\texttt{)} $\ldots$ \texttt{(\itshape vars}$_\texttt{\itshape m}$ : \texttt{{\itshape type}$_\texttt{\itshape m}$)}
\texttt{\itshape statement}\, \li{:=}\, \texttt{\itshape proof}
\end{quote}
%
The \li{:=} symbol separates the lemma's statement and its proof. 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 an actual proof. In Chapters
\ref{chap:tactical-proofs}~and~\ref{chap:structured-proofs-and-proof-terms},
we will see how to eliminate these \li{sorry}s.

\section{Summary of New Syntax}

At the end of this and other chapters, we include a brief summary of the
syntax introduced in the chapter. Some commands have multiple meanings, which
will be introduced gradually. We refer to \emph{The Lean Reference Manual}
\cite{lean-reference-manual} and the \emph{Theorem Proving in Lean}
\cite{theorem-proving-in-lean} and \emph{Programming in Lean}
\cite{programming-in-lean} tutorials for details and to Lean's source code for
the ultimate truth.

\small

\subsection{Declarations}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|constant|(\li|s|) & declares unspecified new constants or types \\
\li|def| & defines a new constant \\
\li|inductive| & introduces a type and its constructors \\
\li|lemma| & states a lemma \\
\li|namespace … end| & puts all declarations in a named scope (to avoid clashes) \\
\end{tabularx}

\subsection{Proof Commands}

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

\subsection{Diagnosis Commands}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|#check| & checks and prints type of a term \\
\li|#eval| & executes a term using an optimized interpreter \\
\li|#print| & prints definition of a constant or function \\
\li|#reduce| & executes a term using Lean's kernel \\
\end{tabularx}
