\chapter{Basic Mathematical Structures}
\label{chap:basic-mathematical-structures}

In this chapter, we introduce definitions and proofs about basic mathematical structures.

\section{Type Classes without Properties}
\label{sec:type-classes-without-properties}

A type class is a collection of abstract constants and their properties. A type
can be declared an instance of a type class by providing concrete definitions
for the constants and proving that the properties hold.

A simple example for a type class is the class \li{inhabited}, which requires
only a constant \li{default} and no properties:
%
\begin{lstlisting}
class inhabited (α : Type) :=
(default : α)
\end{lstlisting}    
%
The type class \li{inhabited} is very similar to the inductive predicate
\li{nonempty} that we discussed in Section \ref{sec:the-axiom-of-choice}. But
since \li{inhabited} lives in \li{Type}, there is a large eliminator and we can
extract the \li{default} that was used to construct an instance of the
type class \li{inhabited α}.

Any type that has at least one element can be declared an instance of this
class. For example, we can declare the natural numbers \li{ℕ} as an instance by
choosing an arbitrary natural number to be the default value:
%
\lstinputlisting[linerange=inhabited_nat-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Using this type class, we can define a variant of the \li{head} operation on
lists that we defined in Section \ref{sec:example-lists}. The issue with
\li{head} is that there is no meaningful value that we can assign to
\li{head []}. Given a type of type class \li{inhabited}, we can simply return
the default value instead of using the \li{option} type.
%
\lstinputlisting[linerange=ihead-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
We require that the type \li{α} must be of type class \li{inhabited} by writing
\li{[inhabited α]}. This allows us to access \li{inhabited.default} in
the definition. The syntax \li{[inhabited α]} adds an implicit argument to the
constant \li{ihead}. But unlike for other implicit arguments, Lean performs not
only type inference but also a type class search through all declared instances
to determine the value of this argument. Thus, when we write
%
\lstinputlisting[linerange=ihead_reduce-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Lean will search for an instance \li{inhabited ℕ} and will find the instance we declared above.
In that instance declaration, we defined \li{default} to be \li{0} and
hence this is what the \li{#reduce} command returns.

We can prove abstract lemmas about the type class \li{inhabited} such as
%
\lstinputlisting[linerange=ihead_ihead-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
For such lemmas, it is important to add the assumption \li{[inhabited α]} to be allowed to use
the operator \li{ihead} on lists of type \li{list α}. If we omit this assumption,
Lean will raise an error telling us that type class synthesis failed.

There are a few more type classes only requiring a constant but no
properties---for example:
%
\begin{lstlisting}
class has_zero (α : Type) := (zero : α)
class has_neg  (α : Type) := (neg : α → α)
class has_add  (α : Type) := (add : α → α → α)
class has_one  (α : Type) := (one : α)
class has_inv  (α : Type) := (inv : α → α)
class has_mul  (α : Type) := (mul : α → α → α)
\end{lstlisting}
%
These \emph{syntactic} type classes introduce constants that are used in many
different contexts with different semantics. For example, \li{one} can stand
for the natural number~1, the integer~1, the real~1, the identity matrix, and
many other concepts of~1. The main purpose of these type classes is to form the
foundation for rich hierarchy of algebraic type classes and to allow
overloading of common symbols such as \li{*}, \li{1}, and \li{⁻¹}.

The syntactic type classes do not impose serious restrictions on the types that
can be declared instances, except that a type of type class \li{has_zero} or
\li{has_one} must be inhabited. In contrast, the \emph{semantic} type classes,
which we will discuss in the following sections, contain properties that
restrict how the given constants behave.

\section{Type Classes over a Single Binary Operator}
\label{sec:type-classes-over-a-single-binary-operator}

The type classes \li{group} and \li{add_group}
are examples of semantic type classes.
In mathematics, a group is a set \textit{G} with a a binary operator
$\bullet$~:~\textit{G} $\times$ \textit{G} $\rightarrow$ \textit{G}
fulfilling the following properties, called group axioms:
%
\begin{itemize}
\item Associativity: For all \textit{a}, \textit{b}, \textit{c} $\in$
\textit{G}, we have (\textit{a} $\bullet$ \textit{b}) $\bullet$ \textit{c} $=$
\textit{a} $\bullet$ (\textit{b} $\bullet$ \textit{c}).

\item Identity element: There exists an element \textit{e} $\in$ \textit{G} such
that for all \textit{a} $\in$ \textit{G}, we have \textit{e} $\bullet$ \textit{a} $=$ \textit{a}.

\item Inverse element: For each \textit{a} $\in$ \textit{G}, there exists an
inverse element denoted \textit{a}${}^{-1}$ such that \textit{a}$^{-1}$
$\bullet$ \textit{a} $=$ \textit{e}.
\end{itemize}
%
Commonly, group operations are written multiplicatively (i.e., with operator
$*$, identity element $1$, and inverse element \textit{a}$^{-1}$) or additively
(i.e., with operator $+$, identity element $0$, and inverse element
$-$\textit{a}). This is why Lean offers two type classes for groups:\ the
multiplicative \li{group} and the additive \li{add_group}. They are essentially
the same but use different names for their constants and properties.

Any type that fulfills the group axioms can be instantiated as \li{group} or
\mbox{\li{add_group}}. To illustrate this, we will define \li{ℤ₂}, also known as
$\mathbb{Z}/2\mathbb{Z}$, and instantiate it as an \li{add_group}. \li{ℤ₂} has
two elements, which we will call \li{zero} and \li{one}:
%
\lstinputlisting[linerange=Z2-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Addition is defined as follows:
%
\lstinputlisting[linerange=Z2_add-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Invoking \li{#print add_group} tells us all the constants and properties we
need to provide:
%
\begin{lstlisting}
structure add_group : Type u → Type u
fields:
add_group.add : Π{α} [add_group α], α → α → α
add_group.add_assoc :
  ∀{α} [add_group α] (a b c : α), a + b + c = a + (b + c)
add_group.zero : Π(α) [add_group α], α
add_group.zero_add : ∀{α} [add_group α] (a : α), 0 + a = a
add_group.add_zero : ∀{α} [add_group α] (a : α), a + 0 = a
add_group.neg : Π{α} [c : add_group α], α → α
add_group.add_left_neg : ∀{α} [add_group α] (a : α), -a + a = 0
\end{lstlisting}
%
The constants \li{add_group.add}, \li{add_group.zero}, and \li{add_group.neg}
respectively correspond to the binary operator $\bullet$, the identity element
\textit{e}, and the inverse $^{-1}$ in the definition of a group above. The
properties \li{add_group.add_assoc}, \li{add_group.zero_add}, and
\li{add_group.add_left_neg} correspond to the three group axioms. Due to the
way the \li{add_group} type class is constructed, we also need to provide the
redundant property \li{add_group.add_zero}.

\li{ℤ₂} can be instantiated as a group as follows:
%
\lstinputlisting[linerange=Z2_add_group-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
With this instance declaration, we can now use the notations \li{0},
\li{+}, and \li{-}:
%
\lstinputlisting[linerange=Z2_notation-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Moreover, we get any lemma that has already been proved in general for the type
class \li{add_group} for free:
%
\lstinputlisting[linerange=Z2_lemmas-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%

\noindent
The algebraic hierarchy contains
some more type classes with one binary operator.
Here is an overview of the most important ones:

\vskip3\smallskipamount

\centerline{\begin{tabular}{@{}ll@{}}
    Structure                   & Properties \\[1\jot]
    \li|semigroup|              & associativity \\
    \li|monoid|                 & \li{semigroup} with unit (\li{1}) \\
    \li|left_cancel_semigroup|  & \li{semigroup} with \li{x * a = x * b → a = b} \\
    \li|right_cancel_semigroup| & \li{semigroup} with \li{a * x = b * x → a = b} \\
    \li|group|                  & \li{monoid} with inverse ($^{-1}$) \\
\end{tabular}}

\vskip3\smallskipamount

\noindent
Most of these structures have commutative versions (where \textit{a} $\bullet$
\textit{b} $=$ \textit{b} $\bullet$ \textit{a} for all elements \textit{a},
\textit{b}), prefixed with \li{comm_}:
%
\[\hbox{\li{comm_semigroup}, \li{comm_monoid}, \li{comm_group}}\]
%
All of these type classes have additive counterparts with
the prefix \li{add_}:
%
\[\begin{array}{c}
\text{\li{add_semigroup}, \li{add_monoid}, \li{add_group}} \\
\text{\li{add_comm_semigroup}, \li{add_comm_monoid}, \li{add_comm_group}} \\
\text{\li{add_left_cancel_semigroup}, \li{add_right_cancel_semigroup}}
\end{array}\]
%
Although these additive type classes are isomorphic to their multiplicative
counterparts, they are crucial when constructing algebraic structures with more
than one binary operator such as rings and fields. To avoid duplicating all
lemmas and definitions based on the multiplicative type classes,
the copying process is automated by a tactic
(\li{transport_}\allowbreak\li{multiplicative_to_additive})
and an attribute (\li{@[to_additive]}).

An example for an instance of \li{add_monoid} is the type \li{list} with the
empty list \li{[]} as zero and the append operator \li{++} as addition:
%
\lstinputlisting[linerange=list_add_monoid-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
We could go further an register this combination as a \li{add_left_cancel_semigroup} and an \li{add_right_cancel_semigroup}.

The graph below illustrates the relationships between some of these
type classes. The arrows mean ``inherits all properties from.''

\begin{center}
\tikzset{>={angle 60}}
\begin{tikzpicture}[node distance = {1.0em and 1.5em}, v/.style = {}]
\graph[nodes={}, grow right=12em, branch down=4em]{
    "\li{comm_group}" -> "\li{comm_monoid}" -> "\li{comm_semigroup}",
    "\li{group}" -> "\li{monoid}" -> "\li{semigroup}",
    "\li{comm_group}" -> "\li{group}",
    "\li{comm_monoid}" -> "\li{monoid}",
    "\li{comm_semigroup}" -> "\li{semigroup}"
};
\end{tikzpicture}

\bigskip

\begin{tikzpicture}[node distance = {1.0em and 1.5em}, v/.style = {}]
\graph[nodes={}, grow right=12em, branch down=4em]{
    "\li{add_comm_group}" -> "\li{add_comm_monoid}" -> "\li{add_comm_semigroup}",
    "\li{add_group}" -> "\li{add_monoid}" -> "\li{add_semigroup}",
    "\li{add_comm_group}" -> "\li{add_group}",
    "\li{add_comm_monoid}" -> "\li{add_monoid}",
    "\li{add_comm_semigroup}" -> "\li{add_semigroup}",
};
\end{tikzpicture}
\end{center}

\section{Type Classes over Two Binary Operators}
\label{sec:type-classes-over-two-binary-operators}

The additive and multiplicative structures are amalgamated to form more complex
type classes over two binary operators. One of these is \li{field}. A field
\textit{F} is defined by the following properties:
%
\begin{itemize}
\item \textit{F} forms a commutative group under an operator $+$, called
addition, with identity element 0.

\item \textit{F}$\backslash\{$0$\}$ forms a commutative group under an operator $*$, called multiplication.

\item Multiplication distributes over addition---i.e.,
\textit{a} $*$ (\textit{b} $+$ \textit{c}) $=$ \textit{a} $*$ \textit{b} $+$
\textit{a} $*$ \textit{c} for all \textit{a}, \textit{b}, \textit{c} $\in$
\textit{F}.
\end{itemize}
%
By invoking \li{#print field}, we can display all constants and properties
required by the \li{field} type class. Again, the class includes some redundant
properties such as \li{left_distrib} and \li{right_distrib}, due to the way in
which it is constructed.

We will now show that \li{ℤ₂} is a field by instantiating the \li{field} type
class with it. First, we define multiplication on \li{ℤ₂} as follows:
%
\lstinputlisting[linerange=Z2_mul-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
To declare \li{ℤ₂} a field,
we can reuse the instance \li{ℤ₂.add_group} that we declared above
using the syntax \li{..ℤ₂.add_group}.
We can prove the remaining properties as follows:
%
\lstinputlisting[linerange=Z2_field-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
With this declaration in place, we can now use the notations \li{1}, \li{*},
\li{/}, and more:
%
\lstinputlisting[linerange=Z2_reduce1-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
The type annotation \li{: ℤ₂} is necessary here to tell Lean that we want to
calculate in \li{ℤ₂} and not in \li{ℕ}, the default. We can even use arbitrary
numerals in \li{ℤ₂}. For example, the numeral \li{3} is interpreted as
\li{1 + 1 + 1}, which is the same as \li{1} in \li{ℤ₂}:
%
\lstinputlisting[linerange=Z2_reduce2-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Moreover, we can use the tactic \li{ring} to normalize terms. For example:
%
\lstinputlisting[linerange=ring-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
This tactic is available for any type that is declared as a \li{field} or more
generally as a \li{ring}. For commutative monoids and groups, there is a
similar normalization tactic called \li{abel}.

Besides \li{field}, there are many more type classes for structures with two
binary operators. These are the most important ones:

\vskip3\smallskipamount

\centerline{\begin{tabular}{@{}lll@{}}
    Structure          & Properties & Examples \\[1\jot]
    \li|semiring|      & \li{monoid} and \li{add_comm_monoid} with distributivity& $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
    \li{comm_semiring} & \li{semiring} with commutativity of \li{*} & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$\\
    \li|ring|          & \li{monoid} and \li{add_comm_group} with distributivity & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$ \\
    \li{comm_ring}  & \li{ring} with commutativity of \li{*} & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$ \\
    \li|division_ring|         & \li{ring} with multiplicative inverse    &  $\mathbb{R}$, $\mathbb{Q}$           \\
    \li{field} & \li{division_ring} with commutativity of \li{*} & $\mathbb{R}$, $\mathbb{Q}$ \\
    \li{discrete_field} & \li{field} with decidable equality and \li{\ ∀n, n / 0 = 0}& $\mathbb{R}$, $\mathbb{Q}$ \\
\end{tabular}}

\vskip3\smallskipamount

\noindent
The property \li{∀n, n / 0 = 0} required by the \li{discrete_field} type class
is simply a convention to make division a total function. Mathematicians would
view division as a partial function.

\begin{center}
\tikzset{>={angle 60}}
\begin{tikzpicture}[node distance = {1.0em and 1.5em}, v/.style = {}]
    \graph[nodes={}, grow right=9em, branch down=4em]{
        "\li{discrete_field}" -> "\li{field}" -> "\li{comm_ring}" ->  "\li{comm_semiring}",
        "\phantom{node}" ->[color=white] "\li{division_ring}" -> "\li{ring}"  ->  "\li{semiring}",
        "\li{field}" -> "\li{division_ring}",
        "\li{comm_ring}" -> "\li{ring}",
        "\li{comm_semiring}" -> "\li{semiring}",
    };
\end{tikzpicture}
\end{center}

\noindent
The hierarchy between \li{ring} and \li{field} is more complex than shown in
this overview and includes type classes for domains, integral domains,
Euclidean rings, and more.

\section{Coercions}
\label{sec:coercions}

When dealing with different kinds of numbers from \li{ℕ}, \li{ℤ}, \li{ℚ}, and
\li{ℝ} at the same time, we may want to cast from one type into another. For
example, given a natural number \li{n}, we may need to convert it to an integer:
%
\lstinputlisting[linerange=neg_mul_neg_nat-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Surprisingly, this statement does not lead to an error,
although negation \li{- n} is not defined on \li{n : ℕ},
multiplication of \li{z : ℤ} with \li{n : ℕ} is not defined,
and the lemma \li{neg_mul_neg} does not apply to natural numbers.
By invoking \li{#print neg_mul_neg_nat}, we can see what happened:
%
\begin{lstlisting}
theorem neg_mul_neg_nat : ∀(z : ℤ) (n : ℕ), -z * -↑n = z * ↑n :=
λ(z : ℤ) (n : ℕ), neg_mul_neg z ↑n
\end{lstlisting}
%
Lean has a mechanism to introduce coercions, represented by \li{↑} or \li{coe},
whenever necessary. This coercion operator can be set up to provide implicit
conversions between arbitrary types. Many coercions are already in place,
including the following:
%
\begin{itemize}
\item \li{coe : ℕ → α} casts \li{ℕ} into another semiring \li{α};
\item \li{coe : ℤ → α} casts \li{ℤ} into another ring \li{α};
\item \li{coe : ℚ → α} casts \li{ℚ} into another division ring \li{α}.
\end{itemize}
%
In some cases, Lean is unable to figure out where to place the coercions. We
can then provide some type annotations to guide Lean's inference algorithm, as
in the following example:
%
\lstinputlisting[linerange=neg_mul_neg_nat₂-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
In proofs involving coercions, the tactic \li{norm_cast} can be convenient. It
can help with proof goals such as
%
\begin{lstlisting}
m n : ℕ,
h : ↑m = ↑n
⊢ m = n
\end{lstlisting}
%
in the proof
%
\lstinputlisting[linerange=norm_cast1-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
or
\begin{lstlisting}
m n : ℕ
⊢ ↑m + ↑n = ↑(m + n)
\end{lstlisting}
in the proof
%
\lstinputlisting[linerange=norm_cast2-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}

\section{Lists, Multisets, and Finite Sets}
\label{sec:lists-multisets-and-finite-sets}

We have seen many examples of how lists can be used in previous chapters. But
when making a new definition or stating a new lemma, we should also reflect on
alternatives such as multisets and finite sets.

Consider this definition based on the binary trees we introduced in
Section~\ref{sec:example-binary-trees}:
%
\lstinputlisting[linerange=nodes_list-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
This function returns a list of all the elements occurring in the tree. It
traverses the tree depth first, from left to right. But for some applications,
we might not care in which order the elements occur in the tree. This is where
multisets can help us. For multisets, we have \li|{3, 2, 1, 2} = {1, 2, 2, 3}|,
whereas the lists \li|[3, 2, 1, 2]| and \li|[1, 2, 2, 3]| are different.
Multisets are defined as the quotient type over lists up to reordering. We can
redo the above definition using multisets as follows:
%
\lstinputlisting[linerange=nodes_multiset-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Using this definition, we can prove lemmas such as
\li{nodes_multiset t = nodes_multiset (mirror t)}, whereas
\li{nodes_list t = nodes_list (mirror t)} does not hold.

For some applications, we might want to go a step further and ignore not only
the order but also how often each element occurs in the tree, distinguishing
only between occurrence and nonoccurrence. This is where finite
sets---finsets---come into play. On finsets, we have
\li|{3, 2, 1, 2} = {1, 2, 3}|. Finsets are defined as the subtype of multisets
that do not contain any repeated elements. We can redo the definition above
using finsets as follows:
%
\lstinputlisting[linerange=nodes_finset-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
For all three of these structures, Lean offers sum and product operators to add
or multiply all of the values of a list, multiset, or finset:
%
\lstinputlisting[linerange=sum_prod-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
The operators \li{finset.sum} and \li{finset.prod} take a second argument, a
function that maps the values of the finset to the values that should be added
or multiplied. If we put the identity function \li{(λx, x)} for that second
argument, they behave like the corresponding operators for lists and multisets.

These operators require the type of the elements to be declared as an instance
of \li{add_monoid} for addition or of \li{monoid} for multiplication.
For \li{multiset} and \li{finset}, we additionally require an instance
declaration for \li{add_comm_monoid} or \li{comm_monoid} because we cannot have
the result depend on the order of adding or multiplying the elements.

\li{mathlib} provides a collections of lemmas describing how the big operators
behave under reorderings, basic operators on \li{list}, \li{multiset}, and
\li{finset}, homomorphisms, order relations, and more.

\section{Summary of New Syntax}

\small

\subsection{Tactics}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|abel| & normalizes terms of commutative monoids and groups \\
\li|norm_cast| & normalizes coercions \\
\li|ring| & normalizes ring terms \\
\end{tabularx}

\subsection{Lemma}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|dec_trivial| & decides a goal (e.g., a true closed expression) \\
\end{tabularx}
