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.MergeSort.Internal.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.

This is an implementation detail of mergeSort.

Equations

• List.MergeSort.Internal.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

• One or more equations did not get rendered due to their size.
• [].mergeSort x✝ = []
• [a].mergeSort x✝ = [a]

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

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

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

Equations

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