Browse chapters

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_02.Section_02_1_Insertion_Sort
import CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.Merge
import CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.MergeSort

2.3. Designing Algorithms

This file introduces merge sort as the Chapter 2 divide-and-conquer example. The executable top-level algorithm splits the input, recursively sorts both halves, and invokes the locally verified, costed MERGE procedure at every combine node. A compatibility theorem identifies its output with Lean's List.mergeSort. Together these developments establish the algorithmic contract:

merge sort returns a sorted list;
merge sort preserves the input elements.
MERGE returns a sorted permutation of two sorted inputs;
MERGE performs at most a linear number of head comparisons and writes each output element exactly once.
the execution-derived merge-sort work satisfies the floor/ceiling recurrence and belongs to Theta(n log n) for all natural input lengths.

It also records the exact solution of the textbook recurrence on powers of two: T(1) = 1 and T(2^(k+1)) = 2 * T(2^k) + 2^(k+1).

Known simplifications

The local MERGE uses immutable lists rather than temporary mutable arrays. Its counters charge head comparisons and output writes, not allocation or word-RAM instructions.

Implementation details

namespace CLRSnamespace Chapter02

The merge-sort recurrence restricted to inputs of size 2^k.

The index k represents the input length 2^k; thus the successor equation is the CLRS recurrence T(2^(k+1)) = 2 * T(2^k) + 2^(k+1) with unit base cost.

def mergeSortRecurrenceOnPowersOfTwo : Nat → Nat
  | 0 => 1
  | k + 1 => 2 * mergeSortRecurrenceOnPowersOfTwo k + 2 ^ (k + 1)

The exact closed form for the power-of-two merge-sort recurrence.


theorem mergeSortRecurrenceOnPowersOfTwo_closedForm (k : Nat) :
    mergeSortRecurrenceOnPowersOfTwo k = (k + 1) * 2 ^ k := by
  induction k with
  | zero =>
      simp [mergeSortRecurrenceOnPowersOfTwo]
  | succ k ih =>
      calc
        mergeSortRecurrenceOnPowersOfTwo (k + 1)
            = 2 * ((k + 1) * 2 ^ k) + 2 ^ (k + 1) := by
                simp [mergeSortRecurrenceOnPowersOfTwo, ih]
        _ = (k + 2) * 2 ^ (k + 1) := by
                rw [Nat.pow_succ]
                let p := 2 ^ k
                have hmul : 2 * ((k + 1) * p) = (k + 1) * (p * 2) := by
                  rw [← Nat.mul_assoc]
                  rw [Nat.mul_comm 2 (k + 1)]
                  rw [Nat.mul_assoc]
                  rw [Nat.mul_comm 2 p]
                calc
                  2 * ((k + 1) * p) + p * 2 = (k + 1) * (p * 2) + p * 2 := by
                    rw [hmul]
                  _ = ((k + 1) + 1) * (p * 2) := by
                    simpa using (Nat.add_mul (k + 1) 1 (p * 2)).symm
                  _ = (k + 2) * (p * 2) := by
                    simp [Nat.add_assoc]

end Chapter02end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.Merge.Correctness

CLRS Section 2.3 - MERGE correctness

The local executable MERGE is related to Mathlib's generic list merge only as a proof bridge. The public theorems speak directly about the Chapter 2 execution: exact erasure, element preservation, length, and sortedness.

namespace CLRSnamespace Chapter02

Reading the value field of the costed execution is exactly merge.

theorem mergeWithCost_value (left right : List Nat) :
    (mergeWithCost left right).value = merge left right := rfl

The explicit Chapter 2 merge has the same value as the generic list merge.

private theorem merge_eq_listMerge (left right : List Nat) :
    merge left right = List.merge left right (fun x y => decide (x ≤ y)) := by
  induction left, right using mergeWithCost.induct with
  | case1 right =>
      simp [merge, mergeWithCost]
  | case2 left hleft =>
      cases left with
      | nil => exact (hleft rfl).elim
      | cons x xs => simp [merge, mergeWithCost]
  | case3 x xs y ys hxy ih =>
      simp [merge, mergeWithCost, hxy]
      change merge xs (y :: ys) = xs.merge (y :: ys) fun x y => decide (x ≤ y)
      exact ih
  | case4 x xs y ys hxy ih =>
      simp [merge, mergeWithCost, hxy]
      change merge (x :: xs) ys = (x :: xs).merge ys fun x y => decide (x ≤ y)
      exact ih

MERGE preserves every input occurrence, including duplicates.


theorem merge_perm (left right : List Nat) :
    (merge left right).Perm (left ++ right) := by
  rw [merge_eq_listMerge]
  exact List.merge_perm_append (fun x y : Nat => decide (x ≤ y))

The output length is the sum of the two input lengths.

theorem merge_length (left right : List Nat) :
    (merge left right).length = left.length + right.length := by
  simpa using (merge_perm left right).length_eq

MERGE returns a nondecreasing list when both inputs are nondecreasing.


theorem merge_sorted {left right : List Nat}
    (hl : left.SortedLE) (hr : right.SortedLE) :
    (merge left right).SortedLE := by
  rw [merge_eq_listMerge]
  exact (List.Pairwise.merge hl.pairwise hr.pairwise).sortedLE

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.Merge.Cost

CLRS Section 2.3 - MERGE comparison cost

This module proves the linear comparison bound for the same execution whose value is proved correct in Merge.Correctness.

namespace CLRSnamespace Chapter02

MERGE performs at most one head comparison per available input element.

theorem merge_comparisons_le (left right : List Nat) :
    (mergeWithCost left right).comparisons ≤ left.length + right.length := by
  induction left, right using mergeWithCost.induct with
  | case1 right =>
      simp [mergeWithCost]
  | case2 left hleft =>
      cases left with
      | nil => exact (hleft rfl).elim
      | cons x xs => simp [mergeWithCost]
  | case3 x xs y ys hxy ih =>
      simp [mergeWithCost, hxy] at ih ⊢
      omega
  | case4 x xs y ys hxy ih =>
      simp [mergeWithCost, hxy] at ih ⊢
      omega

MERGE writes each output element exactly once, including copied suffixes.

theorem merge_outputWrites_eq (left right : List Nat) :
    (mergeWithCost left right).outputWrites = left.length + right.length := by
  induction left, right using mergeWithCost.induct with
  | case1 right =>
      simp [mergeWithCost]
  | case2 left hleft =>
      cases left with
      | nil => exact (hleft rfl).elim
      | cons x xs => simp [mergeWithCost]
  | case3 x xs y ys hxy ih =>
      simp [mergeWithCost, hxy] at ih ⊢
      omega
  | case4 x xs y ys hxy ih =>
      simp [mergeWithCost, hxy] at ih ⊢
      omega

The textbook list-level MERGE contract: sorted output, exact multiset preservation, a linear number of head comparisons, and exactly one output write per input element.

theorem merge_correct {left right : List Nat}
    (hl : left.SortedLE) (hr : right.SortedLE) :
    (merge left right).SortedLE ∧
      (merge left right).Perm (left ++ right) ∧
      (mergeWithCost left right).comparisons ≤ left.length + right.length ∧
      (mergeWithCost left right).outputWrites = left.length + right.length := by
  exact ⟨merge_sorted hl hr, merge_perm left right, merge_comparisons_le left right,
    merge_outputWrites_eq left right⟩

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.Merge.Definitions

CLRS Section 2.3 - MERGE definitions

This module defines the executable two-list core of the textbook MERGE procedure. A single execution records both the merged value and the number of head-to-head element comparisons.

namespace CLRSnamespace Chapter02

The observable result of one list-level MERGE execution.

structure MergeExecution where
  value : List Nat
  comparisons : Nat
  outputWrites : Nat
deriving DecidableEq, Repr

Merge two lists by repeatedly emitting the smaller current head.

The empty-list cases copy the remaining suffix without another element comparison. The recursive cases consume exactly one input element and charge one head comparison.

def mergeWithCost : List Nat → List Nat → MergeExecution
  | [], right => ⟨right, 0, right.length⟩
  | left, [] => ⟨left, 0, left.length⟩
  | x :: xs, y :: ys =>
      if x ≤ y then
        let rest := mergeWithCost xs (y :: ys)
        ⟨x :: rest.value, rest.comparisons + 1, rest.outputWrites + 1⟩
      else
        let rest := mergeWithCost (x :: xs) ys
        ⟨y :: rest.value, rest.comparisons + 1, rest.outputWrites + 1⟩
termination_by left right => left.length + right.length

The value-only projection of the costed MERGE execution.

def merge (left right : List Nat) : List Nat :=
  (mergeWithCost left right).value

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.MergeSort.Compatibility

CLRS Section 2.3 - Merge-sort compatibility API

The historical public mergeSort delegates to Mathlib. The executable Chapter 2 development proves its own recursion separately and connects to this API through the unique sorted-permutation specification.

namespace CLRSnamespace Chapter02

Merge sort over natural numbers, using the standard nondecreasing order.

def mergeSort (xs : List Nat) : List Nat :=
  xs.mergeSort (· ≤ ·)

Merge sort returns a list sorted in Mathlib's standard SortedLE sense.

theorem mergeSort_sortedLE (xs : List Nat) : (mergeSort xs).SortedLE := by
  simpa [mergeSort] using (List.sortedLE_mergeSort (l := xs))

Merge sort preserves the input elements up to permutation.

theorem mergeSort_perm (xs : List Nat) : (mergeSort xs).Perm xs := by
  simpa [mergeSort] using (List.mergeSort_perm xs (· ≤ ·))

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.MergeSort.Correctness

CLRS Section 2.3 - Merge-sort correctness

The recursive execution is proved to return the sorted permutation of its input. The proofs reuse the semantic contract of the exact mergeWithCost call made by the program.

namespace CLRSnamespace Chapter02

The recursive costed merge-sort execution preserves every occurrence.


theorem mergeSortWithCost_perm (xs : List Nat) :
    (mergeSortWithCost xs).value.Perm xs := by
  refine WellFounded.induction (measure List.length).wf xs
    (C := fun ys => (mergeSortWithCost ys).value.Perm ys) ?_
  intro xs ih
  cases xs with
  | nil => simp [mergeSortWithCost.eq_def]
  | cons x tail =>
    cases tail with
    | nil => simp [mergeSortWithCost.eq_def]
    | cons y rest =>
      let input := x :: y :: rest
      let middle := input.length / 2
      let left := input.take middle
      let right := input.drop middle
      let leftRun := mergeSortWithCost left
      let rightRun := mergeSortWithCost right
      have hleftLength : left.length < input.length := by
        simp [left, middle, input]
        omega
      have hrightLength : right.length < input.length := by
        simp [right, middle, input]
        omega
      have ihLeft : leftRun.value.Perm left := by
        apply ih left
        change left.length < input.length
        exact hleftLength
      have ihRight : rightRun.value.Perm right := by
        apply ih right
        change right.length < input.length
        exact hrightLength
      have hmerge :
          (mergeWithCost leftRun.value rightRun.value).value.Perm
            (leftRun.value ++ rightRun.value) := by
        simpa [leftRun, rightRun, merge] using
          merge_perm leftRun.value rightRun.value
      have hhalves : (leftRun.value ++ rightRun.value).Perm (left ++ right) :=
        ihLeft.append ihRight
      have hsplit : left ++ right = input := by
        simp [left, right]
      rw [mergeSortWithCost.eq_def]
      dsimp only
      exact (hmerge.trans hhalves).trans (hsplit ▸ List.Perm.refl input)

The recursive costed merge-sort execution returns nondecreasing output.


theorem mergeSortWithCost_sorted (xs : List Nat) :
    (mergeSortWithCost xs).value.SortedLE := by
  refine WellFounded.induction (measure List.length).wf xs
    (C := fun ys => (mergeSortWithCost ys).value.SortedLE) ?_
  intro xs ih
  cases xs with
  | nil =>
    rw [mergeSortWithCost.eq_def]
    exact List.sortedLE_iff_pairwise.mpr (by simp)
  | cons x tail =>
    cases tail with
    | nil =>
      rw [mergeSortWithCost.eq_def]
      exact List.sortedLE_iff_pairwise.mpr (by simp)
    | cons y rest =>
      let input := x :: y :: rest
      let middle := input.length / 2
      have hleftLength : (input.take middle).length < input.length := by
        simp [middle, input]
        omega
      have hrightLength : (input.drop middle).length < input.length := by
        simp [middle, input]
        omega
      have ihLeft : (mergeSortWithCost (input.take middle)).value.SortedLE := by
        apply ih (input.take middle)
        change (input.take middle).length < input.length
        exact hleftLength
      have ihRight : (mergeSortWithCost (input.drop middle)).value.SortedLE := by
        apply ih (input.drop middle)
        change (input.drop middle).length < input.length
        exact hrightLength
      rw [mergeSortWithCost.eq_def]
      dsimp only
      exact merge_sorted ihLeft ihRight

The complete semantic contract of the executable merge sort.

theorem mergeSortWithCost_correct (xs : List Nat) :
    (mergeSortWithCost xs).value.SortedLE ∧
      (mergeSortWithCost xs).value.Perm xs :=
  ⟨mergeSortWithCost_sorted xs, mergeSortWithCost_perm xs⟩

The costed execution erases to the historical public merge-sort value.

theorem mergeSortWithCost_eq_mergeSort (xs : List Nat) :
    (mergeSortWithCost xs).value = mergeSort xs := by
  have hperm : (mergeSortWithCost xs).value.Perm (mergeSort xs) :=
    (mergeSortWithCost_perm xs).trans (mergeSort_perm xs).symm
  exact hperm.eq_of_sortedLE (mergeSortWithCost_sorted xs) (mergeSort_sortedLE xs)

Value-only erasure of the costed execution.

theorem mergeSortValue_eq (xs : List Nat) :
    mergeSortValue xs = (mergeSortWithCost xs).value := rfl

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.MergeSort.Cost

CLRS Section 2.3 - Execution-derived merge-sort cost

The work recurrence in this module is derived from the counter accumulated by the executable split--recurse--mergeWithCost program. In particular, the linear combine term follows from merge_outputWrites_eq; it is not installed as an unrelated cost formula.

namespace CLRSnamespace Chapter02

Exact comparison-counter equation at a non-base execution node.


theorem mergeSortWithCost_comparisons_two_or_more (x y : Nat) (rest : List Nat) :
    let input := x :: y :: rest
    let middle := input.length / 2
    let leftRun := mergeSortWithCost (input.take middle)
    let rightRun := mergeSortWithCost (input.drop middle)
    (mergeSortWithCost input).comparisons =
      leftRun.comparisons + rightRun.comparisons +
        (mergeWithCost leftRun.value rightRun.value).comparisons := by
  dsimp only
  rw [mergeSortWithCost.eq_def]

Exact output-write-counter equation at a non-base execution node.


theorem mergeSortWithCost_outputWrites_two_or_more (x y : Nat) (rest : List Nat) :
    let input := x :: y :: rest
    let middle := input.length / 2
    let leftRun := mergeSortWithCost (input.take middle)
    let rightRun := mergeSortWithCost (input.drop middle)
    (mergeSortWithCost input).outputWrites =
      leftRun.outputWrites + rightRun.outputWrites +
        (mergeWithCost leftRun.value rightRun.value).outputWrites := by
  dsimp only
  rw [mergeSortWithCost.eq_def]

In a non-base execution, the work counter is the two recursive counters plus exactly one output write for every input element.


theorem mergeSortWithCost_work_two_or_more (x y : Nat) (rest : List Nat) :
    let input := x :: y :: rest
    let middle := input.length / 2
    (mergeSortWithCost input).work =
      (mergeSortWithCost (input.take middle)).work +
        (mergeSortWithCost (input.drop middle)).work + input.length := by
  dsimp only
  rw [mergeSortWithCost.eq_def]
  dsimp only
  rw [merge_outputWrites_eq]
  have hleft := (mergeSortWithCost_perm
    ((x :: y :: rest).take ((x :: y :: rest).length / 2))).length_eq
  have hright := (mergeSortWithCost_perm
    ((x :: y :: rest).drop ((x :: y :: rest).length / 2))).length_eq
  rw [hleft, hright]
  rw [List.length_take, List.length_drop,
    Nat.min_eq_left (Nat.div_le_self (x :: y :: rest).length 2)]
  omega

The execution work is determined only by input length.


theorem mergeSortWithCost_work_eq_of_length_eq {xs ys : List Nat}
    (hlen : xs.length = ys.length) :
    (mergeSortWithCost xs).work = (mergeSortWithCost ys).work := by
  refine WellFounded.induction (measure List.length).wf xs
    (C := fun xs => ∀ ys, xs.length = ys.length →
      (mergeSortWithCost xs).work = (mergeSortWithCost ys).work) ?_ ys hlen
  intro xs ih ys hlen
  cases xs with
  | nil =>
    have : ys = [] := List.length_eq_zero_iff.mp hlen.symm
    subst ys
    rfl
  | cons x tail =>
    cases tail with
    | nil =>
      have hys : ys.length = 1 := by simpa using hlen.symm
      obtain ⟨z, rfl⟩ := List.length_eq_one_iff.mp hys
      simp [mergeSortWithCost.eq_def]
    | cons y rest =>
      cases ys with
      | nil => simp at hlen
      | cons x' tail' =>
        cases tail' with
        | nil => simp at hlen
        | cons y' rest' =>
          let input := x :: y :: rest
          let input' := x' :: y' :: rest'
          let middle := input.length / 2
          let middle' := input'.length / 2
          have hinput : input.length = input'.length := by simpa [input, input'] using hlen
          have hmiddle : middle = middle' := by simp [middle, middle', hinput]
          have hleftLength : (input.take middle).length < input.length := by
            simp [middle, input]
            omega
          have hrightLength : (input.drop middle).length < input.length := by
            simp [middle, input]
            omega
          have htakeLength :
              (input.take middle).length = (input'.take middle').length := by
            simp [List.length_take, hinput, hmiddle]
          have hdropLength :
              (input.drop middle).length = (input'.drop middle').length := by
            simp [List.length_drop, hinput, hmiddle]
          have ihLeft := ih (input.take middle) (by
            change (input.take middle).length < input.length
            exact hleftLength) (input'.take middle') htakeLength
          have ihRight := ih (input.drop middle) (by
            change (input.drop middle).length < input.length
            exact hrightLength) (input'.drop middle') hdropLength
          rw [mergeSortWithCost_work_two_or_more,
            mergeSortWithCost_work_two_or_more]
          rw [ihLeft, ihRight, hinput]

Every execution's work counter is the canonical length-indexed work.

theorem mergeSortWithCost_work_eq_length (xs : List Nat) :
    (mergeSortWithCost xs).work = mergeSortWork xs.length := by
  unfold mergeSortWork
  apply mergeSortWithCost_work_eq_of_length_eq
  simp

Actual head comparisons are bounded by the execution work charged from the same recursive run.


theorem mergeSortWithCost_comparisons_le_work (xs : List Nat) :
    (mergeSortWithCost xs).comparisons ≤ (mergeSortWithCost xs).work := by
  refine WellFounded.induction (measure List.length).wf xs
    (C := fun xs => (mergeSortWithCost xs).comparisons ≤
      (mergeSortWithCost xs).work) ?_
  intro xs ih
  cases xs with
  | nil => simp [mergeSortWithCost.eq_def]
  | cons x tail =>
    cases tail with
    | nil => simp [mergeSortWithCost.eq_def]
    | cons y rest =>
      let input := x :: y :: rest
      let middle := input.length / 2
      let left := input.take middle
      let right := input.drop middle
      let leftRun := mergeSortWithCost left
      let rightRun := mergeSortWithCost right
      have hleftLength : left.length < input.length := by
        simp [left, middle, input]
        omega
      have hrightLength : right.length < input.length := by
        simp [right, middle, input]
        omega
      have ihLeft : leftRun.comparisons ≤ leftRun.work := by
        apply ih left
        change left.length < input.length
        exact hleftLength
      have ihRight : rightRun.comparisons ≤ rightRun.work := by
        apply ih right
        change right.length < input.length
        exact hrightLength
      have hmerge := merge_comparisons_le leftRun.value rightRun.value
      have hwrites := merge_outputWrites_eq leftRun.value rightRun.value
      rw [mergeSortWithCost.eq_def]
      dsimp only
      simp only [leftRun, rightRun, left, right, middle, input] at ihLeft ihRight hmerge hwrites ⊢
      omega

Base work for the empty input.

@[simp] theorem mergeSortWork_zero : mergeSortWork 0 = 0 := by
  simp [mergeSortWork, mergeSortWithCost.eq_def]

Base work for a singleton input.

@[simp] theorem mergeSortWork_one : mergeSortWork 1 = 1 := by
  simp [mergeSortWork, mergeSortWithCost.eq_def]

Exact floor/ceiling recurrence derived from the executable work counter.


theorem mergeSortWork_recurrence_nat (n : Nat) (hn : 2 ≤ n) :
    mergeSortWork n =
      mergeSortWork (n / 2) + mergeSortWork ((n + 1) / 2) + n := by
  obtain ⟨k, rfl⟩ : ∃ k, n = k + 2 := by exact ⟨n - 2, by omega⟩
  change (mergeSortWithCost (List.replicate (k + 2) 0)).work =
    mergeSortWork ((k + 2) / 2) +
      mergeSortWork ((k + 2 + 1) / 2) + (k + 2)
  rw [show List.replicate (k + 2) 0 = 0 :: 0 :: List.replicate k 0 by
    simp [List.replicate_succ]]
  rw [mergeSortWithCost_work_two_or_more]
  rw [mergeSortWithCost_work_eq_length, mergeSortWithCost_work_eq_length]
  rw [List.length_take, List.length_drop]
  simp only [List.length_cons, List.length_replicate]
  have hnorm : k + 1 + 1 = k + 2 := by omega
  rw [hnorm]
  have hceil : k + 2 - (k + 2) / 2 = (k + 2 + 1) / 2 := by omega
  rw [Nat.min_eq_left (Nat.div_le_self (k + 2) 2), hceil]

The real cast of the execution-derived work satisfies the textbook all-input merge-sort recurrence.

theorem mergeSortWork_recurrence :
    MergeSortRecurrence.Recurrence (fun n => (mergeSortWork n : Real)) := by
  intro n hn
  change (mergeSortWork n : Real) =
    (mergeSortWork (n / 2) : Real) +
      (mergeSortWork ((n + 1) / 2) : Real) + (n : Real)
  exact_mod_cast mergeSortWork_recurrence_nat n hn

The execution-derived work does not decrease when the input length grows by one.


private theorem mergeSortWork_le_succ : ∀ n, mergeSortWork n ≤ mergeSortWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hsmall : n ≤ 1
      · interval_cases n
        · simp
        · rw [mergeSortWork_recurrence_nat 2 (by norm_num)]
          norm_num
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hfloorEven : 2 * m / 2 = m := by omega
          have hceilEven : (2 * m + 1) / 2 = m := by omega
          have hceilOdd : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [mergeSortWork_recurrence_nat (2 * m) (by omega),
            mergeSortWork_recurrence_nat (2 * m + 1) (by omega),
            hfloorEven, hceilEven, hceilOdd]
          have ihm := ih m (by omega)
          omega
        · have hfloorOdd : (2 * m + 1) / 2 = m := by omega
          have hceilOdd : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          have hceilEven : (2 * m + 1 + 1 + 1) / 2 = m + 1 := by omega
          rw [mergeSortWork_recurrence_nat (2 * m + 1) (by omega),
            mergeSortWork_recurrence_nat (2 * m + 1 + 1) (by omega),
            hfloorOdd, hceilOdd, hceilEven]
          have ihm := ih m (by omega)
          omega

The work read from the executable merge sort is monotone in input size.

theorem mergeSortWork_monotone : Monotone mergeSortWork :=
  monotone_nat_of_le_succ mergeSortWork_le_succ

The real-valued view of the execution work satisfies the all-input absolute-value monotonicity interface.

theorem mergeSortWork_monotoneAbs :
    Chapter04.MonotoneAbs (fun n => (mergeSortWork n : Real)) :=
  Chapter04.monotoneAbs_natCast mergeSortWork_monotone

The work counter of the executable merge sort is Theta(n log n) on all natural input lengths.

theorem mergeSortWork_isBigTheta_nlogn :
    Chapter03.isBigTheta (fun n => (mergeSortWork n : Real))
      (fun n => (n : Real) * Real.log (n : Real)) := by
  exact MergeSortRecurrence.theta_n_log_n_all_inputs
    (fun n => (mergeSortWork n : Real))
    mergeSortWork_recurrence
    (by norm_num)
    mergeSortWork_monotoneAbs

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.MergeSort.Definitions

CLRS Section 2.3 - Executable costed merge sort

This module defines the textbook split--recurse--merge execution. Unlike the compatibility mergeSort wrapper, its combine step is the Chapter 2 mergeWithCost whose correctness and counters are proved locally.

namespace CLRSnamespace Chapter02

Observable result and accumulated counters of one merge-sort execution.

Textbook recurrence work: one unit at a singleton leaf and one unit for every output written by a combine call.

structure MergeSortExecution where
  value : List Nat
  comparisons : Nat
  outputWrites : Nat

  work : Nat
deriving DecidableEq, Repr

Executable merge sort using the verified local mergeWithCost at every combine node.

Inputs of length at least two are split after length / 2 elements. Both halves are strictly shorter, so input length is a termination measure.

def mergeSortWithCost : List Nat → MergeSortExecution
  | [] => ⟨[], 0, 0, 0⟩
  | [x] => ⟨[x], 0, 0, 1⟩
  | x :: y :: rest =>
      let input := x :: y :: rest
      let middle := input.length / 2
      let leftRun := mergeSortWithCost (input.take middle)
      let rightRun := mergeSortWithCost (input.drop middle)
      let combined := mergeWithCost leftRun.value rightRun.value
      ⟨combined.value,
        leftRun.comparisons + rightRun.comparisons + combined.comparisons,
        leftRun.outputWrites + rightRun.outputWrites + combined.outputWrites,
        leftRun.work + rightRun.work + combined.outputWrites⟩
termination_by input => input.length
decreasing_by
  all_goals
    simp_wf
    omega

Value-only projection of the executable merge-sort run.

def mergeSortValue (xs : List Nat) : List Nat :=
  (mergeSortWithCost xs).value

Work extracted from the execution on a canonical list of length n.

def mergeSortWork (n : Nat) : Nat :=
  (mergeSortWithCost (List.replicate n 0)).work

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.Merge_Sort_Recurrence

CLRS §2.3 — Merge Sort Recurrence and Θ(n log n) Bound

This file formalizes the merge sort recurrence from CLRS §2.3:

T(n) = T(⌊n/2⌋) + T(⌈n/2⌉) + Θ(n)

and proves the tight asymptotic bound T(n) = Θ(n log n) for all input sizes. The exact-power bound T(2^i) = Θ((i+1)·2^i) comes from the Master Theorem; theta_n_log_n_all_inputs extends it to every natural input through the Chapter 4 §4.6 floor/ceiling sandwich bridge.

Approach

The recurrence is stated for arbitrary input sizes using natural-number floor/ceiling division. On exact powers of two (n = 2^k) the recurrence collapses to the standard divide-and-conquer form

T(2^(k+1)) = 2·T(2^k) + 2^(k+1),

which is exactly the Master Theorem pattern with a = b = 2 and f(n) = n. The Chapter 4 Master Theorem (case 2: constant normalized forcing) then yields T(2^k) = Θ((k+1)·2^k), i.e. T(n) = Θ(n log n).

We intentionally place this material in a separate sub-namespace CLRS.Chapter02.MergeSortRecurrence to avoid name conflicts with the existing mergeSort definition and its correctness theorems in CLRS.Chapter02 (Section023DesigningAlgorithms.lean).

References

The verified merge sort implementation: CLRS.Chapter02.mergeSort
The power-of-two closed form: CLRS.Chapter02.mergeSortRecurrenceOnPowersOfTwo_closedForm
The Master Theorem: CLRS.Chapter04.master_case2_constant_forcing

Known simplifications

theta_n_log_n_all_inputs requires MonotoneAbs T (monotonicity of the absolute value of the cost function). The CLRS textbook does not state this condition explicitly, but it is a reasonable implicit assumption for a running-time function: larger inputs should not cost less than smaller ones.

              namespace CLRSnamespace Chapter02namespace MergeSortRecurrence

The recurrence relation

The merge sort recurrence from CLRS §2.3, expressed for an arbitrary cost function T : ℕ → ℝ.

For n ≥ 2: T(n) = T(⌊n/2⌋) + T(⌈n/2⌉) + n

Natural-number division n / 2 gives ⌊n/2⌋ and (n+1) / 2 gives ⌈n/2⌉. The additive term (n : ℝ) stands for the linear-time merge step; the Θ-annotation absorbs constant factors that are irrelevant for the asymptotic analysis.

Base cases T(0) and T(1) are left unspecified by this predicate — clients supply them when instantiating a concrete cost function.

def Recurrence (T : ℕ → ℝ) : Prop :=
  ∀ n, 2 ≤ n → T n = T (n / 2) + T ((n + 1) / 2) + (n : ℝ)

Reduction to the Master Theorem form on exact powers

On exact powers of two, the merge sort recurrence simplifies to the standard divide-and-conquer equation required by the Master Theorem.

For n = 2^(k+1) we have n/2 = (n+1)/2 = 2^k, so the two recursive calls merge into one doubled term.


theorem recurrence_on_exact_power (T : ℕ → ℝ) (hRec : Recurrence T) (k : ℕ) :
    T (2 ^ (k + 1)) = (2 : ℝ) * T (2 ^ k) + ((2 ^ (k + 1) : ℕ) : ℝ) := by
  have hn : 2 ≤ 2 ^ (k + 1) := by
    simpa using Nat.pow_le_pow_right (by norm_num : 0 < 2) (by omega : 1 ≤ k + 1)
  have h := hRec (2 ^ (k + 1)) hn
  have hdiv : 2 ^ (k + 1) / 2 = 2 ^ k := by omega
  have hceil : (2 ^ (k + 1) + 1) / 2 = 2 ^ k := by omega
  simp [hdiv, hceil] at h
  simpa [two_mul, Nat.cast_add, Nat.cast_pow, Nat.cast_ofNat] using h

The merge sort recurrence on exact powers satisfies the Chapter 4 ExactPowerRecurrence structure with a = 2, b = 2, f(n) = n.

theorem exactPowerRecurrence_instance (T : ℕ → ℝ) (hRec : Recurrence T) :
    Chapter04.ExactPowerRecurrence 2 2 (fun n : ℕ => (n : ℝ)) T :=
  ⟨fun i => by
    simpa [Nat.cast_pow] using recurrence_on_exact_power T hRec i⟩

Θ(n log n) bound via the Master Theorem

The normalized forcing term for merge sort is identically 1.

With a = b = 2 and f(n) = n, we have

f(b^(k+1)) / a^(k+1) = 2^(k+1) / 2^(k+1) = 1.

This means the Master Theorem's case 2 applies: the forcing is trapped between positive constants (here, exactly 1), giving T(2^k) = Θ((k+1)·2^k).

lemma normalizedForcing_merge_sort (k : ℕ) :
    Chapter04.normalizedForcing 2 2 (fun n : ℕ => (n : ℝ)) k = (1 : ℝ) := by
  dsimp [Chapter04.normalizedForcing]
  simp [Nat.cast_pow]

Merge sort runs in Θ(n log n) time on exact powers of two.

Formally, for any cost function T satisfying the textbook recurrence with T(1) > 0 and nonnegative values, the sequence n ↦ T(2^k) is Θ(k ↦ (k+1)·2^k). Since 2^k = n and k = log₂ n, this is exactly the textbook statement T(n) = Θ(n log n).


theorem theta_n_log_n_on_exact_powers (T : ℕ → ℝ) (hRec : Recurrence T)
    (hT1 : 0 < T 1) :
    Chapter03.isBigTheta
      (fun k : ℕ => T (2 ^ k))
      (fun k : ℕ => ((k : ℝ) + 1) * ((2 : ℝ) ^ k)) := by
  have h_rec_mt : Chapter04.ExactPowerRecurrence 2 2 (fun n : ℕ => (n : ℝ)) T :=
    exactPowerRecurrence_instance T hRec
  have ha_pos : 0 < (2 : ℝ) := by norm_num
  have h_base_nonneg : 0 ≤ Chapter04.normalizedValue 2 2 T 0 := by
    simpa [Chapter04.normalizedValue] using hT1.le
  have h_forcing_eq (k : ℕ) : Chapter04.normalizedForcing 2 2 (fun n : ℕ => (n : ℝ)) k = (1 : ℝ) :=
    normalizedForcing_merge_sort k
  have h_term_lower : ∀ k, (1 : ℝ) ≤ Chapter04.normalizedForcing 2 2 (fun n : ℕ => (n : ℝ)) k := by
    intro k; rw [h_forcing_eq k]
  have h_term_upper : ∀ k, Chapter04.normalizedForcing 2 2 (fun n : ℕ => (n : ℝ)) k ≤ (1 : ℝ) := by
    intro k; rw [h_forcing_eq k]
  exact Chapter04.master_case2_constant_forcing 2 2 (fun n : ℕ => (n : ℝ)) T
    h_rec_mt ha_pos h_base_nonneg (by norm_num) (by norm_num) h_term_lower h_term_upper

All-input Θ(n log n) bound

On an exact power of two the discrete case-2 scale (⌊log₂ n⌋ + 1)·2^(⌊log₂ n⌋) collapses to (i+1)·2^i.


lemma exactPower_scale_eq_criticalPowerLogScale (i : ℕ) :
    ((i : ℝ) + 1) * ((2 : ℝ) ^ i) = Chapter04.criticalPowerLogScale 2 2 (2 ^ i) := by
  rw [Chapter04.criticalPowerLogScale_exactPower 2 2 i (by norm_num : (1 : ℕ) < 2)]
  norm_num

For a = b = 2 the textbook case-2 scale n^(log₂2)·log n is exactly n·log n.


lemma realLogLogScale_two_two (n : ℕ) :
    Chapter04.realLogLogScale 2 2 n = (n : ℝ) * Real.log (n : ℝ) := by
  unfold Chapter04.realLogLogScale Chapter04.realLogScale Chapter04.realLogExponent
  have hlog2_pos : 0 < Real.log ((2 : ℕ) : ℝ) := by
    exact Real.log_pos (by norm_num : (1 : ℝ) < ((2 : ℕ) : ℝ))
  have hlog2_ne : Real.log ((2 : ℕ) : ℝ) ≠ 0 := ne_of_gt hlog2_pos
  have hexp : Real.log ((2 : ℕ) : ℝ) / Real.log ((2 : ℕ) : ℝ) = 1 := by
    rw [div_self hlog2_ne]
  rw [hexp]
  simp

Merge sort is Θ(n log n) for all input sizes (CLRS §2.3).

For any cost function T satisfying the merge-sort recurrence on every input, with T(1) > 0 and T monotone in absolute value, T is Θ(n·log n).

This extends theta_n_log_n_on_exact_powers from exact powers of two to every natural input using the Chapter 4 §4.6 all-input Master-theorem bridge: the exact-power bound T(2^i) = Θ((i+1)·2^i) is transferred to all inputs through the discrete log scale (⌊log₂ n⌋+1)·2^(⌊log₂ n⌋), which is then identified with n·log n.


theorem theta_n_log_n_all_inputs (T : ℕ → ℝ)
    (hRec : Recurrence T) (hT1 : 0 < T 1)
    (hT_mono : Chapter04.MonotoneAbs T) :
    Chapter03.isBigTheta T (fun n : ℕ => (n : ℝ) * Real.log (n : ℝ)) := by
  have h_power : Chapter03.isBigTheta
      (fun i : ℕ => T (2 ^ i))
      (fun i : ℕ => Chapter04.criticalPowerLogScale 2 2 (2 ^ i)) := by
    convert theta_n_log_n_on_exact_powers T hRec hT1 using 1
    funext i
    exact (exactPower_scale_eq_criticalPowerLogScale i).symm
  have h_all : Chapter03.isBigTheta T (Chapter04.criticalPowerLogScale 2 2) :=
    Chapter04.allInput_bigTheta_of_powerStep 2 T (Chapter04.criticalPowerLogScale 2 2)
      (by norm_num : (1 : ℕ) < 2)
      hT_mono
      (Chapter04.criticalPowerLogScale_monotoneAbs 2 2 (by norm_num : (1 : ℕ) ≤ 2))
      (Chapter04.criticalPowerLogScale_powerStepBound 2 2 (by norm_num : (1 : ℕ) ≤ 2)
        (by norm_num : (1 : ℕ) < 2))
      h_power
  have h_scale : Chapter03.isBigTheta
      (Chapter04.criticalPowerLogScale 2 2) (Chapter04.realLogLogScale 2 2) :=
    Chapter04.criticalPowerLogScale_isBigTheta_realLogLogScale 2 2
      (by norm_num : (1 : ℕ) ≤ 2) (by norm_num : (1 : ℕ) < 2)
  have h_loglog : Chapter03.isBigTheta T (Chapter04.realLogLogScale 2 2) :=
    Chapter03.isBigTheta_trans h_all h_scale
  have h_eq_scale : Chapter03.isBigTheta
      (Chapter04.realLogLogScale 2 2) (fun n : ℕ => (n : ℝ) * Real.log (n : ℝ)) := by
    convert Chapter03.isBigTheta_refl (fun n : ℕ => (n : ℝ) * Real.log (n : ℝ)) using 1
    funext n
    exact realLogLogScale_two_two n
  exact Chapter03.isBigTheta_trans h_loglog h_eq_scale

Connection to existing results

The existing CLRS.Chapter02.mergeSortRecurrenceOnPowersOfTwo_closedForm already proves the exact closed form T(2^k) = (k+1)·2^k for the power-of-two recurrence. The result above recovers the same asymptotic bound (Θ(n log n)) from the general recurrence using the Master Theorem, without computing the exact closed form.

The all-input bound theta_n_log_n_all_inputs now extends this from exact powers of two to every natural input size, using the Chapter 4 §4.6 floor/ceiling sandwich bridge.

              end MergeSortRecurrenceend Chapter02end CLRS