TYPES OF ALGEBRAIC STRUCTURES IN PROOF ASSISTANT SYSTEMS

Abstract

Building a standard library of mathematical knowledge for a proof system is a complex task that relies on human effort. By conducting a survey on the standard library of four proof systems (Agda, Idris, Lean, and Coq), we define the scope for our research to study types of algebraic structures in proof systems. From the result of the survey, we establish our focus to contribute to the Agda standard library. Universal algebra studies structures by abstracting out the specific definitions and properties of algebraic structures. Providing an extensive and well-defined library of algebraic structures and theorems in Agda will enable researchers to explore new domains and build upon existing definitions (and theorems). We explore capturing a select subset of algebraic structures such as quasigroups, loops, semigroups, rings, and Kleene algebra with some of their constructs. Constructs like homomorphism, isomorphism, and direct products are given to us by universal algebra which provides a way to relate different structures in a systematic and rigorous way. Homomorphisms allow us to understand how different structures are related. During our exploration of capturing these structures in Agda, we encountered several issues. We categorized these issues into five classes and analyzed each problem to provide plausible solutions. As part of this research, we define more than 20 algebraic structures and add more than 40 proofs to the Agda standard library