# (Draft) The correctness of insertion sort

## Introduction

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.

## The data structures and algorithms of interest

Definition. Let A be a set. Then a list of elements of A is defined by the following constructors:

• the empty list

• the list with x prepended to xs where x is an element of A and xs is a list of elements of A.

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:

• for the empty list, the singleton list with x

• for the list with x' prepended to xs',

• the list with x prepended to xs, if x is less than or equal to x',

• the list with x' prepended to the list with x inserted into xs' otherwise.

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:

• for the empty list, the empty list

• for the list with x prepended to xs', the list with x inserted into insertion sort applied to xs'.

## Ordered lists

### What is an ordered list?

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:

• for the empty list, it is always true

• for the list with x' prepended to xs', x is less than or equal to x' and xs' is ordered even if x' is prepended.

Definition. Let xs be a list of natural numbers. Then we say that xs is ordered which is defined depending on xs as follows:

• for the empty list, it is always true

• for the list with x prepended to xs', xs' is ordered even if x is prepended.

### What happens when a new element is inserted in an ordered list?

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:

• for the empty list, the list with x1 prepended to the singleton list with x2 is ordered:

• first, by le_x2 we have that x1 is less than or equal to x2.

• Second, the singleton list with x2 is ordered: this is trivial.

• for the list with x prepended to xs', the proof is split in two cases:

• When x2 is less than or equal to x ( h ): the list with x2 prepended to the list with x prepended to xs' is ordered even if x1 is prepended:

• first, by le_x2 we have that x1 is less than or equal to x2.

• Second, the list with x prepended to xs' is ordered even if x2 is prepended:

• first, by h we have that x2 is less than or equal to x.

• Second, xs' is ordered even if x is prepended: by le_xs we have that x1 is less than or equal to x and xs' is ordered even if x is prepended..

• Otherwise ( h ): by le_xs we have that xs is ordered even if x1 is prepended. This allows us to assume

• pp: x1 is less than or equal to x, and

• pq: xs' is ordered even if x is prepended.

Now, the list with x prepended to the list with x2 inserted into xs' is ordered even if x1 is prepended:

• first, by pp we have that x1 is less than or equal to x.

• Second, the list with x2 inserted into xs' is ordered even if x is prepended: this can be proved by the lemma about prepending after inserting, since

• x is less than or equal to x2: by h we have that it is not the case that x2 is less than or equal to x. By antisymmetry, x is less than or equal to x2, and

• by pq we have that xs' is ordered even if x 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:

• for the empty list, the list with x inserted into the empty list is ordered: this is trivial

• for the list with x' prepended to xs', the list with x inserted into the list with x' prepended to xs' is ordered: the proof is split in two cases:

• When x is less than or equal to x' ( h ): the list with x prepended to the list with x' prepended to xs' is ordered:

• first, by h we have that x is less than or equal to x'.

• Second, by oxs we have that xs' is ordered even if x' is prepended.

• Otherwise ( h ): the list with x' prepended to the list with x inserted into xs' is ordered: this can be proved by the lemma about prepending after inserting, since

• by h we have that it is not the case that x is less than or equal to x'. By antisymmetry, x' is less than or equal to x, and

• by oxs we have that xs' is ordered even if x' is prepended.

## Definitions and lemmas relating to permutations

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:

• for the empty list, zero

• for the list with x' prepended to xs',

• the successor of the number of occurences of x in xs', if x is equal to x',

• the number of occurences of x in xs' otherwise.

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:

• for the empty list, the list with x inserted into the empty list is a permutation of the list with x prepended to the empty list. We omit the proof

• for the list with x' prepended to xs', the list with x inserted into the list with x' prepended to xs' is a permutation of the list with x prepended to the list with x' prepended to xs'. We omit the proof.

## The correctness of insertion sort

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.

### Insertion sort yields ordered lists

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:

• when the proposition that insertion sort applied to h is ordered is the empty list: use xs

• when the proposition that insertion sort applied to h is ordered is the list with insertion sort applied to the empty list is ordered: this is trivial prepended to x: use xs'.

### Insertion sort permutes lists

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':

• the list with x prepended to insertion sort applied to xs' is a permutation of the list with x prepended to xs': by h we have that insertion sort applied to xs' is a permutation of xs'. The lists are still permutations when x is prepended

• insertion sort applied to the list with x prepended to xs' is a permutation of the list with x prepended to insertion sort applied to xs': inserting x yields a permutation of prepending x.

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:

• when the proposition that insertion sort applied to xs is a permutation of xs is the empty list: use xs

• when the proposition that insertion sort applied to xs is a permutation of xs is the list with the element constructed as follows:

use the theorem that the empty list is a permutation of itself

prepended to x: use xs'.

### Putting it all together

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.

• first, insertion sort applied to xs is a permutation of xs: use the theorem that insertion sort permutes lists, applied to xs.

• Second, insertion sort applied to xs is ordered: use the theorem that insertion sort yields ordered lists, applied to xs..

This proves that insertion sort applied to xs is a sorted version of xs.

## Conclusions

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:

+
The text can with a relatively small effort be translated into several natural languages.
+
The informal text can be guarranteed to correspond closely to the formal proof. The text will use a consistent terminology. Changes to the formal proof are carried over to the informal text automatically.
The text becomes more repetitive and boring to read.
Grammatical limitations of the natural language tool can prevent you from using the most natural way of expressing things, leading to text that more unwiedly than necessary.

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.

## References

hallgren:alfa-homepage T. Hallgren.