Recently a reader who must not be named told me that they only read the Kublai text boxes on my site, so thus Kublai will write everything for today’s post.

Kublai: Oh, hi. So today we’re gonna prove the correctness of insertion sort in Lean v4.27.0-rc1. Only problem is I don’t know Lean.

OK, never mind, I’ll write–

Kublai: Wait hold up, I do know a tiny bit of Lean. I know how to use the grind tactic!

First, let’s write a simple insertion sort:

variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] [BEq α] [LawfulBEq α] (xs : List α)

@[grind]
def insert (a : α)
  | [] => [a]
  | x :: xs =>
    if a ≤ x then
      a :: x :: xs
    else
      x :: insert a xs

@[grind]
def insertionSort : List α → List α
  | [] => []
  | x :: xs => insert x (insertionSort xs)

Note that the definitions are tagged with @[grind] so that grind will unfold them later.

Let’s define what it means for a list to be sorted:

@[grind]
def Sorted : List α → Prop
  | [] | [_] => True
  | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs)

Now we can prove that insert behaves nicely:

theorem insertCorrect x : (Sorted xs → Sorted (insert x xs)) ∧ (x :: xs).Perm (insert x xs) := by
  induction xs with
  | nil => grind
  | cons _ t => cases t <;> grind

And finally, we can show insertionSort is correct by giving grind the theorem we just proved (we can’t call it a lemma because that would require importing mathlib):

theorem insertionSortCorrect : Sorted (insertionSort xs) ∧ xs.Perm (insertionSort xs) := by
  induction xs with
  | nil => grind
  | cons h t => grind [insertCorrect (insertionSort t) h]

Phew, I did it! Turns out grind is all you need (and maybe a bit of induction and cases too).

Oh and for our Sorted predicate, the more common way to define it is using an inductive predicate but those are scary 🐪😱:

inductive Sorted : List α → Prop where
  | nil : Sorted []
  | single x : Sorted [x]
  | cons_cons x x' xs : x ≤ x' → Sorted (x' :: xs) → Sorted (x :: x' :: xs)

Thanks, Kublai! If you liked this post, you might like my grind-heavy ICan’tBelieveICanProveItCanSort! post. Also, check out these alternate insertion sort proofs using aesop or doing everything manually.