Comparison counts of merge sort with any comparator

CSLib bounds the comparisons of Cslib.Algorithms.Lean.TimeM.mergeSort, which compares with ≤ in a linear order. Clients that sort by a key, such as symbols by weight or edges by weight, call List.mergeSortM with their own comparator. This file gives the same bounds for any comparator le : α → α → TimeM ℕ Bool that costs at most one tick per call: merging takes at most xs.length + ys.length ticks, and merge sort at most n * ⌈log₂ n⌉.

Main results

• Cslib.Algorithms.Lean.TimeM.mergeM_time: the merge bound.
• Cslib.Algorithms.Lean.TimeM.mergeSortM_time_le: merge sort within the recurrence Cslib.Algorithms.Lean.TimeM.timeMergeSortRec.
• Cslib.Algorithms.Lean.TimeM.mergeSortM_time: merge sort within n * ⌈log₂ n⌉ ticks.

theorem Cslib.Algorithms.Lean.TimeM.mergeM_time {α : Type} (xs ys : List α) (le : α → α → TimeM ℕ Bool) (hle : ∀ (x y : α), (le x y).time ≤ 1) : (xs.mergeM ys le).time ≤ xs.length + ys.length

Merging with a comparator that costs at most one tick per call takes at most xs.length + ys.length ticks.

theorem Cslib.Algorithms.Lean.TimeM.mergeSortM_time_le {α : Type} (xs : List α) (le : α → α → TimeM ℕ Bool) (hle : ∀ (x y : α), (le x y).time ≤ 1) : (xs.mergeSortM le).time ≤ timeMergeSortRec xs.length

Merge sort with a comparator that costs at most one tick per call stays within the merge-sort recurrence timeMergeSortRec.

theorem Cslib.Algorithms.Lean.TimeM.mergeSortM_time {α : Type} (xs : List α) (le : α → α → TimeM ℕ Bool) (hle : ∀ (x y : α), (le x y).time ≤ 1) : (xs.mergeSortM le).time ≤ xs.length * Nat.clog 2 xs.length

Merge sort with a comparator that costs at most one tick per call takes at most n * ⌈log₂ n⌉ ticks on a list of length n.