In this post, we will formalize one of the most well-known results of algorithm analysis: no comparison sort can run in asymptotically less than n * log n steps, where n is the size of its input. Before starting, I should point out that this is the first post in this blog to use the Ssreflect and the Mathematical Components (MathComp) libraries. Ssreflect is an amazing Coq extension that brings several improvements, including a nicer set of base tactics. Both libraries cover a wide range of theories, including fairly sophisticated Mathematics - as a matter of fact, they are featured in the Coq formalization of the Feit-Thompson theorem, known for its extremely complex and detailed proof. As we will see, having good library support can help a lot when doing mechanized proofs, even for such simple results as this one. Two things that come in handy here, in particular, are the theories of permutations and sets over finite types that are available in MathComp. Indeed, the MathComp definitions enable many useful, higher-level reasoning principles that don't come for free in Coq, such as extensional and decidable equality. Furthermore, many lemmas on the library require a fair amount of machinery to be developed on their own - for example, showing that there are exactly n! permutations over a set of n elements. Previous versions of this post (which you can still find on the repository) tried to avoid external libraries, but were much longer and more complicated, prompting me to bite the bullet and port everything to Ssreflect/MathComp.

Basics

The informal proof of this result is fairly simple:

• If a comparison sort is correct, then it must be capable of shuffling an input vector of size n according to any of the n! permutations of its elements.
• On the other hand, any such algorithm can recognize at most 2 ^ k distinct permutations, where k is the maximum number of comparisons performed. Hence, n! <= 2 ^ k or, equivalently, log2 n! <= k.
• To conclude, Stirling's approximation tells us that n * log2 n = O(log2 n!), which yields our result.

We'll begin our formalization by defining a convenient datatype for representing the execution of a comparison sort. For our purposes, a comparison sort can be seen as a binary tree: internal nodes indicate when a comparison between two elements occurs, with the right and left branches telling how to proceed depending on its result. The leaves of the tree mark when the algorithm ends and yields back a result. Thus, we obtain the following type:

Let's analyze this declaration in detail. The n parameter will be used later to track the length of the array that we are sorting. 'I_n is the type of natural numbers bounded by n, whereas 'S_n represents permutations of elements of that type. The idea is that, when running our algorithm, the i and j arguments of Compare tell which elements of our array to compare. The permutation in Done specifies how to rearrange the elements of the input array to produce an answer. We can formalize the previous description in the following function:

execute is a polymorphic function that works for any type T with a comparison operator c. Given an algorithm a and an input array xs of length n, the function compares the elements of a, following the appropriate branches along the way, until finding out how to rearrange a's elements. With execute, we can define what it means for a sorting algorithm to be correct, by relating its results to the MathComp sort function:

Finally, to translate the above informal argument, we will need some more definitions. Let's first write a function for computing how many comparisons an algorithm performs in the worst case:

And here's a function for computing the set of permutations that an algorithm can perform (notice the use of the set library of MathComp; here, :|: denotes set union):

(Strictly speaking, both comparisons and perms give upper bounds on the values they should compute, but this does not affect us in any crucial way.)

Show me the proofs

To show that a correct algorithm must be able of performing arbitrary permutations, notice that, if xs is a sorted array with distinct elements, then permuting its elements is an injective operation. That is, different permutations produce different arrays.

Bounding the number of permutations performed by an algorithm is simple, and amounts to invoking basic lemmas about arithmetic and sets.

Doing the last step is a bit trickier, as we don't have a proof of Stirling's approximation we can use. Instead, we take a more direct route, showing the following lemma by induction on n (trunc_log, as its name implies, is the truncated logarithm):

In order to get our proof to go through, we must strengthen our induction hypothesis a little bit:

We can then proceed with a straightforward (although not completlely trivial) inductive argument.

Our main result follows almost immediately from these three intermediate lemmas:

Summary

We've seen how to formalize a result of algorithm analysis in an abstract setting: although it is fair to say that our model of a comparison sort is detailed enough for our purposes, we haven't connected it yet to a more traditional computation model, something I plan to discuss on a future post. Aside from that, we've seen how a rich set of theories, such as the ones in MathComp, allow us to express higher-level concepts in our definitions and proofs, leading to much shorter formalizations.