Replacing merge and mergeSort at runtime with tail-recursive and faster versions.

We replace merge with mergeTR using a @[csimp] lemma.

We replace mergeSort in two steps:

• first with mergeSortTR, which while not tail-recursive itself (it can't be), uses mergeTR internally.
• second with mergeSortTR₂, which achieves an ~20% speed-up over mergeSortTR by avoiding some unnecessary list reversals.

There is no public API in this file; it solely exists to implement the @[csimp] lemmas affecting runtime behaviour.

Future work

The current runtime implementation could be further improved in a number of ways, e.g.:

• only walking the list once during splitting,
• using insertion sort for small chunks rather than splitting all the way down to singletons,
• identifying already sorted or reverse sorted chunks and skipping them.

Because the theory developed for mergeSort is independent of the runtime implementation, as long as such improvements are carefully validated by benchmarking, they can be done without changing the theory, as long as a @[csimp] lemma is provided.

def List.MergeSort.Internal.mergeTR {α : Type u_1} (l₁ l₂ : List α) (le : α → α → Bool) : List α

O(min |l| |r|). Merge two lists using le as a switch.

Equations

• List.MergeSort.Internal.mergeTR l₁ l₂ le = List.MergeSort.Internal.mergeTR.go le l₁ l₂ []

@[irreducible]

def List.MergeSort.Internal.mergeTR.go {α : Type u_1} (le : α → α → Bool) : List α → List α → List α → List α

Equations

• One or more equations did not get rendered due to their size.
• List.MergeSort.Internal.mergeTR.go le [] x✝ x = x.reverseAux x✝
• List.MergeSort.Internal.mergeTR.go le x✝ [] x = x.reverseAux x✝

theorem List.MergeSort.Internal.mergeTR_go_eq {α✝ : Type u_1} {le : α✝ → α✝ → Bool} {l₁ l₂ acc : List α✝} : List.MergeSort.Internal.mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le

@[csimp]

theorem List.MergeSort.Internal.merge_eq_mergeTR : @List.merge = @List.MergeSort.Internal.mergeTR

def List.MergeSort.Internal.splitRevAt {α : Type u_1} (n : Nat) (l : List α) : List α × List α

Variant of splitAt, that does not reverse the first list, i.e splitRevAt n l = ((l.take n).reverse, l.drop n).

This exists solely as an optimization for mergeSortTR and mergeSortTR₂, and should not be used elsewhere.

Equations

• List.MergeSort.Internal.splitRevAt n l = List.MergeSort.Internal.splitRevAt.go l n []

def List.MergeSort.Internal.splitRevAt.go {α : Type u_1} : List α → Nat → List α → List α × List α

Auxiliary for splitAtRev: splitAtRev.go xs n acc = ((take n xs).reverse ++ acc, drop n xs).

Equations

• List.MergeSort.Internal.splitRevAt.go (x_3 :: xs) n.succ x = List.MergeSort.Internal.splitRevAt.go xs n (x_3 :: x)
• List.MergeSort.Internal.splitRevAt.go x✝¹ x✝ x = (x, x✝¹)

theorem List.MergeSort.Internal.splitRevAt_go {α : Type u_1} (xs : List α) (n : Nat) (acc : List α) : List.MergeSort.Internal.splitRevAt.go xs n acc = ((List.take n xs).reverse ++ acc, List.drop n xs)

theorem List.MergeSort.Internal.splitRevAt_eq {α : Type u_1} (n : Nat) (l : List α) : List.MergeSort.Internal.splitRevAt n l = ((List.take n l).reverse, List.drop n l)

def List.MergeSort.Internal.mergeSortTR {α : Type u_1} (l : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α

An intermediate speed-up for mergeSort. This version uses the tail-recurive mergeTR function as a subroutine.

This is not the final version we use at runtime, as mergeSortTR₂ is faster. This definition is useful as an intermediate step in proving the @[csimp] lemma for mergeSortTR₂.

Equations

• List.MergeSort.Internal.mergeSortTR l le = List.MergeSort.Internal.mergeSortTR.run le ⟨l, ⋯⟩

@[irreducible]

def List.MergeSort.Internal.mergeSortTR.run {α : Type u_1} (le : α → α → Bool := by exact fun a b => a ≤ b) {n : Nat} : { l : List α // l.length = n } → List α

Equations

• One or more equations did not get rendered due to their size.
• List.MergeSort.Internal.mergeSortTR.run le ⟨[], property⟩ = []
• List.MergeSort.Internal.mergeSortTR.run le ⟨[a], property⟩ = [a]

def List.MergeSort.Internal.splitRevInTwo {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : { l : List α // l.length = (n + 1) / 2 } × { l : List α // l.length = n / 2 }

Split a list in two equal parts, reversing the first part. If the length is odd, the first part will be one element longer.

Equations

• List.MergeSort.Internal.splitRevInTwo l = (⟨(List.MergeSort.Internal.splitRevAt ((n + 1) / 2) l.val).fst, ⋯⟩, ⟨(List.MergeSort.Internal.splitRevAt ((n + 1) / 2) l.val).snd, ⋯⟩)

def List.MergeSort.Internal.splitRevInTwo' {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : { l : List α // l.length = n / 2 } × { l : List α // l.length = (n + 1) / 2 }

Split a list in two equal parts, reversing the first part. If the length is odd, the second part will be one element longer.

Equations

• List.MergeSort.Internal.splitRevInTwo' l = (⟨(List.MergeSort.Internal.splitRevAt (n / 2) l.val).fst, ⋯⟩, ⟨(List.MergeSort.Internal.splitRevAt (n / 2) l.val).snd, ⋯⟩)

def List.MergeSort.Internal.mergeSortTR₂ {α : Type u_1} (l : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : List α

Faster version of mergeSortTR, which avoids unnecessary list reversals.

Equations

• List.MergeSort.Internal.mergeSortTR₂ l le = List.MergeSort.Internal.mergeSortTR₂.run le ⟨l, ⋯⟩

@[irreducible]

def List.MergeSort.Internal.mergeSortTR₂.run {α : Type u_1} (le : α → α → Bool := by exact fun a b => a ≤ b) {n : Nat} : { l : List α // l.length = n } → List α

Equations

• One or more equations did not get rendered due to their size.
• List.MergeSort.Internal.mergeSortTR₂.run le ⟨[], property⟩ = []
• List.MergeSort.Internal.mergeSortTR₂.run le ⟨[a], property⟩ = [a]

@[irreducible]

def List.MergeSort.Internal.mergeSortTR₂.run' {α : Type u_1} (le : α → α → Bool := by exact fun a b => a ≤ b) {n : Nat} : { l : List α // l.length = n } → List α

Equations

• One or more equations did not get rendered due to their size.
• List.MergeSort.Internal.mergeSortTR₂.run' le ⟨[], property⟩ = []
• List.MergeSort.Internal.mergeSortTR₂.run' le ⟨[a], property⟩ = [a]

theorem List.MergeSort.Internal.splitRevInTwo'_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (List.MergeSort.Internal.splitRevInTwo' l).fst = ⟨(List.splitInTwo ⟨l.val.reverse, ⋯⟩).snd.val, ⋯⟩

theorem List.MergeSort.Internal.splitRevInTwo'_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (List.MergeSort.Internal.splitRevInTwo' l).snd = ⟨(List.splitInTwo ⟨l.val.reverse, ⋯⟩).fst.val.reverse, ⋯⟩

theorem List.MergeSort.Internal.splitRevInTwo_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (List.MergeSort.Internal.splitRevInTwo l).fst = ⟨(List.splitInTwo l).fst.val.reverse, ⋯⟩

theorem List.MergeSort.Internal.splitRevInTwo_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) : (List.MergeSort.Internal.splitRevInTwo l).snd = ⟨(List.splitInTwo l).snd.val, ⋯⟩

@[irreducible]

theorem List.MergeSort.Internal.mergeSortTR_run_eq_mergeSort {α : Type u_1} {le : α → α → Bool} {n : Nat} (l : { l : List α // l.length = n }) : List.MergeSort.Internal.mergeSortTR.run le l = l.val.mergeSort le

theorem List.MergeSort.Internal.mergeSort_eq_mergeSortTR : @List.mergeSort = @List.MergeSort.Internal.mergeSortTR

@[irreducible]

theorem List.MergeSort.Internal.mergeSortTR₂_run_eq_mergeSort {α : Type u_1} {le : α → α → Bool} {n : Nat} (l : { l : List α // l.length = n }) : List.MergeSort.Internal.mergeSortTR₂.run le l = l.val.mergeSort le

@[irreducible]

theorem List.MergeSort.Internal.mergeSortTR₂_run'_eq_mergeSort {α : Type u_1} {l' : List α} {le : α → α → Bool} {n : Nat} (l : { l : List α // l.length = n }) (w : l' = l.val.reverse) : List.MergeSort.Internal.mergeSortTR₂.run' le l = l'.mergeSort le

@[csimp]

theorem List.MergeSort.Internal.mergeSort_eq_mergeSortTR₂ : @List.mergeSort = @List.MergeSort.Internal.mergeSortTR₂