Insertion sort (ACL2)
From LiteratePrograms
- Other implementations: ACL2 | C | C, simple | Eiffel | Erlang | Forth | Haskell | Io | Java | Lisp | OCaml | Python | Python, arrays | Ruby | Scala, list | Smalltalk | Standard ML | Visual Basic .NET
This article describes an implementation of insertion sort in ACL2, along with the theorems necessary to enable ACL2 to verify its correctness. The overall structure is:
<<insertion-sort.lisp>>= (in-package "ACL2") insertion sort functions correctness property functions proof of correctness
Insertion sort functions
Since ACL2 is a Lisp variant with very limited array support, it's easiest to write a list-based implementation of insertion sort. We separate it into two methods. The first, insert-sorted, takes an atom and inserts it into a sorted list in its correct sorted position:
<<insertion sort functions>>= (defun insert-sorted (a lst) (if (or (endp lst) (<= a (car lst))) (cons a lst) (cons (car lst) (insert-sorted a (cdr lst)))))
In English, the function says:
- If the list is empty, or the first element is no smaller than a, just prepend a to the list.
- Otherwise, the result is the first element of the list followed by a inserted into the remainder of the list.
ACL2 has no difficulty proving that the function terminates, since the list becomes shorter in each recursive call and we do not recurse of the list of length zero.
Next, we write insertion-sort, which simply inserts the first element of the list into the insertion-sort of the remainder of the list:
<<insertion sort functions>>= (defun insertion-sort (lst) (if (endp lst) lst (insert-sorted (car lst) (insertion-sort (cdr lst)))))
If the list is empty, we just return it. Again, termination is trivial. In the interactive shell we can try sorting some lists to see that it seems to work:
ACL2 !>(insertion-sort '(4 2 1 3)) (1 2 3 4) ACL2 !>(insertion-sort '(9 2 5 0 1 4 8 3 7)) (0 1 2 3 4 5 7 8 9) ACL2 !>(insertion-sort nil) NIL
Correctness property functions
The most obvious property that a sorting function must have is that its result must be in sorted order. We define a function that enables easy testing of this:
<<correctness property functions>>= (defun is-ordered (lst) (or (endp lst) (endp (cdr lst)) (and (<= (car lst) (car (cdr lst))) (is-ordered (cdr lst)))))
In the base case, lists of length zero or one are ordered; otherwise, we use recursion to step through the list, comparing each adjacent pair of elements.
Another more subtle, but equally important property is that the output of a sort must be a rearrangement (permutation) of its input. Otherwise, a function that always produces the empty list would be a correct sort! To test whether one list is a permutation of another, we first need an auxilary function to delete the first occurence of a given value from a list, if it is present:
<<correctness property functions>>= (defun delete-element (a lst) (if (endp lst) lst (if (equal a (car lst)) (cdr lst) (cons (car lst) (delete-element a (cdr lst))))))
We can now define is-permutation by stating that a list is a permutation of another if either both are empty, or if the first element of the first list is in both lists (according to member), and deleting it from both lists leaves two lists that are permutations of one another:
<<correctness property functions>>= (defun is-permutation (left right) (or (and (endp left) (endp right)) (and (not (endp left)) (member (car left) right) (is-permutation (cdr left) (delete-element (car left) right)))))
Trying examples show that both desired properties seem to hold for a variety of inputs:
ACL2 !>(is-permutation (insertion-sort '(9 2 5 0 1 4 8 3 7)) '(9 2 5 0 1 4 8 3 7)) T ACL2 !>(is-ordered (insertion-sort '(9 2 5 0 1 4 8 3 7))) T ACL2 !>(is-permutation (insertion-sort '()) '()) T ACL2 !>(is-ordered (insertion-sort '())) T
This is great testing, but we don't yet have a formal proof of correctness.
Proof of correctness
Our main theorem is that insertion sort's output is both ordered and a permutation of its input:
<<main theorem>>= (defthm insertion-sort-correct (and (is-ordered (insertion-sort x)) (is-permutation x (insertion-sort x))))
If we simply give this to ACL2 to prove, without loading any books, it is not able to prove the result. The first simplification checkpoint looks like this:
Subgoal *1/3''
(IMPLIES (CONSP X)
(MEMBER (CAR X)
(INSERT-SORTED (CAR X)
(INSERTION-SORT (CDR X))))).
Essentially, it wants to prove that the result of insert-sorted has the supplied element as a member. We state this as a lemma:
<<insert-sorted-has-input-as-member>>= (defthm insert-sorted-has-input-as-member (member a (insert-sorted a x)))
ACL2 proves this successfully using induction. When we attempt the main theorem again, it proves Subgoal *1/3'' and continues to a new simplification checkpoint:
Subgoal *1/2.1
(IMPLIES (AND (CONSP X)
(IS-ORDERED (INSERTION-SORT (CDR X)))
(IS-PERMUTATION (CDR X)
(INSERTION-SORT (CDR X))))
(IS-ORDERED (INSERT-SORTED (CAR X)
(INSERTION-SORT (CDR X))))).
The last hypothesis is irrelevant; what we need to show here is the other fundamental defining property of insert-sorted, that if its input list is ordered, its output list will be ordered too:
<<insert-sorted-preserves-ordered>>= (defthm insert-sorted-preserves-ordered (implies (is-ordered x) (is-ordered (insert-sorted a x))))
ACL2 proves this successfully. Returning to the main theorem, we now get stuck at this simplification checkpoint:
Subgoal *1/2''
(IMPLIES (AND (CONSP X)
(IS-ORDERED (INSERTION-SORT (CDR X)))
(IS-PERMUTATION (CDR X)
(INSERTION-SORT (CDR X))))
(IS-PERMUTATION X
(INSERT-SORTED (CAR X)
(INSERTION-SORT (CDR X))))).
This checkpoint suggests a lemma relating insert-sorted to is-permutation. It's helpful to note that insert-sorted always inserts a somewhere, even if its input list is not sorted. As such, if its second argument is a permutation of some list x, then its result is a permutation of (cons a x), the list x with a prepended. The theorem looks like this:
(defthm insert-sorted-is-permutation-of-cons
(implies (is-permutation x y)
(is-permutation (cons a x)
(insert-sorted a y))))
This theorem is a bit too difficult for ACL2. It reaches a checkpoint that looks like this:
Subgoal *1/4''
(IMPLIES (AND (CONSP X)
(NOT (MEMBER (CAR X)
(DELETE-ELEMENT A (INSERT-SORTED A Y))))
(MEMBER (CAR X) Y))
(NOT (IS-PERMUTATION (CDR X)
(DELETE-ELEMENT (CAR X) Y)))).
The form (DELETE-ELEMENT A (INSERT-SORTED A Y)) is suggestive; this clearly should reduce to Y, and if it did, it would contradict the last hypothesis. Any theorem with a false hypothesis is true. So we add a theorem:
<<delete-element-undoes-insert-sorted>>= (defthm delete-element-undoes-insert-sorted (equal (delete-element a (insert-sorted a x)) x))
ACL2 proves this. We then return to our main theorem, which ACL2 proves successfully, without even requiring a proof of insert-sorted-is-permutation-of-cons:
That completes the proof of *1. Q.E.D. Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INSERTION-SORT-CORRECT
We put together all our lemmas in the correct order and our job is done:
<<proof of correctness>>= insert-sorted-has-input-as-member insert-sorted-preserves-ordered delete-element-undoes-insert-sorted main theorem
| Download code |