In this document, we prove the correctness of insertion sort, i.e., when insertion sort is applied to a list of natural numbers, the result is an ordered permutation of the original list.
We explicitly define lists, the sorting algorithm, what it means for a list to be ordered, what a permutation is and various lemmas relating to these concepts.
We also rely on some definitions not included in this document: propositional logic, predicate logic and natural numbers with the usual equality and ordering.
An unusual aspect of this document is that all definitions, lemmas and proofs have been constructed formally in a proof assistant [hallgren:alfa-homepage]. The proof has in every detail been machine checked (even the parts not included here), and is thus hopefully free from logical flaws. The formal constructions, together with grammatical annotations, have then been translated automatically [hallgren-ranta:lpar2000] into English text to form the bulk of this document.
Definition. Let A be a set. Then a list of elements of A is defined by the following constructors:
Definition. Let A be a set. Let x be an element of A. Then the singleton list with x is a list of elements of A defined as the list with x prepended to the empty list.
Definition. Let x be a natural number. Let xs be a list of natural numbers. Then the list with x inserted into xs is a list of natural numbers defined depending on xs as follows:
Definition. Let xs be a list of natural numbers. Then insertion sort applied to xs is a list of natural numbers defined depending on xs as follows:
Definition. Let x be a natural number. Let xs be a list of natural numbers. Then we say that xs is ordered even if x is prepended which is defined depending on xs as follows:
Definition. Let xs be a list of natural numbers. Then we say that xs is ordered which is defined depending on xs as follows:
Rule of inference. Let x1 and x2 be natural numbers. Let xs be a list of natural numbers. Let le_x2 be a proof that x1 is less than or equal to x2. Let le_xs be a proof that the list with x1 prepended to xs is ordered. Then we may reason as follows:
this can be proved by the lemma about prepending after inserting, since
- use le_x2, and
- use le_xs.
this proves that the list with x1 prepended to the list with x2 inserted into xs is ordered.
Justification: depending on xs as follows:
Now, the list with x prepended to the list with x2 inserted into xs' is ordered even if x1 is prepended:
So, the list with x prepended to the list with x2 inserted into xs' is ordered even if x1 is prepended.
So, the list with x1 prepended to the list with x2 inserted into the list with x prepended to xs' is ordered.
Rule of inference. Let x be a natural number. Let xs be a list of natural numbers. Let oxs be a proof that xs is ordered. Then we may reason as follows:
oxs. We can now use the theorem that the order is preserved when inserting elements in an ordered list.
this proves that the list with x inserted into xs is ordered.
Justification: depending on xs as follows:
Definition. Let x be a natural number. Let xs be a list of natural numbers. Then the number of occurences of x in xs is a natural number defined depending on xs as follows:
Definition. Let xs and ys be lists of natural numbers. Then we say that ys is a permutation of xs if for all natural numbers n, the number of occurences of n in xs is equal to the number of occurences of n in ys.
The theorem that the empty list is a permutation of itself. The empty list is a permutation of the empty list.
Proof. The empty list is a permutation of the empty list. We omit the proof.
Rule of inference. Let x be a natural number. Let ys and zs be lists of natural numbers. Let p be a proof that zs is a permutation of ys. Then we may reason as follows:
use p. The lists are still permutations when x is prepended.
this proves that the list with x prepended to zs is a permutation of the list with x prepended to ys.
Justification: the list with x prepended to zs is a permutation of the list with x prepended to ys. We omit the proof.
Rule of inference. Let xs and ys and zs be lists of natural numbers. Let xy be a proof that ys is a permutation of xs. Let yz be a proof that zs is a permutation of ys. Then we may reason as follows:
- use xy
- use yz.
By transitivity, zs is a permutation of xs.
this proves that zs is a permutation of xs.
Justification: zs is a permutation of xs. We omit the proof.
The theorem that swapping the first two elements of a list yields a permutation. Let x1 and x2 be natural numbers. Let xs be a list of natural numbers. Then the list with x2 prepended to the list with x1 prepended to xs is a permutation of the list with x1 prepended to the list with x2 prepended to xs.
Proof. The list with x2 prepended to the list with x1 prepended to xs is a permutation of the list with x1 prepended to the list with x2 prepended to xs. We omit the proof.
Rule of inference. Let x be a natural number. Let xs be a list of natural numbers. Then we may reason as follows:
inserting x yields a permutation of prepending x.
this proves that the list with x inserted into xs is a permutation of the list with x prepended to xs.
Justification: depending on xs as follows:
Definition. Let xs and ys be lists of natural numbers. Then we say that ys is a sorted version of xs if ys is a permutation of xs and ys is ordered.
The theorem that insertion sort yields ordered lists. For all lists of natural numbers xs, insertion sort applied to xs is ordered.
Proof. Let xs be an arbitrary list of natural numbers. Insertion sort applied to xs is ordered: we split the proof in two cases:
Rule of inference. Let x be a natural number. Let xs' be a list of natural numbers. Let h be a proof that insertion sort applied to xs' is a permutation of xs'. Then we may reason as follows:
use h. We can now use the lemma that sorting before prepending yields a permutation.
this proves that insertion sort applied to the list with x prepended to xs' is a permutation of the list with x prepended to xs'.
Justification: insertion sort applied to the list with x prepended to xs' is a permutation of the list with x prepended to xs':
By transitivity, insertion sort applied to the list with x prepended to xs' is a permutation of the list with x prepended to xs'.
The theorem that insertion sort permutes lists. For all lists of natural numbers xs, insertion sort applied to xs is a permutation of xs.
Proof. Let xs be an arbitrary list of natural numbers. We split the proof in two cases:
use the theorem that the empty list is a permutation of itself
prepended to x: use xs'.
The correctness of insertion sort. Let xs be a list of natural numbers. Then insertion sort applied to xs is a sorted version of xs.
Proof.
This proves that insertion sort applied to xs is a sorted version of xs.
In this paper we have deliberately refrained from using any formal notation, to explore the contrast with the formal notation the user of a proof assisant usually has to cope with. It should thus be possible to read the paper without first learning our particular formal notation. However, it is clear why formal mathematical notation was invented in the first place: the verbosity of the text clearly makes it harder to read (since every little detail requires a lot of text), so, as a not so surprising conclusion, we can say the best readability is probably obtained by a suitably balanced mixture of formal notation and natural language text.
Documents about formal proofs are typically produced by complementing manually authored text with figures containing proof fragments developed in a formal system. Here, the bulk of the text has instead been constructed automatically from the formal proof. There are of course both advantages and disadvantages with text generated automatically in this way:
We have chosen to work with lists of natural numbers and a specific ordering, but the proof could fairly easily be generalised to arbitrary lists and orderings.