Chapter 2 — Getting Started

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import Mathlib

2.1. Insertion Sort

This file is the first Chapter 2 workflow slice. It formalizes a functional version of insertion sort and proves the two correctness facts that correspond to the textbook argument:

the result is ordered;
the result is a permutation of the input.

The CLRS pseudocode is array-based and is usually justified by a loop invariant. Here we use a recursive list algorithm, because it exposes the same invariant as small structural lemmas: inserting into an ordered list keeps it ordered, and it does not change the multiset of elements.

Known simplifications

The algorithm uses immutable List Nat instead of a mutable array, with 0-based indexing instead of the 1-based arrays in CLRS §2.1.
No explicit length parameter n — the list length is implicit in the type.
The loop invariant is not stated as an independent theorem; it is decomposed into insertSorted_ordered and insertSorted_perm, which together prove the same correctness property.

namespace CLRSnamespace Chapter02

Every element of xs is at least lower.

def AllLe (lower : Nat) (xs : List Nat) : Prop :=
  ∀ x ∈ xs, lower ≤ x

A compact sortedness predicate for lists of natural numbers.

def Ordered : List Nat → Prop
  | [] => True
  | [_] => True
  | x :: y :: ys => x ≤ y ∧ Ordered (y :: ys)

Insert an element into an already ordered list.

def insertSorted (x : Nat) : List Nat → List Nat
  | [] => [x]
  | y :: ys =>
      if x ≤ y then
        x :: y :: ys
      else
        y :: insertSorted x ys

Functional insertion sort over lists.

def insertionSort : List Nat → List Nat
  | [] => []
  | x :: xs => insertSorted x (insertionSort xs)

              theorem ordered_tail {x : Nat} {xs : List Nat}
    (h : Ordered (x :: xs)) : Ordered xs := by
  cases xs with
  | nil =>
      trivial
  | cons y ys =>
      exact h.2theorem ordered_allLe_tail {x : Nat} {xs : List Nat}
    (h : Ordered (x :: xs)) : AllLe x xs := by
  induction xs generalizing x with
  | nil =>
      intro y hy
      simp at hy
  | cons y ys ih =>
      intro z hz
      simp at hz
      rcases hz with rfl | hz
      · exact h.1
      · exact Nat.le_trans h.1 (ih h.2 z hz)theorem ordered_cons_of_allLe {x : Nat} {xs : List Nat}
    (hxs : Ordered xs) (hall : AllLe x xs) : Ordered (x :: xs) := by
  cases xs with
  | nil =>
      trivial
  | cons y ys =>
      exact ⟨hall y (by simp), hxs⟩theorem allLe_insertSorted {lower x : Nat} {xs : List Nat}
    (hx : lower ≤ x) (hxs : AllLe lower xs) :
    AllLe lower (insertSorted x xs) := by
  induction xs with
  | nil =>
      simpa [AllLe, insertSorted] using hx
  | cons head tail ih =>
      by_cases hxhead : x ≤ head
      · simp [AllLe, insertSorted, hxhead] at hxs ⊢
        exact ⟨hx, hxs⟩
      · simp [AllLe, insertSorted, hxhead] at hxs ⊢
        exact ⟨hxs.1, ih hxs.2⟩

Inserting into an ordered list keeps it ordered.

theorem insertSorted_ordered {x : Nat} {xs : List Nat}
    (hxs : Ordered xs) : Ordered (insertSorted x xs) := by
  induction xs with
  | nil =>
      trivial
  | cons y ys ih =>
      by_cases hxy : x ≤ y
      · simpa [insertSorted, hxy, Ordered] using
          (And.intro hxy hxs : x ≤ y ∧ Ordered (y :: ys))
      · have hyx : y ≤ x := Nat.le_of_lt (Nat.lt_of_not_ge hxy)
        have htail : Ordered ys := ordered_tail hxs
        have hordered_insert : Ordered (insertSorted x ys) := ih htail
        have hall_tail : AllLe y ys := ordered_allLe_tail hxs
        have hall_insert : AllLe y (insertSorted x ys) :=
          allLe_insertSorted hyx hall_tail
        simpa [insertSorted, hxy] using
          ordered_cons_of_allLe hordered_insert hall_insert

Inserting into a list preserves the input elements up to permutation.

theorem insertSorted_perm (x : Nat) (xs : List Nat) :
    (insertSorted x xs).Perm (x :: xs) := by
  induction xs with
  | nil =>
      simp [insertSorted]
  | cons y ys ih =>
      by_cases hxy : x ≤ y
      · simp [insertSorted, hxy]
      · simpa [insertSorted, hxy] using
          (List.Perm.cons y ih).trans (List.Perm.swap y x ys).symm

Insertion sort returns an ordered list.

theorem insertionSort_sorted (xs : List Nat) : Ordered (insertionSort xs) := by
  induction xs with
  | nil =>
      trivial
  | cons x xs ih =>
      exact insertSorted_ordered ih

Insertion sort preserves the input elements up to permutation.

theorem insertionSort_perm (xs : List Nat) :
    (insertionSort xs).Perm xs := by
  induction xs with
  | nil =>
      simp [insertionSort]
  | cons x xs ih =>
      exact (insertSorted_perm x (insertionSort xs)).trans (List.Perm.cons x ih)

end Chapter02end CLRS

Imports

import Mathlib
import CLRSLean.FourthEdition.Chapter_02.Section_02_1_Insertion_Sort
import CLRSLean.FourthEdition.Chapter_02.Section_02_2_Analyzing_Algorithms.LineCost

2.2. Analyzing Algorithms

This file records the Chapter 2 cost models. The line-cost development assigns the textbook constants c₁, c₂, and c₄--c₈, derives the execution count of every charged pseudocode line from supplied symbolic counts tᵢ, and proves the full seven-term equation for T(n). Its best- and worst-case specializations are exact substitutions into that table; these parameters are not extracted from an input execution.

The recursive comparison counter is bounded on every input by insertionSortComparisons_le_worst. The explicit descending family insertionSortWorstInput attains that bound at every size, including zero. insertionSortWorstComparisons_isGreatest identifies the size formula with the maximum of actual length-n comparison counts, and insertionSortComparisons_worst_case_theta combines this connection with Θ(n²). Already-sorted input has exactly n-1 comparisons and the existing Θ(n) bound.

A ThetaBoundedBy predicate packages the O and Ω directions into a single Θ-notation claim, matching the textbook's asymptotic language in §2.2.

Known simplifications

EventuallyBoundedBy is an O-notation upper-bound predicate; the textbook uses Θ-notation (both upper and lower bounds) in §2.2. The ThetaBoundedBy wrapper combines both directions to recover the Θ claim. insertionSortComparisons_worst_case_theta connects the worst-case Θ(n²) formula to the attained maximum of actual runs; the best-case Θ(n) bound is insertionSortBestComparisons_theta_linear.
The line-cost table is a symbolic unit-cost model. It accounts for the for-loop test, assignments, while-loop tests, shifts, and decrements, but it is not an operational word-RAM or mutable-array semantics. No validity predicate asserts that every supplied tᵢ sequence is a realizable trace.
Discursive content (why worst-case analysis is preferred, RAM-model instruction set enumeration) is not formalized — this is a reasonable omission for a theorem-oriented companion.
Nat subtraction truncates to 0 when n = 0, so triangular (n - 1) gives triangular 0 = 0 for n = 0, which is consistent with the textbook convention of zero comparisons for an empty input.

Implementation details

Line-cost facade (definitions, formula, best/worst cases)

namespace CLRSnamespace Chapter02

A small eventual upper-bound predicate for chapter-level runtime claims.

def EventuallyBoundedBy (f g : Nat → Nat) : Prop :=
  ∃ c n₀, 0 < c ∧ ∀ n, n₀ ≤ n → f n ≤ c * g n

A Θ-notation predicate: f ∈ Θ(g) when both f ∈ O(g) and g ∈ O(f), i.e. f is asymptotically tightly bounded by g up to constant factors.

def ThetaBoundedBy (f g : Nat → Nat) : Prop :=
  EventuallyBoundedBy f g ∧ EventuallyBoundedBy g f

The usual worst-case comparison count for insertion sort on n elements.

def insertionSortWorstComparisons (n : Nat) : Nat :=
  triangular (n - 1)

              theorem triangular_le_square (n : Nat) : triangular n ≤ n * n := by
  induction n with
  | zero =>
      simp [triangular]
  | succ n ih =>
      simp [triangular]
      nlinariththeorem insertionSortWorstComparisons_quadratic (n : Nat) :
    insertionSortWorstComparisons n ≤ n * n := by
  unfold insertionSortWorstComparisons
  exact (triangular_le_square (n - 1)).trans (by nlinarith [Nat.sub_le n 1])theorem insertionSortWorstComparisons_eventually_quadratic :
    EventuallyBoundedBy insertionSortWorstComparisons (fun n => n * n) := by
  refine ⟨1, 0, by decide, ?_⟩
  intro n _hn
  simpa using insertionSortWorstComparisons_quadratic n

Ω(n²) worst-case lower bound (CLRS §2.2)

The closed-form formula for the triangular sum: triangular n * 2 = n * (n + 1).


theorem triangular_eq_mul_two (n : Nat) : triangular n * 2 = n * (n + 1) := by
  induction n with
  | zero =>
      simp [triangular]
  | succ n ih =>
      simp [triangular]
      rw [add_mul, ih]
      nlinarith

Ω(n²) lower bound for the triangular sum (CLRS §2.2 worst-case analysis).

For n ≥ 2, triangular (n - 1) ≥ n² / 4. Reformulated as n² ≤ 4 · triangular (n - 1) to stay in Nat arithmetic.

This is the key ingredient that, together with the quadratic upper bound insertionSortWorstComparisons_quadratic, establishes the tight Θ(n²) worst-case comparison count for insertion sort.


theorem triangular_ge_quarter_square (n : Nat) (hn : 2 ≤ n) : n * n ≤ 4 * triangular (n - 1) := by
  have h_eq := triangular_eq_mul_two (n - 1)
  -- h_eq : triangular (n - 1) * 2 = (n - 1) * ((n - 1) + 1)
  -- Since n ≥ 2, (n - 1) + 1 = n
  have h_n_sub : (n - 1) + 1 = n := by omega
  have h_simp : triangular (n - 1) * 2 = (n - 1) * n := by
    rw [h_n_sub] at h_eq
    exact h_eq
  have h4 : 4 * triangular (n - 1) = 2 * ((n - 1) * n) := by
    calc
      4 * triangular (n - 1) = 2 * (2 * triangular (n - 1)) := by omega
      _ = 2 * (triangular (n - 1) * 2) := by rw [Nat.mul_comm 2 (triangular (n - 1))]
      _ = 2 * ((n - 1) * n) := by rw [h_simp]
  rw [h4]
  have h_bound : n ≤ 2 * (n - 1) := by omega
  have : n * n ≤ (2 * (n - 1)) * n := Nat.mul_le_mul h_bound (le_refl n)
  simpa [Nat.mul_assoc] using this

The Ω(n²) lower bound for the worst-case comparison count of insertion sort.

theorem insertionSortWorstComparisons_quadratic_lower (n : Nat) (hn : 2 ≤ n) :
    n * n ≤ 4 * insertionSortWorstComparisons n := by
  unfold insertionSortWorstComparisons
  exact triangular_ge_quarter_square n hn

The worst-case comparison count of insertion sort is Ω(n²).

theorem insertionSortWorstComparisons_eventually_quadratic_lower :
    EventuallyBoundedBy (fun n => n * n) insertionSortWorstComparisons := by
  refine ⟨4, 2, by decide, ?_⟩
  intro n hn
  exact insertionSortWorstComparisons_quadratic_lower n hn

Θ(n²) worst-case bound for insertion sort (CLRS §2.2).

The tight asymptotic bound is obtained by combining the O(n²) upper bound insertionSortWorstComparisons_eventually_quadratic with the Ω(n²) lower bound insertionSortWorstComparisons_eventually_quadratic_lower.

theorem insertionSortWorstComparisons_theta_quadratic :
    ThetaBoundedBy insertionSortWorstComparisons (fun n => n * n) := by
  refine ⟨insertionSortWorstComparisons_eventually_quadratic,
           insertionSortWorstComparisons_eventually_quadratic_lower⟩

Best-case analysis (CLRS §2.2, eq. (2.1))

The number of comparisons made by insertSorted x xs.

def insertSortedComparisons (x : Nat) : List Nat → Nat
  | [] => 0
  | y :: ys => 1 + (if x ≤ y then 0 else insertSortedComparisons x ys)

The number of comparisons made by insertionSort xs.

def insertionSortComparisons : List Nat → Nat
  | [] => 0
  | x :: xs => insertSortedComparisons x (insertionSort xs) + insertionSortComparisons xs

Attained worst-case count of actual comparison runs

Inserting into a list makes at most one comparison per existing element.

theorem insertSortedComparisons_le_length (x : Nat) (xs : List Nat) :
    insertSortedComparisons x xs ≤ xs.length := by
  induction xs with
  | nil => simp [insertSortedComparisons]
  | cons y ys ih =>
      simp only [insertSortedComparisons, List.length_cons]
      split <;> omega

The triangular worst-case budget grows by the previous input length.

theorem insertionSortWorstComparisons_succ (n : Nat) :
    insertionSortWorstComparisons (n + 1) =
      n + insertionSortWorstComparisons n := by
  cases n with
  | zero => simp [insertionSortWorstComparisons, triangular]
  | succ n => simp [insertionSortWorstComparisons, triangular]; omega

Every actual insertion-sort comparison count is bounded by the size budget.


theorem insertionSortComparisons_le_worst (xs : List Nat) :
    insertionSortComparisons xs ≤ insertionSortWorstComparisons xs.length := by
  induction xs with
  | nil => simp [insertionSortComparisons, insertionSortWorstComparisons, triangular]
  | cons x xs ih =>
      have h := insertSortedComparisons_le_length x (insertionSort xs)
      have hlen := (insertionSort_perm xs).length_eq
      rw [insertionSortComparisons, List.length_cons, insertionSortWorstComparisons_succ]
      omega

An explicit worst-case family: the distinct keys n-1, ..., 0.

def insertionSortWorstInput : Nat → List Nat
  | 0 => []
  | n + 1 => n :: insertionSortWorstInput n

@[simp] theorem insertionSortWorstInput_length (n : Nat) :
    (insertionSortWorstInput n).length = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [insertionSortWorstInput, ih]

private theorem mem_insertionSortWorstInput_lt {n x : Nat}
    (hx : x ∈ insertionSortWorstInput n) : x < n := by
  induction n with
  | zero => simp [insertionSortWorstInput] at hx
  | succ n ih =>
      simp only [insertionSortWorstInput, List.mem_cons] at hx
      rcases hx with rfl | hx
      · omega
      · exact Nat.lt_succ_of_lt (ih hx)

A key larger than every existing element forces a full insertion scan.


theorem insertSortedComparisons_eq_length_of_forall_lt (x : Nat) (xs : List Nat)
    (h : ∀ y ∈ xs, y < x) : insertSortedComparisons x xs = xs.length := by
  induction xs with
  | nil => rfl
  | cons y ys ih =>
      have hxy : ¬x ≤ y := Nat.not_le.mpr (h y (by simp))
      have htail : ∀ z ∈ ys, z < x := fun z hz => h z (by simp [hz])
      simp [insertSortedComparisons, hxy, ih htail, Nat.add_comm]

The descending family attains the worst-case budget at every size.


theorem insertionSortComparisons_worst_input (n : Nat) :
    insertionSortComparisons (insertionSortWorstInput n) =
      insertionSortWorstComparisons n := by
  induction n with
  | zero => simp [insertionSortWorstInput, insertionSortComparisons,
      insertionSortWorstComparisons, triangular]
  | succ n ih =>
      have hall : ∀ y ∈ insertionSort (insertionSortWorstInput n), y < n := by
        intro y hy
        exact mem_insertionSortWorstInput_lt
          ((insertionSort_perm (insertionSortWorstInput n)).mem_iff.mp hy)
      have hscan := insertSortedComparisons_eq_length_of_forall_lt n
        (insertionSort (insertionSortWorstInput n)) hall
      have hlen := (insertionSort_perm (insertionSortWorstInput n)).length_eq
      rw [insertionSortWorstInput, insertionSortComparisons, hscan, hlen,
        insertionSortWorstInput_length, ih, insertionSortWorstComparisons_succ]

The size formula is the attained maximum of actual length-n run counts.

theorem insertionSortWorstComparisons_isGreatest (n : Nat) : IsGreatest
    {c | ∃ xs : List Nat, xs.length = n ∧ insertionSortComparisons xs = c}
    (insertionSortWorstComparisons n) := by
  constructor
  · exact ⟨insertionSortWorstInput n, insertionSortWorstInput_length n,
      insertionSortComparisons_worst_input n⟩
  · rintro c ⟨xs, hlen, rfl⟩
    simpa [hlen] using insertionSortComparisons_le_worst xs

Actual worst-case comparison counts have the proved quadratic Theta bound.

theorem insertionSortComparisons_worst_case_theta :
    (∀ n, IsGreatest
      {c | ∃ xs : List Nat, xs.length = n ∧ insertionSortComparisons xs = c}
      (insertionSortWorstComparisons n)) ∧
    ThetaBoundedBy insertionSortWorstComparisons (fun n => n * n) :=
  ⟨insertionSortWorstComparisons_isGreatest,
    insertionSortWorstComparisons_theta_quadratic⟩

lemma allLe_of_perm {x : Nat} {xs ys : List Nat} (h_perm : xs.Perm ys) (h_allLe : AllLe x xs) :
    AllLe x ys := by
  intro y hy
  have hy' : y ∈ xs := h_perm.symm.mem_iff.mp hy
  exact h_allLe y hy'

Best-case comparison count for insertion sort (CLRS eq. (2.1)).

When the input list is already sorted, insertion sort makes exactly n - 1 comparisons, where n is the length of the input. This is the linear best case described in the textbook.


theorem insertionSortComparisons_best_case (xs : List Nat) (h_ordered : Ordered xs) :
    insertionSortComparisons xs = xs.length - 1 := by
  induction xs with
  | nil =>
      simp [insertionSortComparisons]
  | cons x xs ih =>
      have h_tail : Ordered xs := ordered_tail h_ordered
      have h_allLe : AllLe x xs := ordered_allLe_tail h_ordered
      have h_perm : (insertionSort xs).Perm xs := insertionSort_perm xs
      have h_allLe_sorted : AllLe x (insertionSort xs) :=
        allLe_of_perm h_perm.symm h_allLe
      have ih_eq := ih h_tail
      have h_len_perm : (insertionSort xs).length = xs.length := List.Perm.length_eq h_perm
      rw [insertionSortComparisons, List.length_cons, ih_eq]
      -- Goal: insertSortedComparisons x (insertionSort xs) + (xs.length - 1) = xs.length
      rcases h_ins : insertionSort xs with _ | ⟨y, ys⟩
      · -- insertionSort xs = []
        have h_len0 : xs.length = 0 := by
          simpa [h_ins] using h_len_perm.symm
        simp [insertSortedComparisons, h_len0]
      · -- insertionSort xs = y :: ys
        have h_mem : y ∈ (y :: ys) := by simp
        have h_allLe' : AllLe x (y :: ys) := by rwa [h_ins] at h_allLe_sorted
        have h_le : x ≤ y := h_allLe' y h_mem
        simp [insertSortedComparisons, h_le]
        have h_len_pos : 1 ≤ xs.length := by
          rw [h_ins] at h_len_perm
          simp at h_len_perm
          omega
        omega

The best-case comparison count as a function of input size n (CLRS eq. (2.1)).

def insertionSortBestComparisons (n : Nat) : Nat := n - 1

              try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`

theorem insertionSortBestComparisons_eventually_linear_upper :
    EventuallyBoundedBy insertionSortBestComparisons (fun n => n) := by
  refine ⟨1, 0, by decide, ?_⟩
  intro n _hn
  unfold insertionSortBestComparisons
  try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [Nat.one_mul] using Nat.sub_le n 1theorem insertionSortBestComparisons_eventually_linear_lower_aux (n : Nat) (hn : 2 ≤ n) : n ≤ 2 * (n - 1) := by
  omegatheorem insertionSortBestComparisons_eventually_linear_lower :
    EventuallyBoundedBy (fun n => n) insertionSortBestComparisons := by
  refine ⟨2, 2, by decide, ?_⟩
  intro n hn
  unfold insertionSortBestComparisons
  exact insertionSortBestComparisons_eventually_linear_lower_aux n hn

Θ(n) best-case bound for insertion sort (CLRS eq. (2.1)).

The tight asymptotic bound is obtained by combining the O(n) upper bound insertionSortBestComparisons_eventually_linear_upper with the Ω(n) lower bound insertionSortBestComparisons_eventually_linear_lower.

theorem insertionSortBestComparisons_theta_linear :
    ThetaBoundedBy insertionSortBestComparisons (fun n => n) := by
  refine ⟨insertionSortBestComparisons_eventually_linear_upper,
           insertionSortBestComparisons_eventually_linear_lower⟩

end Chapter02end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_02.Section_02_2_Analyzing_Algorithms.LineCost.BestWorst

CLRS Section 2.2 - Best- and worst-case line counts

This module specializes the generic cost table to the textbook traces tᵢ = 1 (already sorted input) and tᵢ = i (reverse-sorted input).

namespace CLRSnamespace Chapter02

Best-case while trace: each outer iteration tests the condition once.

def insertionSortBestTrace : Nat → Nat := fun _ => 1

Worst-case while trace: outer iteration i tests the condition i times.

def insertionSortWorstTrace : Nat → Nat := fun i => i

private theorem sum_range_succ_eq_triangular (m : Nat) :
    (∑ k ∈ Finset.range m, (k + 1)) = triangular m := by
  induction m with
  | zero => simp [triangular]
  | succ m ih =>
      simp [Finset.sum_range_succ, triangular, ih]

private theorem sum_range_add_two_eq (m : Nat) :
    (∑ k ∈ Finset.range m, (k + 2)) = triangular m + m := by
  induction m with
  | zero => simp [triangular]
  | succ m ih =>
      simp [Finset.sum_range_succ, triangular, ih]
      omega

The exact execution-count table for the already-sorted best case.

theorem insertionSortLineCounts_best_case (n : Nat) :
    insertionSortLineCounts n insertionSortBestTrace =
      { forLoopTests := n
        keyAssignments := n - 1
        indexInitializations := n - 1
        whileLoopTests := n - 1
        shifts := 0
        decrements := 0
        finalAssignments := n - 1 } := by
  ext <;>
    simp [insertionSortLineCounts, insertionSortWhileTestSum,
      insertionSortBodyIterationSum, insertionSortBestTrace]

The exact execution-count table for the reverse-sorted worst case.

theorem insertionSortLineCounts_worst_case (n : Nat) :
    insertionSortLineCounts n insertionSortWorstTrace =
      { forLoopTests := n
        keyAssignments := n - 1
        indexInitializations := n - 1
        whileLoopTests := triangular (n - 1) + (n - 1)
        shifts := triangular (n - 1)
        decrements := triangular (n - 1)
        finalAssignments := n - 1 } := by
  ext <;>
    simp [insertionSortLineCounts, insertionSortWhileTestSum,
      insertionSortBodyIterationSum, insertionSortWorstTrace,
      sum_range_succ_eq_triangular, sum_range_add_two_eq]

Complete best-case line-cost formula after substituting tᵢ = 1.


theorem insertionSortRunningTime_best_case
    (costs : InsertionSortLineCosts) (n : Nat) :
    insertionSortRunningTime costs n insertionSortBestTrace =
      costs.c₁ * n +
        costs.c₂ * (n - 1) +
        costs.c₄ * (n - 1) +
        costs.c₅ * (n - 1) +
        costs.c₈ * (n - 1) := by
  rw [insertionSortRunningTime, insertionSortLineCounts_best_case]
  simp [InsertionSortLineCosts.evaluate]

Complete worst-case line-cost formula after substituting tᵢ = i.


theorem insertionSortRunningTime_worst_case
    (costs : InsertionSortLineCosts) (n : Nat) :
    insertionSortRunningTime costs n insertionSortWorstTrace =
      costs.c₁ * n +
        costs.c₂ * (n - 1) +
        costs.c₄ * (n - 1) +
        costs.c₅ * (triangular (n - 1) + (n - 1)) +
        costs.c₆ * triangular (n - 1) +
        costs.c₇ * triangular (n - 1) +
        costs.c₈ * (n - 1) := by
  rw [insertionSortRunningTime, insertionSortLineCounts_worst_case]
  rfl

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_2_Analyzing_Algorithms.LineCost.Definitions

CLRS Section 2.2 - Insertion-sort line-cost definitions

This module represents the seven charged lines in the textbook insertion-sort cost table. The outer-loop index k ranges over 0, ..., n - 2 and corresponds to the textbook index i = k + 2. The parameter t supplies symbolic while-test counts; this module neither extracts it from an execution nor proves that arbitrary supplied counts are realizable.

namespace CLRSnamespace Chapter02

The triangular sum 1 + 2 + ... + n.

def triangular : Nat → Nat
  | 0 => 0
  | n + 1 => triangular n + (n + 1)

The symbolic costs attached to executable lines 1, 2, and 4--8.

@[ext] structure InsertionSortLineCosts where
  c₁ : Nat
  c₂ : Nat
  c₄ : Nat
  c₅ : Nat
  c₆ : Nat
  c₇ : Nat
  c₈ : Nat
deriving DecidableEq, Repr

The execution-count column of the CLRS insertion-sort cost table.

@[ext] structure InsertionSortLineCounts where
  forLoopTests : Nat
  keyAssignments : Nat
  indexInitializations : Nat
  whileLoopTests : Nat
  shifts : Nat
  decrements : Nat
  finalAssignments : Nat
deriving DecidableEq, Repr

Sum of the textbook tᵢ values for i = 2, ..., n.

def insertionSortWhileTestSum (n : Nat) (t : Nat → Nat) : Nat :=
  ∑ k ∈ Finset.range (n - 1), t (k + 2)

Sum of the loop-body counts tᵢ - 1 for i = 2, ..., n.

def insertionSortBodyIterationSum (n : Nat) (t : Nat → Nat) : Nat :=
  ∑ k ∈ Finset.range (n - 1), (t (k + 2) - 1)

Derive the symbolic seven-line table from size and supplied while-test counts.

def insertionSortLineCounts (n : Nat) (t : Nat → Nat) : InsertionSortLineCounts where
  forLoopTests := n
  keyAssignments := n - 1
  indexInitializations := n - 1
  whileLoopTests := insertionSortWhileTestSum n t
  shifts := insertionSortBodyIterationSum n t
  decrements := insertionSortBodyIterationSum n t
  finalAssignments := n - 1

Evaluate one symbolic cost row against one execution-count row.

def InsertionSortLineCosts.evaluate
    (costs : InsertionSortLineCosts) (counts : InsertionSortLineCounts) : Nat :=
  costs.c₁ * counts.forLoopTests +
    costs.c₂ * counts.keyAssignments +
    costs.c₄ * counts.indexInitializations +
    costs.c₅ * counts.whileLoopTests +
    costs.c₆ * counts.shifts +
    costs.c₇ * counts.decrements +
    costs.c₈ * counts.finalAssignments

Complete line-by-line running time for input size n and trace t.

def insertionSortRunningTime
    (costs : InsertionSortLineCosts) (n : Nat) (t : Nat → Nat) : Nat :=
  costs.evaluate (insertionSortLineCounts n t)

end Chapter02end CLRS

CLRSLean.FourthEdition.Chapter_02.Section_02_2_Analyzing_Algorithms.LineCost.Formula

CLRS Section 2.2 - The complete insertion-sort cost formula

The theorem in this module expands the cost-table evaluator into the seven terms displayed in the textbook analysis.

namespace CLRSnamespace Chapter02

The complete CLRS insertion-sort running-time equation:

T(n) = c₁ n + c₂ (n - 1) + c₄ (n - 1) + c₅ Σtᵢ + c₆ Σ(tᵢ - 1) + c₇ Σ(tᵢ - 1) + c₈ (n - 1).

theorem insertionSortRunningTime_eq_textbook_sum
    (costs : InsertionSortLineCosts) (n : Nat) (t : Nat → Nat) :
    insertionSortRunningTime costs n t =
      costs.c₁ * n +
        costs.c₂ * (n - 1) +
        costs.c₄ * (n - 1) +
        costs.c₅ * insertionSortWhileTestSum n t +
        costs.c₆ * insertionSortBodyIterationSum n t +
        costs.c₇ * insertionSortBodyIterationSum n t +
        costs.c₈ * (n - 1) := by
  rfl

end Chapter02end CLRS

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

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_02.Section_02_1_Insertion_Sort
import CLRSLean.FourthEdition.Chapter_02.Section_02_2_Analyzing_Algorithms
import CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms
import CLRSLean.FourthEdition.Chapter_02.Section_02_3_Designing_Algorithms.Merge_Sort_Recurrence

Current source

Sections 2.1--2.3 are native fourth-edition sections (insertion sort, analyzing algorithms, and designing algorithms), imported directly from Section 2.1, Section 2.2, and Section 2.3. Section 2.2 includes the full symbolic insertion-sort line-cost table and its best/worst symbolic specializations. The actual recursive comparison counter has a universal triangular upper bound and a descending input family attaining it at every size. insertionSortWorstComparisons_isGreatest and insertionSortComparisons_worst_case_theta expose this execution connection. Section 2.3 includes the explicit costed MERGE development, an executable recursive merge sort built from that MERGE, and execution-derived recurrence and asymptotic results. Declarations retain the CLRS.Chapter02 namespace during the compatibility period; the third-edition-numbered imports CLRSLean.Chapter_02 and CLRSLean.Chapter_02.Section_02_* forward to these sources.

Coverage boundary

Insertion sort and merge sort use immutable lists. Section 2.2's line costs are supplied symbolic parameters, not traces extracted from an input or operational word-RAM semantics. The comparison counter, separately, counts key comparisons of the functional recursion; it excludes list allocation and traversal overhead. Section 2.3 proves the executable recursive merge sort correct, identifies it with the compatibility API, and derives its all-input Theta(n log n) work bound. Temporary-array allocation remains outside the advertised boundary.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.

CLRS, fourth edition · Chapter 2 of 35