Documentation

Init.Data.List.Sort.Impl

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:

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.:

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
@[irreducible]
def List.MergeSort.Internal.mergeTR.go {α : Type u_1} (le : ααBool) :
List αList αList αList α
Equations
theorem List.MergeSort.Internal.mergeTR_go_eq {α✝ : Type u_1} {le : α✝α✝Bool} {l₁ l₂ acc : List α✝} :
mergeTR.go le l₁ l₂ acc = acc.reverse ++ l₁.merge l₂ le
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
def List.MergeSort.Internal.splitRevAt.go {α : Type u_1} :
List αNatList αList α × List α

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

Equations
theorem List.MergeSort.Internal.splitRevAt_go {α : Type u_1} (xs : List α) (n : Nat) (acc : List α) :
splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)
theorem List.MergeSort.Internal.splitRevAt_eq {α : Type u_1} (n : Nat) (l : List α) :
splitRevAt n l = ((take n l).reverse, 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
@[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
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
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
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
@[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
@[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
theorem List.MergeSort.Internal.splitRevInTwo'_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
(splitRevInTwo' l).fst = (splitInTwo l.val.reverse, ).snd.val,
theorem List.MergeSort.Internal.splitRevInTwo'_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
(splitRevInTwo' l).snd = (splitInTwo l.val.reverse, ).fst.val.reverse,
theorem List.MergeSort.Internal.splitRevInTwo_fst {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
(splitRevInTwo l).fst = (splitInTwo l).fst.val.reverse,
theorem List.MergeSort.Internal.splitRevInTwo_snd {α : Type u_1} {n : Nat} (l : { l : List α // l.length = n }) :
(splitRevInTwo l).snd = (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 }) :
mergeSortTR.run le l = l.val.mergeSort le
@[irreducible]
theorem List.MergeSort.Internal.mergeSortTR₂_run_eq_mergeSort {α : Type u_1} {le : ααBool} {n : Nat} (l : { l : List α // l.length = n }) :
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) :
mergeSortTR₂.run' le l = l'.mergeSort le