1. Part 1: merge sort, and a proof that it sorts🔗

The code on this page is MergeSort/Simple.lean in the repository, shown here piece by piece and checked against the file when the page is built. Hover over a name to see its type, and over a tactic to see the proof state at that point.

1.1. The specification🔗

A list is sorted when every element is ≤ every later element. Lean's List.Pairwise says exactly that, so the specification is one line:

/-- The specification: every element is `≤` every later element. -/
def Sorted {α : Type} [LE α] (l : List α) : Prop := l.Pairwise (· ≤ ·)

The other half of the specification is that the output must be a rearrangement of the input. List.Perm from the standard library is that relation, so we do not have to define anything.

The order comes from an LE instance on the element type, which is how ≤ is written in Lean. To run the sort we also need to decide ≤; that is the DecidableLE instance the functions below ask for. Proofs about ≤ need nothing more than the two facts stated as hypotheses later.

1.2. The algorithm🔗

merge walks two lists and takes the smaller head at each step. Lean checks that it terminates by itself, because each recursive call is on a structurally smaller argument.

/-- Merge two sorted lists into one sorted list. -/
def merge {α : Type} [LE α] [DecidableLE α] : List α → List α → List α
  | [], ys => ys
  | xs, [] => xs
  | x :: xs, y :: ys =>
    if x ≤ y then x :: merge xs (y :: ys) else y :: merge (x :: xs) ys

mergeSort splits the list in half, sorts both halves and merges. The recursion is on take and drop, which are not structurally smaller, so we say what decreases (l.length) and give a one-line proof that it does.

/-- Split in half, sort both halves, merge. -/
def mergeSort {α : Type} [LE α] [DecidableLE α] (l : List α) : List α :=
  if h : l.length ≤ 1 then l
  else
    let half := l.length / 2
    merge (mergeSort (l.take half)) (mergeSort (l.drop half))
termination_by l.length
decreasing_by all_goals simpα:Typel:List αh:¬l.length ≤ 1half:Nat := l.length / 2⊢ l.length - l.length / 2 < l.length; omegaAll goals completed! 🐙

That is the program. It runs as it stands:

[1, 1, 3, 5, 7, 9]#eval mergeSort [5, 3, 9, 1, 1, 7]

[1, 1, 3, 5, 7, 9]

1.3. The proof: permutation🔗

Because merge and mergeSort are recursive definitions, Lean derives an induction principle for each one (merge.induct, mergeSort.induct) whose cases are exactly the cases of the definition. Proofs follow the shape of the code.

The output of merge is a permutation of the two inputs appended:

theorem merge_perm {α : Type} [LE α] [DecidableLE α] (xs ys : List α) :
    (merge xs ys).Perm (xs ++ ys) := byα:Typeinst✝¹:LE αinst✝:DecidableLE αxs:List αys:List α⊢ (merge xs ys).Perm (xs ++ ys)
  induction xs, ys using merge.induct with
  | case1 ys =>case1α:Typeinst✝¹:LE αinst✝:DecidableLE αys:List α⊢ (merge [] ys).Perm ([] ++ ys) simp [merge]All goals completed! 🐙
  | case2 xs h =>case2α:Typeinst✝¹:LE αinst✝:DecidableLE αxs:List αh:xs = [] → False⊢ (merge xs []).Perm (xs ++ []) simp [merge]All goals completed! 🐙
  | case3 x xs y ys hle ih =>case3α:Typeinst✝¹:LE αinst✝:DecidableLE αx:αxs:List αy:αys:List αhle:x ≤ yih:(merge xs (y :: ys)).Perm (xs ++ y :: ys)⊢ (merge (x :: xs) (y :: ys)).Perm (x :: xs ++ y :: ys) simpa [merge, hle] using ihAll goals completed! 🐙
  | case4 x xs y ys hle ih =>case4α:Typeinst✝¹:LE αinst✝:DecidableLE αx:αxs:List αy:αys:List αhle:¬x ≤ yih:(merge (x :: xs) ys).Perm (x :: xs ++ ys)⊢ (merge (x :: xs) (y :: ys)).Perm (x :: xs ++ y :: ys)
    simp [merge, hle]case4α:Typeinst✝¹:LE αinst✝:DecidableLE αx:αxs:List αy:αys:List αhle:¬x ≤ yih:(merge (x :: xs) ys).Perm (x :: xs ++ ys)⊢ (y :: merge (x :: xs) ys).Perm (x :: (xs ++ y :: ys))
    exact (ih.cons y).trans List.perm_middle.symmAll goals completed! 🐙

The first three cases are what simp can see on its own once it unfolds merge. In the fourth case the output starts with y, which came from the middle of xs ++ y :: ys; List.perm_middle is the library lemma for that.

The same for mergeSort, using that take and drop together give the list back:

theorem mergeSort_perm {α : Type} [LE α] [DecidableLE α] (l : List α) :
    (mergeSort l).Perm l := byα:Typeinst✝¹:LE αinst✝:DecidableLE αl:List α⊢ (mergeSort l).Perm l
  induction l using mergeSort.induct with
  | case1 l h =>case1α:Typeinst✝¹:LE αinst✝:DecidableLE αl:List αh:l.length ≤ 1⊢ (mergeSort l).Perm l simp [mergeSort, h]All goals completed! 🐙
  | case2 l h half ih1 ih2 =>case2α:Typeinst✝¹:LE αinst✝:DecidableLE αl:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:(mergeSort (List.take half l)).Perm (List.take half l)ih2:(mergeSort (List.drop half l)).Perm (List.drop half l)⊢ (mergeSort l).Perm l
    rw [mergeSort,case2α:Typeinst✝¹:LE αinst✝:DecidableLE αl:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:(mergeSort (List.take half l)).Perm (List.take half l)ih2:(mergeSort (List.drop half l)).Perm (List.drop half l)⊢ (if h : l.length ≤ 1 then l
    else
      have half := l.length / 2;
      merge (mergeSort (List.take half l)) (mergeSort (List.drop half l))).Perm
  l dif_neg hcase2α:Typeinst✝¹:LE αinst✝:DecidableLE αl:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:(mergeSort (List.take half l)).Perm (List.take half l)ih2:(mergeSort (List.drop half l)).Perm (List.drop half l)⊢ (have half := l.length / 2;
    merge (mergeSort (List.take half l)) (mergeSort (List.drop half l))).Perm
  l]case2α:Typeinst✝¹:LE αinst✝:DecidableLE αl:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:(mergeSort (List.take half l)).Perm (List.take half l)ih2:(mergeSort (List.drop half l)).Perm (List.drop half l)⊢ (have half := l.length / 2;
    merge (mergeSort (List.take half l)) (mergeSort (List.drop half l))).Perm
  l
    exact (merge_perm _ _).trans ((ih1.append ih2).trans (byα:Typeinst✝¹:LE αinst✝:DecidableLE αl:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:(mergeSort (List.take half l)).Perm (List.take half l)ih2:(mergeSort (List.drop half l)).Perm (List.drop half l)⊢ (List.take half l ++ List.drop half l).Perm l simpAll goals completed! 🐙))

1.4. The proof: sortedness🔗

A merge of two sorted lists is sorted, provided ≤ is transitive and total. These two facts are all the proof needs, and they are stated as hypotheses rather than assumed from a class, so the theorem says exactly which orders it sorts by.

One small lemma first: an element of the merge came from one of the inputs.

theorem mem_merge {α : Type} [LE α] [DecidableLE α] {a : α} {xs ys : List α} :
    a ∈ merge xs ys ↔ a ∈ xs ∨ a ∈ ys := byα:Typeinst✝¹:LE αinst✝:DecidableLE αa:αxs:List αys:List α⊢ a ∈ merge xs ys ↔ a ∈ xs ∨ a ∈ ys
  rw [(merge_perm xs ys).mem_iff,α:Typeinst✝¹:LE αinst✝:DecidableLE αa:αxs:List αys:List α⊢ a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys List.mem_appendα:Typeinst✝¹:LE αinst✝:DecidableLE αa:αxs:List αys:List α⊢ a ∈ xs ∨ a ∈ ys ↔ a ∈ xs ∨ a ∈ ys]All goals completed! 🐙

Now the merge lemma. Case 3 is where x ≤ y and x goes first: x is below everything in xs by the hypothesis, below y by the test, and below the rest of ys by transitivity through y. Case 4 is symmetric, except that y ≤ x has to come from totality, since the test only told us ¬ x ≤ y.

/-- Merging sorted lists gives a sorted list, provided `≤` is transitive and total. -/
theorem merge_sorted {α : Type} [LE α] [DecidableLE α]
    (trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
    (total : ∀ a b : α, a ≤ b ∨ b ≤ a)
    {xs ys : List α} (hx : Sorted xs) (hy : Sorted ys) :
    Sorted (merge xs ys) := byα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ axs:List αys:List αhx:Sorted xshy:Sorted ys⊢ Sorted (merge xs ys)
  induction xs, ys using merge.induct with
  | case1 ys =>case1α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ays:List αhx:Sorted []hy:Sorted ys⊢ Sorted (merge [] ys) simpa [merge]All goals completed! 🐙
  | case2 xs h =>case2α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ axs:List αh:xs = [] → Falsehx:Sorted xshy:Sorted []⊢ Sorted (merge xs []) simpa [merge]All goals completed! 🐙
  | case3 x xs y ys hle ih =>case3α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)⊢ Sorted (merge (x :: xs) (y :: ys))
    simp only [merge, hle, ↓reduceIte]case3α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)⊢ Sorted (x :: merge xs (y :: ys))
    have hx' := List.pairwise_cons.mp hxcase3α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xs⊢ Sorted (x :: merge xs (y :: ys))
    refine List.pairwise_cons.mpr ⟨?_, ih hx'.2 hy⟩case3α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xs⊢ ∀ (a' : α), a' ∈ merge xs (y :: ys) → x ≤ a'
    intro b hbcase3α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb:b ∈ merge xs (y :: ys)⊢ x ≤ b
    rcases mem_merge.mp hb with hb | hbcase3.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb✝:b ∈ merge xs (y :: ys)hb:b ∈ xs⊢ x ≤ bcase3.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb✝:b ∈ merge xs (y :: ys)hb:b ∈ y :: ys⊢ x ≤ b
    ·case3.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb✝:b ∈ merge xs (y :: ys)hb:b ∈ xs⊢ x ≤ b exact hx'.1 b hbAll goals completed! 🐙
    ·case3.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb✝:b ∈ merge xs (y :: ys)hb:b ∈ y :: ys⊢ x ≤ b rcases List.mem_cons.mp hb with rfl | hbcase3.inr.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αys:List αhx:Sorted (x :: xs)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhle:x ≤ bih:Sorted xs → Sorted (b :: ys) → Sorted (merge xs (b :: ys))hy:Sorted (b :: ys)hb✝:b ∈ merge xs (b :: ys)hb:b ∈ b :: ys⊢ x ≤ bcase3.inr.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb✝¹:b ∈ merge xs (y :: ys)hb✝:b ∈ y :: yshb:b ∈ ys⊢ x ≤ b
      ·case3.inr.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αys:List αhx:Sorted (x :: xs)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhle:x ≤ bih:Sorted xs → Sorted (b :: ys) → Sorted (merge xs (b :: ys))hy:Sorted (b :: ys)hb✝:b ∈ merge xs (b :: ys)hb:b ∈ b :: ys⊢ x ≤ b exact hleAll goals completed! 🐙
      ·case3.inr.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:x ≤ yih:Sorted xs → Sorted (y :: ys) → Sorted (merge xs (y :: ys))hx:Sorted (x :: xs)hy:Sorted (y :: ys)hx':(∀ (a' : α), a' ∈ xs → x ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) xsb:αhb✝¹:b ∈ merge xs (y :: ys)hb✝:b ∈ y :: yshb:b ∈ ys⊢ x ≤ b exact trans _ _ _ hle ((List.pairwise_cons.mp hy).1 b hb)All goals completed! 🐙
  | case4 x xs y ys hle ih =>case4α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)⊢ Sorted (merge (x :: xs) (y :: ys))
    simp only [merge, hle, ↓reduceIte]case4α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)⊢ Sorted (y :: merge (x :: xs) ys)
    have hy' := List.pairwise_cons.mp hycase4α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ys⊢ Sorted (y :: merge (x :: xs) ys)
    have hyx : y ≤ x := byα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ axs:List αys:List αhx:Sorted xshy:Sorted ys⊢ Sorted (merge xs ys)
      rcases total x y with h | hinlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ysh:x ≤ y⊢ y ≤ xinrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ysh:y ≤ x⊢ y ≤ x
      ·inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ysh:x ≤ y⊢ y ≤ x exact absurd h hleAll goals completed! 🐙
      ·inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ysh:y ≤ x⊢ y ≤ x exact hcase4α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ x⊢ Sorted (y :: merge (x :: xs) ys)
    refine List.pairwise_cons.mpr ⟨?_, ih hx hy'.2⟩case4α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ x⊢ ∀ (a' : α), a' ∈ merge (x :: xs) ys → y ≤ a'
    intro b hbcase4α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb:b ∈ merge (x :: xs) ys⊢ y ≤ b
    rcases mem_merge.mp hb with hb | hbcase4.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb✝:b ∈ merge (x :: xs) yshb:b ∈ x :: xs⊢ y ≤ bcase4.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb✝:b ∈ merge (x :: xs) yshb:b ∈ ys⊢ y ≤ b
    ·case4.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb✝:b ∈ merge (x :: xs) yshb:b ∈ x :: xs⊢ y ≤ b rcases List.mem_cons.mp hb with rfl | hbcase4.inl.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ axs:List αy:αys:List αhy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ysb:αhle:¬b ≤ yih:Sorted (b :: xs) → Sorted ys → Sorted (merge (b :: xs) ys)hx:Sorted (b :: xs)hyx:y ≤ bhb✝:b ∈ merge (b :: xs) yshb:b ∈ b :: xs⊢ y ≤ bcase4.inl.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb✝¹:b ∈ merge (x :: xs) yshb✝:b ∈ x :: xshb:b ∈ xs⊢ y ≤ b
      ·case4.inl.inlα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ axs:List αy:αys:List αhy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) ysb:αhle:¬b ≤ yih:Sorted (b :: xs) → Sorted ys → Sorted (merge (b :: xs) ys)hx:Sorted (b :: xs)hyx:y ≤ bhb✝:b ∈ merge (b :: xs) yshb:b ∈ b :: xs⊢ y ≤ b exact hyxAll goals completed! 🐙
      ·case4.inl.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb✝¹:b ∈ merge (x :: xs) yshb✝:b ∈ x :: xshb:b ∈ xs⊢ y ≤ b exact trans _ _ _ hyx ((List.pairwise_cons.mp hx).1 b hb)All goals completed! 🐙
    ·case4.inrα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ ax:αxs:List αy:αys:List αhle:¬x ≤ yih:Sorted (x :: xs) → Sorted ys → Sorted (merge (x :: xs) ys)hx:Sorted (x :: xs)hy:Sorted (y :: ys)hy':(∀ (a' : α), a' ∈ ys → y ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) yshyx:y ≤ xb:αhb✝:b ∈ merge (x :: xs) yshb:b ∈ ys⊢ y ≤ b exact hy'.1 b hbAll goals completed! 🐙

Sortedness of mergeSort is then induction again. Lists of length at most one are sorted, and the other case is the merge lemma applied to the two induction hypotheses.

theorem mergeSort_sorted {α : Type} [LE α] [DecidableLE α]
    (trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
    (total : ∀ a b : α, a ≤ b ∨ b ≤ a)
    (l : List α) : Sorted (mergeSort l) := byα:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List α⊢ Sorted (mergeSort l)
  induction l using mergeSort.induct with
  | case1 l h =>case1α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:l.length ≤ 1⊢ Sorted (mergeSort l)
    rw [mergeSort,case1α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:l.length ≤ 1⊢ Sorted
  (if h : l.length ≤ 1 then l
  else
    have half := l.length / 2;
    merge (mergeSort (List.take half l)) (mergeSort (List.drop half l))) dif_pos hcase1α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:l.length ≤ 1⊢ Sorted l]case1α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:l.length ≤ 1⊢ Sorted l
    match l, h with
    | [], _ =>α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:l.length ≤ 1x✝:[].length ≤ 1⊢ Sorted [] simp [Sorted]All goals completed! 🐙
    | [x], _ =>α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:l.length ≤ 1x:αx✝:[x].length ≤ 1⊢ Sorted [x] simp [Sorted]All goals completed! 🐙
  | case2 l h half ih1 ih2 =>case2α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:Sorted (mergeSort (List.take half l))ih2:Sorted (mergeSort (List.drop half l))⊢ Sorted (mergeSort l)
    rw [mergeSort,case2α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:Sorted (mergeSort (List.take half l))ih2:Sorted (mergeSort (List.drop half l))⊢ Sorted
  (if h : l.length ≤ 1 then l
  else
    have half := l.length / 2;
    merge (mergeSort (List.take half l)) (mergeSort (List.drop half l))) dif_neg hcase2α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:Sorted (mergeSort (List.take half l))ih2:Sorted (mergeSort (List.drop half l))⊢ Sorted
  (have half := l.length / 2;
  merge (mergeSort (List.take half l)) (mergeSort (List.drop half l)))]case2α:Typeinst✝¹:LE αinst✝:DecidableLE αtrans:∀ (a b c : α), a ≤ b → b ≤ c → a ≤ ctotal:∀ (a b : α), a ≤ b ∨ b ≤ al:List αh:¬l.length ≤ 1half:Nat := l.length / 2ih1:Sorted (mergeSort (List.take half l))ih2:Sorted (mergeSort (List.drop half l))⊢ Sorted
  (have half := l.length / 2;
  merge (mergeSort (List.take half l)) (mergeSort (List.drop half l)))
    exact merge_sorted trans total ih1 ih2All goals completed! 🐙

Both halves together:

/-- The headline theorem. -/
theorem mergeSort_correct {α : Type} [LE α] [DecidableLE α]
    (trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
    (total : ∀ a b : α, a ≤ b ∨ b ≤ a)
    (l : List α) : Sorted (mergeSort l) ∧ (mergeSort l).Perm l :=
  ⟨mergeSort_sorted trans total l, mergeSort_perm l⟩

Lean can report what a proof rests on. The axioms below are standard ones; there is no sorry and nothing else was assumed.

'MergeSort.mergeSort_correct' depends on axioms: [propext, Quot.sound]#print axioms mergeSort_correct

'MergeSort.mergeSort_correct' depends on axioms: [propext, Quot.sound]

1.5. Compile and run🔗

A main that reads numbers from standard input and prints them sorted:

def main : IO Unit := do
  let line ← (← IO.getStdin).getLine
  let xs := (line.trimAscii.copy.splitOn " ").filterMap String.toNat?
  IO.println (mergeSort xs)

The program below was compiled and run while this page was built, with the input shown, and its output is what it printed.

stdin5 3 9 1 1 7

stdout[1, 1, 3, 5, 7, 9]

The same program is a standalone Lake project in the repository, part1/, one file with the code of this page and the main above:

cd part1
lake build
echo 5 3 9 1 1 7 | lake exe part1

lake build compiles Lean to C (part1/.lake/build/ir/Main.c, if you want to look) and the C to a native executable with the clang that ships with Lean. The proofs are checked in the same step; they cost nothing at runtime, since a theorem compiles to nothing.

On a million pseudo-random numbers this sort takes about 770 ms (lake exe listbench 1000000 in the repository). That is a linked list of boxed numbers being taken apart and rebuilt twenty times over. The next part changes the data representation and keeps the proof.