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

In this chapter, we introduce definitions and proofs about basic mathematical
structures such as groups, fields, and linear orders.

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

In mathematics, a \emph{group} is a set \textit{G} with 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}

In Lean, a type class for groups could be defined as follows:
%
\lstinputlisting[linerange=group-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
However, this is not the official definition. Groups are part of a larger
hierarchy of algebraic structures.

Group operations can be written multiplicatively (with operator $*$, identity
element $1$, and inverse element \textit{a}$^{-1}$) or additively (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 satisfies the group axioms can be registered as a \li{group} or
\hbox{\li{add_}}\allowbreak\hbox{\li{group}.} To illustrate this, we will
define \li{ℤ₂}, also known as $\mathbb{Z}/2\mathbb{Z}$, and register it as an
\li{add_group}. The type \li{ℤ₂} has two elements:
%
\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}
%
Running \li{#print add_group} tells us all the constants and properties we
need to provide:
%
\begin{lstlisting}[language=,procnamekeys={}]
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 \hbox{\li{add_group.neg}}
correspond to the binary operator $\bullet$, the identity element
\textit{e}, and the inverse $^{-1}$. The
properties \li{add_group.add_assoc}, \li{add_group.}\allowbreak\li{zero_add}, and
\li{add_group.add_left_neg} correspond to the three group axioms. For technical
reasons, we must also prove the redundant property
\li{add_group.}\allowbreak\li{add_zero}.

The type \li{ℤ₂} can be registered 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 write \li{0}, \li{+}, and \li{-}:
%
\lstinputlisting[linerange=Z2_notation-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
We can also use any lemma that has been proved for \li{add_group}:
%
\lstinputlisting[linerange=Z2_lemmas-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}

The algebraic hierarchy contains further type classes with one binary
operator. The main ones are listed below:

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}lll@{}}
\toprule
Type class                  & Properties                                     & Examples \\
\midrule
\li|semigroup|              & associativity of \li{*}                        & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
\li|monoid|                 & \li{semigroup} with unit \li{1}                & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
\li|left_cancel_semigroup|  & \li{semigroup} with \li{c * a = c * b → a = b} & \\
\li|right_cancel_semigroup| & \li{semigroup} with \li{a * c = b * c → a = b} & \\
\li|group|                  & \li{monoid} with inverse $^{-1}$ \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\begin{sloppypar}
\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 \hbox{\li{comm_}:}
\li{comm_semigroup}, \li{comm_monoid}, \li{comm_}\allowbreak\hbox{\li{group}.}
All of these type classes have additive counterparts prefixed with \li{add_}:
\li{add_semigroup}, \li{add_monoid}, \li{add_group}, \li{add_comm_semigroup},
\hbox{\li{add_comm_monoid},} \li{add_comm_group}, \li{add_left_cancel_semigroup},
\li{add_right_cancel_semigroup}:
\end{sloppypar}

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}lll@{}}
\toprule
Type class                      & Properties                              & Examples \\
\midrule
\li|add_semigroup|              & associativity of \li{+}                 & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
\li|add_monoid|                 & \li{add_semigroup} with unit \li{0}     & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
\li|add_left_cancel_semigroup|  & \li{add_semigroup} with                 & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\[-1pt]
  & \li{c + a = c + b → a = b} \\[1pt]
\li|add_right_cancel_semigroup| & \li{add_semigroup} with                 & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\[-1pt]
  & \li{a + c = b + c → a = b} \\[1pt]
\li|add_group|                  & \li{add_monoid} with inverse \texttt{-} & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$ \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

Although the 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 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 continue and register \li{list} with \li{[]} and \li{++} as an
\li{add_}\allowbreak\li{left_cancel_}\allowbreak\li{semigroup} and an \li{add_right_cancel_semigroup}.

The graph below illustrates the relationships between some of these
type classes. An arrow from \textit{X} to \textit{Y} means ``\textit{X}
inherits all properties from \textit{Y}.''

\begin{center}
\tabletsmall
\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 field. A \emph{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 running \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 its
construction.

We will now show that \li{ℤ₂} is a field by instantiating the \li{field} type
class with it. First, we must define multiplication on \li{ℤ₂}:
%
\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_reduce_1-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
The command prints \li{ℤ₂.zero}. 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_reduce_3-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
The command prints \li{ℤ₂.one}.

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

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}lll@{}}
\toprule
Type class          & Properties                                                  & Examples \\
\midrule
\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}$ \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\noindent
The property \li{∀n, n / 0 = 0} required by the \li{field} type class is simply
a convention to make division a total function. Mathematicians would regard
division as a partial function. The graph below illustrates the relationships
between these type classes.

\begin{center}
\tabletsmall
\tikzset{>={angle 60}}
\begin{tikzpicture}[node distance = {1.0em and 1.5em}, v/.style = {}]
    \graph[nodes={}, grow right=9em, branch down=4em]{
        "\li{field}" -> "\li{comm_ring}" ->  "\li{comm_semiring}",
        "\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 depicted
and includes type classes for domains, integral domains, Euclidean rings, and
more.

Once we have instantiated the type classes with types of interest, we can use
the \li{ring} and \li{ring_exp} tactics \cite{baanen-2020} to normalize terms
containing operators on those types. For example:
%
\lstinputlisting[linerange=ring_example-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
These tactics are available for any type that is declared as a field or more
generally as a commutative semiring. The distinguishing feature of \li{ring_exp} is
that it can reason about exponents containing variables.

For commutative monoids and groups, there is a similar normalization tactic
called \li{abel}:
%
\lstinputlisting[linerange=abel_example-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}

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

When combining numbers from \li{ℕ}, \li{ℤ}, \li{ℚ}, and \li{ℝ} in the same
lemmas, we may want to cast from one type to another. For example, given a
natural number, we may need to convert it to an integer. Consider the
following lemma and notice the type of the arguments of multiplication:
%
\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 : ℤ} and \li{n : ℕ} is not defined,
and the lemma \li{neg_mul_neg} does not apply to natural numbers.

The diagnosis command \li{#print} \li{neg_mul_neg_nat} tells us what happened:
%
\begin{lstlisting}[language=,procnamekeys={}]
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, denoted by \li{↑} or \li{coe},
when necessary. This coercion operator can be set up to provide implicit
conversions between arbitrary types. Many coercions are already in place,
including these:
%
\begin{itemize}
\item \li{coe : ℕ → α} casts \li{ℕ} to another semiring \li{α};
\item \li{coe : ℤ → α} casts \li{ℤ} to another ring \li{α};
\item \li{coe : ℚ → α} casts \li{ℚ} to 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_nat_mul_neg-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 goals such as \li{⊢ m n : ℕ, h : ↑m = ↑n ⊢ m = n} in the proof
%
\lstinputlisting[linerange=norm_cast_example_1-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
or \li{⊢ m n : ℕ ⊢ ↑m + ↑n = ↑(m + n)} in the proof
%
\lstinputlisting[linerange=norm_cast_example_2-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}

The \li{norm_cast} tactic relies on lemmas such as the following:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|nat.cast_add| & \lic| : ∀a b : ℕ, ↑(a + b) = ↑a + ↑b| \\
\lic|int.cast_add| & \lic| : ∀a b : ℤ, ↑(a + b) = ↑a + ↑b| \\
\lic|rat.cast_add| & \lic| : ∀a b : ℚ, ↑(a + b) = ↑a + ↑b| \\
\end{tabular}
\end{center}

\section{Normalization Tactics}
\label{sec:normalization-tactics}

The algebraic tactics \li{ring}, \li{ring_exp}, and \li{abel} and the coercion
tactic \li{norm_cast} all work by normalization: They rewrite expressions in
the hope that they become syntactically equal, at which point equality is
trivial to prove. Like \li{rw} and \li{simp}, they produce a subgoal when
they make some progress but do not fully succeed.

The optional \ttvar{position} is as for the rewriting tactics
(Section~\ref{sec:rewriting-tactics}).

\subsection*{ring and ring\_exp}

\smallskip

\begin{quote}
\lic{ring} \,$\bigl[$\lic{at} \,\ttvar{position}$\bigr]$ \\
\lic{ring_exp} \,$\bigl[$\lic{at} \,\ttvar{position}$\bigr]$
\end{quote}
%
The \li{ring} and \li{ring_exp} tactics prove equalities over commutative
rings and semirings (such as \li{ℕ}, \li{ℤ}, \li{ℚ}, and \li{ℝ}) by normalizing
expressions and syntactically comparing the result. The \li{ring_exp} variant
performs more aggressive normalization in the presence of variables in
exponents.

\subsection*{abel}

\smallskip

\begin{quote}
\lic{abel} \,$\bigl[$\lic{at} \,\ttvar{position}$\bigr]$
\end{quote}
%
The \li{abel} tactic proves equalities over additive commutative monoids and
groups (such as \li{ℕ}, \li{ℤ}, \li{ℚ}, and \li{ℝ}) by normalizing expressions
and syntactically comparing the result.

\subsection*{norm\_cast}

\smallskip

\begin{quote}
\lic{norm_cast} \,$\bigl[$\lic{at} \,\ttvar{position}$\bigr]$
\end{quote}
%
The \li{norm_cast} tactic moves coercions towards the inside of expressions, as
a form of simplification.

\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 the following definition, based on the binary trees we introduced in
Section~\ref{sec:binary-trees}:
%
\lstinputlisting[linerange=list.elems-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 about the order of the elements.

\begin{sloppypar}
This is where multisets can help us. For multisets, we have
\hbox{\li|{3, 2, 1, 2} =|} \hbox{\li|{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=multiset.elems-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
Using this definition, we can prove that
\li{multiset.elems t = multiset.elems} \hbox{\li{(mirror t)},} whereas
\li{list.elems t = list.elems (mirror t)} does not hold.
\end{sloppypar}

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, or \emph{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. (Another possible definition would
have been as the subtype of sets that are finite.) We can redo the definition
above using finsets as follows:
%
\lstinputlisting[linerange=finset.elems-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 elements:
%
\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{λn, n} 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}, they additionally require an instance
declaration for \li{add_comm_monoid} or \li{comm_monoid} because the result
cannot depend on the order of adding or multiplying the elements.

Lean's \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{Order Type Classes}
\label{sec:order-type-classes}

Many of the structures introduced above can be ordered.
For example, the well-known order on the natural numbers can be defined as
%
\lstinputlisting[linerange=nat.le-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
This is an example of a linear order. A \emph{linear order} (or \emph{total
order}) is a binary relation $\le$ such that for all \textit{a}, \textit{b},
and \textit{c}, the following properties hold:
%
\begin{itemize}
\item Reflexivity: \textit{a} $\le$ \textit{a}.
\item Transitivity: If \textit{a} $\le$ \textit{b} and
  \textit{b} $\le$ \textit{c}, then \textit{a} $\le$ \textit{c}.
\item Antisymmetry: If \textit{a} $\le$ \textit{b} and
  \textit{b} $\le$ \textit{a}, then \textit{a} $=$ \textit{b}.
\item Totality: \textit{a} $\le$ \textit{b} or \textit{b} $\le$ \textit{a}.
\end{itemize}
%
If a relation has the first three properties, it is a \emph{partial order}. An
example is the subset relation $\subseteq$ on sets, finite sets, or multisets.
%
If a relation has the first two properties, it is a \emph{preorder}. An example
is comparing lists by their length.

In Lean, there are type classes for the different kinds of orders:
\hbox{\li{linear_order},} \li{partial_order}, and \li{preorder}.
The \li{preorder} class has the fields
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|le| & \lic| : α → α → Prop| \\
\lic|le_refl| & \lic| : ∀a : α, le a a| \\
\lic|le_trans| & \lic| : ∀a b c : α, le a b → le b c → le a c| \\
\end{tabular}
\end{center}
%
The \li{partial_order} class has the additional field
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|le_antisymm| & \lic| : ∀a b : α, le a b → le b a → a = b| \\
\end{tabular}
\end{center}
%
and \li{linear_order} has the additional field
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|le_total| & \lic| : ∀a b : α, le a b ∨ le b a| \\
\end{tabular}
\end{center}

We can declare the preorder on \li{list α} that compares lists by their length
as follows:
%
\lstinputlisting[linerange=list.length.preord-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
This type class instance gives us access to the infix syntax \li{≤} and to the
corresponding relations \li{≥}, \li{<}, and \li{>}:
%
\lstinputlisting[linerange=list.length.preord_example-q]{../lean/love12_basic_mathematical_structures_demo_master.lean}
%
\li{dec_trivial} is a special lemma that relies on type class inference to
prove trivial decidable goals.

Complete lattices, which we discussed in
Chapter~\ref{chap:denotational-semantics}, are formalized as another type class,
\li{complete_lattice}, which inherits from \li{partial_order}.
In the following diagram, an arrow from \textit{X} to \textit{Y}
means ``\textit{X} inherits all properties from \textit{Y}.''

\begin{center}
\tabletsmall
\tikzset{>={angle 60}}
\begin{tikzpicture}[node distance = {1.0em and 1.5em}, v/.style = {}]
    \graph[nodes={}, grow right=9em, branch down=4em]{
        "\li{linear_order}" -> "\li{partial_order}" -> "\li{preorder}",
        "\phantom{node}" ->[color=white] "\li{complete_lattice}" -> "\li{partial_order}"
    };
\end{tikzpicture}
\end{center}

\noindent
\begin{sloppypar}
Finally, Lean provides type classes that combine orders and algebraic
structures: \hbox{\li{ordered_cancel_comm_monoid},} \li{ordered_comm_group},
\li{ordered_semiring}, \li{linear_ordered_semiring},
\li{linear_ordered_comm_ring}, \li{linear_ordered_field}.
%
All these mathematical structures relate \li{≤} and \li{<}
with the constants \li{0}, \li{1}, \li{+}, and \li{*}
by monotonicity rules (e.g., \li{a ≤ b → c ≤ d → a + c ≤ b + d})
and cancellation rules (e.g., \li{c + a ≤ c + b → a ≤ b}).
\end{sloppypar}

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Notation}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|\↑| & coercion operator \li|coe| \\
\end{xltabular}

\subsection*{Lemma}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|dec_trivial| & decidable truth (e.g., a true closed executable expression) \\
\end{xltabular}

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|abel| & normalizes terms of commutative monoids and groups \\
\li|norm_cast| & normalizes coercions \\
\li|ring| & normalizes ring expressions \\
\li|ring_exp| & normalizes ring expressions including exponents \hbox{with variables} \\
\end{xltabular}

\endgroup
