\section{Lean}
Lean is an interactive theorem prover based on dependent type theory -- specifically, the \emph{Calculus of Inductive Constructions} (CIC). CIC is also used in other theorem provers, chief among them Coq, from which it originates. Dependent type theory has a computational interpretation, and as such, Lean can be used as a functional programming language. For instance, consider \cref{ex:haskell}, which defines the datatype \lean{Nat} of natural numbers, as well as an addition function on \lean{Nat}:

\begin{example}[Addition on the natural numbers in Haskell]\label{ex:haskell}~ %
  %\begin{noindent}
\begin{minted}{haskell}
data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

add :: Nat -> Nat -> Nat
add Zero b     = b
add (Succ a) b = Succ (add a b)
\end{minted}
%\end{noindent}
\end{example}

The equivalent Lean code looks fairly similar, using an inductive type for \lean{Nat} and similarly performing pattern matching in \lean{add} (\cref{ex:leanadd}).

\begin{example}[Addition on the natural numbers in Lean]\label{ex:leanadd}~ %
  % \begin{noindent}
\begin{leancode}
inductive Nat where
  | zero: Nat
  | succ: Nat → Nat

def add: Nat → Nat → Nat
  | Nat.zero, b     => b
  | (Nat.succ a), b => Nat.succ (add a b)
\end{leancode}
% \end{noindent}
\end{example}
%

Whereas previous versions of Lean were intended to be theorem provers first, with the ability to encode and evaluate programs second, the version we are using, Lean 4, forms an integrated functional programming language and theorem prover, similar in some sense to Agda. As such, Lean has all the features you would expect from a modern functional programming language.

What makes Lean special is its support for proving properties of our definitions. Alongside its computational interpretation, dependent type theory also has a logical interpretation. Namely, we can state propositions as types, and give proofs as inhabitants of that type. Take, for example, logical implication. The statement $p \implies q$ in propositional logic can be seen as the function type \lean{p → q}: if we have a function of type \lean{p → q}, and we provide an element of type \lean{p}, we can get an element of type \lean{q}, just as, by modus ponens, a proof of $p \implies q$ and a proof of $p$ yield a proof of $q$. Therefore, if we can define a function \lean{p → q}, we have a proof of $p \implies q$.

Of course, implication is only one of the standard logical connectives. Lean's type theory also allows us to encode the rest of the logical primitives of higher-order logic. For instance, conjunction and disjunction (\leandoc{And} and \leandoc{Or}):

\begin{definition}[Conjunction and disjunction in Lean]~ %
  % \begin{noindent}
\begin{leancode}
    inductive And: Prop → Prop → Prop where
      | intro: (a b: Prop) → a → b → And a b
    
    inductive Or: Prop → Prop → Prop where
      | inl: (a b: Prop) → a → Or a b
      | inr: (a b: Prop) → b → Or a b
\end{leancode}
% \end{noindent}
\end{definition}

We define the inductive types \lean{And} and \lean{Or}. Both \emph{type constructors} \lean{And} and \lean{Or} take two propositions and return a proposition; this is represented in their type signature \lean{Prop → Prop → Prop}. \lean{And} has a single introduction rule \lean{intro}, which takes two propositions \lean{a}, \lean{b} as well as proofs of \lean{a} and \lean{b}, and returns a proof of \lean{And a b}, more commonly written \lean{a ∧ b}. \lean{Or} instead has two introduction rules, \lean{inl} and \lean{inr}, corresponding to a proof via the left disjunct and a proof via the right disjunct.

The perceptive reader may notice some unfamiliar syntax in the introduction rules for \lean{And} and \lean{Or}. Instead of a regular function type, which takes the form \lean{σ → τ}, we are greeted by the dependent function type \lean{(x: σ) → τ[x]}, where \lean{x} has the type \lean{σ}, and may appear in \lean{τ}. This allows \lean{τ} to \emph{depend} on \lean{x} -- hence the name dependent type theory.

Although the syntax above shows the underlying dependent function types well, we generally use slightly different syntax, which moves the common parameters to the header. Additionally, since \lean{And} is a single-constructor type, we use the \lean{structure} keyword, which allows us to refer to the left and right conjunct using the \leandoc{And.left} and \leandoc{And.right} functions (also written \lean{h.left} and \lean{h.right} if \lean{h: a ∧ b}). The following definitions come straight from the Lean standard library \ldsym{And}:

\begin{definition}[Conjunction and disjunction in Lean 2]~ %
  % \begin{noindent}
\begin{leancode}
    structure And (a b : Prop) : Prop where
      /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
      intro ::
      /-- Extract the left conjunct from a conjunction. `h : a ∧ b` then
          `h.left`, also notated as `h.1`, is a proof of `a`. -/
      left : a
      /-- Extract the right conjunct from a conjunction. `h : a ∧ b` then
          `h.right`, also notated as `h.2`, is a proof of `b`. -/
      right : b

    inductive Or (a b : Prop) : Prop where
      /-- `Or.inl` is "left injection" into an `Or`.
          If `h : a` then `Or.inl h : a ∨ b`. -/
      | inl (h : a) : Or a b
      /-- `Or.inr` is "right injection" into an `Or`.
          If `h : b` then `Or.inr h : a ∨ b`. -/
      | inr (h : b) : Or a b
\end{leancode}
% \end{noindent}

\end{definition}

Similar definitions exist for $\top$ (\leandoc{True}), $\bot$ (\leandoc{False}), $\exists$ (\lean{∃}, \leandoc{Exists}), $\Leftrightarrow$ (\lean{↔}, \leandoc{Iff}), and $=$ (\lean{=}, \leandoc{Eq}). $\neg a$ (\lean{¬}, \leandoc{Not}) is defined as \lean{a → False}, and $\forall$ is simply alternative notation for the dependent function type: \lean{(∀x: σ, τ[x])} is definitionally equal to \lean{((x : σ) → τ[x])}. This completes our complement of standard logical symbols.

Although proofs can be written in the same functional language as definitions and programs, most Lean proofs make use of the built-in \emph{tactic language}. A similar system exists in Coq (\emph{Ltac}), and there are loosely related concepts in Isabelle/HOL and Agda, although they work significantly differently. As an example, let's prove the simple statement that adding zero to a natural number yields the number unchanged:

\begin{example}[A proof of $\forall n, n + 0 = n$]~ %
  % \begin{noindent}
\begin{leancode}
    theorem add_zero: ∀a: Nat, add a 0 = a := by
      intro a            -- We introduce a, moving it into the context.
      induction a        -- We perform induction on a.

      /- The base case is trivial, by reduction of `add 0 0` to `0`. -/
      case zero =>
        trivial          

      /- In the inductive step, we have `n: Nat, ih: add n 0 = n`,
         and we must show `add (n + 1) 0 = n + 1`. -/
      case succ n ih =>
        rw [add]         -- `add (n + 1) 0` = `(add n 0) + 1` (by `add`)
        rw [ih]          -- `(add n 0) + 1` = `n + 1` (by `ih`). QED.
\end{leancode}
% \end{noindent}
\end{example}

Using the tactic language, the proof is written in a way that somewhat resembles pen-and-paper mathematics. Aside from basic operations (introduction, induction, cases, rewriting, ...), tactics are also the main way to access proof automation in Lean. For instance, there are tactics which automatically resolve integer and natural linear arithmetic problems (\leandoc*{Lean.Parser.Tactic.omega}{omega}), simplify the goal or hypotheses in various ways (\leandoc*{Lean.Parser.Tactic.simp}{simp}), et cetera.

Formalizing mathematics in Lean, then, is a question of defining types and functions, formulating propositions, and writing proofs. To help us get started, Lean ships with a number of built-in types, functions, and lemmas, which we can use in our formalization: the Lean \emph{standard library}. Aside from the standard library, most of the mathematics that has been formalized in Lean lives in \href{https://leanprover-community.github.io/mathlib-overview.html}{\emph{mathlib}}, the community-maintained mathematical library.

\subsection{Set-theoretic definitions in Lean}\label{sec:settheory}
Much of traditional mathematics is written in the language of set theory, and this is also the case with abstract rewriting. Since Lean is not based on set theory, but on type theory, we will often have to make some adjustments to set-theoretic definitions in order to represent them in Lean. To illustrate the differences, consider the following objects:

\begin{itemize}
  \item $\NN$, the natural numbers,
  \item $\{ 1, 2, 3 \}$, a set of natural numbers,
  \item $1$, a natural number.
\end{itemize}

In set theory, all three of these are sets, just like every other object in set theory. In this way, set theory is essentially untyped. This means we can state things like $\NN = \{ n \mid n \in \NN \}$, or even $1 \in 2$, without violating the rules of set theory.

In Lean's type theory, these three objects also exist, but they are distinctly different kinds of objects. The natural numbers are a \emph{type}, with individual natural numbers (like $1$) being inhabitants of the type. The only object of the above that we would also call a set in type theory is our set of natural numbers $\{ 1, 2, 3 \}$ -- in Lean, this object would have the type \leandoc*{Set}{Set ℕ}. As you can see, a set in Lean is always a set of elements \emph{of some type} -- in this case, natural numbers. In some sense, the natural numbers are a `base set' which would be represented as a type in Lean, and any subsets of a base set are what we call \lean{Set}s in Lean.

Because these three kinds of objects have different types, many `nonsensical' statements become invalid. For instance, $\in$ is only defined if the right-hand side is a \lean{Set} with elements of the same type as the left-hand side, so the expression \lean{1 ∈ 2} is not well-typed. Additionally, trivial equalities in set theory like $\NN = \{ n \mid n \in \NN \}$ are not well-typed in Lean, because the natural numbers are distinct from the set containing all natural numbers.

Aside from sets, Lean has the concept of \emph{subtypes} (\leandoc{Subtype}). Subtypes are essentially sets with the membership predicate lifted into the type system. That is, the set \lean{s := { m: ℕ | m < 10 }} contains elements \lean{n: ℕ} which satisfy \lean{n < 10}, and the subtype \lean{{ m // m < 10 }} has inhabitants \lean{n : { m // m < 10 }}, which consist of a value \lean{n.val : ℕ} and a proof \lean{n.prop: n.val < 10}.

Choosing between sets and subtypes is a trade-off: do you always want to carry the membership proof with the element? For instance, if you find yourself writing a lot of proofs that take an element of some type along with a proof that the element is a member of a set, it might be more convenient to use subtypes. Additionally, because subtypes are types, they can be used wherever a type is expected. Both subtypes and sets occur in various definitions in this thesis, and it is fairly easy to convert between the two.

\subsection{Parameter notation}
There are various ways of writing the parameters in function definitions in Lean. For instance, our addition function on natural numbers from \cref{ex:leanadd} can also be written as follows:

\begin{example}[Addition on natural numbers, revisited]~ %
  % \begin{noindent}
\begin{leancode}
def add (a b: ℕ): ℕ :=
  match a, b with
    | Nat.zero,      b' => b'
    | (Nat.succ a'), b' => Nat.succ (add a' b')    
\end{leancode}
% \end{noindent}
\end{example}

Here, we name the parameters in the function header, and we mark the type of \lean{add a b} as \lean{ℕ}. Note that we then immediately perform a pattern match, so this notation is not so useful. It often can be useful, though; for instance, when we want to pass in \emph{implicit} parameters.

Often, lemmas and definitions are given parameters that can be inferred from the explicit parameters -- these \emph{implicit} parameters are surrounded by curly braces instead of parentheses. When using such a declaration, the user does not need to supply the implicit parameters. For example:

\begin{example}[Implicit and explicit parameters]\label{ex:verboselean}~ %
  % \begin{noindent}
\begin{leancode}
def is_symmetric {α: Type} (r: Rel α α) := 
  ∀(a b: α), r a b → r b a

def is_reflexive {α: Type} (r: Rel α α) :=
  ∀(a: α), r a a

def example_rel {α: Type}: Rel α α
| a, b => True

lemma example_rel_rfl {α: Type}:
    is_reflexive example_rel := ...
\end{leancode}
% \end{noindent}
\end{example}

The declarations in \cref{ex:verboselean} all take a type argument \lean{α}, but \lean{α} can be inferred from the relation that we pass in. Therefore, we can mark \lean{α} as implicit. Additionally, it can often be nice to not have to repeat these arguments time and time again. Instead, we can use a \lean{variable} declaration to declare them upfront. Lean will recognize that we are referring to the previously declared variables, and automatically insert arguments in our definition for us.
\newpage
\begin{example}[Variable declarations]\label{ex:lessverboselean}~ %
  % \begin{noindent}
\begin{leancode}
variable {α} (r: Rel α α)

def is_symmetric := 
  ∀(a b: α), r a b → r b a

def is_reflexive :=
  ∀(a: α), r a a

def example_rel: Rel α α
| a, b => True

lemma example_rel_rfl:
    is_reflexive example_rel := ...

#check is_symmetric -- is_symmetric has type {α: Type} → (r: Rel α) → Prop
\end{leancode}
% \end{noindent}
\end{example}

The \lean{variable} declaration declares an implicit parameter \lean{α: Type} and an explicit parameter \lean{r: Rel α α}. Note that we have not even said that \lean{α} should be a \lean{Type}; Lean can also infer that from the context.

\subsection{Lean conventions}\label{sec:leanconventions}
The rest of this thesis contains numerous snippets of Lean code. The following variables may be assumed to exist in any Lean code snippet included from chapter 3 onwards:

% \begin{noindent}
\begin{leancode}
    variable {α β I J: Type} (r s: Rel α α) (A: ARS α I)
\end{leancode}
% \end{noindent}

That is, we introduce four types \lean{α, β, I, J}; two relations \lean{r, s}, and an ARS \lean{A}. What these are will become clear in the coming chapters.

Note that we use the standard Lean convention of denoting arbitrary type variables by a Greek letter (\lean{α, β, γ, ...}). This occasionally clashes with the use of Greek letters for indices in the literature. We instead use the letters $i, j, k, \ldots$ for these indices.

When describing definitions and lemmas for the first time, we will often link to their page in the library documentation. These links are printed in \textcolor{Green}{\texttt{Monospaced Green}}, e.g. \leandoc{Set}.
