\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
$\cdot$~:~\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} $\cdot$ \textit{b}) $\cdot$ \textit{c} $=$
\textit{a} $\cdot$ (\textit{b} $\cdot$ \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} $\cdot$ \textit{a} $=$
%\textit{a} $\cdot$ \textit{e}
\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}$
$\cdot$ \textit{a} %$=$ \textit{a} $\cdot$ \textit{a}$^{-1}$
$=$ \textit{e}.
\end{itemize}

In Lean, a type class for groups could be defined as follows:
%
\lstinputlisting[linerange=Group-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.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{AddGroup}. 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
\li{Add}\-\li{Group}. To illustrate this, we will
define the type \li{Int2} of integers modulo~2, also known as
$\mathbb{Z}/2\mathbb{Z}$ or $\mathbb{Z}_2$, and register it as an \li{AddGroup}.
The type \li{Int2} has two elements:
%
\lstinputlisting[linerange=Int2-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

Addition is defined as follows:
%
\lstinputlisting[linerange=Int2.add-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

To instantiate \li{AddGroup}, we need to provide the following constants and
properties:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|add| & \lic| : α → α → α| \\
\lic|zero| & \lic| : α| \\
\lic|neg| & \lic| : α → α| \\
\lic|add_assoc| & \lic| : ∀a b c, add (add a b) c = add a (add b c)| \\
\lic|zero_add| & \lic| : ∀a, add zero a = a| \\
\lic|add_zero| & \lic| : ∀a, add a zero = a| \\
\lic|add_left_neg| & \lic| : ∀a, add (neg a) a = zero| \\
\end{tabular}
\end{center}
%
The constants \li{AddGroup.add}, \li{AddGroup.zero}, and \hbox{\li{AddGroup.neg}}
correspond to the binary operator, the identity element, and the inverse. The
properties \li{Add}\-\li{Group.add_assoc},
\li{AddGroup.}\allowbreak\li{zero_add}, and \li{AddGroup.add_left_neg}
correspond to the three group axioms. For technical reasons, we must also prove
the redundant property \li{AddGroup.}\allowbreak\li{add_zero}.

The type \li{Int2} can be registered as a group as follows:
%
\lstinputlisting[linerange=Int2.AddGroup-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

Thanks to this instance, we can now write \li{0}, \li{+}, and \li{-}:
%
\lstinputlisting[linerange=Int2_notation-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.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|LeftCancelSemigroup|  & \li{Semigroup} with \li{c * a = c * b → a = b} & \\
\li|RightCancelSemigroup| & \li{Semigroup} with \li{a * c = b * c → a = b} & \\
\li|Group|                & \li{Monoid} with inverse $^{-1}$ \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\noindent
For most of these structures, commutative versions (where \textit{a} $\cdot$
\textit{b} $=$ \textit{b} $\cdot$ \textit{a} for all elements \textit{a},
\textit{b}) are available:\
\li{CommSemigroup}, \li{CommMonoid}, \li{CommGroup}.
They also all have additive counterparts prefixed with \li{Add}:

\vskip4\smallskipamount

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

\vskip4\smallskipamount

Although the additive type classes are merely copies of 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
theorems and definitions based on the multiplicative type classes,
the copying process is automated via metaprograms.

An example instance of \li{AddMonoid} is the type \li{List α} with the
empty list \li{[]} as zero and the append operator \li{++} as addition:
%
\lstinputlisting[linerange=List.AddMonoid-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
We could continue and register \li{List α} with \li{[]} and \li{++} as an
\li{Add}\-\li{LeftCancel}\-\li{Semi}\-\li{group} and an \li{AddRightCancelSemigroup}.

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 constants and 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{Semigroup}" <- "\li{Monoid}" <- "\li{Group}",
    "\li{CommSemigroup}" <- "\li{CommMonoid}" <- "\li{CommGroup}",
    "\li{CommGroup}" -> "\li{Group}",
    "\li{CommMonoid}" -> "\li{Monoid}",
    "\li{CommSemigroup}" -> "\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{AddSemigroup}" <- "\li{AddMonoid}" <- "\li{AddGroup}",
    "\li{AddCommSemigroup}" <- "\li{AddCommMonoid}" <- "\li{AddCommGroup}",
    "\li{AddCommGroup}" -> "\li{AddGroup}",
    "\li{AddCommMonoid}" -> "\li{AddMonoid}",
    "\li{AddCommSemigroup}" -> "\li{AddSemigroup}"
};
\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
structures 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 \li{Field}. Again, the type class includes some redundant
properties %, such as \li{left_distrib} and \li{right_distrib},
due to its construction.

We will now show that \li{Int2} is a field by instantiating the \hbox{\li{Field}} type
class with it. First, we must define multiplication on \li{Int2}:
%
\lstinputlisting[linerange=Int2_mul-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
To declare \li{Int2} as a field, we can reuse the instance
\li{Int2}\allowbreak\hbox{\li{.AddGroup}} that we defined above using the
syntax \li{Int2.AddGroup with}. We can prove the remaining properties as follows:
%
\lstinputlisting[linerange=Int2_field-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

With this declaration in place, we can now use the notations \li{1}, \li{*},
\li{/}, and more:
%
\lstinputlisting[linerange=Int2_reduce_1-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
This command prints \li{Int2.zero}. The type annotation \li{: Int2} is necessary
here to tell Lean that we want to calculate in \li{Int2} and not in \li{ℕ}, the
default. We can even use arbitrary numerals in \hbox{\li{Int2}.} For example, the
numeral \li{3} is interpreted as \li{1 + 1 + 1}, which is the same as \li{1} in
\li{Int2}:
%
\lstinputlisting[linerange=Int2_reduce_3-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
This command prints \li{Int2.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{AddCommMonoid} with distributivity    & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
\li{CommSemiring}  & \li{Semiring} with commutativity of \li{*}                & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{N}$ \\
\li|Ring|          & \li{Monoid} and \li{AddCommGroup} with distributivity     & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$ \\
\li{CommRing}      & \li{Ring} with commutativity of \li{*}                    & $\mathbb{R}$, $\mathbb{Q}$, $\mathbb{Z}$ \\
\li|DivisionRing|  & \li{Ring} with multiplicative inverse                     & $\mathbb{R}$, $\mathbb{Q}$ \\
\li{Field}         & \li{DivisionRing} with commutativity of \li{*}            & $\mathbb{R}$, $\mathbb{Q}$ \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\noindent
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{Semiring}" <- "\li{Ring}"  <-  "\li{DivisionRing}",
        "\li{CommSemiring}" <- "\li{CommRing}" <-  "\li{Field}",
        "\li{Field}" -> "\li{DivisionRing}",
        "\li{CommRing}" -> "\li{Ring}",
        "\li{CommSemiring}" -> "\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, and Euclidean rings.

The \li{Field} type class requires the property \li{∀a, a / 0 = 0}. This is
simply a convention to make division a total function. Mathematicians would
regard division as a partial function. There is no harm in totalizing a partial
function in this way. 

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}
tactic to normalize terms containing operators on those types. For example:
%
\lstinputlisting[linerange=ring_example-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
This tactic is 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/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

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

When combining numbers from \li{ℕ}, \li{ℤ}, \li{ℚ}, and \li{ℝ} in the same
theorems, 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 theorem and notice the type of the arguments of multiplication:
%
\lstinputlisting[linerange=neg_mul_neg_nat-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
Surprisingly, this statement does not lead to an error,
although negation \li{- n} is not defined on \li{n : ℕ},
and multiplication of \li{z : ℤ} and \li{n : ℕ} is not defined.

The diagnosis command \li{#check} \li{neg_mul_neg_Nat} tells us what happened:
%
\begin{lstlisting}[language=,procnamekeys={}]
neg_mul_neg_Nat : ∀ (n : ℕ) (z : ℤ), -z * -↑n = 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}

We can provide type annotations to document our intentions or help
Lean figure out where to place the coercions, as in the following example:
%
\lstinputlisting[linerange=neg_nat_mul_neg-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

In proofs involving coercions, the \li{norm_cast} tactic can be convenient. It
helps with goals such as \li{⊢ m n : ℕ, h : ↑m = ↑n ⊢ m = n} in
%
\lstinputlisting[linerange=norm_cast_example_1-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
Similarly, it helps with the goal \li{⊢ m n : ℕ ⊢ ↑m + ↑n = ↑(m + n)} in
%
\lstinputlisting[linerange=norm_cast_example_2-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}

The \li{norm_cast} tactic relies on theorems 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 tactic \li{ring} %, \li{ring_exp}, and \li{abel}
and the coercion
tactic \li{norm_cast} 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 prove the goal.

The optional \ttvar{position} argument 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
tactic proves 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 theorem, 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/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.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 come into play. For multisets, we have
\hbox{\li|{3, 2, 1, 2} =|} \hbox{\li|{1, 2, 2, 3}|,} whereas the two 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/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
Using this definition, we can prove that
\hbox{\li{Multiset.elems t = Multiset.elems}} \hbox{\li{(mirror t)},} whereas
\li{List.elems t = List.elems (mirror t)} does not hold in general.
\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/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
For lists and multisets, Lean offers sum and product operators to add
or multiply all of the elements. Below, the first two commands print 9, and
the last two print 24:
%
\lstinputlisting[linerange=sum_prod-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
%The operators \li{Finset.sum} and \li{Finset.prod} take as 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{fun 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{AddMonoid} for sum or of \li{Monoid} for product. The
\li{Multiset} and \li{Finset} versions also require an instance
declaration for \li{AddCommMonoid} or \hbox{\li{CommMonoid}} because the result
cannot depend on the order of adding or multiplying the elements.

%Lean's \li{mathlib} provides a collections of theorems 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 familiar order on the natural numbers can be defined as
%
\lstinputlisting[linerange=nat.le-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.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 lengths.

In Lean, there are type classes for the different kinds of orders:
\hbox{\li{LinearOrder},} \li{PartialOrder}, and \li{Preorder}.
The \li{Preorder} class has one constant and two properties:
%
\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{PartialOrder} class has the additional property
%
\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{LinearOrder} has the additional property
%
\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 lengths
as follows:
%
\lstinputlisting[linerange=list.length.preord-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
This type class instance gives access to the infix syntax \li{≤} and to the
corresponding relations \li{≥}, \li{<}, and \li{>}:
%
\lstinputlisting[linerange=list.length.preord_example-q]{../lean/LoVe/LoVe13_BasicMathematicalStructures_DemoMaster.lean}
%
The proof features a new tactic:\ \li{decide}. It 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{CompleteLattice}, which extends \li{PartialOrder}.
In the following diagram, an arrow from \textit{X} to \textit{Y}
means ``\textit{X} inherits all constants and 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{Preorder}" <- "\li{PartialOrder}" <- "\li{LinearOrder}",
        "\phantom{node}" ->[color=white] "\li{CompleteLattice}" -> "\li{PartialOrder}"
    };
\end{tikzpicture}
\end{center}

\noindent
\begin{sloppypar}
Finally, Lean provides type classes that combine orders and algebraic
structures: \hbox{\li{OrderedCancelCommMonoid},} \li{OrderedCommGroup},
\li{OrderedSemiring}, \li{Linear}\-\li{Ordered}\-\li{Semiring},
\li{LinearOrderedCommRing}, \li{LinearOrderedField}.
%
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 +} \li{a ≤ c + b → a ≤ b}).
\end{sloppypar}

\section{Decision Tactic}
\label{sec:decision-tactic}

\subsection*{decide}

The \li{decide} tactic can be used to prove true decidable goals. Decidability
is determined by checking membership of the \li{Decidable} type class. Unlike
\li{rfl}, \li{decide} is not limited to proving equalities.

\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*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
%\lic|abel| & normalizes terms of commutative monoids and groups \\
\lic|decide| & proves decidable truths (e.g., a true executable expression) \\
\lic|norm_cast| & normalizes coercions \\
\lic|ring| & normalizes ring expressions \\
%\lic|ring_exp| & normalizes ring expressions including exponents \hbox{with variables} \\
\end{xltabular}

\endgroup
