AlgebraSurvey.tex

\chapter{Types Of Algebraic Structures In Proof Assistant Systems - Survey}

A survey of coverage of algebraic structures in proof systems will help to
identify the gaps in the system. A survey can provide insights into how well
each proof assistant supports the formalization of algebraic structures, making
it easier for researchers and developers to choose the right platform for their
mathematical formalization. Researchers and developers may be inspired to work
on formalizing missing algebraic structures, which can lead to improvements in
the tools and expand their utility.

This chapter provides the coverage of algebraic structures in proof assistant
systems. Since I was exposed to Agda in the coursework, it added bias to select
systems that are comparable with Agda thus eliminating systems such as Mizar and
Isabelle. We consider four proof assistant systems that are all dependently
typed higher-order programming languages \cite{2019arXiv191203028S}. A standard
library for a system is a collection of mathematical definitions with logical
constructs, proof tactics, and utility functions that provide a foundational set
of tools and definitions for users of these proof assistants
\cite{kohlhase2021experiences}. For the scope of the thesis, we consider the
libraries as standard libraries that are commonly used and referenced for the
respective proof systems in the context of algebra. This chapter aims to provide
documentation for the algebraic coverage in the standard libraries of proof
assistant systems Agda, Idris, Coq, and Lean. In this chapter, the latest
available versions are considered i.e., Agda standard library v1.7
\cite{danielsson2011agda}, Idris 2.0 \cite{Brady2021Idris2Q}, The Mathematical
Components Library v1.13.0 \cite{assia_mahboubi_2021_4457887}, and The Lean
mathematical library\cite{10.1145/3372885.3373824}.

The rest of the chapter is organized as follows: Section \ref{Proof_system}
gives a brief overview of the proof systems that we discuss in this chapter.
The experiment setup is discussed in Section \ref{experiment}. In Section
\ref{threat}, we discuss the threat to validity. Section \ref{algebraic_structure}
discuss how algebraic structures are defined in each system by taking Monoid as
an example. Section \ref{table} provides a table that provides the results of the
survey.

\section{Proof Assistant Systems}
\label{Proof_system}
This section provides an overview of proof assistant systems Coq, Idris, and
Lean. We intentionally omit discussing Agda in this section since it is
discussed in the previous chapter. 

\subsection{Coq}
Coq \cite{Paulin-Mohring2012} is a theorem-proving system that is written in the
OCaml programming language. It is designed to assist in the formalization of
mathematical theorems by using constructive and higher-order logic. It was first
released in 1989 and is one of the most widely used proof assistant systems to
define mathematical definitions, and theory and to write proofs. The Coq
specification language is called Gallina. Users can write functions and
algorithms in Gallina and then formally verify their correctness within the Coq
environment \cite{bertot2013interactive}. Coq provides an interactive proof
development environment where users can interact with Coq through a command line
interface (or supported IDEs) to construct proofs.

The mathematical components library (v1.13.0) \cite{assia_mahboubi_2021_4457887}
includes various topics from data structures to algebra. The library provides an
extensive collection of predefined data structures, algebraic structures (e.g.,
groups, rings, fields), and mathematical concepts (e.g., natural numbers,
integers, rational numbers) \cite{2019arXiv191203028S}. The mathcomp library was
started with the Four Colour Theorem to support formal proof of the odd order
theorem. 

\subsection{Idris}
Idris is a functional programming language and interactive theorem prover
created by Dr. Edwin Brady. Idris is built on a foundation of dependent type
theory. The proofs are alike with Coq and the type system in Idris is uniform
with Agda \cite{brady2022idris}. Idris includes a totality checker, which helps
ensure that functions are defined for all inputs and that programs are
guaranteed to terminate \cite{brady2013idris}. Idris 2 is a self-hosted
programming language that combines linear-type systems. Idris like Agda, supports
literate programming, this helps code and documentation to be interleaved in a
natural and readable way. This is helpful for creating well-documented, readable
formalizations. In this chapter, Idris 2 and Idris are used interchangeably and
refer to Idris 2. Currently, there are no official package managers for Idris
2. However, several versions are under development. 

\subsection{Lean}

Lean \cite{de2015lean} is an open-source project by Microsoft Research. Lean is
a proof assistant system written in C++. Lean is based on a foundation of
dependent type theory, similar to Coq and Idris. Lean has a powerful
metaprogramming system that allows users to extend the language and develop
domain-specific features \cite{ebner2017metaprogramming}. The last official
version of Lean was 3.4.2 and is now supported by the Lean community. Lean 4 is
the latest version of Lean and is a complete rewrite of previous versions of
Lean. Lean has been used in various research projects and has seen adoption in
both academia and industry. Lean has found applications in formal mathematics,
formalization of mathematical proofs, software verification, and formal methods
research. It has been used to verify complex software systems and to formalize
mathematical concepts.

Lean comes with a standard library that covers a wide range of mathematics,
including number theory, algebra, analysis, and set theory. The mathematical
library (mathlib) \cite{10.1145/3372885.3373824} for Lean 3 has the most
coverage of algebra compared to the other 3 proof assistant systems discussed in
the paper. The mathlib library of Lean is also maintained by the Lean community
for community versions of Lean. It was developed on a small library that was in
Lean. It contained definitions of natural numbers, integers, and lists and had
some coverage over the algebra hierarchy. The latest version of mathlib has over
2794 definitions of algebra \cite{2019arXiv191203028S}. 

\section{Experimental Setup}
\label{experiment}
It is not time-efficient to manually look for the definitions in a large
library. The source code of the standard libraries of Agda, Idris, Coq, and Lean
are publicly available. We created a web crawler that extracts the code from the
source code webpage and built a regular expression that is unique to each system
to extract definitions. To build the web crawler, we first manually select the
source pages where the algebraic definitions can be found in each system. The
regular expression will make use of the keyword used in each system to
define algebraic structure. Thus, a part of the process of building the table
~\ref{tab:long} was automated. We then verify manually to make sure the
algebraic structures are correctly extracted by the web crawler. Since the
standard libraries are open-source projects, it is difficult to maintain
uniformity in the code. For example, the definition might start with a comment
in the same line or structure parameters might be written in a new line. All
this makes it difficult to correctly build the regular expression and will
necessitate the task of verifying the results manually to some extent. Section
\ref{threat} will discuss the threat to validity of this approach.

\section{Threat To Validity}
\label{threat}
In this section, we discuss threat to validity of the survey data. 
\begin{itemize}

  \item The libraries that we considered are under continuous
  development. The definitions that our web crawler extracted may not reflect
  the most recent code. We limit to a specific version of the library so that
  all the definitions in that version are captured. 
  \item The threat in using regular expression is that it may not capture all
  variations and formats of definitions. Some definitions may be missed, leading
  to incomplete data. We manually verify the result to look for missing
  definitions in the library.
  \item Each proof assistant has different language features that regular
  expressions need to account for. Ensuring that regular expressions work
  seamlessly across multiple proof assistants is challenging. We build unique
  regular expressions for each system.
  \item Different formalizations of algebraic structures may vary in their
  definitions and naming conventions. For example, In Agda a ring without
  multiplicative identity is called \inline{RingWithoutOne}. The same structure
  in Idris is called \inline{Ring}. These changes in naming will necessitate 
  manually verifying the result in building the table \ref{tab:long}.
  \item Regular expressions might capture irrelevant text that matches the
  pattern but is not part of the actual definition. For example, the comments in
  the source file may mislead the web crawler.
  \item Regular expressions are typically pattern-based and may not consider the
  broader context in which the definitions appear. This lack of context can
  result in misinterpretations.
\end{itemize} 

\section{Algebraic Structures}
\label{algebraic_structure}
In this section, we discuss the characterization of the monoid structure in
different libraries. A monoid is a mathematical structure consisting of a set,
an associative binary operation, and an identity element for that operation.
This section discusses the definition of the monoid structure in each proof
system and gives a brief overview of the syntax used in the definition. We
intentionally keep some overlap from the previous chapter when discussing the
definition of monoid in Agda to have uniform coverage for each system.

\subsection{Agda Standard Library}
In the Agda standard library, algebraic structures are defined over a setoid
\cite{danielsson2011agda}.

\begin{minted}[breaklines,samepage]{Agda}
record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identity    : Identity ε ∙

  open IsSemigroup isSemigroup public
\end{minted}

\inline{IsMonoid} is defined as a record type over set \inline{A} and
equivalence \inline{_≈_} that takes two parameters: \inline{∙}, is a binary
operation \inline{Op₂ A} on a set A. \inline{ε}, an element. The \inline{Set (a
⊔ ℓ)} specifies the universe level at which this record exists. \inline{field}
the keyword indicates the start of the field declaration. Field
\inline{isSemigroup}, says that the binary operation \inline{∙} forms a
semigroup, which means it is associative. The \inline{IsSemigroup} type is
defined as proof of associativity for the binary operation. Field
\inline{identity} indicates that \inline{ε} is an identity element for the
binary operation \inline{∙}. The \inline{Identity} type says that \inline{ε}
behaves as a left and right identity element for \inline{∙}. Agda opens the
\inline{IsSemigroup} field \inline{isSemigroup} so that when you have an
instance of \inline{IsMonoid}, you can directly access its \inline{isSemigroup}
field without any additional qualifiers.

The same follows for the bundled definitions of respective structures. A
hierarchical approach is adapted to define algebraic structures to make the
system scalable with minimal redundancy. One exemption for this hierarchical
definition is the definition of a lattice. A lattice is defined independently in
the standard library to overcome the redundant idempotent fields. A lattice
structure that is defined in terms of join and meet semi-lattice is added as a
biased structure. The Agda standard library defines left, right, and bi
semi-modules and modules. A similar hierarchical approach as other algebraic
structures is followed in defining modules. For example, a module is defined
using bimodules and bi-modules using bi-semimodules. An alternative definition
of modules is given in \inline{Algebra.Module.Structure.Biased}.

\subsection{The Mathematical Components Library}
The algebra structures design hierarchy of the mathcomp library is inspired by
the Packing mathematical structures. The \inlineCode{Coq}{ssralg.v} file defines
some of the simple algebraic structures with their type, packers, and canonical
properties. The hierarchy extends from Zmodule, rings to ring morphisms. The
\inlineCode{Coq}{countalg} file extends \inlineCode{Coq}{ssralg} file to define
countable types. A monoid in the mathcomp library is defined as:

\begin{minted}[samepage,breaklines]{Coq}
Module Monoid.

Section Definitions.
Variables (T : Type) (idm : T).

Structure law := Law {
  operator : T -> T -> T;
  _ : associative operator;
  _ : left_id idm operator;
  _ : right_id idm operator
}.
Local Coercion operator : law >-> Funclass
\end{minted}

The definition starts a new Coq module named \inlineCode{Coq}{Monoid}. Modules
in Coq are used to group related definitions and theorems together for better
organization and encapsulation. A new section named
\inlineCode{Coq}{Definitions} is opened to manage the scope of variables and
definitions. Two variables within the scope of the definition section are:
\inlineCode{Coq}{T} is a type variable representing the underlying set and
\inline{idm} is a variable of type \inline{T} representing the identity element
of the monoid. \inlineCode{Coq}{Structure law := Law { ... }} line represents
the properties of a monoid. \inline{operator} is a binary operation of type
\inlineCode{Coq}{T -> T -> T}. The next three lines denote associativity and
left and right identity laws.

\subsection{Idris}

In Idris 2, there is considerable overlap between abstract algebra and category
theory. Some algebraic structures are provided as an extension of two other
algebraic structures. The structures also include respective bundle definitions.
A module is an Abelian group with a ring of scalars. The ring of scalars has an
identity element. The library defines various algebraic structures that include
semigroup, monoid, group, Abelian-group, semiring, and ring. It follows a
hierarchical approach in defining structures similar to that in Agda. For
example, a semigroup is defined as a set with a binary operation that is
associative, and a monoid is defined in terms of a semigroup with an identity
element. Idris addresses identity as a neutral element.

\begin{minted}[breaklines,samepage]{Idris}
public export
interface Semigroup t => Monoid t where
  neutral : t

  monoidNeutralIsNeutralL : (l : t) -> l <+> neutral = l
  monoidNeutralIsNeutralR : (r : t) -> neutral <+> r = r
\end{minted}

The definition is made public and available for export, making them
accessible outside the module or scope where they are defined. An interface
named \inlineCode{Idris}{Monoid} extends the Semigroup interface so that any
type \inline{t} that is an instance of \inlineCode{Idris}{Monoid} must also
satisfy the requirements of the Semigroup interface. \inlineCode{Idris}{neutral}
represents the identity element for the binary operation defined on type
\inline{t}. \inlineCode{Idris}{monoidNeutralIsNeutralL} and
\inlineCode{Idris}{monoidNeutralIsNeutralR} specifies that for any value
\inline{l} (or \inline{r}) of type \inline{t} when you combine (using the
\inline{<+>} operator) \inline{l} (or \inline{r}) with the neutral element on
the left side (or right side), it should result in \inline{l} (or \inline{r}).
\inline{neutral} element acts as an identity element on the binary operation.

\subsection{The Mathematical Library}

The mathlib library for Lean extends the algebra hierarchy from semigroup to
ordered fields. The library defines instances of free magma, free semigroup,
free Abelian group, etc. An example of the monoid structure definition in the
library is given below \cite{baanen2022use}: 

\begin{minted}[breaklines,samepage]{Lean}
@[ancestor semigroup mul_one_class, to_additive]
class monoid (M : Type u) extends semigroup M, mul_one_class M :=
(npow : ℕ → M → M := npow_rec)
(npow_zero' : ∀ x, npow 0 x = 1 . try_refl_tac)
(npow_succ' : ∀ (n : ℕ) x, npow n.succ x = x * npow n x . try_refl_tac)
\end{minted}

In Lean, classes can inherit properties and methods from other classes. The
monoid class inherits from the \inlineCode{Lean}{semigroup} and
\inlineCode{Lean}{mul_one_class} classes. \inlineCode{Lean}{to_additive}
indicates that an additive version of the monoid class should be generated. The
parameter \inlineCode{Lean}{(M : Type u)} specifies that \inline{M} is a type
parameter that is the underlying set and \inlineCode{Lean}{Type u} indicates
that \inline{M} is of a certain universe level. \inlineCode{Lean}{monoid} class
introduces an operation \inlineCode{Lean}{npow}, a power operation that takes a
natural number and an element of the monoid and calculates the repeated
application of the monoid's binary operation. The class provides two properties
for this npow operation: \inlineCode{Lean}{npow_zero'} specifies that raising
any element to the power of \inline{0} results in the identity element, and
\inlineCode{Lean}{npow_succ'} specifies the recursive behavior of the
\inlineCode{Lean}{npow} operation, where raising an element to a successor
natural number is equivalent to multiplying it with the element raised to the
previous power. The \inlineCode{Lean}{. try_refl_tac} suggests that Lean should
try to automatically prove this property using reflexivity tactics.

\section{Result}
\label{table}
In table \ref{tab:long}, every checkmark links to the implementation in the
source code of the library. In the Agda column, the checkmark in blue
(\bluecheck) indicates the algebraic structures defined as part of this thesis. 
\begin{longtable}{|l|l|l|l|l|}
\caption{ Algebraic structures in proof assistant systems} \label{tab:long} \\

\hline \multicolumn{1}{|c|}{\textbf{Algebraic Structure}} & \multicolumn{1}{c|}{\textbf{Agda}} & \multicolumn{1}{c|}{\textbf{Coq}} & \multicolumn{1}{c|}{\textbf{Idris}} & \multicolumn{1}{c|}{\textbf{Lean}} \\ \hline 
\endfirsthead

\multicolumn{5}{c}%
{{\bfseries \tablename\ \thetable{} -- continued from previous page}} \\
\hline \multicolumn{1}{|c|}{\textbf{Algebraic Structure}} & \multicolumn{1}{c|}{\textbf{Agda}} & \multicolumn{1}{c|}{\textbf{Coq}} &  \multicolumn{1}{c|}{\textbf{Idris}} & \multicolumn{1}{c|}{\textbf{Lean}}  \\ \hline 
\endhead

\hline \multicolumn{5}{|r|}{{Continued on next page}} \\ \hline
\endfoot

\hline \hline
\endlastfoot
        Magma &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L32}{\checkmark} & - & - & - \\ \hline
        Commutative Magma &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L49}{\checkmark} & - & - & - \\ \hline
        Selective Magma &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L57}{\checkmark} & - & - & - \\ \hline
	IdempotentMagma & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L56}{\bluecheck} & - & - &  - \\ \hline
	AlternativeMagma & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L63}{\bluecheck} & - & - &  - \\ \hline
	FlexibleMagma & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L76}{\bluecheck} & - & - &  - \\ \hline
	MedialMagma & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L832}{\bluecheck} & - & - &  - \\ \hline
	SemiMedialMagma & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L90}{\bluecheck} & - & - &  - \\ \hline
        Semigroup &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L65}{\checkmark} & \href{https://github.com/math-comp/math-comp/blob/c553e54b4c5465539fb6e45295e2b9e778cd4ef1/mathcomp/ssreflect/bigop.v#L1184}{\checkmark} &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L7}{\checkmark} & \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/group/defs.lean#L94}{\checkmark} \\ \hline
        Band &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L73}{\checkmark} & - & - & - \\ \hline
        Commutative Semigroup &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L81}{\checkmark} & - & - &\href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/group/defs.lean#L116}{\checkmark} \\ \hline
        Semilattice &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L32}{\checkmark} & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/395e27554fc8db530ad6a1c3dbaff0a602653aa6/src/order/lattice.lean#L86}{\checkmark} \\ \hline
        Unital magma &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L98}{\bluecheck} & - & - & - \\ \hline
        Monoid &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L112}{\checkmark} & \href{https://github.com/math-comp/math-comp/blob/c553e54b4c5465539fb6e45295e2b9e778cd4ef1/mathcomp/ssreflect/bigop.v#L323}{\checkmark} &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L12}{\checkmark} &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/group/defs.lean#L377}{\checkmark} \\ \hline
        Commutative monoid &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L132}{\checkmark} & \href{https://github.com/math-comp/math-comp/blob/c553e54b4c5465539fb6e45295e2b9e778cd4ef1/mathcomp/ssreflect/bigop.v#L336}{\checkmark} & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/group/defs.lean#L420}{\checkmark} \\ \hline
        Idempotent commutative monoid &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L149}{\checkmark} & - & - & - \\ \hline
        Bounded Semilattice &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L70}{\checkmark} & - & - & - \\ \hline
	Bounded Meetsemilattice &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L84}{\checkmark} & - & - & - \\ \hline
	Bounded Joinsemilattice &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L97}{\checkmark} & - & - & - \\ \hline
	Invertible Magma  &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L165}{\bluecheck} & - & - & - \\ \hline
	IsInvertible UnitalMagma  &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L179}{\bluecheck} & - & - & - \\ \hline
        Quasigroup &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L557}{\bluecheck} & - & - & - \\ \hline
        Loop &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L565}{\bluecheck} & - & - & - \\ \hline
	Moufang Loop &  \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L932}{\bluecheck}  & - & - & -\\ \hline
	Left Bol Loop &  \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L918}{\bluecheck}  & - & - & -\\ \hline
	Middle Bol Loop &  \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L940}{\bluecheck}  & - & - & -\\ \hline
	Right Bol Loop &  \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L925}{\bluecheck}  & - & - & -\\ \hline
        NilpotentGroup & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/group_theory/nilpotent.lean#L135}{\checkmark} \\ \hline
        CyclicGroup & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/395e27554fc8db530ad6a1c3dbaff0a602653aa6/src/group_theory/specific_groups/cyclic.lean#L56}{\checkmark} \\ \hline
        SubGroup & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/395e27554fc8db530ad6a1c3dbaff0a602653aa6/src/group_theory/subgroup/basic.lean#L100}{\checkmark} \\ \hline
        Group &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L199}{\checkmark} & \href{https://github.com/math-comp/math-comp/blob/c553e54b4c5465539fb6e45295e2b9e778cd4ef1/mathcomp/fingroup/fingroup.v#L734}{\checkmark} &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L29}{\checkmark} &  \href{https://github.com/leanprover-community/mathlib/blob/395e27554fc8db530ad6a1c3dbaff0a602653aa6/src/algebra/group/defs.lean#L600}{\checkmark} \\ \hline
        Abelian group &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L238}{\checkmark} & - &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L53}{\checkmark} &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/group_theory/abelianization.lean#L35}{\checkmark} \\ \hline
        Lattice &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L125}{\checkmark} & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/order/lattice.lean#L460}{\checkmark} \\ \hline
        Distributive lattice &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L157}{\checkmark} & - & - & - \\ \hline
        Near semiring &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L260}{\checkmark} & - & - & - \\ \hline
        Semiringwithout one &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L292}{\checkmark} & - & - & - \\ \hline
        Idempotent Semiring &  \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L545}{\bluecheck} & - & - & - \\ \hline
        Commutative semiring without one &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L325}{\checkmark} & - & - & - \\ \hline
        Semiring without annihilating zero &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L346}{\checkmark} & - & - & - \\ \hline
        Semiring   &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L394}{\checkmark} & \href{https://github.com/math-comp/math-comp/blob/c553e54b4c5465539fb6e45295e2b9e778cd4ef1/mathcomp/algebra/ssralg.v#L3575}{\checkmark} & - &\href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/ring/basic.lean#L119}{\checkmark} \\ \hline
        Commutative semiring &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L419}{\checkmark} & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/ring/basic.lean#L588}{\checkmark} \\ \hline
	Non associative ring & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L695}{\bluecheck} & - & - &  - \\ \hline
	Nearring & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L741}{\bluecheck} & - & - &  - \\ \hline
	Quasiring & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L572	}{\bluecheck} & - & - &  - \\ \hline
        Local ring & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/ring_theory/ideal/local_ring.lean#L35}{\checkmark} \\ \hline
        Noetherian ring & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/ring_theory/noetherian.lean#L661}{\checkmark} \\ \hline
        Ordered ring & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/order/ring.lean#L853}{\checkmark} \\ \hline
        Cancellative commutative semiring &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L446}{\checkmark} & - & - & - \\ \hline
        Sub ring & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/order/ring.lean#L853}{\checkmark} \\ \hline
        Ring &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L459}{\checkmark} &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L905}{\checkmark} &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L85}{\checkmark} &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/ring/basic.lean#L632}{\checkmark} \\ \hline
        Unit Ring & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L626}{\bluecheck} &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L2878}{\checkmark} &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L119}{\checkmark} & - \\ \hline
        Commutative Unit ring & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L3203}{\checkmark} & - & - \\ \hline
        Commutative ring &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L531}{\checkmark} &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L2529}{\checkmark} & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/ring/basic.lean#L812}{\checkmark} \\ \hline
        Integral Domain & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L4593}{\checkmark} & - & - \\ \hline
        LieAlgebra & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/lie/basic.lean#L61}{\checkmark} \\ \hline
        LieRing module & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/lie/basic.lean#L68}{\checkmark} \\ \hline
	Lie module & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/lie/basic.lean#L76}{\checkmark} \\ \hline
        Boolean algebra &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Lattice/Structures.agda#L180}{\checkmark} & - & - & - \\ \hline
        Preleft semimodule &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L31}{\checkmark} & - & - & - \\ \hline
        Left semimodule &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L42}{\checkmark} & - & - & - \\ \hline
        Preright semimodule &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L78}{\checkmark} & - & - & - \\ \hline
        right semimodule &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L89}{\checkmark} & - & - & - \\ \hline
        Bi semimodule &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L132}{\checkmark} & - & - & - \\ \hline
        Semimodule &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L169}{\checkmark} & - & - &  - \\ \hline
        Left module &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L183}{\checkmark} &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L1550}{\checkmark} & - & - \\ \hline
        Right module &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L211}{\checkmark} & - & - & - \\ \hline
        Bi module &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L246}{\checkmark} & - & - & - \\ \hline
        Module &  \href{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Module/Structures.agda#L284}{\checkmark} & \href{https://github.com/math-comp/math-comp/blob/c553e54b4c5465539fb6e45295e2b9e778cd4ef1/mathcomp/algebra/ssralg.v#L5073}{\checkmark} & - &  \href{https://github.com/leanprover-community/mathlib/blob/395e27554fc8db530ad6a1c3dbaff0a602653aa6/src/algebra/module/basic.lean#L50}{\checkmark} \\ \hline
        Field & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L4777}{\checkmark} &  \href{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L153}{\checkmark} &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/field/basic.lean#L163}{\checkmark} \\ \hline
        Decidable Field & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L5068}{\checkmark} & - & - \\ \hline
        Closed field & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L5311}{\checkmark} & - & - \\ \hline
        Algebra & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L2681}{\checkmark} & - &  -\\ \hline
        Unit algebra & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L3281}{\checkmark} & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/algebra/basic.lean#L114}{\checkmark} \\ \hline
        Lalgebra & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L1710}{\checkmark} & - & - \\ \hline
        Commutative unit algebra & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L3353}{\checkmark} & - & - \\ \hline
        Commutative algebra & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L2754}{\checkmark} & - & - \\ \hline
        NumDomain & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssrnum.v#L160}{\checkmark} & - & - \\ \hline
        Normed Zmodule & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssrnum.v#L252}{\checkmark} & - & - \\ \hline
        Num field & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssrnum.v#L500}{\checkmark} & - & - \\ \hline
        Real domain & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssrnum.v#L706}{\checkmark} & - & - \\ \hline
        Real field & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssrnum.v#L860}{\checkmark} & - & - \\ \hline
        Real closed field & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssrnum.v#L1067}{\checkmark} & - & - \\ \hline
        Vector space & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/vector.v#L110}{\checkmark} & - & - \\ \hline
        Zmodule Quotients type & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ring_quotient.v#L99}{\checkmark} & - & - \\ \hline
        Ring Quotient type & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ring_quotient.v#L204}{\checkmark} & - & - \\ \hline
        Unit rint quotient type & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ring_quotient.v#L313}{\checkmark} & - & - \\ \hline
        Additive group & - &  \href{https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/finalg.v#L155}{\checkmark} & - & - \\ \hline
        characteristic zero & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/char_zero.lean#L38}{\checkmark} \\ \hline
        Domain & - & - & - &  \href{https://github.com/leanprover-community/mathlib/blob/c25bd03efeb4f89dfd92e1a598a5ae86c61a26d3/src/algebra/ring/basic.lean#L999}{\checkmark} \\ \hline
        Chain Complex & - & - & - &  \href{}{\checkmark} \\ \hline
	Kleene Algebra & \href{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L552}{\bluecheck} & - & - &  - \\ \hline
	HeytingCommutativeRing & \href{https://github.com/agda/agda-stdlib/blob/53433ec465de63d77a38e3e4f5d9d486c69544f2/src/Algebra/Apartness/Structures.agda#L29}{\checkmark} & - & - &  - \\ \hline
	HeytingField & \href{https://github.com/agda/agda-stdlib/blob/53433ec465de63d77a38e3e4f5d9d486c69544f2/src/Algebra/Apartness/Structures.Agda#L46}{\checkmark} & - & - &  - \\ \hline
\end{longtable}