Verification of Integers and Sorting Algorithms in Coq

A short project using the Coq proof assistant to explore multiple different definitions of the integers and various properties of them (such as the sign of an integer, or an ordering on the integers), and defining multiple different definitions of sorting algorithms and proving various properties of them (such as proving that insertion sort is a sorting algorithm). Both of these are from scratch, i.e. without relying on the vast majority of the Coq standard library.

Key outcomes include exploring different higher inductive definitions of the integers and successfully proving that they coincide (i.e. are ring isomorphic), and exploring different definitions of sorting algorithms and proving that they coincide (e.g. inductive definitions are equivalent to recursive definitions).

Notable outcomes include machine-verifiable proofs of the triangle inequality and verification of insertion sort. Project scope was reduced due to falling ill with COVID-19 during December/January.