← Mathematical handbook

@[irreducible]

def Verification.mergeComparisons {α : Type u_1} (le : α → α → Bool) : List α → List α → ℕ

Comparison count of the standard stable merge procedure.

Equations

• Verification.mergeComparisons le [] x✝ = 0
• Verification.mergeComparisons le x✝ [] = 0
• Verification.mergeComparisons le (x_2 :: xs) (y :: ys) = if le x_2 y = true then 1 + Verification.mergeComparisons le xs (y :: ys) else 1 + Verification.mergeComparisons le (x_2 :: xs) ys

theorem Verification.mergeComparisons_le {α : Type u_1} (le : α → α → Bool) (xs ys : List α) : mergeComparisons le xs ys ≤ xs.length + ys.length

@[irreducible]

def Verification.mergeSortWork {α : Type u_1} (le : α → α → Bool) : List α → ℕ

Work in merge-sort recursion: merge comparisons plus two linear traversals per split/merge level. Input comparisons have unit cost, as in the paper.

Equations

• One or more equations did not get rendered due to their size.
• Verification.mergeSortWork le [] = 0
• Verification.mergeSortWork le [head] = 0

theorem Verification.mergeSortWork_le_depth {α : Type u_1} (le : α → α → Bool) (d : ℕ) (xs : List α) (h : xs.length ≤ 2 ^ d) : mergeSortWork le xs ≤ 3 * xs.length * d

Each balanced level costs at most three times the input length.

theorem Verification.mergeSortWork_le {α : Type u_1} (le : α → α → Bool) (xs : List α) : mergeSortWork le xs ≤ 3 * xs.length * Nat.clog 2 xs.length