Definition of merge and mergeSort.

These definitions are intended for verification purposes, and are replaced at runtime by efficient versions in Init.Data.List.Sort.Impl.

@[irreducible]

def List.merge {α : Type u_1} (le : α → α → Bool) : List α → List α → List α

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

This version is not tail-recursive, but it is replaced at runtime by mergeTR using a @[csimp] lemma.

Equations

• List.merge le [] x = x
• List.merge le x [] = x
• List.merge le (x_2 :: xs) (y :: ys) = if le x_2 y = true then x_2 :: List.merge le xs (y :: ys) else y :: List.merge le (x_2 :: xs) ys

@[simp]

theorem List.nil_merge {α : Type u_1} {le : α → α → Bool} (ys : List α) : List.merge le [] ys = ys

@[simp]

theorem List.merge_right {α : Type u_1} {le : α → α → Bool} (xs : List α) : List.merge le xs [] = xs

def List.splitInTwo {α : 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. If the length is odd, the first part will be one element longer.

Equations

• List.splitInTwo l = (⟨(List.splitAt ((n + 1) / 2) l.val).fst, ⋯⟩, ⟨(List.splitAt ((n + 1) / 2) l.val).snd, ⋯⟩)

@[irreducible]

def List.mergeSort {α : Type u_1} (le : α → α → Bool) : List α → List α

Simplified implementation of stable merge sort.

This function is designed for reasoning about the algorithm, and is not efficient. (It particular it uses the non tail-recursive merge function, and so can not be run on large lists, but also makes unnecessary traversals of lists.) It is replaced at runtime in the compiler by mergeSortTR₂ using a @[csimp] lemma.

Because we want the sort to be stable, it is essential that we split the list in two contiguous sublists.

Equations

• List.mergeSort le [] = []
• List.mergeSort le [a] = [a]
• List.mergeSort le (a :: b :: xs) = List.merge le (List.mergeSort le (List.splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val) (List.mergeSort le (List.splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val)

def List.enumLE {α : Type u_1} (le : α → α → Bool) (a : Nat × α) (b : Nat × α) : Bool

Given an ordering relation le : α → α → Bool, construct the reverse lexicographic ordering on Nat × α. which first compares the second components using le, but if these are equivalent (in the sense le a.2 b.2 && le b.2 a.2) then compares the first components using ≤.

This function is only used in stating the stability properties of mergeSort.

Equations

• List.enumLE le a b = if le a.snd b.snd = true then if le b.snd a.snd = true then decide (a.fst ≤ b.fst) else true else false