conclusion.tex

\chapter{Conclusion And Future Work}
The primary of this work was to study types of algebraic structures in proof
assistant systems. To define the scope of the work, we do a survey on the
coverage of types of algebraic structures in four proof assistant systems which
are Agda, Idris, Coq, and Lean. The thesis shows how to define a structure with
some of its constructs and properties in Agda. We divided this into three main
chapters based on the closeness of structures that is quasigroup and loop,
semigroup and ring, and Kleene algebra. We then analyzed five problems that arise
when defining types of algebraic structures in proof systems.

In section ~\ref{contribution}, we summarize the contributions of this work and
how it refers to the research outline described in Chapter 1. Section
~\ref{future} discuss some extensions or future work of this work. 

\section{Summary Of Contributions}
\label{contribution}
Universal algebra is a well-studied and evolving branch of mathematics. Proof
systems are useful in automated reasoning and becoming popular in research and
applications more than ever. With an introduction to universal algebra in
Chapter 1 and Agda in Chapter 2, and Chapter 3 provide an overview of the
quantitative use of algebraic structures in proof assistant systems. We create a
clickable table that takes to the definition of structures in the standard
libraries of the systems studied (Agda, Idris, Lean, and Coq).

This leads to defining the scope of contribution to the Agda standard library.
Chapter 5 is dedicated to studying the structures quasigroup, loop, and their
variations. Chapter 6 provides an overview of semigroup and ring structures with
definitions of their constructs and prove their properties. Chapter 7 is
dedicated to the study of Kleene algebra and its properties in Agda. Along with
these structures, we define structures unital magma, invertible magma,
invertible unital magma, idempotent magma, alternate magma, flexible magma,
semimedial magma, medial magma, with their constructs.

Our approach to defining these structures led us to encounter and analyze some
problems such as ambiguity in naming, equivalent and identical structures.
Chapter 8 discussed how these problems become more evident in proof systems that
might be ignored in classical the 'pen-and-paper' technique.

\section{Future Work}
\label{future}
Our work can be extended in different ways. The direct products defined in this
thesis do not clearly differentiate between direct products, products, and
co-products of algebraic structures. There is currently a discussion on the Agda
standard library to overcome this issue, but the changes are yet to come. The
current solution adapted in the Agda standard library to remove the redundant
field will only remove the equivalence. However, there can be other redundant
fields. For example, in commutative monoid, right identity can be obtained from
left identity and commutativity. These problems are yet to be addressed. The
current work will rely on human efforts in building strong libraries in the
field of abstract algebra. A more robust and reliable generative library will be
helpful to reduce human efforts.