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⌉.

@[irreducible]

def Cslib.Algorithms.Lean.TimeM.merge {α : Type} [LinearOrder α] : List α → 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.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Algorithms.Lean.TimeM.merge [] x✝ = pure x✝
• Cslib.Algorithms.Lean.TimeM.merge x✝ [] = pure x✝

@[irreducible]

def 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.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

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

Equations

• Cslib.Algorithms.Lean.TimeM.IsSorted l = List.Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l

@[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.

Equations

• Cslib.Algorithms.Lean.TimeM.MinOfList x l = ∀ b ∈ l, x ≤ b

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)

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Algorithms.Lean.TimeM.timeMergeSortRec 0 = 0
• Cslib.Algorithms.Lean.TimeM.timeMergeSortRec 1 = 0

def Cslib.Algorithms.Lean.TimeM.clog2 (n : ℕ) : ℕ

The ceiling of Nat.log 2

Equations

• Cslib.Algorithms.Lean.TimeM.clog2 n = if n ≤ 1 then 0 else Nat.log 2 (n - 1) + 1

theorem Cslib.Algorithms.Lean.TimeM.clog2_half_le (n : ℕ) (h : n > 1) : clog2 ((n + 1) / 2) ≤ clog2 n - 1

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

theorem Cslib.Algorithms.Lean.TimeM.clog2_floor_half_le (n : ℕ) (h : n > 1) : clog2 (n / 2) ≤ clog2 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⌉

Equations

• Cslib.Algorithms.Lean.TimeM.T n = n * Cslib.Algorithms.Lean.TimeM.clog2 n

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

Solve the recurrence

@[simp]

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

@[simp]

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 * clog2 n

Time complexity of mergeSort