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} (xs ys : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : 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

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

@[simp]

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

@[simp]

theorem List.merge_right {α : Type u_1} {le : α → α → Bool} (xs : List α) : xs.merge [] le = 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} (xs : List α) (le : α → α → Bool := by exact fun a b => a ≤ b) : 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

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

def List.enumLE {α : Type u_1} (le : α → α → Bool) (a 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