MergeSort on a list

In this file we introduce merge and mergeSort algorithms that returns a time monad over the list TimeM ℕ (List α). The time complexity of mergeSort is the number of comparisons.

--

Main results

• mergeSort_correct: mergeSort permutes the list into a sorted one.
• mergeSort_time: The number of comparisons of mergeSort is at most n*⌈log₂ n⌉.

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_mergeM {α : Type} {T : Type u_1} [AddMonoid T] (xs ys : List α) (le : α → α → TimeM T Bool) : (xs.mergeM ys le).ret = xs.merge ys fun (x y : α) => (le x y).ret

TimeM.ret passes through List.mergeM into the comparator.

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.ret_mergeSortM {α : Type} {T : Type u_1} [AddMonoid T] (xs : List α) (le : α → α → TimeM T Bool) : (xs.mergeSortM le).ret = xs.mergeSort fun (x y : α) => (le x y).ret

TimeM.ret passes through List.mergeSortM into the comparator.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.TimeM.merge {α : Type} [LinearOrder α] (xs ys : List α) : TimeM ℕ (List α)

Merges two lists into a single list, counting comparisons as time cost. Returns a TimeM ℕ (List α) where the time represents the number of comparisons performed.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.TimeM.mergeSort {α : Type} [LinearOrder α] (xs : List α) : TimeM ℕ (List α)

Sorts a list using the merge sort algorithm, counting comparisons as time cost. Returns a TimeM ℕ (List α) where the time represents the total number of comparisons.

theorem Cslib.Algorithms.Lean.TimeM.ret_merge {α : Type} [LinearOrder α] (xs ys : List α) : (merge xs ys).ret = xs.merge ys fun (a b : α) => decide (a ≤ b)

Our merge computes the one already in mathlib.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.TimeM.IsSorted {α : Type} [LinearOrder α] (l : List α) : Prop

A list is sorted if it satisfies the Pairwise (· ≤ ·) predicate.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.TimeM.MinOfList {α : Type} [LinearOrder α] (x : α) (l : List α) : Prop

x is a minimum element of list l if x ≤ b for all b ∈ l.

theorem Cslib.Algorithms.Lean.TimeM.mem_either_merge {α : Type} [LinearOrder α] (xs ys : List α) (z : α) (hz : z ∈ (merge xs ys).ret) : z ∈ xs ∨ z ∈ ys

theorem Cslib.Algorithms.Lean.TimeM.min_all_merge {α : Type} [LinearOrder α] (x : α) (xs ys : List α) (hxs : MinOfList x xs) (hys : MinOfList x ys) : MinOfList x (merge xs ys).ret

theorem Cslib.Algorithms.Lean.TimeM.sorted_merge {α : Type} [LinearOrder α] {l1 l2 : List α} (hxs : IsSorted l1) (hys : IsSorted l2) : IsSorted (merge l1 l2).ret

theorem Cslib.Algorithms.Lean.TimeM.mergeSort_sorted {α : Type} [LinearOrder α] (xs : List α) : IsSorted (mergeSort xs).ret

theorem Cslib.Algorithms.Lean.TimeM.merge_perm {α : Type} [LinearOrder α] (l₁ l₂ : List α) : (merge l₁ l₂).ret.Perm (l₁ ++ l₂)

theorem Cslib.Algorithms.Lean.TimeM.mergeSort_perm {α : Type} [LinearOrder α] (xs : List α) : (mergeSort xs).ret.Perm xs

theorem Cslib.Algorithms.Lean.TimeM.mergeSort_correct {α : Type} [LinearOrder α] (xs : List α) : IsSorted (mergeSort xs).ret ∧ (mergeSort xs).ret.Perm xs

MergeSort is functionally correct.

@[irreducible]

def Cslib.Algorithms.Lean.TimeM.timeMergeSortRec : ℕ → ℕ

Recurrence relation for the time complexity of merge sort. For a list of length n, this counts the total number of comparisons:

• Base cases: 0 comparisons for lists of length 0 or 1
• Recursive case: split the list, sort both halves, then merge (which takes at most n comparisons)

theorem Cslib.Algorithms.Lean.TimeM.clog2_half_le (n : ℕ) (h : 1 < n) : Nat.clog 2 ((n + 1) / 2) ≤ Nat.clog 2 n - 1

Key Lemma: ⌈log2 ⌈n/2⌉⌉ ≤ ⌈log2 n⌉ - 1 for n > 1

theorem Cslib.Algorithms.Lean.TimeM.clog2_floor_half_le (n : ℕ) (h : 1 < n) : Nat.clog 2 (n / 2) ≤ Nat.clog 2 n - 1

Same logic for the floor half: ⌈log2 ⌊n/2⌋⌉ ≤ ⌈log2 n⌉ - 1

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.TimeM.T (n : ℕ) : ℕ

Upper bound function for merge sort time complexity: T(n) = n * ⌈log₂ n⌉

theorem Cslib.Algorithms.Lean.TimeM.timeMergeSortRec_le (n : ℕ) : timeMergeSortRec n ≤ T n

Solve the recurrence

theorem Cslib.Algorithms.Lean.TimeM.merge_ret_length_eq_sum {α : Type} [LinearOrder α] (xs ys : List α) : (merge xs ys).ret.length = xs.length + ys.length

theorem Cslib.Algorithms.Lean.TimeM.mergeSort_same_length {α : Type} [LinearOrder α] (xs : List α) : (mergeSort xs).ret.length = xs.length

@[simp]

theorem Cslib.Algorithms.Lean.TimeM.merge_time {α : Type} [LinearOrder α] (xs ys : List α) : (merge xs ys).time ≤ xs.length + ys.length

theorem Cslib.Algorithms.Lean.TimeM.mergeSort_time_le {α : Type} [LinearOrder α] (xs : List α) : (mergeSort xs).time ≤ timeMergeSortRec xs.length

theorem Cslib.Algorithms.Lean.TimeM.mergeSort_time {α : Type} [LinearOrder α] (xs : List α) : have n := xs.length; (mergeSort xs).time ≤ n * Nat.clog 2 n

Time complexity of mergeSort