LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS

Abstract

We present a fully mechanized proof of correctness and stability of the insertion sort algorithm, while handling stability not as an afterthought in its formal specification, but rather as a property removing any unspecified behaviour from the algorithm, by explaining what happens to elements that are considered equivalent. We therefore express the combined notion of being sorted along with stability as a single inductive predicate, allowing us to share uncovered information in proofs, resulting in a more elegant approach to showing correctness and stability of sorting algorithms. Naturally, there are also cases when we can indeed forget about stability. We prove, that under the assumption that the sequence to be sorted contains unique elements only, sorting and stable sorting are equivalent notions. Formalization is conducted in the Lean theorem prover.