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:

- 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.

- the list with

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'*.

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.

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

this can be proved by the lemma about prepending after inserting, since

- use
le, and_x2

- 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*we have that**_**x2*x1*is less than or equal to*x2*. - Second, the singleton list with
*x2*is ordered: this is trivial.

- first, by
- 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*we have that**_**x2*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*we have that**_**xs*x1*is less than or equal to*x*and*xs'*is ordered even if*x*is prepended..

- first, by

- first, by
- Otherwise (
*h*): by*le*we have that**_**xs*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. - When

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.

- first, by
- 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.

- by

- When

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.

- the successor of the number of occurences of

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:

usep. The lists are still permutations whenxis 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,

zsis a permutation ofxs.

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:

insertingxyields a permutation of prependingx.

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.

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:

- 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'*.

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:

useh. 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'*.

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*.

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.

- hallgren:alfa-homepage T. Hallgren.
- Home Page of the Proof Editor Alfa.
`www.cse.chalmers.se/~hallgren/Alfa/`, 1996-2004.- hallgren-ranta:lpar2000 T. Hallgren and A. Ranta.
- An extensible proof text editor.
- In
*Logic for Programming and Automated Reasoning (LPAR'2000)*, number 1955 in LNCS/LNAI, pages 70--84. Springer Verlag, November 2000.