The goal of this research project submitted as part of requirements for my MS, was to use Agda (a computerized proof assistant) to constructively build a set of proofs. These proofs are reasoned about intuitionistically, starting from base constructs all the way to various algebraic properties required for a certain abstract mathematical structure referred to as a Ring.
This project was supervised by Dr Thorsten Altenkirch, and I'm forever grateful for all his time, expertise and most importantly, empathy towards my journey with Type Theory.
The final solution involves an object of type "Ring" which satisfies all algebraic commutative ring axioms.
-
Define, construct and prove algebraic properties of natural numbers using the Peano axioms.
Ex: Operations over naturals, properties over natural addition, properties over natural multiplication.
-
Use naturals constructively to define, construct, and prove algebraic properties of integers.
Ex: Properties over integral addition, properties over integral multiplication, distributive laws.
-
Use our proofs alongside tools for predicate logic, to culminate our final proof for the "type" Ring.
Ex: Final proof.
-
constructs\: Basic types and type variables. -
natural_numbers\: Definition, operations and properties over natural numbers. -
integers_MAIN\: Definition, operations and properties over Integers. Main folder of interest. -
predicate_logic\: Tools for predicates.