Case Study: Correct Sorting

Understand the computation and its specification separately.

18.1 What do we want to prove?

A sorting function must do more than produce ascending output. It must preserve every element: nothing lost, nothing added, only reordered.

Sorting specification = the output is sorted ∧ the output is a permutation of the input

Tauto lets you separate the function sort from the theorems stating its properties. This is the insertion sort from Chapter 6: insert puts an element in the correct position of an already sorted list.

18.2 The final theorem

The proof is in examples/sort/proof/sort.taut in the repository. The function sorted returns a proposition saying that each element is at most the next one. Perm is an inductive proposition expressing permutation.

inductive Perm(A: Type): (List(A)) -> (List(A)) -> Prop {
  perm_nil(): Perm(A, Nil, Nil)
  perm_skip<x: A, l: List(A), m: List(A)>(h: Perm(A, l, m)): Perm(A, Cons(x, l), Cons(x, m))
  perm_swap<x: A, y: A, l: List(A)>(): Perm(A, Cons(x, Cons(y, l)), Cons(y, Cons(x, l)))
  perm_trans<l: List(A), m: List(A), n: List(A)>(a: Perm(A, l, m), b: Perm(A, m, n)): Perm(A, l, n)
}

Prove the two properties separately:

theorem sort_perm<A>(l: List(A)): Perm(A, l, sort(l)) where Ord(A) { ... }
theorem sort_sorted<A>(l: List(A)): sorted(sort(l)) where Ord(A) { ... }

Then combine them with AndIntro to obtain sort_correct:

theorem sort_correct<A>(l: List(A)): sorted(sort(l)) ∧ Perm(A, l, sort(l)) where Ord(A) {
  AndIntro(sort_sorted(l), sort_perm(l))
}

Check the proof:

tauto check examples/sort/proof/sort.taut

ok      sort_perm
ok      insert_after
ok      insert_sorted
ok      sort_sorted
ok      sort_correct

(The output also includes other lemmas.)

Simply declaring a theorem named sort_correct provides no assurance. The lemmas must actually be checked, and their assumptions must be traceable. This example uses no axioms.

18.3 Understand where the proof applies

This sorting theorem applies to types satisfying Ord(A). The proof uses only the laws of Ord as properties of A. A supposed “ordering” that violates those laws invalidates the assumptions. The more general a theorem is, the more carefully you should understand its prerequisites.

Exercise 18.1: A function produces ascending output but drops an element. Which part of the sorting specification does it violate?