26.3. Parallel Merge Sort

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.S1_CostModel

CLRS Chapter 26 — Execution-Attached Work and Span

This module gives the parallel algorithms in §§26.2–26.3 a small executable cost layer. A computation carries its value together with exact natural-number work and span. Sequential composition adds both costs; balanced parallel composition adds work across branches, takes the maximum branch span, and charges one unit for each fork/join node.

The four-way and eight-way combinators use balanced binary trees. Their values therefore have shapes ((a, b), (c, d)) and (((a, b), (c, d)), ((e, f), (g, h))), respectively.

              namespace CLRSnamespace Chapter27universe u v

An executable value annotated with its exact work and span costs.

structure Costed (α : Type u) where
  value : α
  work : ℕ
  span : ℕ
deriving Repr, DecidableEq

namespace Costed

Lift a value without charging any work or span.

def pure (x : α) : Costed α := ⟨x, 0, 0⟩

Attach explicitly supplied work and span costs to a value.

def charge (work span : ℕ) (x : α) : Costed α := ⟨x, work, span⟩

Transform the result of a computation without changing its costs.

def map (f : α → β) (x : Costed α) : Costed β :=
  ⟨f x.value, x.work, x.span⟩

Run two computations sequentially, adding both work and span.

def seq (x : Costed α) (f : α → Costed β) : Costed β :=
  let y := f x.value
  ⟨y.value, x.work + y.work, x.span + y.span⟩

Run two independent computations in parallel.

The work is the sum of branch work plus one fork/join node. The span follows the slower branch and likewise includes the fork/join node.

def par (x : Costed α) (y : Costed β) : Costed (α × β) :=
  ⟨(x.value, y.value), x.work + y.work + 1, max x.span y.span + 1⟩

Balanced four-way parallel composition using three binary parallel nodes. The returned tuple has the explicit shape ((a, b), (c, d)).

def par4 (a b c d : Costed α) : Costed ((α × α) × (α × α)) :=
  par (par a b) (par c d)

Balanced eight-way parallel composition using seven binary parallel nodes. The returned tuple has the explicit shape (((a, b), (c, d)), ((e, f), (g, h))).

def par8 (a b c d e f g h : Costed α) :
    Costed (((α × α) × (α × α)) × ((α × α) × (α × α))) :=
  par (par4 a b c d) (par4 e f g h)

              @[simp] theorem pure_value (x : α) : (pure x).value = x := rfl@[simp] theorem pure_work (x : α) : (pure x).work = 0 := rfl@[simp] theorem pure_span (x : α) : (pure x).span = 0 := rfl@[simp] theorem charge_value (work span : ℕ) (x : α) :
    (charge work span x).value = x := rfl@[simp] theorem charge_work (work span : ℕ) (x : α) :
    (charge work span x).work = work := rfl@[simp] theorem charge_span (work span : ℕ) (x : α) :
    (charge work span x).span = span := rfl@[simp] theorem map_value (f : α → β) (x : Costed α) :
    (map f x).value = f x.value := rfl@[simp] theorem map_work (f : α → β) (x : Costed α) :
    (map f x).work = x.work := rfl@[simp] theorem map_span (f : α → β) (x : Costed α) :
    (map f x).span = x.span := rfl@[simp] theorem seq_value (x : Costed α) (f : α → Costed β) :
    (seq x f).value = (f x.value).value := by
  simp [seq]@[simp] theorem seq_work (x : Costed α) (f : α → Costed β) :
    (seq x f).work = x.work + (f x.value).work := by
  simp [seq]@[simp] theorem seq_span (x : Costed α) (f : α → Costed β) :
    (seq x f).span = x.span + (f x.value).span := by
  simp [seq]@[simp] theorem par_value (x : Costed α) (y : Costed β) :
    (par x y).value = (x.value, y.value) := rfl@[simp] theorem par_work (x : Costed α) (y : Costed β) :
    (par x y).work = x.work + y.work + 1 := rfl@[simp] theorem par_span (x : Costed α) (y : Costed β) :
    (par x y).span = max x.span y.span + 1 := rfl@[simp] theorem par4_value (a b c d : Costed α) :
    (par4 a b c d).value = ((a.value, b.value), (c.value, d.value)) := by
  rfl@[simp] theorem par4_work (a b c d : Costed α) :
    (par4 a b c d).work = a.work + b.work + c.work + d.work + 3 := by
  simp [par4]
  omega@[simp] theorem par4_span (a b c d : Costed α) :
    (par4 a b c d).span = max (max a.span b.span) (max c.span d.span) + 2 := by
  simp [par4]@[simp] theorem par8_value (a b c d e f g h : Costed α) :
    (par8 a b c d e f g h).value =
      (((a.value, b.value), (c.value, d.value)),
        ((e.value, f.value), (g.value, h.value))) := by
  rfl@[simp] theorem par8_work (a b c d e f g h : Costed α) :
    (par8 a b c d e f g h).work =
      a.work + b.work + c.work + d.work + e.work + f.work + g.work + h.work + 7 := by
  simp [par8]
  omega@[simp] theorem par8_span (a b c d e f g h : Costed α) :
    (par8 a b c d e f g h).span =
      max (max (max a.span b.span) (max c.span d.span))
          (max (max e.span f.span) (max g.span h.span)) + 3 := by
  simp [par8]end Costedend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.S2_Recurrences

26.2–26.3. Parallel Recurrences

This module defines the Chapter 26 main-text work/span recurrence models for P-MATMUL, P-MERGE, and P-MERGE-SORT, together with their exact power-of-two solutions.

              namespace CLRSnamespace Chapter27

private theorem pow_two_succ_eq (k : ℕ) : 2 ^ (k + 1) / 2 = 2 ^ k := by
  rw [pow_succ]
  omega

private theorem pow_two_succ_sub (k : ℕ) : 2 ^ (k + 1) - 2 ^ (k + 1) / 2 = 2 ^ k := by
  rw [pow_succ]
  omegaprivate theorem log_two_pow (k : ℕ) : Nat.log 2 (2 ^ k) = k :=
  Nat.log_pow (by norm_num) k

private theorem two_le_two_pow_succ (k : ℕ) : 2 ≤ 2 ^ (k + 1) := by
  rw [pow_succ]
  have := Nat.one_le_pow k 2 (by norm_num)
  omega

private theorem two_pow_succ_mul (k : ℕ) : 2 ^ (k + 1) * 2 ^ (k + 1) = 4 ^ (k + 1) := by
  have h42 : (4 : ℕ) = 2 ^ 2 := by norm_num
  rw [h42, ← pow_mul, ← pow_add]
  congr 1
  omega

§26.2: Parallel matrix multiplication (P-MATMUL)

Work recurrence for P-MATMUL: T₁(n) = 8 T₁(n/2) + n².

def pMatMulWork (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    8 * pMatMulWork (n / 2) + n * n
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)



theorem pMatMulWork_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMatMulWork n = 8 * pMatMulWork (n / 2) + n * n := by
  rw [pMatMulWork]
  simp [show ¬n ≤ 1 by omega]

Exact work on powers of two: T₁(2ᵏ) + 4ᵏ = 2·8ᵏ (work Θ(n³)).


theorem pMatMulWork_pow_two (k : ℕ) :
    pMatMulWork (2 ^ k) + 4 ^ k = 2 * 8 ^ k := by
  induction k with
  | zero => native_decide
  | succ k ih =>
      rw [pMatMulWork_unfold (two_le_two_pow_succ k), pow_two_succ_eq,
        two_pow_succ_mul]
      nlinarith [ih, pow_succ (4 : ℕ) k, pow_succ (8 : ℕ) k]

Span recurrence for P-MATMUL: T∞(n) = T∞(n/2) + 1.

def pMatMulSpan (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    pMatMulSpan (n / 2) + 1
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)



theorem pMatMulSpan_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMatMulSpan n = pMatMulSpan (n / 2) + 1 := by
  rw [pMatMulSpan]
  simp [show ¬n ≤ 1 by omega]

Exact span on powers of two: T∞(2ᵏ) = k + 1 (span Θ(log n)).


theorem pMatMulSpan_pow_two (k : ℕ) : pMatMulSpan (2 ^ k) = k + 1 := by
  induction k with
  | zero => native_decide
  | succ k ih =>
      rw [pMatMulSpan_unfold (two_le_two_pow_succ k), pow_two_succ_eq, ih]

§26.3: Parallel merge (P-MERGE)

Work recurrence for P-MERGE: two parallel recursive merges on the two halves plus a Θ(log n) binary-search combine, T₁(n) = T₁(⌊n/2⌋) + T₁(⌈n/2⌉) + (⌊log₂ n⌋ + 1).

def pMergeWork (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    pMergeWork (n / 2) + pMergeWork (n - n / 2) + (Nat.log 2 n + 1)
termination_by n
decreasing_by
  · exact Nat.div_lt_self (by omega) (by norm_num)
  · exact Nat.sub_lt (by omega) (Nat.div_pos (by omega) (by norm_num))



theorem pMergeWork_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMergeWork n =
      pMergeWork (n / 2) + pMergeWork (n - n / 2) + (Nat.log 2 n + 1) := by
  rw [pMergeWork]
  simp [show ¬n ≤ 1 by omega]

Exact work on powers of two: T₁(2ᵏ) + (k + 3) = 4·2ᵏ (work Θ(n)).


theorem pMergeWork_pow_two (k : ℕ) :
    pMergeWork (2 ^ k) + (k + 3) = 4 * 2 ^ k := by
  induction k with
  | zero =>
      rw [pMergeWork]
      norm_num
  | succ k ih =>
      rw [pMergeWork_unfold (two_le_two_pow_succ k), pow_two_succ_sub,
        pow_two_succ_eq, log_two_pow]
      nlinarith [ih, pow_succ (2 : ℕ) k]

Span recurrence for P-MERGE: the critical path follows the larger half, T∞(n) = T∞(⌈n/2⌉) + (⌊log₂ n⌋ + 1).

def pMergeSpan (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    pMergeSpan (n - n / 2) + (Nat.log 2 n + 1)
termination_by n
decreasing_by exact Nat.sub_lt (by omega) (Nat.div_pos (by omega) (by norm_num))



theorem pMergeSpan_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMergeSpan n = pMergeSpan (n - n / 2) + (Nat.log 2 n + 1) := by
  rw [pMergeSpan]
  simp [show ¬n ≤ 1 by omega]

Exact span on powers of two: 2·T∞(2ᵏ) = (k+1)(k+2) (span Θ(log² n)).


theorem pMergeSpan_pow_two (k : ℕ) :
    2 * pMergeSpan (2 ^ k) = (k + 1) * (k + 2) := by
  induction k with
  | zero =>
      rw [pMergeSpan]
      norm_num
  | succ k ih =>
      rw [pMergeSpan_unfold (two_le_two_pow_succ k), pow_two_succ_sub,
        log_two_pow]
      nlinarith [ih]

§26.3: Parallel merge sort (P-MERGE-SORT)

Work recurrence for P-MERGE-SORT: T₁(n) = T₁(⌊n/2⌋) + T₁(⌈n/2⌉) + n.

def pMergeSortWork (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    pMergeSortWork (n / 2) + pMergeSortWork (n - n / 2) + n
termination_by n
decreasing_by
  · exact Nat.div_lt_self (by omega) (by norm_num)
  · exact Nat.sub_lt (by omega) (Nat.div_pos (by omega) (by norm_num))



theorem pMergeSortWork_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMergeSortWork n = pMergeSortWork (n / 2) + pMergeSortWork (n - n / 2) + n := by
  rw [pMergeSortWork]
  simp [show ¬n ≤ 1 by omega]

Exact work on powers of two: T₁(2ᵏ) = 2ᵏ·(k+1) (work Θ(n log n)).


theorem pMergeSortWork_pow_two (k : ℕ) :
    pMergeSortWork (2 ^ k) = 2 ^ k * (k + 1) := by
  induction k with
  | zero =>
      rw [pMergeSortWork]
      norm_num
  | succ k ih =>
      rw [pMergeSortWork_unfold (two_le_two_pow_succ k), pow_two_succ_sub,
        pow_two_succ_eq]
      nlinarith [ih, pow_succ (2 : ℕ) k]

Span recurrence for P-MERGE-SORT: T∞(n) = T∞(⌈n/2⌉) + (P-MERGE span on n elements).

def pMergeSortSpan (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    pMergeSortSpan (n - n / 2) + pMergeSpan n
termination_by n
decreasing_by exact Nat.sub_lt (by omega) (Nat.div_pos (by omega) (by norm_num))



theorem pMergeSortSpan_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMergeSortSpan n = pMergeSortSpan (n - n / 2) + pMergeSpan n := by
  rw [pMergeSortSpan]
  simp [show ¬n ≤ 1 by omega]

Exact span on powers of two: 6·T∞(2ᵏ) = 6 + k·(k² + 6k + 11) (span Θ(log³ n)).


theorem pMergeSortSpan_pow_two (k : ℕ) :
    6 * pMergeSortSpan (2 ^ k) = 6 + k * (k * k + 6 * k + 11) := by
  induction k with
  | zero =>
      rw [pMergeSortSpan]
      norm_num
  | succ k ih =>
      rw [pMergeSortSpan_unfold (two_le_two_pow_succ k), pow_two_succ_sub]
      have hS := pMergeSpan_pow_two (k + 1)
      nlinarith [ih, hS]

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.S3_AllInputBounds

26.2–26.3. All-Input Bounds

This module lifts the Chapter 26 main-text exact power-of-two recurrence solutions to arbitrary positive inputs.

namespace CLRSnamespace Chapter27

All-input upper bound: T₁(n) + n² ≤ 2n³.


theorem pMatMulWork_le (n : ℕ) : pMatMulWork n + n * n ≤ 2 * n * n * n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n <;> native_decide
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv : 2 * m / 2 = m := by omega
          rw [pMatMulWork_unfold (by omega), hdiv]
          have ihm := ih m (by omega)
          nlinarith [ihm]
        · have hdiv : (2 * m + 1) / 2 = m := by omega
          rw [pMatMulWork_unfold (by omega), hdiv]
          have ihm := ih m (by omega)
          nlinarith [ihm]

All-input span bound: T∞(n) ≤ ⌊log₂ n⌋ + 1.


theorem pMatMulSpan_le (n : ℕ) : pMatMulSpan n ≤ Nat.log 2 n + 1 := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n <;> native_decide
      · rw [pMatMulSpan_unfold (by omega)]
        have ihm := ih (n / 2) (by omega)
        have hlog := Nat.log_div_base 2 n
        have hlogpos : 1 ≤ Nat.log 2 n :=
          Nat.le_log_of_pow_le (by norm_num) (by omega)
        omega

The P-MERGE work recurrence does not decrease at a successor step.


private theorem pMergeWork_le_succ : ∀ n, pMergeWork n ≤ pMergeWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n
        · rw [show pMergeWork 0 = 0 by rw [pMergeWork]; norm_num]
          exact Nat.zero_le _
        · have hone : pMergeWork 1 = 1 := by rw [pMergeWork]; norm_num
          rw [hone, pMergeWork_unfold (n := 2) (by norm_num)]
          norm_num [hone]
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          have hceil0 : 2 * m - 2 * m / 2 = m := by omega
          have hceil1 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          rw [pMergeWork_unfold (n := 2 * m) (by omega),
            pMergeWork_unfold (n := 2 * m + 1) (by omega),
            hceil0, hceil1, hdiv0, hdiv1]
          have ihm := ih m (by omega)
          have hlog : Nat.log 2 (2 * m) ≤ Nat.log 2 (2 * m + 1) :=
            Nat.log_mono_right (by omega)
          omega
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          have hceil0 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          have hceil1 : 2 * m + 1 + 1 - (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pMergeWork_unfold (n := 2 * m + 1) (by omega),
            pMergeWork_unfold (n := 2 * m + 1 + 1) (by omega),
            hceil0, hceil1, hdiv0, hdiv1]
          have ihm := ih m (by omega)
          have hlog : Nat.log 2 (2 * m + 1) ≤ Nat.log 2 (2 * m + 1 + 1) :=
            Nat.log_mono_right (by omega)
          omega

P-MERGE work is monotone in the input size.

theorem pMergeWork_monotone : Monotone pMergeWork :=
  monotone_nat_of_le_succ pMergeWork_le_succ

Every positive P-MERGE work cost lies between its adjacent power-of-two costs.

theorem pMergeWork_power_sandwich (n : ℕ) (hn : 0 < n) :
    pMergeWork (2 ^ Nat.log 2 n) ≤ pMergeWork n ∧
      pMergeWork n ≤ pMergeWork (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pMergeWork_monotone 2 n (by norm_num) hn.ne'

The P-MERGE span recurrence does not decrease at a successor step.


private theorem pMergeSpan_le_succ : ∀ n, pMergeSpan n ≤ pMergeSpan (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n
        · rw [show pMergeSpan 0 = 0 by rw [pMergeSpan]; norm_num]
          exact Nat.zero_le _
        · have hone : pMergeSpan 1 = 1 := by rw [pMergeSpan]; norm_num
          rw [hone, pMergeSpan_unfold (n := 2) (by norm_num)]
          norm_num [hone]
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hceil0 : 2 * m - 2 * m / 2 = m := by omega
          have hceil1 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          rw [pMergeSpan_unfold (n := 2 * m) (by omega),
            pMergeSpan_unfold (n := 2 * m + 1) (by omega),
            hceil0, hceil1]
          have ihm := ih m (by omega)
          have hlog : Nat.log 2 (2 * m) ≤ Nat.log 2 (2 * m + 1) :=
            Nat.log_mono_right (by omega)
          omega
        · have hceil0 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          have hceil1 : 2 * m + 1 + 1 - (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pMergeSpan_unfold (n := 2 * m + 1) (by omega),
            pMergeSpan_unfold (n := 2 * m + 1 + 1) (by omega),
            hceil0, hceil1]
          have hlog : Nat.log 2 (2 * m + 1) ≤ Nat.log 2 (2 * m + 1 + 1) :=
            Nat.log_mono_right (by omega)
          omega

P-MERGE span is monotone in the input size.

theorem pMergeSpan_monotone : Monotone pMergeSpan :=
  monotone_nat_of_le_succ pMergeSpan_le_succ

Every positive P-MERGE span cost lies between its adjacent power-of-two costs.

theorem pMergeSpan_power_sandwich (n : ℕ) (hn : 0 < n) :
    pMergeSpan (2 ^ Nat.log 2 n) ≤ pMergeSpan n ∧
      pMergeSpan n ≤ pMergeSpan (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pMergeSpan_monotone 2 n (by norm_num) hn.ne'

The P-MERGE-SORT work recurrence does not decrease at a successor step.


private theorem pMergeSortWork_le_succ : ∀ n, pMergeSortWork n ≤ pMergeSortWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n
        · rw [show pMergeSortWork 0 = 0 by rw [pMergeSortWork]; norm_num]
          exact Nat.zero_le _
        · have hone : pMergeSortWork 1 = 1 := by rw [pMergeSortWork]; norm_num
          rw [hone, pMergeSortWork_unfold (n := 2) (by norm_num)]
          norm_num [hone]
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          have hceil0 : 2 * m - 2 * m / 2 = m := by omega
          have hceil1 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          rw [pMergeSortWork_unfold (n := 2 * m) (by omega),
            pMergeSortWork_unfold (n := 2 * m + 1) (by omega),
            hceil0, hceil1, hdiv0, hdiv1]
          have ihm := ih m (by omega)
          omega
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          have hceil0 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          have hceil1 : 2 * m + 1 + 1 - (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pMergeSortWork_unfold (n := 2 * m + 1) (by omega),
            pMergeSortWork_unfold (n := 2 * m + 1 + 1) (by omega),
            hceil0, hceil1, hdiv0, hdiv1]
          have ihm := ih m (by omega)
          omega

P-MERGE-SORT work is monotone in the input size.

theorem pMergeSortWork_monotone : Monotone pMergeSortWork :=
  monotone_nat_of_le_succ pMergeSortWork_le_succ

Every positive P-MERGE-SORT work cost lies between its adjacent power-of-two costs.

theorem pMergeSortWork_power_sandwich (n : ℕ) (hn : 0 < n) :
    pMergeSortWork (2 ^ Nat.log 2 n) ≤ pMergeSortWork n ∧
      pMergeSortWork n ≤ pMergeSortWork (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pMergeSortWork_monotone 2 n (by norm_num) hn.ne'

The P-MERGE-SORT span recurrence does not decrease at a successor step.


private theorem pMergeSortSpan_le_succ : ∀ n, pMergeSortSpan n ≤ pMergeSortSpan (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n
        · rw [show pMergeSortSpan 0 = 0 by rw [pMergeSortSpan]; norm_num]
          exact Nat.zero_le _
        · have hone : pMergeSortSpan 1 = 1 := by rw [pMergeSortSpan]; norm_num
          rw [hone, pMergeSortSpan_unfold (n := 2) (by norm_num)]
          norm_num [hone]
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hceil0 : 2 * m - 2 * m / 2 = m := by omega
          have hceil1 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          rw [pMergeSortSpan_unfold (n := 2 * m) (by omega),
            pMergeSortSpan_unfold (n := 2 * m + 1) (by omega), hceil0, hceil1]
          have ihm := ih m (by omega)
          have hp : pMergeSpan (2 * m) ≤ pMergeSpan (2 * m + 1) :=
            pMergeSpan_monotone (by omega)
          omega
        · have hceil0 : 2 * m + 1 - (2 * m + 1) / 2 = m + 1 := by omega
          have hceil1 : 2 * m + 1 + 1 - (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pMergeSortSpan_unfold (n := 2 * m + 1) (by omega),
            pMergeSortSpan_unfold (n := 2 * m + 1 + 1) (by omega), hceil0, hceil1]
          have hp : pMergeSpan (2 * m + 1) ≤ pMergeSpan (2 * m + 1 + 1) :=
            pMergeSpan_monotone (by omega)
          omega

P-MERGE-SORT span is monotone in the input size.

theorem pMergeSortSpan_monotone : Monotone pMergeSortSpan :=
  monotone_nat_of_le_succ pMergeSortSpan_le_succ

Every positive P-MERGE-SORT span cost lies between its adjacent power-of-two costs.

theorem pMergeSortSpan_power_sandwich (n : ℕ) (hn : 0 < n) :
    pMergeSortSpan (2 ^ Nat.log 2 n) ≤ pMergeSortSpan n ∧
      pMergeSortSpan n ≤ pMergeSortSpan (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pMergeSortSpan_monotone 2 n (by norm_num) hn.ne'

All-input work and span bounds

              

private theorem add_three_le_three_mul_pow_two (k : ℕ) :
    k + 3 ≤ 3 * 2 ^ k := by
  induction k with
  | zero => norm_num
  | succ k ih =>
      rw [pow_succ]
      have hpow : 1 ≤ 2 ^ k := Nat.one_le_pow k 2 (by norm_num)
      nlinarithprivate theorem pMergeWork_exactPower_bounds (k : ℕ) :
    2 ^ k ≤ pMergeWork (2 ^ k) ∧ pMergeWork (2 ^ k) ≤ 4 * 2 ^ k := by
  have hexact := pMergeWork_pow_two k
  have hlinear := add_three_le_three_mul_pow_two k
  omega

private theorem pMergeWork_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pMergeWork (2 ^ k) : ℝ))
      (fun k : ℕ => (2 : ℝ) ^ k) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨4, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hreal :
        (pMergeWork (2 ^ k) : ℝ) ≤ ((4 * 2 ^ k : ℕ) : ℝ) := by
      exact_mod_cast (pMergeWork_exactPower_bounds k).2
    simpa [Nat.cast_mul, Nat.cast_pow] using hreal
  · refine (Chapter03.isBigOmega_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ (2 : ℝ) ^ k),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hreal : ((2 ^ k : ℕ) : ℝ) ≤ (pMergeWork (2 ^ k) : ℝ) := by
      exact_mod_cast (pMergeWork_exactPower_bounds k).1
    simpa [Nat.cast_pow] using hreal

private theorem pMergeSpan_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pMergeSpan (2 ^ k) : ℝ))
      (fun k : ℕ => ((k : ℝ) + 1) ^ 2) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hexact :
        (2 : ℝ) * (pMergeSpan (2 ^ k) : ℝ) =
          ((k : ℝ) + 1) * ((k : ℝ) + 2) := by
      exact_mod_cast pMergeSpan_pow_two k
    have hk : 0 ≤ (k : ℝ) := Nat.cast_nonneg k
    have hproduct : 0 ≤ (k : ℝ) * ((k : ℝ) + 1) :=
      mul_nonneg hk (by positivity)
    nlinarith
  · refine (Chapter03.isBigOmega_iff _ _).mpr
      ⟨(2 : ℝ)⁻¹, by positivity, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ ((k : ℝ) + 1) ^ 2),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hexact :
        (2 : ℝ) * (pMergeSpan (2 ^ k) : ℝ) =
          ((k : ℝ) + 1) * ((k : ℝ) + 2) := by
      exact_mod_cast pMergeSpan_pow_two k
    have hk : 0 ≤ (k : ℝ) := Nat.cast_nonneg k
    nlinarith

private theorem pMergeSortWork_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pMergeSortWork (2 ^ k) : ℝ))
      (fun k : ℕ => ((k : ℝ) + 1) * (2 : ℝ) ^ k) := by
  have hfun :
      (fun k : ℕ => (pMergeSortWork (2 ^ k) : ℝ)) =
        (fun k : ℕ => ((k : ℝ) + 1) * (2 : ℝ) ^ k) := by
    funext k
    rw [pMergeSortWork_pow_two]
    push_cast
    ring
  rw [hfun]
  exact Chapter03.isBigTheta_refl _

private theorem pMergeSortSpan_exactPower_closed (k : ℕ) :
    6 * pMergeSortSpan (2 ^ k) = (k + 1) * (k + 2) * (k + 3) := by
  rw [pMergeSortSpan_pow_two]
  ring

private theorem pMergeSortSpan_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pMergeSortSpan (2 ^ k) : ℝ))
      (fun k : ℕ => ((k : ℝ) + 1) ^ 3) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hexact :
        (6 : ℝ) * (pMergeSortSpan (2 ^ k) : ℝ) =
          ((k : ℝ) + 1) * ((k : ℝ) + 2) * ((k : ℝ) + 3) := by
      exact_mod_cast pMergeSortSpan_exactPower_closed k
    have hk : 0 ≤ (k : ℝ) := Nat.cast_nonneg k
    have hk2 : 0 ≤ (k : ℝ) * (k : ℝ) := mul_nonneg hk hk
    have hk3 : 0 ≤ (k : ℝ) * ((k : ℝ) * (k : ℝ)) := mul_nonneg hk hk2
    nlinarith
  · refine (Chapter03.isBigOmega_iff _ _).mpr
      ⟨(6 : ℝ)⁻¹, by positivity, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ ((k : ℝ) + 1) ^ 3),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hexact :
        (6 : ℝ) * (pMergeSortSpan (2 ^ k) : ℝ) =
          ((k : ℝ) + 1) * ((k : ℝ) + 2) * ((k : ℝ) + 3) := by
      exact_mod_cast pMergeSortSpan_exactPower_closed k
    have hk : 0 ≤ (k : ℝ) := Nat.cast_nonneg k
    have hk2 : 0 ≤ (k : ℝ) * (k : ℝ) := mul_nonneg hk hk
    nlinarith

P-MERGE has linear work on every positive input size.


theorem pMergeWork_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pMergeWork n : ℝ))
      (Chapter04.polynomialScale 1) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (pMergeWork n : ℝ))
        (Chapter04.criticalPowerScale 2 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerScale 2 2
      (fun n : ℕ => (pMergeWork n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast pMergeWork_monotone)
      pMergeWork_exactPower_bigTheta
  exact Chapter03.isBigTheta_trans hcritical (by
    simpa using Chapter04.criticalPowerScale_isBigTheta_polynomialScale 2 1
      (by norm_num))

P-MERGE has quadratic-logarithmic span on every positive input size.


theorem pMergeSpan_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pMergeSpan n : ℝ))
      (Chapter04.criticalPowerLogPolylogScale 1 2 1) := by
  have hpower :
      Chapter03.isBigTheta
        (fun i : ℕ => (pMergeSpan (2 ^ i) : ℝ))
        (fun i : ℕ => Chapter04.criticalPowerLogPolylogScale 1 2 1 (2 ^ i)) := by
    have hscale :
        (fun i : ℕ => Chapter04.criticalPowerLogPolylogScale 1 2 1 (2 ^ i)) =
          (fun i : ℕ => ((i : ℝ) + 1) ^ 2) := by
      funext i
      simp [Chapter04.criticalPowerLogPolylogScale_exactPower]
    rw [hscale]
    exact pMergeSpan_exactPower_bigTheta
  exact Chapter04.allInput_bigTheta_of_powerStep 2
    (fun n : ℕ => (pMergeSpan n : ℝ))
    (Chapter04.criticalPowerLogPolylogScale 1 2 1) (by norm_num)
    (Chapter04.monotoneAbs_natCast pMergeSpan_monotone)
    (Chapter04.criticalPowerLogPolylogScale_monotoneAbs 1 2 1 (by norm_num))
    (Chapter04.criticalPowerLogPolylogScale_powerStepBound 1 2 1
      (by norm_num) (by norm_num))
    hpower

P-MERGE-SORT has n log n work on every positive input size.


theorem pMergeSortWork_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pMergeSortWork n : ℝ))
      (Chapter04.polynomialLogScale 2 1) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (pMergeSortWork n : ℝ))
        (Chapter04.criticalPowerLogScale 2 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerLogScale 2 2
      (fun n : ℕ => (pMergeSortWork n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast pMergeSortWork_monotone)
      pMergeSortWork_exactPower_bigTheta
  exact Chapter03.isBigTheta_trans hcritical (by
    simpa using Chapter04.criticalPowerLogScale_isBigTheta_polynomialLogScale 2 1
      (by norm_num))

P-MERGE-SORT has cubic-logarithmic span on every positive input size.


theorem pMergeSortSpan_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pMergeSortSpan n : ℝ))
      (Chapter04.criticalPowerLogPolylogScale 1 2 2) := by
  have hpower :
      Chapter03.isBigTheta
        (fun i : ℕ => (pMergeSortSpan (2 ^ i) : ℝ))
        (fun i : ℕ => Chapter04.criticalPowerLogPolylogScale 1 2 2 (2 ^ i)) := by
    have hscale :
        (fun i : ℕ => Chapter04.criticalPowerLogPolylogScale 1 2 2 (2 ^ i)) =
          (fun i : ℕ => ((i : ℝ) + 1) ^ 3) := by
      funext i
      simp [Chapter04.criticalPowerLogPolylogScale_exactPower]
    rw [hscale]
    exact pMergeSortSpan_exactPower_bigTheta
  exact Chapter04.allInput_bigTheta_of_powerStep 2
    (fun n : ℕ => (pMergeSortSpan n : ℝ))
    (Chapter04.criticalPowerLogPolylogScale 1 2 2) (by norm_num)
    (Chapter04.monotoneAbs_natCast pMergeSortSpan_monotone)
    (Chapter04.criticalPowerLogPolylogScale_monotoneAbs 1 2 2 (by norm_num))
    (Chapter04.criticalPowerLogPolylogScale_powerStepBound 1 2 2
      (by norm_num) (by norm_num))
    hpower

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.LowerBound.Definitions

CLRS Chapter 26.3 — Binary Lower-Bound Definitions

This module defines the sequential lower-bound search used by P-MERGE. The search works over half-open index ranges and records one unit of work and span for every inspected element.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace Internal

Internal half-open-range lower-bound search.

loop xs pivot lo hi searches the range [lo, hi). It is intentionally namespaced, rather than Lean-private, so that the correctness module can state and prove its range invariant without adding the helper to Chapter 26's public surface.

def loop [LinearOrder α] (xs : List α) (pivot : α) (lo hi : ℕ) : Costed ℕ :=
  if lo < hi then
    let mid := (lo + hi) / 2
    match xs[mid]? with
    | none => Costed.charge 1 1 lo
    | some x =>
        Costed.seq (Costed.charge 1 1 ()) fun _ =>
          if x < pivot then
            loop xs pivot (mid + 1) hi
          else
            loop xs pivot lo mid
  else
    Costed.pure lo
termination_by hi - lo
decreasing_by
  all_goals omega

end Internalend ParallelMerge

Return the first position at which pivot can be inserted into xs.

Correctness is established in the following module under the usual sortedness hypothesis. The executable definition remains total on arbitrary lists.

def binaryLowerBound [LinearOrder α] (xs : List α) (pivot : α) : Costed ℕ :=
  ParallelMerge.Internal.loop xs pivot 0 xs.length

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.PMerge.Definitions

CLRS Chapter 26.3 — Executable P-MERGE

This module implements the pure functional control structure of CLRS P-MERGE. Each nonempty call selects the midpoint of the longer input, binary-searches the other input, spawns the lower and upper merges in parallel, and places the pivot between their outputs. The definition is total even when the inputs are not sorted; sortedness is needed only by the later correctness theorem.

namespace CLRSnamespace Chapter27

Parallel merge with execution-attached work and span.

Binary search is sequential, the two recursive subproblems use one parallel fork/join, and pivot placement is charged one unit of work and span.

def pMerge [LinearOrder α] (xs ys : List α) : Costed (List α) :=
  if hzero : xs.length + ys.length = 0 then
    Costed.pure []
  else
    let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
    Costed.seq S.search fun _ =>
      let lower := pMerge S.lowerPrimary S.lowerSecondary
      let upper := pMerge S.upperPrimary S.upperSecondary
      Costed.seq (Costed.par lower upper) fun parts =>
        Costed.charge 1 1 (parts.1 ++ S.pivot :: parts.2)
termination_by xs.length + ys.length
decreasing_by
  · change S.leftSize < xs.length + ys.length
    calc
      S.leftSize < S.totalSize := S.leftSize_lt
      _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
  · change S.rightSize < xs.length + ys.length
    calc
      S.rightSize < S.totalSize := S.rightSize_lt
      _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.LowerBound.Correctness

CLRS Chapter 26.3 — Binary Lower-Bound Correctness

This module proves the partition specification used by P-MERGE's sequential binary search. The internal proof follows the half-open search interval and makes both boundary invariants explicit.

Main results:

binaryLowerBound_partition proves the complete lower-bound partition.
binaryLowerBound_index_le_length proves the index bound even for an unsorted input list.

namespace CLRSnamespace Chapter27

The insertion index splits a list into values strictly below the pivot and values greater than or equal to the pivot.

structure LowerBoundSpec [LinearOrder α] (xs : List α) (pivot : α) (i : ℕ) : Prop where
  index_le_length : i ≤ xs.length
  left_lt : ∀ x ∈ xs.take i, x < pivot
  right_ge : ∀ x ∈ xs.drop i, pivot ≤ x

namespace ParallelMergenamespace LowerBound

The strong invariant of the half-open interval [lo, hi): all indices strictly before lo are already known to be below the pivot, while all indices at or after hi are already known to be at least the pivot.

private structure LoopInvariant [LinearOrder α] (xs : List α) (pivot : α)
    (lo hi : ℕ) : Prop where
  lo_le_hi : lo ≤ hi
  hi_le_length : hi ≤ xs.length
  left_lt : ∀ j : Fin xs.length, j.1 < lo → xs.get j < pivot
  right_ge : ∀ j : Fin xs.length, hi ≤ j.1 → pivot ≤ xs.get j



private theorem loopInvariant_to_spec [LinearOrder α]
    {xs : List α} {pivot : α} {i : ℕ}
    (hinv : LoopInvariant xs pivot i i) : LowerBoundSpec xs pivot i := by
  constructor
  · exact hinv.hi_le_length
  · intro x hx
    obtain ⟨j, hj, hval⟩ := List.mem_iff_getElem.mp hx
    have hj_lt_i : j < i := by
      rw [List.length_take] at hj
      omega
    have hj_lt_len : j < xs.length := by
      rw [List.length_take] at hj
      omega
    have hlt := hinv.left_lt ⟨j, hj_lt_len⟩ hj_lt_i
    rw [List.get_eq_getElem, ← List.getElem_take (h := hj)] at hlt
    simpa [hval] using hlt
  · intro x hx
    obtain ⟨j, hj, hval⟩ := List.mem_iff_getElem.mp hx
    have hglobal : i + j < xs.length := by
      rw [List.length_drop] at hj
      omega
    have hge := hinv.right_ge ⟨i + j, hglobal⟩ (by simp)
    rw [List.get_eq_getElem, ← List.getElem_drop (h := hj)] at hge
    simpa [hval] using hge

The lower-bound loop preserves its two boundary facts and returns the unique global partition index once the interval closes.


private theorem loop_correct [LinearOrder α] (xs : List α) (pivot : α) (lo hi : ℕ)
    (hinv : LoopInvariant xs pivot lo hi)
    (hxs : xs.Pairwise (· ≤ ·)) :
    LowerBoundSpec xs pivot (Internal.loop xs pivot lo hi).value := by
  induction lo, hi using Internal.loop.induct xs with
  | case1 lo hi hlohi mid hnone =>
      have hmid_lt : (lo + hi) / 2 < xs.length := by
        have := hinv.hi_le_length
        omega
      rw [List.getElem?_eq_getElem hmid_lt] at hnone
      contradiction
  | case2 lo hi hlohi mid x hget ihRight ihLeft =>
      have hlo_mid : lo ≤ mid := by
        dsimp [mid]
        omega
      have hmid_hi : mid < hi := by
        dsimp [mid]
        omega
      have hmid_len : mid < xs.length := lt_of_lt_of_le hmid_hi hinv.hi_le_length
      have hx_at : xs.get ⟨mid, hmid_len⟩ = x := by
        obtain ⟨_, hx⟩ := List.getElem?_eq_some_iff.mp hget
        simpa [List.get_eq_getElem] using hx
      by_cases hxlt : x < pivot
      · rw [Internal.loop]
        simp only [hlohi, if_true, mid, hget, Costed.seq_value, hxlt]
        apply ihRight
        · refine ⟨by omega, hinv.hi_le_length, ?_, hinv.right_ge⟩
          intro j hj
          by_cases hjlo : j.1 < lo
          · exact hinv.left_lt j hjlo
          by_cases hjmid : j.1 = mid
          · have hj_eq : j = ⟨mid, hmid_len⟩ := Fin.ext hjmid
            rw [hj_eq, hx_at]
            exact hxlt
          · have hj_lt_mid : j.1 < mid := by omega
            have hle := hxs.rel_get_of_lt (a := j) (b := ⟨mid, hmid_len⟩) hj_lt_mid
            rw [hx_at] at hle
            exact lt_of_le_of_lt hle hxlt
      · have hpivot_le_x : pivot ≤ x := le_of_not_gt hxlt
        rw [Internal.loop]
        simp only [hlohi, if_true, mid, hget, Costed.seq_value, hxlt, if_false]
        apply ihLeft
        · refine ⟨hlo_mid, le_trans (Nat.le_of_lt hmid_hi) hinv.hi_le_length,
            hinv.left_lt, ?_⟩
          intro j hj
          by_cases hjmid : j.1 = mid
          · have hj_eq : j = ⟨mid, hmid_len⟩ := Fin.ext hjmid
            rw [hj_eq, hx_at]
            exact hpivot_le_x
          · have hmid_lt_j : mid < j.1 := by omega
            have hle := hxs.rel_get_of_lt (a := ⟨mid, hmid_len⟩) (b := j) hmid_lt_j
            rw [hx_at] at hle
            exact le_trans hpivot_le_x hle
  | case3 lo hi hnlt =>
      have hlo_eq_hi : lo = hi := Nat.le_antisymm hinv.lo_le_hi (Nat.le_of_not_gt hnlt)
      rw [Internal.loop]
      simp only [hnlt, if_false, Costed.pure_value]
      exact loopInvariant_to_spec (hlo_eq_hi ▸ hinv)

Independently of sortedness, the internal search never returns beyond its upper interval endpoint.


private theorem loop_value_le_hi [LinearOrder α] (xs : List α) (pivot : α) (lo hi : ℕ)
    (hlohi : lo ≤ hi) (hhilen : hi ≤ xs.length) :
    (Internal.loop xs pivot lo hi).value ≤ hi := by
  induction lo, hi using Internal.loop.induct xs with
  | case1 lo hi hlt mid hnone =>
      have hmid_lt : (lo + hi) / 2 < xs.length := by omega
      rw [List.getElem?_eq_getElem hmid_lt] at hnone
      contradiction
  | case2 lo hi hlt mid x hget ihRight ihLeft =>
      have hlo_mid : lo ≤ mid := by dsimp [mid]; omega
      have hmid_hi : mid < hi := by dsimp [mid]; omega
      by_cases hxlt : x < pivot
      · rw [Internal.loop]
        simp only [hlt, if_true, mid, hget, Costed.seq_value, hxlt]
        exact ihRight (by omega) hhilen
      · rw [Internal.loop]
        simp only [hlt, if_true, mid, hget, Costed.seq_value, hxlt, if_false]
        exact le_trans (ihLeft hlo_mid (le_trans (Nat.le_of_lt hmid_hi) hhilen))
          (Nat.le_of_lt hmid_hi)
  | case3 lo hi hnlt =>
      rw [Internal.loop]
      simp only [hnlt, if_false, Costed.pure_value]
      exact hlohi

end LowerBoundend ParallelMerge

Public theorems

Binary lower bound returns a valid index even when the input is unsorted.

theorem binaryLowerBound_index_le_length [LinearOrder α]
    (xs : List α) (pivot : α) :
    (binaryLowerBound xs pivot).value ≤ xs.length := by
  exact ParallelMerge.LowerBound.loop_value_le_hi xs pivot 0 xs.length
    (Nat.zero_le _) le_rfl

On a sorted input, binary lower bound produces the textbook strict-left, nonstrict-right partition, including the correct behavior on duplicates.

theorem binaryLowerBound_partition [LinearOrder α] (xs : List α) (pivot : α)
    (hxs : xs.Pairwise (· ≤ ·)) :
    LowerBoundSpec xs pivot (binaryLowerBound xs pivot).value := by
  apply ParallelMerge.LowerBound.loop_correct xs pivot 0 xs.length
  · exact ⟨Nat.zero_le _, le_rfl, by simp, by simp⟩
  · exact hxs

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.LowerBound.Costs

CLRS Chapter 26.3 — Binary Lower-Bound Costs

The lower-bound helper is sequential: every comparison contributes one unit to both work and span. Its live interval is at least halved by every comparison, which gives the logarithmic public bound.

Main results:

binaryLowerBound_work_le_log bounds work on every input.
binaryLowerBound_span_eq_work records sequentiality.
binaryLowerBound_span_le_log transfers the work bound to span.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace LowerBound

private theorem log_half_add_one_le (n : ℕ) (hn : 2 ≤ n) :
    Nat.log 2 (n / 2) + 1 ≤ Nat.log 2 n := by
  rw [Nat.log_div_base]
  have hlogpos : 1 ≤ Nat.log 2 n := Nat.log_pos (by omega) hn
  omega

private theorem comparison_cost_le_log (n child work : ℕ)
    (hn : 0 < n)
    (hchild : child ≤ n / 2)
    (hwork : work ≤ Nat.log 2 child + 1)
    (hzero : child = 0 → work = 0) :
    1 + work ≤ Nat.log 2 n + 1 := by
  by_cases hc : child = 0
  · simp [hzero hc]
  · have hcpos : 0 < child := Nat.pos_of_ne_zero hc
    have hn_two : 2 ≤ n := by omega
    have hlogmono : Nat.log 2 child ≤ Nat.log 2 (n / 2) :=
      Nat.log_monotone hchild
    have hhalf := log_half_add_one_le n hn_two
    omega

On every valid half-open interval, binary-search work is logarithmic in the interval length. The proof is strong recursion through the generated loop induction principle; both recursive intervals are bounded by half the parent.


private theorem loop_work_le_log [LinearOrder α]
    (xs : List α) (pivot : α) (lo hi : ℕ)
    (hlohi : lo ≤ hi) (hhilen : hi ≤ xs.length) :
    (Internal.loop xs pivot lo hi).work ≤ Nat.log 2 (hi - lo) + 1 := by
  induction lo, hi using Internal.loop.induct xs with
  | case1 lo hi hlt mid hnone =>
      have hmid_lt : mid < xs.length := by dsimp [mid]; omega
      rw [List.getElem?_eq_getElem hmid_lt] at hnone
      contradiction
  | case2 lo hi hlt mid x hget ihRight ihLeft =>
      have hlo_mid : lo ≤ mid := by dsimp [mid]; omega
      have hmid_hi : mid < hi := by dsimp [mid]; omega
      have hright_bound : hi - (mid + 1) ≤ (hi - lo) / 2 := by
        dsimp [mid]
        omega
      have hleft_bound : mid - lo ≤ (hi - lo) / 2 := by
        dsimp [mid]
        omega
      have ihR := ihRight (by omega) hhilen
      have ihL := ihLeft hlo_mid (le_trans (Nat.le_of_lt hmid_hi) hhilen)
      by_cases hxlt : x < pivot
      · rw [Internal.loop]
        simp only [hlt, if_true, mid, hget, Costed.seq_work, Costed.charge_work, hxlt]
        apply comparison_cost_le_log (hi - lo) (hi - (mid + 1))
          (Internal.loop xs pivot (mid + 1) hi).work (by omega) hright_bound ihR
        intro hz
        have heq : mid + 1 = hi := by omega
        simp [heq, Internal.loop]
      · rw [Internal.loop]
        simp only [hlt, if_true, mid, hget, Costed.seq_work, Costed.charge_work,
          hxlt, if_false]
        apply comparison_cost_le_log (hi - lo) (mid - lo)
          (Internal.loop xs pivot lo mid).work (by omega) hleft_bound ihL
        intro hz
        have heq : mid = lo := by omega
        simp [heq, Internal.loop]
  | case3 lo hi hnlt =>
      rw [Internal.loop]
      simp only [hnlt, if_false, Costed.pure_work]
      omega

The internal lower-bound computation has identical work and span because it performs no parallel composition.


private theorem loop_span_eq_work [LinearOrder α]
    (xs : List α) (pivot : α) (lo hi : ℕ) :
    (Internal.loop xs pivot lo hi).span = (Internal.loop xs pivot lo hi).work := by
  induction lo, hi using Internal.loop.induct xs with
  | case1 lo hi hlt mid hnone =>
      rw [Internal.loop]
      simp [hlt, mid, hnone]
  | case2 lo hi hlt mid x hget ihRight ihLeft =>
      by_cases hxlt : x < pivot
      · rw [Internal.loop]
        simp [hlt, mid, hget, hxlt, ihRight]
      · rw [Internal.loop]
        simp [hlt, mid, hget, hxlt, ihLeft]
  | case3 lo hi hnlt =>
      rw [Internal.loop]
      simp [hnlt]

end LowerBoundend ParallelMerge

Public theorems

Binary lower bound uses at most log₂(length) + 1 comparisons.

theorem binaryLowerBound_work_le_log [LinearOrder α]
    (xs : List α) (pivot : α) :
    (binaryLowerBound xs pivot).work ≤ Nat.log 2 xs.length + 1 := by
  simpa [binaryLowerBound] using
    ParallelMerge.LowerBound.loop_work_le_log xs pivot 0 xs.length
      (Nat.zero_le _) le_rfl

Binary lower bound is sequential, so its span equals its work exactly.

theorem binaryLowerBound_span_eq_work [LinearOrder α]
    (xs : List α) (pivot : α) :
    (binaryLowerBound xs pivot).span = (binaryLowerBound xs pivot).work := by
  exact ParallelMerge.LowerBound.loop_span_eq_work xs pivot 0 xs.length

The sequential span of binary lower bound is logarithmic as well.


theorem binaryLowerBound_span_le_log [LinearOrder α]
    (xs : List α) (pivot : α) :
    (binaryLowerBound xs pivot).span ≤ Nat.log 2 xs.length + 1 := by
  rw [binaryLowerBound_span_eq_work]
  exact binaryLowerBound_work_le_log xs pivot

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.PMerge.Correctness.Boundaries

CLRS Chapter 26.3 — P-MERGE Order Boundaries

This module isolates the order facts behind one P-MERGE split. In particular, lower bound puts every duplicate of the pivot on the upper side, so the lower secondary partition is strictly below the pivot while the upper partition is greater than or equal to it.

namespace CLRSnamespace Chapter27

The semantic result of merging two sorted lists.

structure PMergeSpec [LinearOrder α] (xs ys out : List α) : Prop where
  sorted : out.Pairwise (· ≤ ·)
  perm : out.Perm (xs ++ ys)
  length_eq : out.length = xs.length + ys.length

              namespace ParallelMergenamespace PMergenamespace Correctnessvariable [LinearOrder α]

Normalization preserves sortedness of the primary input.

theorem primary_sorted (S : MergeSplit α)
    (hxs : S.xs.Pairwise (· ≤ ·)) (hys : S.ys.Pairwise (· ≤ ·)) :
    S.primary.Pairwise (· ≤ ·) := by
  rcases S.inputOrder with h | h
  · simpa [h.1] using hxs
  · simpa [h.1] using hys

Normalization preserves sortedness of the secondary input.

theorem secondary_sorted (S : MergeSplit α)
    (hxs : S.xs.Pairwise (· ≤ ·)) (hys : S.ys.Pairwise (· ≤ ·)) :
    S.secondary.Pairwise (· ≤ ·) := by
  rcases S.inputOrder with h | h
  · simpa [h.2] using hys
  · simpa [h.2] using hxs

Taking the lower primary partition preserves sortedness.

theorem lowerPrimary_sorted (S : MergeSplit α)
    (hprimary : S.primary.Pairwise (· ≤ ·)) :
    S.lowerPrimary.Pairwise (· ≤ ·) := by
  exact hprimary.take

Dropping the pivot and the lower prefix preserves primary sortedness.

theorem upperPrimary_sorted (S : MergeSplit α)
    (hprimary : S.primary.Pairwise (· ≤ ·)) :
    S.upperPrimary.Pairwise (· ≤ ·) := by
  exact hprimary.drop

Taking the binary-search prefix preserves secondary sortedness.

theorem lowerSecondary_sorted (S : MergeSplit α)
    (hsecondary : S.secondary.Pairwise (· ≤ ·)) :
    S.lowerSecondary.Pairwise (· ≤ ·) := by
  exact hsecondary.take

Dropping the binary-search prefix preserves secondary sortedness.

theorem upperSecondary_sorted (S : MergeSplit α)
    (hsecondary : S.secondary.Pairwise (· ≤ ·)) :
    S.upperSecondary.Pairwise (· ≤ ·) := by
  exact hsecondary.drop

The primary input is its lower prefix, pivot, and upper suffix.


theorem primary_reconstruct (S : MergeSplit α) :
    S.lowerPrimary ++ S.pivot :: S.upperPrimary = S.primary := by
  have hi : S.pivotIndex < S.primary.length := by
    simpa [MergeSplit.pivotIndex] using S.pivotIndex_lt
  have hpivot : S.primary.get ⟨S.pivotIndex, hi⟩ = S.pivot := by
    simpa [MergeSplit.pivotIndex] using S.pivot_eq
  simp only [MergeSplit.lowerPrimary, MergeSplit.upperPrimary]
  rw [← hpivot, List.cons_get_drop_succ, List.take_append_drop]

Every element in the primary lower partition is at most the pivot.


theorem lowerPrimary_le_pivot (S : MergeSplit α)
    (hprimary : S.primary.Pairwise (· ≤ ·)) :
    ∀ x ∈ S.lowerPrimary, x ≤ S.pivot := by
  have hsplit :
      (S.lowerPrimary ++ S.pivot :: S.upperPrimary).Pairwise (· ≤ ·) := by
    rw [primary_reconstruct S]
    exact hprimary
  have hcross := (List.pairwise_append.mp hsplit).2.2
  intro x hx
  exact hcross x hx S.pivot (by simp)

Every element in the primary upper partition is at least the pivot.


theorem pivot_le_upperPrimary (S : MergeSplit α)
    (hprimary : S.primary.Pairwise (· ≤ ·)) :
    ∀ x ∈ S.upperPrimary, S.pivot ≤ x := by
  have hsplit :
      (S.lowerPrimary ++ S.pivot :: S.upperPrimary).Pairwise (· ≤ ·) := by
    rw [primary_reconstruct S]
    exact hprimary
  have htail := (List.pairwise_append.mp hsplit).2.1
  simpa using (List.pairwise_cons.mp htail).1

Binary lower bound gives the duplicate-sensitive secondary partition.


theorem secondary_partition (S : MergeSplit α)
    (hsecondary : S.secondary.Pairwise (· ≤ ·)) :
    LowerBoundSpec S.secondary S.pivot S.splitIndex := by
  rw [MergeSplit.splitIndex, S.search_eq]
  exact binaryLowerBound_partition S.secondary S.pivot hsecondary

Every element in the lower secondary partition is at most the pivot.

The binary-search theorem is stronger: these elements are strictly below the pivot. Weakening here is exactly what the sorted join needs.

theorem lowerSecondary_le_pivot (S : MergeSplit α)
    (hsecondary : S.secondary.Pairwise (· ≤ ·)) :
    ∀ x ∈ S.lowerSecondary, x ≤ S.pivot := by
  intro x hx
  exact (secondary_partition S hsecondary).left_lt x hx |>.le

Every element in the upper secondary partition is at least the pivot.

theorem pivot_le_upperSecondary (S : MergeSplit α)
    (hsecondary : S.secondary.Pairwise (· ≤ ·)) :
    ∀ x ∈ S.upperSecondary, S.pivot ≤ x := by
  exact (secondary_partition S hsecondary).right_ge

A permutation of the two lower partitions remains bounded by the pivot.

theorem lower_output_le_pivot (S : MergeSplit α) {out : List α}
    (hprimary : S.primary.Pairwise (· ≤ ·))
    (hsecondary : S.secondary.Pairwise (· ≤ ·))
    (hout : out.Perm (S.lowerPrimary ++ S.lowerSecondary)) :
    ∀ x ∈ out, x ≤ S.pivot := by
  intro x hx
  have hx' := hout.mem_iff.mp hx
  rcases List.mem_append.mp hx' with hxPrimary | hxSecondary
  · exact lowerPrimary_le_pivot S hprimary x hxPrimary
  · exact lowerSecondary_le_pivot S hsecondary x hxSecondary

A permutation of the two upper partitions remains above the pivot.

theorem pivot_le_upper_output (S : MergeSplit α) {out : List α}
    (hprimary : S.primary.Pairwise (· ≤ ·))
    (hsecondary : S.secondary.Pairwise (· ≤ ·))
    (hout : out.Perm (S.upperPrimary ++ S.upperSecondary)) :
    ∀ x ∈ out, S.pivot ≤ x := by
  intro x hx
  have hx' := hout.mem_iff.mp hx
  rcases List.mem_append.mp hx' with hxPrimary | hxSecondary
  · exact pivot_le_upperPrimary S hprimary x hxPrimary
  · exact pivot_le_upperSecondary S hsecondary x hxSecondary

Sorted recursive results join around the pivot into a sorted result.

theorem join_sorted (S : MergeSplit α) {lowerOut upperOut : List α}
    (hprimary : S.primary.Pairwise (· ≤ ·))
    (hsecondary : S.secondary.Pairwise (· ≤ ·))
    (hlower : PMergeSpec S.lowerPrimary S.lowerSecondary lowerOut)
    (hupper : PMergeSpec S.upperPrimary S.upperSecondary upperOut) :
    (lowerOut ++ S.pivot :: upperOut).Pairwise (· ≤ ·) := by
  apply List.pairwise_append.mpr
  refine ⟨hlower.sorted, ?_, ?_⟩
  · apply List.pairwise_cons.mpr
    exact ⟨pivot_le_upper_output S hprimary hsecondary hupper.perm, hupper.sorted⟩
  · intro x hx y hy
    rcases List.mem_cons.mp hy with rfl | hy
    · exact lower_output_le_pivot S hprimary hsecondary hlower.perm x hx
    · exact le_trans
        (lower_output_le_pivot S hprimary hsecondary hlower.perm x hx)
        (pivot_le_upper_output S hprimary hsecondary hupper.perm y hy)

              end Correctnessend PMergeend ParallelMergeend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.PMerge.Correctness.Permutation

CLRS Chapter 26.3 — P-MERGE Permutation Accounting

This module proves that the four recursive partitions and the midpoint pivot reconstruct exactly the two normalized inputs. The final normalization lemma then transports this accounting back to the caller's original input order.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace PMergenamespace Correctnessvariable [LinearOrder α]

The secondary lower and upper partitions reconstruct the secondary input.

theorem secondary_reconstruct (S : MergeSplit α) :
    S.lowerSecondary ++ S.upperSecondary = S.secondary := by
  exact List.take_append_drop S.splitIndex S.secondary

The normalized pair is either the original concatenation or its block swap.

theorem normalized_inputs_perm (S : MergeSplit α) :
    (S.primary ++ S.secondary).Perm (S.xs ++ S.ys) := by
  rcases S.inputOrder with h | h
  · simp [h.1, h.2]
  · simpa [h.1, h.2] using
      (List.perm_append_comm (l₁ := S.ys) (l₂ := S.xs))

The lower partitions, pivot, and upper partitions are a permutation of the normalized inputs.


theorem split_inputs_perm_normalized (S : MergeSplit α) :
    ((S.lowerPrimary ++ S.lowerSecondary) ++
      S.pivot :: (S.upperPrimary ++ S.upperSecondary)).Perm
      (S.primary ++ S.secondary) := by
  rw [← primary_reconstruct S, ← secondary_reconstruct S]
  have hswap := List.perm_append_comm
    (l₁ := S.lowerSecondary) (l₂ := S.pivot :: S.upperPrimary)
  simpa [List.append_assoc] using
    (hswap.append_left S.lowerPrimary).append_right S.upperSecondary

Replacing both child partitions by arbitrary permutations preserves the full original-input permutation.

theorem join_perm (S : MergeSplit α) {lowerOut upperOut : List α}
    (hlower : lowerOut.Perm (S.lowerPrimary ++ S.lowerSecondary))
    (hupper : upperOut.Perm (S.upperPrimary ++ S.upperSecondary)) :
    (lowerOut ++ S.pivot :: upperOut).Perm (S.xs ++ S.ys) := by
  exact (hlower.append (hupper.cons S.pivot)).trans
    ((split_inputs_perm_normalized S).trans (normalized_inputs_perm S))

              end Correctnessend PMergeend ParallelMergeend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.PMerge.Correctness.Main

CLRS Chapter 26.3 — P-MERGE Correctness

P-MERGE is proved correct by strong induction on the sum of the input lengths. The induction follows the algorithm's actual midpoint/lower-bound split: both recursive problems are strictly smaller because the primary pivot is removed.

Main results:

pMerge_correct: sortedness, permutation, and exact output length.
pMerge_value_sorted, pMerge_value_perm, and pMerge_value_length: direct projections for downstream proofs.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace PMergenamespace Correctnessvariable [LinearOrder α]

The value projection of a nonempty P-MERGE call is the two recursive values joined around the chosen pivot.


theorem value_eq_join (xs ys : List α)
    (hzero : xs.length + ys.length ≠ 0) :
    let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
    (pMerge xs ys).value =
      (pMerge S.lowerPrimary S.lowerSecondary).value ++
        S.pivot :: (pMerge S.upperPrimary S.upperSecondary).value := by
  have hnotNil : ¬ (xs = [] ∧ ys = []) := by
    rintro ⟨rfl, rfl⟩
    exact hzero rfl
  rw [pMerge]
  simp [hnotNil]

Strong-induction form of P-MERGE correctness, indexed by total input size.


private theorem correct_of_total (n : ℕ) :
    ∀ (xs ys : List α),
      xs.length + ys.length = n →
      xs.Pairwise (· ≤ ·) →
      ys.Pairwise (· ≤ ·) →
      PMergeSpec xs ys (pMerge xs ys).value := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs ys htotal hxs hys
      by_cases hzero : xs.length + ys.length = 0
      · have hxsNil : xs = [] := by
          simpa using (show xs.length = 0 by omega)
        have hysNil : ys = [] := by
          simpa using (show ys.length = 0 by omega)
        subst xs
        subst ys
        have hvalue : (pMerge ([] : List α) []).value = [] := by
          simp [pMerge]
        rw [hvalue]
        exact ⟨List.Pairwise.nil, List.Perm.refl [], rfl⟩
      · let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
        have hSxs : S.xs.Pairwise (· ≤ ·) := by
          simpa [S] using hxs
        have hSys : S.ys.Pairwise (· ≤ ·) := by
          simpa [S] using hys
        have hprimary := primary_sorted S hSxs hSys
        have hsecondary := secondary_sorted S hSxs hSys
        have hleft_lt : S.leftSize < n := by
          calc
            S.leftSize < S.totalSize := S.leftSize_lt
            _ = xs.length + ys.length := by
              simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hright_lt : S.rightSize < n := by
          calc
            S.rightSize < S.totalSize := S.rightSize_lt
            _ = xs.length + ys.length := by
              simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hlower : PMergeSpec S.lowerPrimary S.lowerSecondary
            (pMerge S.lowerPrimary S.lowerSecondary).value :=
          ih S.leftSize hleft_lt S.lowerPrimary S.lowerSecondary rfl
            (lowerPrimary_sorted S hprimary)
            (lowerSecondary_sorted S hsecondary)
        have hupper : PMergeSpec S.upperPrimary S.upperSecondary
            (pMerge S.upperPrimary S.upperSecondary).value :=
          ih S.rightSize hright_lt S.upperPrimary S.upperSecondary rfl
            (upperPrimary_sorted S hprimary)
            (upperSecondary_sorted S hsecondary)
        have hsorted := join_sorted S hprimary hsecondary hlower hupper
        have hperm := join_perm S hlower.perm hupper.perm
        have hjoined : PMergeSpec S.xs S.ys
            ((pMerge S.lowerPrimary S.lowerSecondary).value ++
              S.pivot :: (pMerge S.upperPrimary S.upperSecondary).value) := by
          refine ⟨hsorted, hperm, ?_⟩
          simpa using hperm.length_eq
        have hvalue : (pMerge xs ys).value =
            (pMerge S.lowerPrimary S.lowerSecondary).value ++
              S.pivot :: (pMerge S.upperPrimary S.upperSecondary).value := by
          simpa [S] using value_eq_join xs ys hzero
        rw [hvalue]
        simpa [S] using hjoined

              end Correctnessend PMergeend ParallelMerge

Public theorems

P-MERGE returns a sorted permutation of its two sorted inputs, with exact output length.

theorem pMerge_correct [LinearOrder α] (xs ys : List α)
    (hxs : xs.Pairwise (· ≤ ·)) (hys : ys.Pairwise (· ≤ ·)) :
    PMergeSpec xs ys (pMerge xs ys).value := by
  exact ParallelMerge.PMerge.Correctness.correct_of_total
    (xs.length + ys.length) xs ys rfl hxs hys

The value returned by P-MERGE is sorted.

theorem pMerge_value_sorted [LinearOrder α] (xs ys : List α)
    (hxs : xs.Pairwise (· ≤ ·)) (hys : ys.Pairwise (· ≤ ·)) :
    (pMerge xs ys).value.Pairwise (· ≤ ·) :=
  (pMerge_correct xs ys hxs hys).sorted

The value returned by P-MERGE contains exactly the two input multisets.

theorem pMerge_value_perm [LinearOrder α] (xs ys : List α)
    (hxs : xs.Pairwise (· ≤ ·)) (hys : ys.Pairwise (· ≤ ·)) :
    (pMerge xs ys).value.Perm (xs ++ ys) :=
  (pMerge_correct xs ys hxs hys).perm

P-MERGE's value has exactly the sum of the two input lengths.

theorem pMerge_value_length [LinearOrder α] (xs ys : List α)
    (hxs : xs.Pairwise (· ≤ ·)) (hys : ys.Pairwise (· ≤ ·)) :
    (pMerge xs ys).value.length = xs.length + ys.length :=
  (pMerge_correct xs ys hxs hys).length_eq

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Structure

CLRS Chapter 26.3 — P-MERGE Structural Cost Bounds

This module exposes the exact child-size accounting of the executable split and proves the actual CLRS three-quarter shrink bound. The proof uses the midpoint of the longer normalized input and the lower-bound index in the shorter input; it does not replace P-MERGE by a half-size recurrence.

              namespace CLRSnamespace Chapter27universe u

The two recursive P-MERGE children contain every input element except the chosen primary pivot.

theorem pMerge_childSizes_add_one [LinearOrder α] (S : MergeSplit α) :
    S.leftSize + S.rightSize + 1 = S.totalSize :=
  S.childSizes_add_one

private theorem child_size_le_threeQuarters_arith
    (primary secondary split : ℕ)
    (hsecondary : secondary ≤ primary)
    (hsplit : split ≤ secondary) :
    primary / 2 + split ≤
        primary + secondary - (primary + secondary) / 4 ∧
      (primary - (primary / 2 + 1)) + (secondary - split) ≤
        primary + secondary - (primary + secondary) / 4 := by
  omega

Each actual P-MERGE child has size at most three quarters of the parent.

The statement deliberately uses n - n / 4, the natural-number form that also covers all small totals without auxiliary positivity side conditions.


theorem pMerge_childSize_le_threeQuarters [LinearOrder α] (S : MergeSplit α) :
    S.leftSize ≤ S.totalSize - S.totalSize / 4 ∧
      S.rightSize ≤ S.totalSize - S.totalSize / 4 := by
  have hi : S.primary.length / 2 ≤ S.primary.length :=
    Nat.le_of_lt S.pivotIndex_lt
  have hj : S.splitIndex ≤ S.secondary.length := S.splitIndex_le_secondary
  have harith := child_size_le_threeQuarters_arith
    S.primary.length S.secondary.length S.splitIndex
    S.secondary_length_le_primary hj
  have htotal : S.primary.length + S.secondary.length = S.totalSize := by
    simpa [MergeSplit.totalSize] using S.normalized_total
  simpa [MergeSplit.leftSize, MergeSplit.rightSize,
    MergeSplit.lowerPrimary, MergeSplit.lowerSecondary,
    MergeSplit.upperPrimary, MergeSplit.upperSecondary,
    MergeSplit.pivotIndex, List.length_take, Nat.min_eq_left hi,
    Nat.min_eq_left hj, htotal] using harith

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Step

CLRS Chapter 26.3 — One P-MERGE Cost Step

These reader theorems unfold one nonempty executable P-MERGE call. They keep the actual normalized split visible so later strong-induction proofs can use the exact child sizes and the three-quarter shrink theorem.

namespace CLRSnamespace Chapter27

Exact work of one nonempty P-MERGE step: sequential search, two recursive children, one parallel fork/join, and one pivot-placement operation.


theorem pMerge_work_step_eq [LinearOrder α] (xs ys : List α)
    (hzero : xs.length + ys.length ≠ 0) :
    let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
    (pMerge xs ys).work =
      S.search.work +
        (pMerge S.lowerPrimary S.lowerSecondary).work +
        (pMerge S.upperPrimary S.upperSecondary).work + 2 := by
  rw [pMerge]
  simp only [hzero, ↓reduceDIte]
  simp [Costed.seq_work, Costed.par_work, Costed.charge_work]
  omega

Exact span of one nonempty P-MERGE step. Binary search precedes the slower recursive child; fork/join and pivot placement contribute two more units.


theorem pMerge_span_step_eq [LinearOrder α] (xs ys : List α)
    (hzero : xs.length + ys.length ≠ 0) :
    let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
    (pMerge xs ys).span =
      S.search.span +
        max (pMerge S.lowerPrimary S.lowerSecondary).span
          (pMerge S.upperPrimary S.upperSecondary).span + 2 := by
  rw [pMerge]
  simp only [hzero, ↓reduceDIte]
  simp [Costed.seq_span, Costed.par_span, Costed.charge_span]
  omega



private theorem split_search_work_le_total_log [LinearOrder α]
    (S : MergeSplit α) :
    S.search.work ≤ Nat.log 2 S.totalSize + 1 := by
  have hsearch :
      S.search.work ≤ Nat.log 2 S.secondary.length + 1 := by
    rw [S.search_eq]
    exact binaryLowerBound_work_le_log S.secondary S.pivot
  have hsecondary : S.secondary.length ≤ S.totalSize := by
    calc
      S.secondary.length ≤ S.primary.length + S.secondary.length := Nat.le_add_left _ _
      _ = S.totalSize := by
        simpa [MergeSplit.totalSize] using S.normalized_total
  have hlog : Nat.log 2 S.secondary.length ≤ Nat.log 2 S.totalSize :=
    Nat.log_monotone hsecondary
  omega



private theorem split_search_span_le_total_log [LinearOrder α]
    (S : MergeSplit α) :
    S.search.span ≤ Nat.log 2 S.totalSize + 1 := by
  have hsearch :
      S.search.span ≤ Nat.log 2 S.secondary.length + 1 := by
    rw [S.search_eq]
    exact binaryLowerBound_span_le_log S.secondary S.pivot
  have hsecondary : S.secondary.length ≤ S.totalSize := by
    calc
      S.secondary.length ≤ S.primary.length + S.secondary.length := Nat.le_add_left _ _
      _ = S.totalSize := by
        simpa [MergeSplit.totalSize] using S.normalized_total
  have hlog : Nat.log 2 S.secondary.length ≤ Nat.log 2 S.totalSize :=
    Nat.log_monotone hsecondary
  omega

One-step work upper bound in a form suitable for strong induction.

theorem pMerge_work_step_le [LinearOrder α] (xs ys : List α)
    (hzero : xs.length + ys.length ≠ 0) :
    let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
    (pMerge xs ys).work ≤
      (pMerge S.lowerPrimary S.lowerSecondary).work +
        (pMerge S.upperPrimary S.upperSecondary).work +
        Nat.log 2 S.totalSize + 3 := by
  dsimp only
  let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
  have heq := pMerge_work_step_eq xs ys hzero
  have hsearch := split_search_work_le_total_log S
  change (pMerge xs ys).work ≤
    (pMerge S.lowerPrimary S.lowerSecondary).work +
      (pMerge S.upperPrimary S.upperSecondary).work +
      Nat.log 2 S.totalSize + 3
  change (pMerge xs ys).work = S.search.work +
    (pMerge S.lowerPrimary S.lowerSecondary).work +
    (pMerge S.upperPrimary S.upperSecondary).work + 2 at heq
  omega

One-step span upper bound in a form suitable for strong induction.

theorem pMerge_span_step_le [LinearOrder α] (xs ys : List α)
    (hzero : xs.length + ys.length ≠ 0) :
    let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
    (pMerge xs ys).span ≤
      max (pMerge S.lowerPrimary S.lowerSecondary).span
          (pMerge S.upperPrimary S.upperSecondary).span +
        Nat.log 2 S.totalSize + 3 := by
  dsimp only
  let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
  have heq := pMerge_span_step_eq xs ys hzero
  have hsearch := split_search_span_le_total_log S
  change (pMerge xs ys).span ≤
    max (pMerge S.lowerPrimary S.lowerSecondary).span
        (pMerge S.upperPrimary S.upperSecondary).span +
      Nat.log 2 S.totalSize + 3
  change (pMerge xs ys).span = S.search.span +
    max (pMerge S.lowerPrimary S.lowerSecondary).span
      (pMerge S.upperPrimary S.upperSecondary).span + 2 at heq
  omega

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Work.LogPotential

CLRS Chapter 26.3 — P-MERGE Work Potential

This module isolates the natural-logarithm arithmetic that pays for the binary search performed at every P-MERGE node. The actual three-quarter child bound implies that, once the parent is moderately large, both children retain at least one quarter of its elements up to the removed pivot.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace Costsnamespace Work

The two child logarithms, together with a fixed budget of 64, pay for the parent's binary-search charge and the change in logarithmic potential.

The small range n < 64 is covered by the fixed budget. Above that range, a + 1 and b + 1 are at least n / 4, so each child logarithm is at least log₂ n - 2.


theorem logPotential_step (a b n : ℕ)
    (hn : 0 < n)
    (hsum : a + b + 1 = n)
    (ha : a ≤ n - n / 4)
    (hb : b ≤ n - n / 4) :
    Nat.log 2 n + 3 + 8 * Nat.log 2 (n + 1) ≤
      64 + 8 * Nat.log 2 (a + 1) + 8 * Nat.log 2 (b + 1) := by
  by_cases hsmall : n < 64
  · have hn_ne : n ≠ 0 := Nat.ne_of_gt hn
    have hlogn : Nat.log 2 n < 6 := by
      apply Nat.log_lt_of_lt_pow hn_ne
      norm_num
      exact hsmall
    have hsucc : n + 1 ≤ 64 := by omega
    have hlogsucc : Nat.log 2 (n + 1) ≤ 6 := by
      calc
        Nat.log 2 (n + 1) ≤ Nat.log 2 64 := Nat.log_monotone hsucc
        _ = 6 := by norm_num
    omega
  · have hn64 : 64 ≤ n := by omega
    have hn_ne : n ≠ 0 := by omega
    have haquarter : n / 4 ≤ a + 1 := by omega
    have hbquarter : n / 4 ≤ b + 1 := by omega
    have hlogdiv : Nat.log 2 (n / 4) = Nat.log 2 n - 2 := by
      simpa using Nat.log_div_base_pow 2 n 2
    have hloga : Nat.log 2 n - 2 ≤ Nat.log 2 (a + 1) := by
      rw [← hlogdiv]
      exact Nat.log_monotone haquarter
    have hlogb : Nat.log 2 n - 2 ≤ Nat.log 2 (b + 1) := by
      rw [← hlogdiv]
      exact Nat.log_monotone hbquarter
    have hlogn : 6 ≤ Nat.log 2 n := by
      calc
        6 = Nat.log 2 64 := by norm_num
        _ ≤ Nat.log 2 n := Nat.log_monotone hn64
    have hlogsucc : Nat.log 2 (n + 1) ≤ Nat.log 2 n + 1 := by
      have hsucc : n + 1 ≤ n * 2 := by omega
      calc
        Nat.log 2 (n + 1) ≤ Nat.log 2 (n * 2) := Nat.log_monotone hsucc
        _ = Nat.log 2 n + 1 := Nat.log_mul_base (by norm_num) hn_ne
    omega

              end Workend Costsend ParallelMergeend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Work.Bounds

CLRS Chapter 26.3 — P-MERGE Linear Work

The lower bound counts the pivot removed at every nonempty recursive node. The upper bound uses a logarithmic potential to amortize the binary searches over the actual midpoint/lower-bound recursion tree.

Main results:

pMerge_work_lower: P-MERGE has at least linear pointwise work.
pMerge_work_upper: P-MERGE has at most linear pointwise work.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace Costsnamespace Work

private theorem lower_of_total [LinearOrder α] (n : ℕ) :
    ∀ (xs ys : List α), xs.length + ys.length = n →
      n ≤ (pMerge xs ys).work + 1 := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs ys htotal
      by_cases hzero : xs.length + ys.length = 0
      · omega
      · let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
        have hleft_lt : S.leftSize < n := by
          calc
            S.leftSize < S.totalSize := S.leftSize_lt
            _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hright_lt : S.rightSize < n := by
          calc
            S.rightSize < S.totalSize := S.rightSize_lt
            _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hleft : S.leftSize ≤
            (pMerge S.lowerPrimary S.lowerSecondary).work + 1 :=
          ih S.leftSize hleft_lt S.lowerPrimary S.lowerSecondary rfl
        have hright : S.rightSize ≤
            (pMerge S.upperPrimary S.upperSecondary).work + 1 :=
          ih S.rightSize hright_lt S.upperPrimary S.upperSecondary rfl
        have hchildren := pMerge_childSizes_add_one S
        have hwork : (pMerge xs ys).work =
            S.search.work +
              (pMerge S.lowerPrimary S.lowerSecondary).work +
              (pMerge S.upperPrimary S.upperSecondary).work + 2 := by
          simpa only [S] using pMerge_work_step_eq xs ys hzero
        have hSn : S.totalSize = n := by
          calc
            S.totalSize = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        subst n
        omega

Stronger internal-namespace upper invariant. The subtracted logarithmic potential prevents the binary-search charges from adding an extra logarithmic factor. It is visible so later divide-and-conquer algorithms can absorb their fork charge; the top-level P-MERGE interface remains the linear bound below.


theorem potential_of_total [LinearOrder α] (n : ℕ) :
    ∀ (xs ys : List α), xs.length + ys.length = n →
      (pMerge xs ys).work + 8 * Nat.log 2 (n + 1) ≤ 64 * n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs ys htotal
      by_cases hzero : xs.length + ys.length = 0
      · have hn : n = 0 := by omega
        subst n
        have hxs : xs = [] := by simpa using (show xs.length = 0 by omega)
        have hys : ys = [] := by simpa using (show ys.length = 0 by omega)
        subst xs
        subst ys
        simp [pMerge]
      · let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
        have hleft_lt : S.leftSize < n := by
          calc
            S.leftSize < S.totalSize := S.leftSize_lt
            _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hright_lt : S.rightSize < n := by
          calc
            S.rightSize < S.totalSize := S.rightSize_lt
            _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hleft :=
          ih S.leftSize hleft_lt S.lowerPrimary S.lowerSecondary rfl
        have hright :=
          ih S.rightSize hright_lt S.upperPrimary S.upperSecondary rfl
        change (pMerge S.lowerPrimary S.lowerSecondary).work +
          8 * Nat.log 2 (S.leftSize + 1) ≤ 64 * S.leftSize at hleft
        change (pMerge S.upperPrimary S.upperSecondary).work +
          8 * Nat.log 2 (S.rightSize + 1) ≤ 64 * S.rightSize at hright
        have hchildren := pMerge_childSizes_add_one S
        have hquarters := pMerge_childSize_le_threeQuarters S
        have hpotential := logPotential_step S.leftSize S.rightSize S.totalSize
          S.total_positive hchildren hquarters.1 hquarters.2
        have hwork : (pMerge xs ys).work ≤
            (pMerge S.lowerPrimary S.lowerSecondary).work +
              (pMerge S.upperPrimary S.upperSecondary).work +
              Nat.log 2 S.totalSize + 3 := by
          simpa only [S] using pMerge_work_step_le xs ys hzero
        have hSn : S.totalSize = n := by
          calc
            S.totalSize = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        rw [← hSn]
        omega

              end Workend Costsend ParallelMerge

Public theorems

Every input element except possibly the final zero-work boundary accounts for a pivot-placement node in the P-MERGE recursion tree.

theorem pMerge_work_lower [LinearOrder α] (xs ys : List α) :
    xs.length + ys.length ≤ (pMerge xs ys).work + 1 := by
  exact ParallelMerge.Costs.Work.lower_of_total
    (xs.length + ys.length) xs ys rfl

The work of the actual midpoint/binary-search P-MERGE execution is linear in the total input size.

theorem pMerge_work_upper [LinearOrder α] (xs ys : List α) :
    (pMerge xs ys).work ≤ 64 * (xs.length + ys.length + 1) := by
  have h := ParallelMerge.Costs.Work.potential_of_total
    (xs.length + ys.length) xs ys rfl
  omega

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Span.Envelope

CLRS Chapter 26.3 — A Three-Quarter Span Envelope

This module solves the recurrence generated by the actual P-MERGE child-size bound. Three applications of n - n / 4 (rather than two) cross a binary-log level above the finite base kernel.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace Costsnamespace Spanset_option maxRecDepth 100000

The natural-number three-quarter shrink used by the P-MERGE analysis.

def shrink (n : ℕ) : ℕ := n - n / 4

private theorem shrink_lt (n : ℕ) (hn : 64 ≤ n) : shrink n < n := by
  simp only [shrink]
  omega

private theorem shrink_monotone : Monotone shrink := by
  intro a b hab
  simp only [shrink]
  omega

A total recurrence envelope for the span of P-MERGE. Values below 64 form a finite kernel; larger values pay one logarithmic search level and recur on the three-quarter bound.

def pMergeSpanUpper (n : ℕ) : ℕ :=
  if h : n < 64 then
    64 * (Nat.log 2 n + 1) ^ 2
  else
    pMergeSpanUpper (shrink n) + Nat.log 2 n + 3
termination_by n
decreasing_by
  exact shrink_lt n (by omega)

              

theorem pMergeSpanUpper_small (n : ℕ) (hn : n < 64) :
    pMergeSpanUpper n = 64 * (Nat.log 2 n + 1) ^ 2 := by
  rw [pMergeSpanUpper]
  simp [hn]

theorem pMergeSpanUpper_large (n : ℕ) (hn : 64 ≤ n) :
    pMergeSpanUpper n =
      pMergeSpanUpper (shrink n) + Nat.log 2 n + 3 := by
  rw [pMergeSpanUpper]
  simp [show ¬n < 64 by omega]

private theorem pMergeSpanUpper_le_succ (n : ℕ) :
    pMergeSpanUpper n ≤ pMergeSpanUpper (n + 1) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n < 63
      · rw [pMergeSpanUpper_small n (by omega),
          pMergeSpanUpper_small (n + 1) (by omega)]
        have hlog := Nat.log_monotone (b := 2)
          (show n ≤ n + 1 by omega : n ≤ n + 1)
        nlinarith
      · by_cases hn63 : n = 63
        · subst n
          rw [pMergeSpanUpper_small 63 (by omega),
            pMergeSpanUpper_large 64 (by omega),
            show shrink 64 = 48 by norm_num [shrink],
            pMergeSpanUpper_small 48 (by omega)]
          norm_num
        · have hn64 : 64 ≤ n := by omega
          rw [pMergeSpanUpper_large n hn64,
            pMergeSpanUpper_large (n + 1) (by omega)]
          have hs : shrink n ≤ shrink (n + 1) :=
            shrink_monotone (by omega)
          have hs_lt : shrink (n + 1) < n := by
            simp only [shrink]
            omega
          have hupper : pMergeSpanUpper (shrink n) ≤
              pMergeSpanUpper (shrink (n + 1)) := by
            exact Nat.le_induction (m := shrink n)
              (P := fun k _ => k ≤ shrink (n + 1) →
                pMergeSpanUpper (shrink n) ≤ pMergeSpanUpper k)
              (fun _ => le_rfl)
              (fun k _ hk hksucc =>
                (hk (by omega)).trans (ih k (by omega)))
              (shrink (n + 1)) hs le_rfl
          have hlog := Nat.log_monotone (b := 2)
            (show n ≤ n + 1 by omega : n ≤ n + 1)
          omega

The recurrence envelope is monotone in the input-size bound.

theorem pMergeSpanUpper_monotone : Monotone pMergeSpanUpper :=
  monotone_nat_of_le_succ pMergeSpanUpper_le_succ

              private theorem shrink_three_twice_lt (n : ℕ) (hn : 128 ≤ n) :
    2 * shrink (shrink (shrink n)) < n := by
  simp only [shrink]
  omega

private theorem shrink_three_log (n : ℕ) (hn : 128 ≤ n) :
    Nat.log 2 (shrink (shrink (shrink n))) + 1 ≤ Nat.log 2 n := by
  let p := 2 ^ Nat.log 2 n
  have hn0 : n ≠ 0 := by omega
  have hp_le : p ≤ n := by
    simpa [p] using Nat.pow_log_le_self 2 hn0
  have hn_lt : n < 2 * p := by
    simpa [p, pow_succ, Nat.mul_comm] using
      Nat.lt_pow_succ_log_self (by omega : 1 < 2) n
  have hthree := shrink_three_twice_lt n hn
  have hlt : shrink (shrink (shrink n)) < p := by omega
  have hlog0 : Nat.log 2 n ≠ 0 := by
    have : 7 ≤ Nat.log 2 n := by
      calc
        7 = Nat.log 2 128 := by norm_num
        _ ≤ Nat.log 2 n := Nat.log_monotone hn
    omega
  have := Nat.log_lt_of_lt_pow' hlog0 hlt
  omegaprivate theorem shrink_lower_64 (n : ℕ) (hn : 128 ≤ n) :
    64 ≤ shrink n ∧ 64 ≤ shrink (shrink n) := by
  simp only [shrink]
  omega

The three-quarter recurrence is bounded by a quadratic binary logarithm. The proof unfolds exactly three large levels; the third shrink lies below the current highest power of two.


theorem pMergeSpanUpper_le_quadratic (n : ℕ) :
    pMergeSpanUpper n ≤ 64 * (Nat.log 2 n + 1) ^ 2 := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn64 : n < 64
      · exact (pMergeSpanUpper_small n hn64).le
      · have hn64 : 64 ≤ n := by omega
        by_cases hn128 : n < 128
        · have hlogn : 6 ≤ Nat.log 2 n := by
            calc
              6 = Nat.log 2 64 := by norm_num
              _ ≤ Nat.log 2 n := Nat.log_monotone hn64
          have hs1le : shrink n ≤ n := by simp [shrink]
          have hs2le : shrink (shrink n) ≤ n :=
            (show shrink (shrink n) ≤ shrink n by simp [shrink]).trans hs1le
          have hs3lt64 : shrink (shrink (shrink n)) < 64 := by
            simp only [shrink]
            omega
          rw [pMergeSpanUpper_large n hn64]
          by_cases hs1 : shrink n < 64
          · rw [pMergeSpanUpper_small (shrink n) hs1]
            have hdrop : Nat.log 2 (shrink n) + 1 ≤ Nat.log 2 n := by
              have hchild : Nat.log 2 (shrink n) ≤ Nat.log 2 63 :=
                Nat.log_monotone (by omega)
              norm_num at hchild
              omega
            nlinarith
          · rw [pMergeSpanUpper_large (shrink n) (by omega)]
            by_cases hs2 : shrink (shrink n) < 64
            · rw [pMergeSpanUpper_small (shrink (shrink n)) hs2]
              have hdrop : Nat.log 2 (shrink (shrink n)) + 1 ≤ Nat.log 2 n := by
                have hchild : Nat.log 2 (shrink (shrink n)) ≤ Nat.log 2 63 :=
                  Nat.log_monotone (by omega)
                norm_num at hchild
                omega
              have hlog1 := Nat.log_monotone (b := 2) hs1le
              nlinarith
            · rw [pMergeSpanUpper_large (shrink (shrink n)) (by omega),
                pMergeSpanUpper_small (shrink (shrink (shrink n))) hs3lt64]
              have hdrop : Nat.log 2 (shrink (shrink (shrink n))) + 1 ≤
                  Nat.log 2 n := by
                have hchild : Nat.log 2 (shrink (shrink (shrink n))) ≤
                    Nat.log 2 63 := Nat.log_monotone (by omega)
                norm_num at hchild
                omega
              have hlog1 := Nat.log_monotone (b := 2) hs1le
              have hlog2 := Nat.log_monotone (b := 2) hs2le
              nlinarith
        · have hn128 : 128 ≤ n := by omega
          obtain ⟨hs1, hs2⟩ := shrink_lower_64 n hn128
          rw [pMergeSpanUpper_large n (by omega),
            pMergeSpanUpper_large (shrink n) hs1,
            pMergeSpanUpper_large (shrink (shrink n)) hs2]
          have hs3lt : shrink (shrink (shrink n)) < n := by
            have := shrink_three_twice_lt n hn128
            omega
          have hrec := ih (shrink (shrink (shrink n))) hs3lt
          have hdrop := shrink_three_log n hn128
          have hlog1 : Nat.log 2 (shrink n) ≤ Nat.log 2 n :=
            Nat.log_monotone (show shrink n ≤ n by simp [shrink])
          have hlog2 : Nat.log 2 (shrink (shrink n)) ≤ Nat.log 2 n := by
            exact Nat.log_monotone (b := 2) (le_trans
              (shrink_monotone (show shrink n ≤ n by simp [shrink]))
              (show shrink n ≤ n by simp [shrink]))
          nlinarith

              end Spanend Costsend ParallelMergeend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Span.Bounds

CLRS Chapter 26.3 — Pointwise P-MERGE Span Upper Bound

This module connects the executable split to the monotone three-quarter envelope and publishes the quadratic-logarithmic upper bound.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace Costsnamespace Spanprivate theorem log_charge_le_removed (n : ℕ) (hn : 9 ≤ n) :
    Nat.log 2 n + 3 ≤ 8 * (n - shrink n) := by
  have hlog := Nat.log_le_self 2 n
  simp only [shrink]
  omega

private theorem linear_of_total [LinearOrder α] (n : ℕ) :
    ∀ (xs ys : List α), xs.length + ys.length = n →
      (pMerge xs ys).span ≤ 8 * n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs ys htotal
      by_cases hzero : xs.length + ys.length = 0
      · have hn : n = 0 := by omega
        subst n
        have hxs : xs = [] := by simpa using (show xs.length = 0 by omega)
        have hys : ys = [] := by simpa using (show ys.length = 0 by omega)
        subst xs
        subst ys
        simp [pMerge]
      · let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
        have hnpos : 0 < n := by omega
        have hSn : S.totalSize = n := by
          calc
            S.totalSize = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hleft_lt : S.leftSize < n := by
          rw [← hSn]
          exact S.leftSize_lt
        have hright_lt : S.rightSize < n := by
          rw [← hSn]
          exact S.rightSize_lt
        have hleft := ih S.leftSize hleft_lt
          S.lowerPrimary S.lowerSecondary rfl
        have hright := ih S.rightSize hright_lt
          S.upperPrimary S.upperSecondary rfl
        have hquarters := pMerge_childSize_le_threeQuarters S
        have hstep : (pMerge xs ys).span ≤
            max (pMerge S.lowerPrimary S.lowerSecondary).span
                (pMerge S.upperPrimary S.upperSecondary).span +
              Nat.log 2 n + 3 := by
          have := pMerge_span_step_le xs ys hzero
          simpa only [S, hSn] using this
        have hmax : max (pMerge S.lowerPrimary S.lowerSecondary).span
              (pMerge S.upperPrimary S.upperSecondary).span ≤
            8 * shrink n := by
          apply max_le
          · calc
              (pMerge S.lowerPrimary S.lowerSecondary).span ≤
                  8 * S.leftSize := hleft
              _ ≤ 8 * shrink n := Nat.mul_le_mul_left 8 (by simpa [hSn, shrink]
                using hquarters.1)
          · calc
              (pMerge S.upperPrimary S.upperSecondary).span ≤
                  8 * S.rightSize := hright
              _ ≤ 8 * shrink n := Nat.mul_le_mul_left 8 (by simpa [hSn, shrink]
                using hquarters.2)
        by_cases hnsmall : n < 9
        · have hmaxSmall : max (pMerge S.lowerPrimary S.lowerSecondary).span
              (pMerge S.upperPrimary S.upperSecondary).span ≤ 8 * (n - 1) := by
            apply max_le
            · exact hleft.trans (Nat.mul_le_mul_left 8 (by omega))
            · exact hright.trans (Nat.mul_le_mul_left 8 (by omega))
          calc
            (pMerge xs ys).span ≤
                max (pMerge S.lowerPrimary S.lowerSecondary).span
                    (pMerge S.upperPrimary S.upperSecondary).span +
                  Nat.log 2 n + 3 := hstep
            _ ≤ 8 * (n - 1) + Nat.log 2 n + 3 := by omega
            _ ≤ 8 * n := by interval_cases n <;> norm_num
        · have hcharge := log_charge_le_removed n (by omega)
          omegaprivate theorem small_linear_le_quadratic (n : ℕ) (hn : n < 64) :
    8 * n ≤ 64 * (Nat.log 2 n + 1) ^ 2 := by
  interval_cases n <;> norm_num

private theorem envelope_of_total [LinearOrder α] (n : ℕ) :
    ∀ (xs ys : List α), xs.length + ys.length = n →
      (pMerge xs ys).span ≤ pMergeSpanUpper n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs ys htotal
      by_cases hnsmall : n < 64
      · calc
          (pMerge xs ys).span ≤ 8 * n := linear_of_total n xs ys htotal
          _ ≤ 64 * (Nat.log 2 n + 1) ^ 2 := small_linear_le_quadratic n hnsmall
          _ = pMergeSpanUpper n := (pMergeSpanUpper_small n hnsmall).symm
      · have hn64 : 64 ≤ n := by omega
        have hzero : xs.length + ys.length ≠ 0 := by omega
        let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
        have hSn : S.totalSize = n := by
          calc
            S.totalSize = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hleft_lt : S.leftSize < n := by rw [← hSn]; exact S.leftSize_lt
        have hright_lt : S.rightSize < n := by rw [← hSn]; exact S.rightSize_lt
        have hleft := ih S.leftSize hleft_lt
          S.lowerPrimary S.lowerSecondary rfl
        have hright := ih S.rightSize hright_lt
          S.upperPrimary S.upperSecondary rfl
        have hquarters := pMerge_childSize_le_threeQuarters S
        have hleftE : (pMerge S.lowerPrimary S.lowerSecondary).span ≤
            pMergeSpanUpper (shrink n) := hleft.trans
          (pMergeSpanUpper_monotone (by simpa [hSn, shrink] using hquarters.1))
        have hrightE : (pMerge S.upperPrimary S.upperSecondary).span ≤
            pMergeSpanUpper (shrink n) := hright.trans
          (pMergeSpanUpper_monotone (by simpa [hSn, shrink] using hquarters.2))
        have hstep := pMerge_span_step_le xs ys hzero
        rw [pMergeSpanUpper_large n hn64]
        change (pMerge xs ys).span ≤
          pMergeSpanUpper (shrink n) + Nat.log 2 n + 3
        change (pMerge xs ys).span ≤
          max (pMerge S.lowerPrimary S.lowerSecondary).span
              (pMerge S.upperPrimary S.upperSecondary).span +
            Nat.log 2 S.totalSize + 3 at hstep
        rw [hSn] at hstep
        omegaend Spanend Costsend ParallelMerge

Public theorem

P-MERGE has pointwise O(log² n) span on every pair of inputs.

theorem pMerge_span_upper [LinearOrder α] (xs ys : List α) :
    (pMerge xs ys).span ≤
      64 * (Nat.log 2 (xs.length + ys.length) + 1) ^ 2 := by
  exact (ParallelMerge.Costs.Span.envelope_of_total
    (xs.length + ys.length) xs ys rfl).trans
      (ParallelMerge.Costs.Span.pMergeSpanUpper_le_quadratic _)

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Span.WitnessLists

CLRS Chapter 26.3 — Interleaved P-MERGE Witness Lists

The even and odd key lists are sorted, have transparent lengths, and their prefixes reproduce the same witness family at smaller sizes.

namespace CLRSnamespace Chapter27

The first n even natural numbers.

def evenKeys (n : ℕ) : List ℕ := (List.range n).map (fun i => 2 * i)

The first n odd natural numbers.

def oddKeys (n : ℕ) : List ℕ := (List.range n).map (fun i => 2 * i + 1)

              @[simp] theorem evenKeys_length (n : ℕ) : (evenKeys n).length = n := by
  simp [evenKeys]@[simp] theorem oddKeys_length (n : ℕ) : (oddKeys n).length = n := by
  simp [oddKeys]

theorem evenKeys_sorted (n : ℕ) : (evenKeys n).Pairwise (· ≤ ·) := by
  rw [evenKeys, List.pairwise_map]
  exact List.pairwise_lt_range.imp (by omega)

theorem oddKeys_sorted (n : ℕ) : (oddKeys n).Pairwise (· ≤ ·) := by
  rw [oddKeys, List.pairwise_map]
  exact List.pairwise_lt_range.imp (by omega)@[simp] theorem evenKeys_take (m n : ℕ) :
    (evenKeys n).take m = evenKeys (min m n) := by
  simp [evenKeys, ← List.map_take]@[simp] theorem oddKeys_take (m n : ℕ) :
    (oddKeys n).take m = oddKeys (min m n) := by
  simp [oddKeys, ← List.map_take]theorem evenKeys_take_of_le (m n : ℕ) (h : m ≤ n) :
    (evenKeys n).take m = evenKeys m := by simp [h]theorem oddKeys_take_of_le (m n : ℕ) (h : m ≤ n) :
    (oddKeys n).take m = oddKeys m := by simp [h]@[simp] theorem evenKeys_get (n : ℕ) (i : Fin (evenKeys n).length) :
    (evenKeys n).get i = 2 * i.1 := by
  simp [evenKeys, List.get_eq_getElem]@[simp] theorem evenKeys_getElem (n i : ℕ) (h : i < (evenKeys n).length) :
    (evenKeys n)[i] = 2 * i := by
  simp [evenKeys]@[simp] theorem oddKeys_get (n : ℕ) (i : Fin (oddKeys n).length) :
    (oddKeys n).get i = 2 * i.1 + 1 := by
  simp [oddKeys, List.get_eq_getElem]namespace ParallelMergenamespace Costsnamespace Span

private theorem lowerBoundSpec_not_lt [LinearOrder α] {xs : List α} {pivot : α}
    {i j : ℕ} (hi : LowerBoundSpec xs pivot i)
    (hj : LowerBoundSpec xs pivot j) (hij : i < j) : False := by
  have hiLen : i < xs.length := lt_of_lt_of_le hij hj.index_le_length
  let x := xs.get ⟨i, hiLen⟩
  have hxDrop : x ∈ xs.drop i := by
    rw [List.mem_iff_getElem]
    refine ⟨0, ?_, ?_⟩
    · simp [hiLen]
    · simp [x, List.get_eq_getElem]
  have hxTake : x ∈ xs.take j := by
    rw [List.mem_iff_getElem]
    refine ⟨i, ?_, ?_⟩
    · simp [hiLen, hij]
    · simp [x, List.get_eq_getElem]
  exact (not_lt_of_ge (hi.right_ge x hxDrop)) (hj.left_lt x hxTake)private theorem lowerBoundSpec_unique [LinearOrder α] {xs : List α} {pivot : α}
    {i j : ℕ} (hi : LowerBoundSpec xs pivot i)
    (hj : LowerBoundSpec xs pivot j) : i = j := by
  by_contra hne
  rcases lt_or_gt_of_ne hne with hij | hji
  · exact lowerBoundSpec_not_lt hi hj hij
  · exact lowerBoundSpec_not_lt hj hi hji

private theorem oddKeys_mid_spec (m n : ℕ) (hmn : m ≤ n) :
    LowerBoundSpec (oddKeys n) (2 * m) m := by
  constructor
  · simpa using hmn
  · intro x hx
    rw [oddKeys_take_of_le m n hmn] at hx
    simp only [oddKeys, List.mem_map] at hx
    obtain ⟨i, hi, rfl⟩ := hx
    simp only [List.mem_range] at hi
    omega
  · intro x hx
    obtain ⟨j, hj, hval⟩ := List.mem_iff_getElem.mp hx
    have hglobal : m + j < (oddKeys n).length := by
      rw [List.length_drop] at hj
      omega
    have hget : (oddKeys n)[m + j] = 2 * (m + j) + 1 := by
      simp [oddKeys]
    rw [← hval, List.getElem_drop, hget]
    omega

Binary lower bound splits an odd-key list exactly at the even pivot's rank.

theorem binaryLowerBound_oddKeys_value (m n : ℕ) (hmn : m ≤ n) :
    (binaryLowerBound (oddKeys n) (2 * m)).value = m := by
  apply lowerBoundSpec_unique (α := ℕ)
  · exact binaryLowerBound_partition (oddKeys n) (2 * m) (oddKeys_sorted n)
  · exact oddKeys_mid_spec m n hmn

              end Spanend Costsend ParallelMergeend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.Costs.Span.LowerBound

CLRS Chapter 26.3 — Interleaved Span Lower Witness

The half-open binary search satisfies a robust reader lemma saying that its span is at least the binary logarithm of one plus the interval length. On the interleaved power-of-two family, the lower recursive child is the same family at half the size, yielding a quadratic span recurrence.

              namespace CLRSnamespace Chapter27namespace ParallelMergenamespace Costsnamespace Span

private theorem log_two_mul_add_one_le (x : ℕ) :
    Nat.log 2 (2 * x + 1) ≤ Nat.log 2 x + 1 := by
  have hxlt := Nat.lt_pow_succ_log_self (by omega : 1 < 2) x
  have hpowpos : 0 < 2 ^ (Nat.log 2 x + 1) := pow_pos (by omega) _
  have hlt : 2 * x + 1 < 2 ^ (Nat.log 2 x + 2) := by
    rw [show Nat.log 2 x + 2 = (Nat.log 2 x + 1) + 1 by omega, pow_succ]
    omega
  have hlog := Nat.log_lt_of_lt_pow' (by omega : Nat.log 2 x + 2 ≠ 0) hlt
  omegaprivate theorem log_parent_le_succ_log_child (parent child : ℕ)
    (hsize : parent + 1 ≤ 2 * (child + 1) + 1) :
    Nat.log 2 (parent + 1) ≤ Nat.log 2 (child + 1) + 1 := by
  calc
    Nat.log 2 (parent + 1) ≤ Nat.log 2 (2 * (child + 1) + 1) :=
      Nat.log_monotone hsize
    _ ≤ Nat.log 2 (child + 1) + 1 :=
      log_two_mul_add_one_le (child + 1)

private theorem loop_log_succ_le_span [LinearOrder α]
    (xs : List α) (pivot : α) (lo hi : ℕ)
    (hlohi : lo ≤ hi) (hhilen : hi ≤ xs.length) :
    Nat.log 2 (hi - lo + 1) ≤
      (ParallelMerge.Internal.loop xs pivot lo hi).span := by
  induction lo, hi using ParallelMerge.Internal.loop.induct xs with
  | case1 lo hi hlt mid hnone =>
      have hmid_lt : mid < xs.length := by dsimp [mid]; omega
      rw [List.getElem?_eq_getElem hmid_lt] at hnone
      contradiction
  | case2 lo hi hlt mid x hget ihRight ihLeft =>
      have hlo_mid : lo ≤ mid := by dsimp [mid]; omega
      have hmid_hi : mid < hi := by dsimp [mid]; omega
      have ihR := ihRight (by omega) hhilen
      have ihL := ihLeft hlo_mid (le_trans (Nat.le_of_lt hmid_hi) hhilen)
      dsimp only [mid] at ihR ihL
      by_cases hxlt : x < pivot
      · rw [ParallelMerge.Internal.loop]
        simp only [hlt, if_true, mid, hget, Costed.seq_span,
          Costed.charge_span, hxlt]
        have hlevel := log_parent_le_succ_log_child
          (hi - lo) (hi - (mid + 1)) (by dsimp [mid]; omega)
        dsimp only [mid] at hlevel
        omega
      · rw [ParallelMerge.Internal.loop]
        simp only [hlt, if_true, mid, hget, Costed.seq_span,
          Costed.charge_span, hxlt, if_false]
        have hlevel := log_parent_le_succ_log_child
          (hi - lo) (mid - lo) (by dsimp [mid]; omega)
        dsimp only [mid] at hlevel
        omega
  | case3 lo hi hnlt =>
      have heq : hi = lo := by omega
      rw [ParallelMerge.Internal.loop]
      simp [heq]private theorem binaryLowerBound_log_succ_le_span [LinearOrder α]
    (xs : List α) (pivot : α) :
    Nat.log 2 (xs.length + 1) ≤ (binaryLowerBound xs pivot).span := by
  simpa [binaryLowerBound] using
    loop_log_succ_le_span xs pivot 0 xs.length (Nat.zero_le _) le_rfl

private theorem binaryLowerBound_oddKeys_span (k : ℕ) :
    k + 1 ≤
      (binaryLowerBound (oddKeys (2 ^ (k + 1))) (2 ^ (k + 1))).span := by
  have hgeneric := binaryLowerBound_log_succ_le_span
    (oddKeys (2 ^ (k + 1))) (2 ^ (k + 1))
  have hpow : Nat.log 2 (2 ^ (k + 1)) = k + 1 :=
    Nat.log_pow (by norm_num) (k + 1)
  have hmono : Nat.log 2 (2 ^ (k + 1)) ≤
      Nat.log 2 ((oddKeys (2 ^ (k + 1))).length + 1) :=
    Nat.log_monotone (by simp)
  omega

private theorem witness_lower_split (k : ℕ) :
    let n := 2 ^ (k + 1)
    let S := mergeSplit (evenKeys n) (oddKeys n) (by
      simp only [evenKeys_length, oddKeys_length]
      positivity)
    S.lowerPrimary = evenKeys (2 ^ k) ∧
      S.lowerSecondary = oddKeys (2 ^ k) ∧
      S.search = binaryLowerBound (oddKeys n) n := by
  dsimp only
  have hv := binaryLowerBound_oddKeys_value (2 ^ k) (2 ^ (k + 1)) (by
    rw [pow_succ]
    omega)
  have hv' :
      (binaryLowerBound (oddKeys (2 * 2 ^ k)) (2 * 2 ^ k)).value = 2 ^ k := by
    simpa [pow_succ, Nat.mul_comm] using hv
  have hp : 0 < 2 ^ k := pow_pos (by omega) _
  have hle : 2 ^ k ≤ 2 * 2 ^ k := by omega
  simp [mergeSplit, MergeSplit.lowerPrimary, MergeSplit.lowerSecondary,
    MergeSplit.pivotIndex, MergeSplit.splitIndex, hv', hle,
    pow_succ, Nat.mul_comm]

private theorem witness_span_step (k : ℕ) :
    2 * (pMerge (evenKeys (2 ^ (k + 1))) (oddKeys (2 ^ (k + 1)))).span ≥
      2 * (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span + (k + 1) + 4 := by
  let n := 2 ^ (k + 1)
  have hzero : (evenKeys n).length + (oddKeys n).length ≠ 0 := by simp [n]
  let S := mergeSplit (evenKeys n) (oddKeys n) (Nat.pos_of_ne_zero hzero)
  obtain ⟨hlowerP, hlowerS, hsearch⟩ := witness_lower_split k
  have hstep := pMerge_span_step_eq (evenKeys n) (oddKeys n) hzero
  change (pMerge (evenKeys n) (oddKeys n)).span =
    S.search.span +
      max (pMerge S.lowerPrimary S.lowerSecondary).span
        (pMerge S.upperPrimary S.upperSecondary).span + 2 at hstep
  have hsearchSpan : k + 1 ≤ S.search.span := by
    rw [hsearch]
    simpa [n] using binaryLowerBound_oddKeys_span k
  have hchild : (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span ≤
      max (pMerge S.lowerPrimary S.lowerSecondary).span
        (pMerge S.upperPrimary S.upperSecondary).span := by
    rw [hlowerP, hlowerS]
    exact Nat.le_max_left _ _
  have hraw : S.search.span +
        (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span + 2 ≤
      (pMerge (evenKeys n) (oddKeys n)).span := by
    rw [hstep]
    omega
  have hcost : 2 * (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span +
        (k + 1) + 4 ≤
      2 * (S.search.span +
        (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span + 2) := by
    omega
  exact hcost.trans (Nat.mul_le_mul_left 2 hraw)

private theorem witness_span_quadratic (k : ℕ) :
    (k + 1) ^ 2 ≤
      8 * (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span := by
  induction k with
  | zero =>
      have hzero : (evenKeys 1).length + (oddKeys 1).length ≠ 0 := by simp
      have hstep := pMerge_span_step_eq (evenKeys 1) (oddKeys 1) hzero
      have hbase : 2 ≤ (pMerge (evenKeys 1) (oddKeys 1)).span := by
        rw [hstep]
        omega
      norm_num only [zero_add, pow_zero]
      calc
        1 ≤ 8 * 2 := by norm_num
        _ ≤ 8 * (pMerge (evenKeys 1) (oddKeys 1)).span :=
          Nat.mul_le_mul_left 8 hbase
  | succ k ih =>
      have hstep := witness_span_step k
      nlinarithend Spanend Costsend ParallelMerge

Public theorem

Interleaved even/odd inputs attain quadratic logarithmic span on exact powers of two, up to the explicit constant factor eight.

theorem pMerge_interleaved_span_lower (k : ℕ) :
    (k + 1) ^ 2 ≤
      8 * (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span := by
  exact ParallelMerge.Costs.Span.witness_span_quadratic k

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Definitions

CLRS Chapter 26.3 — Executable P-MERGE-SORT

This module implements the pure functional control structure of CLRS P-MERGE-SORT. Nontrivial inputs are split at their midpoint, the two halves are sorted in parallel, and their sorted values are combined by the executable P-MERGE algorithm.

namespace CLRSnamespace Chapter27

Parallel merge sort with execution-attached work and span.

Lists of length zero or one are returned unchanged, charging one unit per element. Larger lists recursively sort their midpoint halves through one fork/join and then invoke P-MERGE sequentially on the two results.

def pMergeSort [LinearOrder α] (xs : List α) : Costed (List α) :=
  if hsmall : xs.length ≤ 1 then
    Costed.charge xs.length xs.length xs
  else
    let mid := xs.length / 2
    let left := xs.take mid
    let right := xs.drop mid
    Costed.seq (Costed.par (pMergeSort left) (pMergeSort right)) fun sorted =>
      pMerge sorted.1 sorted.2
termination_by xs.length
decreasing_by
  · simp_wf
    omega
  · simp_wf
    omega

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Correctness.Spec

CLRS Chapter 26.3 — P-MERGE-SORT Specification

This module defines the semantic result predicate used by the P-MERGE-SORT proof and records the two value-reconstruction facts needed by its induction.

namespace CLRSnamespace Chapter27

Semantic specification for a P-MERGE-SORT result: it is sorted, preserves the input multiset, and has exactly the input length.

structure PMergeSortSpec [LinearOrder α] (xs out : List α) : Prop where
  sorted : out.Pairwise (· ≤ ·)
  perm : out.Perm xs
  length_eq : out.length = xs.length

              namespace ParallelMergeSortnamespace Correctnessvariable [LinearOrder α]

Every list of length at most one is sorted, whether or not sortedness was assumed of the input.


theorem pairwise_of_length_le_one (xs : List α) (hsmall : xs.length ≤ 1) :
    xs.Pairwise (· ≤ ·) := by
  cases xs with
  | nil => exact List.Pairwise.nil
  | cons x tail =>
      have htail : tail = [] := by
        apply List.eq_nil_of_length_eq_zero
        simp only [List.length_cons] at hsmall
        omega
      subst tail
      simp

On the base branch, the value returned by P-MERGE-SORT is the input list.


theorem value_eq_self (xs : List α) (hsmall : xs.length ≤ 1) :
    (pMergeSort xs).value = xs := by
  rw [pMergeSort]
  simp [hsmall]

On a recursive branch, the value returned by P-MERGE-SORT is the value of P-MERGE applied to the two recursively sorted halves.


theorem value_eq_merge (xs : List α) (hsmall : ¬ xs.length ≤ 1) :
    let mid := xs.length / 2
    let left := xs.take mid
    let right := xs.drop mid
    (pMergeSort xs).value =
      (pMerge (pMergeSort left).value (pMergeSort right).value).value := by
  rw [pMergeSort]
  simp [hsmall]

              end Correctnessend ParallelMergeSortend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Correctness.Main

CLRS Chapter 26.3 — P-MERGE-SORT Correctness

P-MERGE-SORT is proved correct by strong induction on the input length. The recursive case sorts the midpoint halves, invokes the already proved P-MERGE specification, and reconstructs the original input through take/drop.

Main results:

pMergeSort_correct: sortedness, permutation, and exact output length.
pMergeSort_value_sorted, pMergeSort_value_perm, and pMergeSort_value_length: direct projections for downstream proofs.

              namespace CLRSnamespace Chapter27namespace ParallelMergeSortnamespace Correctnessvariable [LinearOrder α]

Strong-induction form of P-MERGE-SORT correctness, indexed by input length.


private theorem correct_of_length (n : ℕ) :
    ∀ (xs : List α), xs.length = n →
      PMergeSortSpec xs (pMergeSort xs).value := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs hlength
      by_cases hsmall : xs.length ≤ 1
      · have hvalue := value_eq_self xs hsmall
        rw [hvalue]
        exact ⟨pairwise_of_length_le_one xs hsmall, List.Perm.refl xs, rfl⟩
      · let mid := xs.length / 2
        let left := xs.take mid
        let right := xs.drop mid
        have hn : 2 ≤ n := by omega
        have hleftLength : left.length = mid := by
          simp [left, mid]
          omega
        have hleft_lt : left.length < n := by
          rw [hleftLength]
          simp [mid]
          omega
        have hrightLength : right.length = xs.length - mid := by
          simp [right]
        have hright_lt : right.length < n := by
          rw [hrightLength]
          simp [mid]
          omega
        have hleft : PMergeSortSpec left (pMergeSort left).value :=
          ih left.length hleft_lt left rfl
        have hright : PMergeSortSpec right (pMergeSort right).value :=
          ih right.length hright_lt right rfl
        have hmerge : PMergeSpec (pMergeSort left).value (pMergeSort right).value
            (pMerge (pMergeSort left).value (pMergeSort right).value).value :=
          pMerge_correct _ _ hleft.sorted hright.sorted
        have hvalue : (pMergeSort xs).value =
            (pMerge (pMergeSort left).value (pMergeSort right).value).value := by
          simpa [mid, left, right] using value_eq_merge xs hsmall
        have hperm :
            (pMerge (pMergeSort left).value (pMergeSort right).value).value.Perm xs := by
          have hparts : ((pMergeSort left).value ++
              (pMergeSort right).value).Perm (left ++ right) :=
            hleft.perm.append hright.perm
          have htakeDrop : left ++ right = xs := by
            simp [left, right]
          rw [htakeDrop] at hparts
          exact hmerge.perm.trans hparts
        rw [hvalue]
        exact ⟨hmerge.sorted, hperm, hperm.length_eq⟩

end Correctnessend ParallelMergeSort

Public theorems

P-MERGE-SORT returns a sorted permutation of every input list, with exact output length.

theorem pMergeSort_correct [LinearOrder α] (xs : List α) :
    PMergeSortSpec xs (pMergeSort xs).value := by
  exact ParallelMergeSort.Correctness.correct_of_length xs.length xs rfl

The value returned by P-MERGE-SORT is sorted.

theorem pMergeSort_value_sorted [LinearOrder α] (xs : List α) :
    (pMergeSort xs).value.Pairwise (· ≤ ·) :=
  (pMergeSort_correct xs).sorted

The value returned by P-MERGE-SORT contains exactly the input multiset.

theorem pMergeSort_value_perm [LinearOrder α] (xs : List α) :
    (pMergeSort xs).value.Perm xs :=
  (pMergeSort_correct xs).perm

P-MERGE-SORT's value has exactly the input length.

theorem pMergeSort_value_length [LinearOrder α] (xs : List α) :
    (pMergeSort xs).value.length = xs.length :=
  (pMergeSort_correct xs).length_eq

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.Step

CLRS Chapter 26.3 — P-MERGE-SORT Step Costs

This module exposes the exact work and span equations for one nontrivial midpoint-split step of the executable P-MERGE-SORT algorithm.

namespace CLRSnamespace Chapter27

Exact work charged by a non-base P-MERGE-SORT step.


theorem pMergeSort_work_step_eq [LinearOrder α] (xs : List α)
    (hsmall : ¬ xs.length ≤ 1) :
    let mid := xs.length / 2
    let left := xs.take mid
    let right := xs.drop mid
    (pMergeSort xs).work =
      (pMergeSort left).work + (pMergeSort right).work + 1 +
        (pMerge (pMergeSort left).value (pMergeSort right).value).work := by
  rw [pMergeSort]
  simp [hsmall]

Exact span charged by a non-base P-MERGE-SORT step.


theorem pMergeSort_span_step_eq [LinearOrder α] (xs : List α)
    (hsmall : ¬ xs.length ≤ 1) :
    let mid := xs.length / 2
    let left := xs.take mid
    let right := xs.drop mid
    (pMergeSort xs).span =
      max (pMergeSort left).span (pMergeSort right).span + 1 +
        (pMerge (pMergeSort left).value (pMergeSort right).value).span := by
  rw [pMergeSort]
  simp [hsmall]

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.RecurrenceLinks

CLRS Chapter 26.3 — P-MERGE-SORT Work Recurrence Links

The executable sorter is sandwiched by constant multiples of the existing textbook work recurrence. These lemmas keep the algorithmic cost proof tied to the recurrence model rather than re-proving a second abstract analysis.

              namespace CLRSnamespace Chapter27namespace ParallelMergeSortnamespace Costsvariable [LinearOrder α]

The textbook work recurrence is a lower bound for actual execution work.


theorem recurrenceWork_le_execution (n : ℕ) :
    ∀ (xs : List α), xs.length = n →
      pMergeSortWork n ≤ (pMergeSort xs).work := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs hlength
      by_cases hsmall : xs.length ≤ 1
      · have hn : n ≤ 1 := by omega
        rw [pMergeSort]
        simp only [hsmall]
        rw [pMergeSortWork]
        simp [hn, hlength]
      · let mid := xs.length / 2
        let left := xs.take mid
        let right := xs.drop mid
        have hn : 2 ≤ n := by omega
        have hleftLength : left.length = n / 2 := by
          simp [left, mid, hlength]
          omega
        have hrightLength : right.length = n - n / 2 := by
          simp [right, mid, hlength]
        have hleft_lt : left.length < n := by rw [hleftLength]; omega
        have hright_lt : right.length < n := by rw [hrightLength]; omega
        have hleft := ih left.length hleft_lt left rfl
        have hright := ih right.length hright_lt right rfl
        have hmerge := pMerge_work_lower
          (pMergeSort left).value (pMergeSort right).value
        have hleftValue := pMergeSort_value_length left
        have hrightValue := pMergeSort_value_length right
        have hstep := pMergeSort_work_step_eq xs hsmall
        rw [pMergeSortWork_unfold hn]
        change (pMergeSort xs).work =
          (pMergeSort left).work + (pMergeSort right).work + 1 +
            (pMerge (pMergeSort left).value (pMergeSort right).value).work at hstep
        rw [hleftLength] at hleft
        rw [hrightLength] at hright
        omega

Actual execution work is at most sixty-four copies of the textbook work recurrence. P-MERGE's logarithmic potential pays for the fork at each node.


theorem executionWork_le_recurrence (n : ℕ) :
    ∀ (xs : List α), xs.length = n →
      (pMergeSort xs).work ≤ 64 * pMergeSortWork n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs hlength
      by_cases hsmall : xs.length ≤ 1
      · have hn : n ≤ 1 := by omega
        rw [pMergeSort]
        simp only [hsmall]
        rw [pMergeSortWork]
        simp [hn, hlength]
        omega
      · let mid := xs.length / 2
        let left := xs.take mid
        let right := xs.drop mid
        have hn : 2 ≤ n := by omega
        have hleftLength : left.length = n / 2 := by
          simp [left, mid, hlength]
          omega
        have hrightLength : right.length = n - n / 2 := by
          simp [right, mid, hlength]
        have hleft_lt : left.length < n := by rw [hleftLength]; omega
        have hright_lt : right.length < n := by rw [hrightLength]; omega
        have hleft := ih left.length hleft_lt left rfl
        have hright := ih right.length hright_lt right rfl
        rw [hleftLength] at hleft
        rw [hrightLength] at hright
        have hleftValue := pMergeSort_value_length left
        have hrightValue := pMergeSort_value_length right
        have htotal :
            (pMergeSort left).value.length + (pMergeSort right).value.length = n := by
          rw [hleftValue, hrightValue, hleftLength, hrightLength]
          omega
        have hpotential :=
          ParallelMerge.Costs.Work.potential_of_total n
            (pMergeSort left).value (pMergeSort right).value htotal
        have hlogpos : 0 < Nat.log 2 (n + 1) :=
          Nat.log_pos (by norm_num) (by omega)
        have hmergeFork :
            (pMerge (pMergeSort left).value (pMergeSort right).value).work + 1 ≤
              64 * n := by
          omega
        have hstep := pMergeSort_work_step_eq xs hsmall
        change (pMergeSort xs).work =
          (pMergeSort left).work + (pMergeSort right).work + 1 +
            (pMerge (pMergeSort left).value (pMergeSort right).value).work at hstep
        rw [pMergeSortWork_unfold hn]
        omega

              end Costsend ParallelMergeSortend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.Work.Bounds

CLRS Chapter 26.3 — Executable P-MERGE-SORT Work Bounds

The lower theorem transfers the adjacent-power lower bound through the exact recurrence link. The upper theorem counts at most one linear-work merge level per ceiling-logarithmic recursion level.

Main results:

pMergeSort_work_lower: pointwise logarithmic-linear work lower bound.
pMergeSort_work_upper: pointwise logarithmic-linear work upper bound.

              namespace CLRSnamespace Chapter27namespace ParallelMergeSortnamespace Costsnamespace Work

The abstract work recurrence has at most one total-size charge at each ceiling-logarithmic level.


private theorem recurrence_le_clog : ∀ n : ℕ,
    pMergeSortWork n ≤ n * (Nat.clog 2 n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hnsmall : n ≤ 1
      · interval_cases n <;> simp [pMergeSortWork]
      · have hn : 2 ≤ n := by omega
        have hfloor_lt : n / 2 < n := by omega
        have hceil_lt : n - n / 2 < n := by omega
        have hfloor := ih (n / 2) hfloor_lt
        have hceil := ih (n - n / 2) hceil_lt
        have hfloor_le_ceil : n / 2 ≤ n - n / 2 := by omega
        have hhalf : (n + 2 - 1) / 2 = n - n / 2 := by omega
        have hclogFloor : Nat.clog 2 (n / 2) + 1 ≤ Nat.clog 2 n := by
          rw [Nat.clog_of_two_le (by norm_num) hn, hhalf]
          exact Nat.add_le_add_right
            (Nat.clog_mono_right 2 hfloor_le_ceil) 1
        have hclogCeil : Nat.clog 2 (n - n / 2) + 1 ≤ Nat.clog 2 n := by
          rw [Nat.clog_of_two_le (by norm_num) hn, hhalf]
        have hfloor' : pMergeSortWork (n / 2) ≤
            (n / 2) * Nat.clog 2 n :=
          hfloor.trans (Nat.mul_le_mul_left _ hclogFloor)
        have hceil' : pMergeSortWork (n - n / 2) ≤
            (n - n / 2) * Nat.clog 2 n :=
          hceil.trans (Nat.mul_le_mul_left _ hclogCeil)
        have hsplit : n / 2 + (n - n / 2) = n := by omega
        rw [pMergeSortWork_unfold hn]
        calc
          pMergeSortWork (n / 2) + pMergeSortWork (n - n / 2) + n ≤
              (n / 2) * Nat.clog 2 n +
                (n - n / 2) * Nat.clog 2 n + n := by omega
          _ = (n / 2 + (n - n / 2)) * Nat.clog 2 n + n := by
            rw [Nat.add_mul]
          _ = n * Nat.clog 2 n + n := by rw [hsplit]
          _ = n * (Nat.clog 2 n + 1) := by rw [Nat.mul_succ]

The exact-power lower solution and monotonicity give a simple floor-log lower bound for the abstract recurrence.


private theorem floorLog_lower (n : ℕ) :
    n * (Nat.log 2 n + 1) ≤ 2 * pMergeSortWork n := by
  by_cases hnzero : n = 0
  · subst n
    simp [pMergeSortWork]
  · let k := Nat.log 2 n
    let q := 2 ^ k
    have hq_le : q ≤ n := by
      exact Nat.pow_log_le_self 2 hnzero
    have hn_lt : n < 2 ^ (k + 1) := by
      exact Nat.lt_pow_succ_log_self (by norm_num) n
    have hn_le : n ≤ 2 * q := by
      apply Nat.le_of_lt
      simpa [q, k, pow_succ, Nat.mul_comm] using hn_lt
    have hmodel : pMergeSortWork q ≤ pMergeSortWork n :=
      pMergeSortWork_monotone hq_le
    calc
      n * (Nat.log 2 n + 1) = n * (k + 1) := by rfl
      _ ≤ (2 * q) * (k + 1) := Nat.mul_le_mul_right (k + 1) hn_le
      _ = 2 * (q * (k + 1)) := by ring
      _ = 2 * pMergeSortWork q := by rw [pMergeSortWork_pow_two]
      _ ≤ 2 * pMergeSortWork n := Nat.mul_le_mul_left 2 hmodel

              end Workend Costsend ParallelMergeSort

Public theorems

Every P-MERGE-SORT execution has logarithmic-linear work from below, with an explicit constant valid at all input sizes.

theorem pMergeSort_work_lower [LinearOrder α] (xs : List α) :
    xs.length * (Nat.log 2 xs.length + 1) ≤
      16 * ((pMergeSort xs).work + xs.length + 1) := by
  have hmodel := ParallelMergeSort.Costs.Work.floorLog_lower xs.length
  have hlink := ParallelMergeSort.Costs.recurrenceWork_le_execution
    xs.length xs rfl
  omega

Every P-MERGE-SORT execution has logarithmic-linear work from above, with an explicit all-input bound.


theorem pMergeSort_work_upper [LinearOrder α] (xs : List α) :
    (pMergeSort xs).work ≤
      128 * (xs.length + 1) * (Nat.log 2 xs.length + 1) := by
  have hlink := ParallelMergeSort.Costs.executionWork_le_recurrence
    xs.length xs rfl
  have hmodel := ParallelMergeSort.Costs.Work.recurrence_le_clog xs.length
  have hclog : Nat.clog 2 xs.length ≤ Nat.log 2 xs.length + 1 := by
    rw [Nat.clog_le_iff_le_pow (by norm_num)]
    exact (Nat.lt_pow_succ_log_self (by norm_num) xs.length).le
  have hmodel' : pMergeSortWork xs.length ≤
      xs.length * (Nat.log 2 xs.length + 2) := by
    exact hmodel.trans (Nat.mul_le_mul_left xs.length (by omega))
  calc
    (pMergeSort xs).work ≤ 64 * pMergeSortWork xs.length := hlink
    _ ≤ 64 * (xs.length * (Nat.log 2 xs.length + 2)) :=
      Nat.mul_le_mul_left 64 hmodel'
    _ ≤ 128 * (xs.length + 1) * (Nat.log 2 xs.length + 1) := by
      nlinarith

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.Span.Bounds

CLRS Chapter 26.3 — Executable P-MERGE-SORT Span Upper Bound

The actual critical path is compared to the textbook P-MERGE-SORT span recurrence. The comparison uses the proved pointwise quadratic-logarithmic P-MERGE span bound, then the recurrence's exact power-of-two solution yields the cubic-logarithmic all-input result.

              namespace CLRSnamespace Chapter27namespace ParallelMergeSortnamespace Costsnamespace Span

The P-MERGE span recurrence dominates a quadratic floor-log expression.


private theorem mergeRecurrence_floorLog_lower (n : ℕ) (hn : 0 < n) :
    (Nat.log 2 n + 1) * (Nat.log 2 n + 2) ≤ 2 * pMergeSpan n := by
  let k := Nat.log 2 n
  let q := 2 ^ k
  have hq_le : q ≤ n := Nat.pow_log_le_self 2 hn.ne'
  have hmodel : pMergeSpan q ≤ pMergeSpan n :=
    pMergeSpan_monotone hq_le
  calc
    (Nat.log 2 n + 1) * (Nat.log 2 n + 2) =
        (k + 1) * (k + 2) := by rfl
    _ = 2 * pMergeSpan q := by rw [pMergeSpan_pow_two]
    _ ≤ 2 * pMergeSpan n := Nat.mul_le_mul_left 2 hmodel

The actual P-MERGE-SORT critical path is at most 128 copies of the textbook span recurrence.


private theorem execution_le_recurrence [LinearOrder α] (n : ℕ) :
    ∀ (xs : List α), xs.length = n →
      (pMergeSort xs).span ≤ 128 * pMergeSortSpan n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs hlength
      by_cases hsmall : xs.length ≤ 1
      · have hn : n ≤ 1 := by omega
        rw [pMergeSort]
        simp only [hsmall]
        rw [pMergeSortSpan]
        simp [hn, hlength]
        omega
      · let mid := xs.length / 2
        let left := xs.take mid
        let right := xs.drop mid
        have hn : 2 ≤ n := by omega
        have hleftLength : left.length = n / 2 := by
          simp [left, mid, hlength]
          omega
        have hrightLength : right.length = n - n / 2 := by
          simp [right, mid, hlength]
        have hleft_lt : left.length < n := by rw [hleftLength]; omega
        have hright_lt : right.length < n := by rw [hrightLength]; omega
        have hleft := ih left.length hleft_lt left rfl
        have hright := ih right.length hright_lt right rfl
        rw [hleftLength] at hleft
        rw [hrightLength] at hright
        have hfloor_le_ceil : n / 2 ≤ n - n / 2 := by omega
        have hmodelMono : pMergeSortSpan (n / 2) ≤
            pMergeSortSpan (n - n / 2) :=
          pMergeSortSpan_monotone hfloor_le_ceil
        have hchildren : max (pMergeSort left).span (pMergeSort right).span ≤
            128 * pMergeSortSpan (n - n / 2) := by
          apply max_le
          · exact hleft.trans (Nat.mul_le_mul_left 128 hmodelMono)
          · exact hright
        have hleftValue := pMergeSort_value_length left
        have hrightValue := pMergeSort_value_length right
        have htotal :
            (pMergeSort left).value.length + (pMergeSort right).value.length = n := by
          rw [hleftValue, hrightValue, hleftLength, hrightLength]
          omega
        have hmerge := pMerge_span_upper
          (pMergeSort left).value (pMergeSort right).value
        rw [htotal] at hmerge
        have hmergeModel := mergeRecurrence_floorLog_lower n (by omega)
        have hmergeFork :
            (pMerge (pMergeSort left).value (pMergeSort right).value).span + 1 ≤
              128 * pMergeSpan n := by
          nlinarith
        have hstep := pMergeSort_span_step_eq xs hsmall
        change (pMergeSort xs).span =
          max (pMergeSort left).span (pMergeSort right).span + 1 +
            (pMerge (pMergeSort left).value (pMergeSort right).value).span at hstep
        rw [pMergeSortSpan_unfold hn]
        omega

The textbook span recurrence is bounded by twice a floor-log cube.


private theorem recurrence_le_cube (n : ℕ) :
    pMergeSortSpan n ≤ 2 * (Nat.log 2 n + 1) ^ 3 := by
  by_cases hnsmall : n ≤ 1
  · interval_cases n <;> simp [pMergeSortSpan]
  · have hn : 2 ≤ n := by omega
    let k := Nat.log 2 n
    have hk : 1 ≤ k := Nat.log_pos (by norm_num) hn
    have hupper : pMergeSortSpan n ≤ pMergeSortSpan (2 ^ (k + 1)) := by
      simpa [k] using (pMergeSortSpan_power_sandwich n (by omega)).2
    have hclosed : 6 * pMergeSortSpan (2 ^ (k + 1)) =
        (k + 2) * (k + 3) * (k + 4) := by
      rw [pMergeSortSpan_pow_two]
      ring
    change pMergeSortSpan n ≤ 2 * (k + 1) ^ 3
    obtain ⟨t, hk_eq⟩ : ∃ t, k = t + 1 := by
      exact ⟨k - 1, by omega⟩
    rw [hk_eq] at hupper hclosed ⊢
    have hpoly : (t + 3) * (t + 4) * (t + 5) ≤
        12 * (t + 2) ^ 3 := by
      have hnonneg : 0 ≤ 11 * t ^ 3 + 60 * t ^ 2 + 97 * t + 36 :=
        Nat.zero_le _
      nlinarith
    nlinarith

              end Spanend Costsend ParallelMergeSort

Public theorem

Every executable P-MERGE-SORT run has cubic-logarithmic span.

theorem pMergeSort_span_upper [LinearOrder α] (xs : List α) :
    (pMergeSort xs).span ≤
      256 * (Nat.log 2 xs.length + 1) ^ 3 := by
  have hlink := ParallelMergeSort.Costs.Span.execution_le_recurrence
    xs.length xs rfl
  have hmodel := ParallelMergeSort.Costs.Span.recurrence_le_cube xs.length
  nlinarith

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.Span.LowerBound

CLRS Chapter 26.3 — P-MERGE-SORT Cubic-Log Span Witness

Each witness level recursively sorts an order-embedded copy of the preceding level, then merges the canonical interleaved even/odd lists. Order-embedding cost invariance preserves the recursive critical path, while the P-MERGE witness contributes a quadratic term at every level.

              namespace CLRSnamespace Chapter27namespace ParallelMergeSortnamespace Costsnamespace Spanprivate theorem double_strictMono : StrictMono (fun x : ℕ => 2 * x) := by
  intro a b hab
  change 2 * a < 2 * b
  omega

One witness level contains the preceding witness critical path plus the quadratic interleaved P-MERGE critical path.


private theorem witness_span_step (k : ℕ) :
    (pMergeSort (worstMergeSortInput k)).span +
        (pMerge (evenKeys (2 ^ k)) (oddKeys (2 ^ k))).span + 1 ≤
      (pMergeSort (worstMergeSortInput (k + 1))).span := by
  have hsmall : ¬ (worstMergeSortInput (k + 1)).length ≤ 1 := by
    rw [worstMergeSortInput_length, pow_succ]
    have hp : 0 < 2 ^ k := pow_pos (by omega) _
    omega
  have hmid : (worstMergeSortInput (k + 1)).length / 2 = 2 ^ k := by
    rw [worstMergeSortInput_length, pow_succ]
    omega
  have hstep := pMergeSort_span_step_eq
    (worstMergeSortInput (k + 1)) hsmall
  change (pMergeSort (worstMergeSortInput (k + 1))).span =
    max
      (pMergeSort ((worstMergeSortInput (k + 1)).take
        ((worstMergeSortInput (k + 1)).length / 2))).span
      (pMergeSort ((worstMergeSortInput (k + 1)).drop
        ((worstMergeSortInput (k + 1)).length / 2))).span + 1 +
    (pMerge
      (pMergeSort ((worstMergeSortInput (k + 1)).take
        ((worstMergeSortInput (k + 1)).length / 2))).value
      (pMergeSort ((worstMergeSortInput (k + 1)).drop
        ((worstMergeSortInput (k + 1)).length / 2))).value).span at hstep
  rw [hmid, witness_take_half, witness_drop_half,
    sorted_even_half, sorted_odd_half] at hstep
  have hmapCost := pMergeSort_map (fun x : ℕ => 2 * x) double_strictMono
    (worstMergeSortInput k).length (worstMergeSortInput k) rfl
  have hmapSpan := congrArg Costed.span hmapCost
  simp only [Costed.map_span] at hmapSpan
  rw [hmapSpan] at hstep
  omega

Inductive cubic accumulation for the complete witness family.


private theorem witness_span_cubic (k : ℕ) :
    (k + 1) ^ 3 ≤ 64 * (pMergeSort (worstMergeSortInput k)).span := by
  induction k with
  | zero =>
      norm_num only [zero_add, one_pow]
      rw [pMergeSort]
      simp only [worstMergeSortInput, List.length_cons, List.length_nil,
        Nat.zero_add, Nat.reduceLeDiff]
      norm_num
  | succ k ih =>
      have hstep := witness_span_step k
      have hmerge := pMerge_interleaved_span_lower k
      nlinarith [sq_nonneg (k : ℤ)]

              end Spanend Costsend ParallelMergeSort

Public theorem

The recursively interleaved power-of-two family has cubic-logarithmic P-MERGE-SORT span from below.

theorem pMergeSort_worstFamily_span_lower (k : ℕ) :
    (k + 1) ^ 3 ≤ 64 * (pMergeSort (worstMergeSortInput k)).span := by
  exact ParallelMergeSort.Costs.Span.witness_span_cubic k

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_1_Multithreading_Model.S1_ComputationDAG

26.1 S1. Computation DAGs

The foundational dynamic-multithreading model: strands, computation DAGs, work, span, speedup, and parallelism.

namespace CLRSnamespace Chapter27

Strands and computation DAGs

A strand is an atomic unit of computation with a nonnegative work weight: the number of time units it takes on a single processor.

Work weight in time units.

structure Strand where

  work : ℕ
deriving Repr, DecidableEq

A computation DAG models a multithreaded computation.

Nodes are 0, …, n - 1, each carrying a strand weight. An edge (u, v) means u must complete before v can begin. Edges are required to point forward (u < v), so the node order is a topological order.

Number of nodes in the DAG.

Work weight for each node.

Dependency edges.

All edges reference valid, distinct nodes.

Edges point forward, so the graph is acyclic and topologically ordered.

              structure CompDAG where  n : ℕ  node_work : ℕ → ℕ  edges : List (ℕ × ℕ)  h_edges_in_bounds : ∀ uv ∈ edges, uv.1 < n ∧ uv.2 < n ∧ uv.1 ≠ uv.2 := by
    simp  h_edges_forward : ∀ uv ∈ edges, uv.1 < uv.2

namespace CompDAG

The total work T₁: the sum of the work over all nodes.

def work (G : CompDAG) : ℕ :=
  ∑ i ∈ Finset.range G.n, G.node_work i

The longest weighted path ending at node v: v's own weight plus the maximum over the longest paths ending at its immediate predecessors (0 when v has no predecessors).

def longestTo (G : CompDAG) (v : ℕ) : ℕ :=
  G.node_work v +
    ((G.edges.filter fun e => e.2 = v).attach.map fun e =>
      G.longestTo e.1.1).foldr max 0
termination_by v
decreasing_by
  have hfilt := List.mem_filter.mp e.2
  have hfwd := G.h_edges_forward e.1 hfilt.1
  have hveq : e.1.2 = v := of_decide_eq_true hfilt.2
  omega

The span T∞: the maximum of longestTo over all nodes — the critical path length, a lower bound on the parallel running time.

def span (G : CompDAG) : ℕ :=
  ((List.range G.n).map G.longestTo).foldr max 0

The speedup on p processors with observed time Tp: T₁ / Tp.

def speedup (G : CompDAG) (Tp : ℕ) : ℚ :=
  if Tp = 0 then 0 else (G.work : ℚ) / (Tp : ℚ)

The parallelism of the computation: T₁ / T∞.

noncomputable def parallelism (G : CompDAG) : ℚ :=
  if G.span = 0 then 0 else (G.work : ℚ) / (G.span : ℚ)

private theorem foldr_max_le (l : List ℕ) (B : ℕ) (h : ∀ x ∈ l, x ≤ B) :
    l.foldr max 0 ≤ B := by
  induction l with
  | nil => exact Nat.zero_le B
  | cons x xs ih =>
      simp only [List.foldr_cons]
      have hx := h x List.mem_cons_self
      have hxs := ih (fun y hy => h y (List.mem_cons_of_mem x hy))
      omega

The longest path ending at v uses only nodes ≤ v, so its weight is bounded by the partial work sum.


theorem longestTo_le (G : CompDAG) (v : ℕ) :
    G.longestTo v ≤ ∑ i ∈ Finset.range (v + 1), G.node_work i := by
  induction v using Nat.strong_induction_on with
  | h v ih =>
      rw [Finset.sum_range_succ, longestTo]
      have hfold :
          ((G.edges.filter fun e => e.2 = v).attach.map fun e =>
              G.longestTo e.1.1).foldr max 0 ≤
            ∑ i ∈ Finset.range v, G.node_work i := by
        apply foldr_max_le
        intro x hx
        rcases List.mem_map.mp hx with ⟨⟨e, he⟩, -, rfl⟩
        have hfilt := List.mem_filter.mp he
        have hfwd := G.h_edges_forward e hfilt.1
        have hveq : e.2 = v := of_decide_eq_true hfilt.2
        have hlt : e.1 < v := by rw [← hveq]; exact hfwd
        calc G.longestTo e.1
            ≤ ∑ i ∈ Finset.range (e.1 + 1), G.node_work i := ih e.1 hlt
          _ ≤ ∑ i ∈ Finset.range v, G.node_work i :=
            Finset.sum_le_sum_of_subset_of_nonneg
              (Finset.subset_iff.mpr fun x hx =>
                Finset.mem_range.mpr (by
                  have hx' := Finset.mem_range.mp hx
                  omega))
              (by simp)
      omega

T∞ ≤ T₁: the span never exceeds the total work.

theorem span_le_work (G : CompDAG) : G.span ≤ G.work := by
  unfold span work
  apply foldr_max_le
  intro x hx
  rcases List.mem_map.mp hx with ⟨i, hi, rfl⟩
  have hi' : i < G.n := List.mem_range.mp hi
  calc G.longestTo i
      ≤ ∑ j ∈ Finset.range (i + 1), G.node_work j := G.longestTo_le i
    _ ≤ ∑ j ∈ Finset.range G.n, G.node_work j :=
      Finset.sum_le_sum_of_subset_of_nonneg
        (Finset.subset_iff.mpr fun x hx =>
          Finset.mem_range.mpr (by
            have hx' := Finset.mem_range.mp hx
            omega))
        (by simp)

              end CompDAGend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_1_Multithreading_Model.S2_ReadyExecution

26.1 S2. Ready execution

Residual computation states, ready strands, and the work/span progress lemmas for executing a set of ready nodes.

              namespace CLRSnamespace Chapter27namespace CompDAG

Residual computation states

Work remaining in a partially executed computation.

def remainingWork (G : CompDAG) (remaining : ℕ → ℕ) : ℕ :=
  ∑ i ∈ Finset.range G.n, remaining i

Reuse the dependency graph with a new node-work function.

def withWork (G : CompDAG) (nodeWork : ℕ → ℕ) : CompDAG where
  n := G.n
  node_work := nodeWork
  edges := G.edges
  h_edges_in_bounds := G.h_edges_in_bounds
  h_edges_forward := G.h_edges_forward

Critical-path work remaining in a partially executed computation.

def remainingSpan (G : CompDAG) (remaining : ℕ → ℕ) : ℕ :=
  (G.withWork remaining).span

Execute one unit of work at each selected node.

def execute (_G : CompDAG) (remaining : ℕ → ℕ) (run : Finset ℕ) : ℕ → ℕ :=
  fun v => if v ∈ run then remaining v - 1 else remaining v

private theorem foldr_max_map_le {α : Type} (items : List α) (f g : α → ℕ)
    (hfg : ∀ item ∈ items, f item ≤ g item) :
    (items.map f).foldr max 0 ≤ (items.map g).foldr max 0 := by
  induction items with
  | nil => simp
  | cons item items ih =>
      simp only [List.map_cons, List.foldr_cons]
      exact max_le_max (hfg item List.mem_cons_self)
        (ih fun tailItem hmem => hfg tailItem (List.mem_cons_of_mem item hmem))



private theorem foldr_max_map_add_one_le {α : Type} (items : List α)
    (f : α → ℕ) (bound : ℕ) (hbound : 0 < bound)
    (hf : ∀ item ∈ items, f item + 1 ≤ bound) :
    (items.map f).foldr max 0 + 1 ≤ bound := by
  induction items with
  | nil => simp; omega
  | cons item items ih =>
      have hitem := hf item List.mem_cons_self
      have htail := ih fun tailItem hmem =>
        hf tailItem (List.mem_cons_of_mem item hmem)
      simp only [List.map_cons, List.foldr_cons]
      rcases le_total (f item) ((items.map f).foldr max 0) with hle | hge
      · rw [max_eq_right hle]
        exact htail
      · rw [max_eq_left hge]
        exact hitem

Increasing node work can only increase the longest path ending at a node.


theorem longestTo_mono_work (G : CompDAG) (smaller larger : ℕ → ℕ)
    (hwork : ∀ v, smaller v ≤ larger v) (v : ℕ) :
    (G.withWork smaller).longestTo v ≤ (G.withWork larger).longestTo v := by
  induction v using Nat.strong_induction_on with
  | h v ih =>
      rw [longestTo, longestTo]
      apply Nat.add_le_add (hwork v)
      apply foldr_max_map_le
      intro edge _hmem
      have hfilt := List.mem_filter.mp edge.property
      have htarget : edge.val.2 = v := of_decide_eq_true hfilt.2
      have hsource_lt : edge.val.1 < v := by
        have hforward := G.h_edges_forward edge.val hfilt.1
        omega
      exact ih edge.val.1 hsource_lt

Residual span is monotone in every node's remaining work.

theorem remainingSpan_mono (G : CompDAG) (smaller larger : ℕ → ℕ)
    (hwork : ∀ v, smaller v ≤ larger v) :
    G.remainingSpan smaller ≤ G.remainingSpan larger := by
  unfold remainingSpan span
  apply foldr_max_map_le
  intro v _hv
  exact G.longestTo_mono_work smaller larger hwork v

Executing work cannot increase the residual critical path.

theorem remainingSpan_execute_le (G : CompDAG) (remaining : ℕ → ℕ)
    (run : Finset ℕ) :
    G.remainingSpan (G.execute remaining run) ≤ G.remainingSpan remaining := by
  apply G.remainingSpan_mono
  intro v
  simp only [execute]
  split <;> omega

Nodes that have positive remaining work and whose immediate predecessors have finished.

def ready (G : CompDAG) (remaining : ℕ → ℕ) : Finset ℕ :=
  (Finset.range G.n).filter fun v =>
    0 < remaining v ∧
      ∀ edge ∈ G.edges, edge.2 = v → remaining edge.1 = 0

theorem mem_ready_iff (G : CompDAG) (remaining : ℕ → ℕ) (v : ℕ) :
    v ∈ G.ready remaining ↔
      v < G.n ∧ 0 < remaining v ∧
        ∀ edge ∈ G.edges, edge.2 = v → remaining edge.1 = 0 := by
  simp [ready]



private theorem longestTo_execute_ready_add_one_le (G : CompDAG)
    (remaining : ℕ → ℕ) (v : ℕ) (hv : v < G.n)
    (hpositive : 0 < (G.withWork remaining).longestTo v) :
    (G.withWork (G.execute remaining (G.ready remaining))).longestTo v + 1 ≤
      (G.withWork remaining).longestTo v := by
  induction v using Nat.strong_induction_on with
  | h v ih =>
      let predEdges := (G.edges.filter fun edge => edge.2 = v).attach
      let beforeMax :=
        (predEdges.map fun edge =>
          (G.withWork remaining).longestTo edge.val.1).foldr max 0
      let afterMax :=
        (predEdges.map fun edge =>
          (G.withWork (G.execute remaining (G.ready remaining))).longestTo
            edge.val.1).foldr max 0
      rw [longestTo] at hpositive
      rw [longestTo, longestTo]
      change 0 < remaining v + beforeMax at hpositive
      change G.execute remaining (G.ready remaining) v + afterMax + 1 ≤
        remaining v + beforeMax
      have hnode_mono : ∀ node,
          G.execute remaining (G.ready remaining) node ≤ remaining node := by
        intro node
        simp only [execute]
        split <;> omega
      have hmax_mono : afterMax ≤ beforeMax := by
        apply foldr_max_map_le
        intro edge _hmem
        exact G.longestTo_mono_work _ _ hnode_mono edge.val.1
      have hmax_drop (hmax_positive : 0 < beforeMax) :
          afterMax + 1 ≤ beforeMax := by
        apply foldr_max_map_add_one_le predEdges _ beforeMax hmax_positive
        intro edge _hmem
        have hfilt := List.mem_filter.mp edge.property
        have htarget : edge.val.2 = v := of_decide_eq_true hfilt.2
        have hsource_lt : edge.val.1 < v := by
          have hforward := G.h_edges_forward edge.val hfilt.1
          omega
        have hsource_bound : edge.val.1 < G.n :=
          (G.h_edges_in_bounds edge.val hfilt.1).1
        by_cases hpred_positive :
            0 < (G.withWork remaining).longestTo edge.val.1
        · have hdrop := ih edge.val.1 hsource_lt hsource_bound hpred_positive
          have hmem : (G.withWork remaining).longestTo edge.val.1 ∈
              predEdges.map fun predecessor =>
                (G.withWork remaining).longestTo predecessor.val.1 :=
            List.mem_map.mpr ⟨edge, _hmem, rfl⟩
          have hle := List.le_max_of_le' 0 hmem (le_refl _)
          exact hdrop.trans hle
        · have hbefore_zero :
              (G.withWork remaining).longestTo edge.val.1 = 0 :=
            Nat.eq_zero_of_not_pos hpred_positive
          have hafter_le :=
            G.longestTo_mono_work _ _ hnode_mono edge.val.1
          have hafter_zero :
              (G.withWork (G.execute remaining (G.ready remaining))).longestTo
                  edge.val.1 = 0 := by
            omega
          omega
      by_cases hready : v ∈ G.ready remaining
      · have hvpos := ((G.mem_ready_iff remaining v).mp hready).2.1
        have hexecute :
            G.execute remaining (G.ready remaining) v = remaining v - 1 := by
          simp [execute, hready]
        rw [hexecute]
        omega
      · have hbefore_max_positive : 0 < beforeMax := by
          by_cases hvpos : 0 < remaining v
          · have hnot_all :
                ¬ ∀ edge ∈ G.edges,
                  edge.2 = v → remaining edge.1 = 0 := by
              intro hall
              exact hready ((G.mem_ready_iff remaining v).mpr ⟨hv, hvpos, hall⟩)
            push Not at hnot_all
            obtain ⟨edge, hedge, htarget, hsource_ne⟩ := hnot_all
            let attached :
                { candidate // candidate ∈
                  (G.edges.filter fun candidate => candidate.2 = v) } :=
              ⟨edge, List.mem_filter.mpr ⟨hedge, by simp [htarget]⟩⟩
            have hsource_pos : 0 < remaining edge.1 := Nat.pos_of_ne_zero hsource_ne
            have hlongest_pos :
                0 < (G.withWork remaining).longestTo edge.1 := by
              rw [longestTo]
              change 0 < remaining edge.1 + _
              omega
            have hmem :
                (G.withWork remaining).longestTo edge.1 ∈
                  predEdges.map fun predecessor =>
                    (G.withWork remaining).longestTo predecessor.val.1 :=
              List.mem_map.mpr ⟨attached, by
                simp [predEdges], rfl⟩
            have hle := List.le_max_of_le' 0 hmem (le_refl _)
            exact Nat.lt_of_lt_of_le hlongest_pos hle
          · have hvzero : remaining v = 0 := Nat.eq_zero_of_not_pos hvpos
            omega
        have hexecute :
            G.execute remaining (G.ready remaining) v = remaining v := by
          simp [execute, hready]
        rw [hexecute]
        exact Nat.add_le_add_left (hmax_drop hbefore_max_positive) (remaining v)

If unfinished work remains, executing every ready node removes at least one unit from the residual critical path.


theorem remainingSpan_execute_ready_add_one_le (G : CompDAG)
    (remaining : ℕ → ℕ) (hwork : 0 < G.remainingWork remaining) :
    G.remainingSpan (G.execute remaining (G.ready remaining)) + 1 ≤
      G.remainingSpan remaining := by
  have hwork' : 0 < ∑ v ∈ Finset.range G.n, remaining v := by
    simpa [remainingWork] using hwork
  obtain ⟨v, hvrange, hvpos⟩ := Finset.sum_pos_iff.mp hwork'
  have hvlt : v < G.n := Finset.mem_range.mp hvrange
  have hlongest_pos : 0 < (G.withWork remaining).longestTo v := by
    rw [longestTo]
    change 0 < remaining v + _
    omega
  have hspan_positive : 0 < G.remainingSpan remaining := by
    unfold remainingSpan span
    have hmem : (G.withWork remaining).longestTo v ∈
        (List.range G.n).map (G.withWork remaining).longestTo :=
      List.mem_map.mpr ⟨v, List.mem_range.mpr hvlt, rfl⟩
    have hle := List.le_max_of_le' 0 hmem (le_refl _)
    exact Nat.lt_of_lt_of_le hlongest_pos hle
  unfold remainingSpan span
  apply foldr_max_map_add_one_le (List.range G.n) _ _ hspan_positive
  intro node hnode
  have hnode_lt : node < G.n := List.mem_range.mp hnode
  by_cases hnode_positive : 0 < (G.withWork remaining).longestTo node
  · have hdrop :=
      G.longestTo_execute_ready_add_one_le remaining node hnode_lt hnode_positive
    have hmem : (G.withWork remaining).longestTo node ∈
        (List.range G.n).map (G.withWork remaining).longestTo :=
      List.mem_map.mpr ⟨node, hnode, rfl⟩
    have hle := List.le_max_of_le' 0 hmem (le_refl _)
    exact hdrop.trans hle
  · have hbefore_zero : (G.withWork remaining).longestTo node = 0 :=
      Nat.eq_zero_of_not_pos hnode_positive
    have hnode_mono : ∀ i,
        G.execute remaining (G.ready remaining) i ≤ remaining i := by
      intro i
      simp only [execute]
      split <;> omega
    have hafter_le := G.longestTo_mono_work _ _ hnode_mono node
    omega

Executing a set of ready nodes consumes exactly one work unit per selected node.


theorem remainingWork_execute_add_card (G : CompDAG) (remaining : ℕ → ℕ)
    (run : Finset ℕ) (hrun : run ⊆ G.ready remaining) :
    G.remainingWork (G.execute remaining run) + run.card =
      G.remainingWork remaining := by
  have hrun_range : run ⊆ Finset.range G.n := by
    intro v hv
    exact Finset.mem_range.mpr ((G.mem_ready_iff remaining v).mp (hrun hv)).1
  have hfilter :
      (Finset.range G.n).filter (fun v => v ∈ run) = run := by
    ext v
    simp only [Finset.mem_filter]
    constructor
    · exact fun hv => hv.2
    · exact fun hv => ⟨hrun_range hv, hv⟩
  have hcard :
      (∑ v ∈ Finset.range G.n, if v ∈ run then 1 else 0) = run.card := by
    rw [← Finset.sum_filter, hfilter]
    simp
  rw [remainingWork, remainingWork, ← hcard, ← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro v hv
  by_cases hvrun : v ∈ run
  · have hvpos : 0 < remaining v :=
      ((G.mem_ready_iff remaining v).mp (hrun hvrun)).2.1
    simp [execute, hvrun, Nat.sub_add_cancel hvpos]
  · simp [execute, hvrun]

              end CompDAGend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_1_Multithreading_Model.S3_GreedyAccounting

26.1 S3. Greedy accounting

Greedy-schedule accounting certificates, traces, concrete DAG steps, and the CLRS work/span running-time bound.

namespace CLRSnamespace Chapter27

Greedy-scheduler accounting

CLRS partitions a greedy execution into complete steps, which execute one strand on every processor, and incomplete steps, which execute every ready strand. Complete steps are paid for by total work; incomplete steps are paid for by a unit decrease in the remaining span. This structure records exactly the two obligations needed by that argument, independently of the concrete DAG execution representation that produces them.

The accounting certificate extracted from a greedy schedule.

completeSteps steps each consume processors units of work, while the number of incompleteSteps is bounded by the initial span.

Number of processors used by the schedule.

Total work T₁ of the computation.

Initial span T∞ of the computation.

Number of time steps that use every processor.

Number of time steps that execute fewer than all processors.

A schedule has at least one processor.

Complete steps cannot consume more than the available total work.

Every incomplete step consumes at least one unit of remaining span.

              structure GreedyScheduleAccounting where  processors : ℕ  totalWork : ℕ  totalSpan : ℕ  completeSteps : ℕ  incompleteSteps : ℕ  processors_pos : 0 < processors  complete_work_bound : completeSteps * processors ≤ totalWork  incomplete_span_bound : incompleteSteps ≤ totalSpan

namespace GreedyScheduleAccounting

Parallel running time is the number of complete plus incomplete steps.

def time (A : GreedyScheduleAccounting) : ℕ :=
  A.completeSteps + A.incompleteSteps

CLRS Theorems 26.1/26.2 at the accounting boundary: Tₚ ≤ T₁ / p + T∞.

theorem time_le_work_div_add_span (A : GreedyScheduleAccounting) :
    A.time ≤ A.totalWork / A.processors + A.totalSpan := by
  have hcomplete : A.completeSteps ≤ A.totalWork / A.processors :=
    (Nat.le_div_iff_mul_le A.processors_pos).2 A.complete_work_bound
  exact Nat.add_le_add hcomplete A.incomplete_span_bound

end GreedyScheduleAccounting

Greedy-schedule traces

Whether a greedy-schedule step keeps every processor busy or exhausts the currently ready strands before doing so.

inductive GreedyStepKind where
  | complete
  | incomplete
deriving Repr, DecidableEq

A finite greedy-schedule trace together with the two global bounds that justify its complete and incomplete steps. Unlike GreedyScheduleAccounting, this representation retains the order of steps.

Number of processors used by the schedule.

Total work T₁ of the computation.

Initial span T∞ of the computation.

Complete and incomplete steps, in execution order.

A schedule has at least one processor.

The complete steps cannot consume more than the available work.

The incomplete steps cannot outnumber the initial span.

              structure GreedyScheduleTrace where  processors : ℕ  totalWork : ℕ  totalSpan : ℕ  steps : List GreedyStepKind  processors_pos : 0 < processors  complete_work_bound : steps.count .complete * processors ≤ totalWork  incomplete_span_bound : steps.count .incomplete ≤ totalSpan

namespace GreedyScheduleTrace

Parallel running time is the number of recorded schedule steps.

def time (S : GreedyScheduleTrace) : ℕ :=
  S.steps.length

Forget step order and retain the accounting data used by the bound.

def accounting (S : GreedyScheduleTrace) : GreedyScheduleAccounting where
  processors := S.processors
  totalWork := S.totalWork
  totalSpan := S.totalSpan
  completeSteps := S.steps.count .complete
  incompleteSteps := S.steps.count .incomplete
  processors_pos := S.processors_pos
  complete_work_bound := S.complete_work_bound
  incomplete_span_bound := S.incomplete_span_bound

private theorem count_complete_add_count_incomplete
    (steps : List GreedyStepKind) :
    steps.count .complete + steps.count .incomplete = steps.length := by
  induction steps with
  | nil => simp
  | cons step steps ih =>
      cases step <;> simp <;> omega

The schedule-trace form of the greedy-scheduler bound: Tₚ ≤ T₁ / p + T∞.


theorem time_le_work_div_add_span (S : GreedyScheduleTrace) :
    S.time ≤ S.totalWork / S.processors + S.totalSpan := by
  have h := S.accounting.time_le_work_div_add_span
  rw [GreedyScheduleAccounting.time] at h
  rw [time, ← count_complete_add_count_incomplete S.steps]
  exact h

end GreedyScheduleTrace

Per-step greedy-schedule accounting

The metric changes caused by one greedy-schedule step.

Whether the step filled every processor.

Amount of remaining work consumed by the step.

Amount by which the remaining span decreases.

              structure GreedyScheduleStep where  kind : GreedyStepKind  workConsumed : ℕ  spanDecrease : ℕ
deriving Repr, DecidableEq

Concrete computation-DAG steps

One greedy time step over an explicit residual CompDAG state.

run contains only ready nodes and has the largest cardinality allowed by the processor count. Thus an incomplete step necessarily executes every ready node.

Work remaining at every DAG node before the step.

Ready nodes selected for one unit of execution.

Only ready nodes may execute.

A greedy step uses as many processors as the ready set permits.

              structure DAGScheduleStep (G : CompDAG) (processors : ℕ) where  remaining : ℕ → ℕ  run : Finset ℕ  run_subset_ready : run ⊆ G.ready remaining  run_card_eq_min : run.card = min processors (G.ready remaining).card

namespace DAGScheduleStep

Residual state after executing the selected ready nodes.

def after {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) : ℕ → ℕ :=
  G.execute S.remaining S.run

A step is complete exactly when it fills every processor.

def kind {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) : GreedyStepKind :=
  if S.run.card = processors then .complete else .incomplete

Expose a concrete DAG step at the per-step accounting boundary.

def metricStep {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) : GreedyScheduleStep where
  kind := S.kind
  workConsumed := S.run.card
  spanDecrease := G.remainingSpan S.remaining - G.remainingSpan S.after

theorem kind_eq_complete_iff {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) :
    S.kind = .complete ↔ S.run.card = processors := by
  simp [kind]

theorem kind_eq_incomplete_iff {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) :
    S.kind = .incomplete ↔ S.run.card ≠ processors := by
  simp [kind]

The concrete residual-work balance for one DAG step.

theorem remainingWork_after_add_card {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) :
    G.remainingWork S.after + S.run.card = G.remainingWork S.remaining := by
  exact G.remainingWork_execute_add_card S.remaining S.run S.run_subset_ready

The accounting work obligation is automatic for complete DAG steps.

theorem complete_progress {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) (hcomplete : S.kind = .complete) :
    processors ≤ S.metricStep.workConsumed := by
  have hcard := (S.kind_eq_complete_iff).mp hcomplete
  simp [metricStep, hcard]

If a greedy step is incomplete, it executes the entire ready set.


theorem incomplete_run_eq_ready {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors) (hincomplete : S.kind = .incomplete) :
    S.run = G.ready S.remaining := by
  have hcard_ne : S.run.card ≠ processors :=
    (S.kind_eq_incomplete_iff).mp hincomplete
  have hready_lt : (G.ready S.remaining).card < processors := by
    by_contra hnot
    have hprocessors_le : processors ≤ (G.ready S.remaining).card :=
      Nat.le_of_not_gt hnot
    have : S.run.card = processors := by
      rw [S.run_card_eq_min, Nat.min_eq_left hprocessors_le]
    exact hcard_ne this
  have hcards : S.run.card = (G.ready S.remaining).card := by
    rw [S.run_card_eq_min, Nat.min_eq_right (Nat.le_of_lt hready_lt)]
  exact Finset.eq_of_subset_of_card_le S.run_subset_ready hcards.ge

The accounting span obligation is automatic for every active incomplete DAG step.


theorem incomplete_progress {G : CompDAG} {processors : ℕ}
    (S : DAGScheduleStep G processors)
    (hactive : 0 < G.remainingWork S.remaining)
    (hincomplete : S.kind = .incomplete) :
    1 ≤ S.metricStep.spanDecrease := by
  have hrun := S.incomplete_run_eq_ready hincomplete
  have hdrop := G.remainingSpan_execute_ready_add_one_le S.remaining hactive
  simp only [metricStep, after]
  rw [hrun]
  omega

end DAGScheduleStep

Chained computation-DAG schedules

A type-safe sequence of active greedy DAG steps ending at zero work.

The index is the initial residual state. In the step constructor the tail is indexed by S.after, so consecutive states agree by construction; done requires that no work remains.

inductive DAGSchedule (G : CompDAG) (processors : ℕ) : (ℕ → ℕ) → Type where
  | done (remaining : ℕ → ℕ) (complete : G.remainingWork remaining = 0) :
      DAGSchedule G processors remaining
  | step (S : DAGScheduleStep G processors)
      (active : 0 < G.remainingWork S.remaining)
      (tail : DAGSchedule G processors S.after) :
      DAGSchedule G processors S.remaining

namespace DAGSchedule

Per-step accounting records of a chained DAG execution.

def metricSteps {G : CompDAG} {processors : ℕ} :
    {remaining : ℕ → ℕ} → DAGSchedule G processors remaining →
      List GreedyScheduleStep
  | _, .done _ _ => []
  | _, .step S _ tail => S.metricStep :: tail.metricSteps

The residual state where the recorded execution stops.

def finalState {G : CompDAG} {processors : ℕ} :
    {remaining : ℕ → ℕ} → DAGSchedule G processors remaining → ℕ → ℕ
  | _, .done remaining _ => remaining
  | _, .step _ _ tail => tail.finalState

Every recorded execution stops only after all DAG work is complete.

theorem final_work_eq_zero {G : CompDAG} {processors : ℕ}
    {remaining : ℕ → ℕ} (D : DAGSchedule G processors remaining) :
    G.remainingWork D.finalState = 0 := by
  induction D with
  | done _ complete => exact complete
  | step _ _ _ ih => exact ih

Parallel time of the chained execution.

def time {G : CompDAG} {processors : ℕ} {remaining : ℕ → ℕ}
    (D : DAGSchedule G processors remaining) : ℕ :=
  D.metricSteps.length

Work consumption telescopes over a chained execution.

theorem work_balance {G : CompDAG} {processors : ℕ} {remaining : ℕ → ℕ}
    (D : DAGSchedule G processors remaining) :
    (D.metricSteps.map GreedyScheduleStep.workConsumed).sum +
        G.remainingWork D.finalState =
      G.remainingWork remaining := by
  induction D with
  | done => simp [metricSteps, finalState]
  | step S _active tail ih =>
      have hstep := S.remainingWork_after_add_card
      simp only [metricSteps, List.map_cons, List.sum_cons,
        DAGScheduleStep.metricStep]
      change S.run.card +
          (tail.metricSteps.map GreedyScheduleStep.workConsumed).sum +
            G.remainingWork tail.finalState =
        G.remainingWork S.remaining
      omega

Span decreases telescope over a chained execution.


theorem span_balance {G : CompDAG} {processors : ℕ} {remaining : ℕ → ℕ}
    (D : DAGSchedule G processors remaining) :
    (D.metricSteps.map GreedyScheduleStep.spanDecrease).sum +
        G.remainingSpan D.finalState =
      G.remainingSpan remaining := by
  induction D with
  | done => simp [metricSteps, finalState]
  | step S _active tail ih =>
      have hmono : G.remainingSpan S.after ≤ G.remainingSpan S.remaining := by
        simpa [DAGScheduleStep.after] using
          G.remainingSpan_execute_le S.remaining S.run
      simp only [metricSteps, List.map_cons, List.sum_cons,
        DAGScheduleStep.metricStep, DAGScheduleStep.after]
      change (G.remainingSpan S.remaining - G.remainingSpan S.after) +
          (tail.metricSteps.map GreedyScheduleStep.spanDecrease).sum +
            G.remainingSpan tail.finalState =
        G.remainingSpan S.remaining
      omega

              private theorem all_complete_progress {G : CompDAG} {processors : ℕ}
    {remaining : ℕ → ℕ} (D : DAGSchedule G processors remaining) :
    ∀ step ∈ D.metricSteps,
      step.kind = .complete → processors ≤ step.workConsumed := by
  induction D with
  | done => simp [metricSteps]
  | step S _active tail ih =>
      intro step hmem hcomplete
      simp only [metricSteps, List.mem_cons] at hmem
      rcases hmem with rfl | htail
      · simpa [DAGScheduleStep.metricStep] using S.complete_progress hcomplete
      · exact ih step htail hcompleteprivate theorem all_incomplete_progress {G : CompDAG} {processors : ℕ}
    {remaining : ℕ → ℕ} (D : DAGSchedule G processors remaining) :
    ∀ step ∈ D.metricSteps,
      step.kind = .incomplete → 1 ≤ step.spanDecrease := by
  induction D with
  | done => simp [metricSteps]
  | step S active tail ih =>
      intro step hmem hincomplete
      simp only [metricSteps, List.mem_cons] at hmem
      rcases hmem with rfl | htail
      · simpa [DAGScheduleStep.metricStep] using
          S.incomplete_progress active hincomplete
      · exact ih step htail hincompleteend DAGSchedule

A schedule run whose resource bounds and progress obligations are stated locally, one execution step at a time.

DAGSchedule.toRun produces this interface from the concrete ready-set semantics: a complete step consumes at least processors work, and an incomplete step decreases the remaining span by at least one.

Number of processors used by the schedule.

Initial work T₁.

Initial span T∞.

Metric changes of the execution steps, in order.

A schedule has at least one processor.

All step work consumptions fit within the initial work.

All span decreases fit within the initial span.

Every complete step keeps all processors busy.

Every incomplete step advances the critical path.

              structure GreedyScheduleRun where  processors : ℕ  totalWork : ℕ  totalSpan : ℕ  steps : List GreedyScheduleStep  processors_pos : 0 < processors  work_budget : (steps.map GreedyScheduleStep.workConsumed).sum ≤ totalWork  span_budget : (steps.map GreedyScheduleStep.spanDecrease).sum ≤ totalSpan  complete_progress : ∀ step ∈ steps,
    step.kind = .complete → processors ≤ step.workConsumed  incomplete_progress : ∀ step ∈ steps,
    step.kind = .incomplete → 1 ≤ step.spanDecrease

namespace GreedyScheduleRun

Parallel running time is the number of execution steps.

def time (S : GreedyScheduleRun) : ℕ :=
  S.steps.length



private theorem complete_count_mul_le_work
    (processors : ℕ) (steps : List GreedyScheduleStep)
    (hprogress : ∀ step ∈ steps,
      step.kind = .complete → processors ≤ step.workConsumed) :
    (steps.map GreedyScheduleStep.kind).count .complete * processors ≤
      (steps.map GreedyScheduleStep.workConsumed).sum := by
  induction steps with
  | nil => simp
  | cons step steps ih =>
      have htail : ∀ tailStep ∈ steps,
          tailStep.kind = .complete → processors ≤ tailStep.workConsumed := by
        intro tailStep hmem
        exact hprogress tailStep (List.mem_cons_of_mem step hmem)
      have ih' := ih htail
      cases hkind : step.kind with
      | complete =>
          have hstep : processors ≤ step.workConsumed :=
            hprogress step List.mem_cons_self hkind
          simp [hkind]
          rw [Nat.add_mul]
          omega
      | incomplete =>
          simp [hkind]
          omega



private theorem incomplete_count_le_span
    (steps : List GreedyScheduleStep)
    (hprogress : ∀ step ∈ steps,
      step.kind = .incomplete → 1 ≤ step.spanDecrease) :
    (steps.map GreedyScheduleStep.kind).count .incomplete ≤
      (steps.map GreedyScheduleStep.spanDecrease).sum := by
  induction steps with
  | nil => simp
  | cons step steps ih =>
      have htail : ∀ tailStep ∈ steps,
          tailStep.kind = .incomplete → 1 ≤ tailStep.spanDecrease := by
        intro tailStep hmem
        exact hprogress tailStep (List.mem_cons_of_mem step hmem)
      have ih' := ih htail
      cases hkind : step.kind with
      | complete =>
          simp [hkind]
          omega
      | incomplete =>
          have hstep : 1 ≤ step.spanDecrease :=
            hprogress step List.mem_cons_self hkind
          simp [hkind]
          omega

Forget metric magnitudes while deriving the global trace bounds from the per-step progress and resource-budget obligations.

def trace (S : GreedyScheduleRun) : GreedyScheduleTrace where
  processors := S.processors
  totalWork := S.totalWork
  totalSpan := S.totalSpan
  steps := S.steps.map GreedyScheduleStep.kind
  processors_pos := S.processors_pos
  complete_work_bound :=
    (complete_count_mul_le_work S.processors S.steps S.complete_progress).trans
      S.work_budget
  incomplete_span_bound :=
    (incomplete_count_le_span S.steps S.incomplete_progress).trans S.span_budget

The aggregate accounting certificate derived from local step progress.

def accounting (S : GreedyScheduleRun) : GreedyScheduleAccounting :=
  S.trace.accounting

The per-step execution form of the greedy-scheduler bound: Tₚ ≤ T₁ / p + T∞.

theorem time_le_work_div_add_span (S : GreedyScheduleRun) :
    S.time ≤ S.totalWork / S.processors + S.totalSpan := by
  have h := S.trace.time_le_work_div_add_span
  simpa [time, GreedyScheduleTrace.time, trace] using h

end GreedyScheduleRunnamespace DAGSchedule

Convert a type-safe DAG execution into the local per-step accounting interface. Both global budgets are derived by telescoping; neither is supplied by the caller.

def toRun {G : CompDAG} {processors : ℕ} {remaining : ℕ → ℕ}
    (D : DAGSchedule G processors remaining) (hprocessors : 0 < processors) :
    GreedyScheduleRun where
  processors := processors
  totalWork := G.remainingWork remaining
  totalSpan := G.remainingSpan remaining
  steps := D.metricSteps
  processors_pos := hprocessors
  work_budget := by
    have hbalance := D.work_balance
    omega
  span_budget := by
    have hbalance := D.span_balance
    omega
  complete_progress := all_complete_progress D
  incomplete_progress := all_incomplete_progress D

Greedy-scheduler bound for a chained execution from an arbitrary residual state.

theorem time_le_remainingWork_div_add_remainingSpan
    {G : CompDAG} {processors : ℕ} {remaining : ℕ → ℕ}
    (D : DAGSchedule G processors remaining) (hprocessors : 0 < processors) :
    D.time ≤ G.remainingWork remaining / processors + G.remainingSpan remaining := by
  have hbound := (D.toRun hprocessors).time_le_work_div_add_span
  simpa [time, toRun, GreedyScheduleRun.time] using hbound

CLRS Theorems 26.1/26.2 for an explicit greedy execution of a computation DAG: Tₚ ≤ T₁ / p + T∞.

theorem time_le_work_div_add_span {G : CompDAG} {processors : ℕ}
    (D : DAGSchedule G processors G.node_work) (hprocessors : 0 < processors) :
    D.time ≤ G.work / processors + G.span := by
  have hbound := D.time_le_remainingWork_div_add_remainingSpan hprocessors
  simpa [CompDAG.remainingWork, CompDAG.work, CompDAG.remainingSpan,
    CompDAG.withWork] using hbound

              end DAGScheduleend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_1_Multithreading_Model.S4_ExecutableScheduler

26.1 S4. Executable scheduler

Deterministic ready-set selection and the resulting certified greedy step.

The scheduler chooses the first ready vertices in increasing vertex order, up to the processor count. The resulting finite set carries the readiness and maximal-cardinality proofs required by the certified schedule-step structure. Positive residual work therefore yields a nonempty run and strictly decreases the residual-work measure. Recursing on that measure constructs a total, deterministic greedy schedule and exposes the CLRS Graham--Brent bound.

              namespace CLRSnamespace Chapter27namespace CompDAG

The first processors ready vertices in increasing vertex order.

def readyRun (G : CompDAG) (remaining : ℕ → ℕ) (processors : ℕ) : Finset ℕ :=
  (((G.ready remaining).sort (· ≤ ·)).take processors).toFinset

Every vertex selected by readyRun is ready in the current state.

theorem readyRun_subset_ready (G : CompDAG) (remaining : ℕ → ℕ)
    (processors : ℕ) :
    G.readyRun remaining processors ⊆ G.ready remaining := by
  intro v hv
  simp only [readyRun, List.mem_toFinset] at hv
  exact (Finset.mem_sort (· ≤ ·)).mp (List.mem_of_mem_take hv)

readyRun fills every processor unless fewer ready vertices exist.


theorem readyRun_card (G : CompDAG) (remaining : ℕ → ℕ)
    (processors : ℕ) :
    (G.readyRun remaining processors).card =
      min processors (G.ready remaining).card := by
  rw [readyRun, List.toFinset_card_of_nodup]
  · simp
  · exact (List.take_sublist processors _).nodup
      (Finset.sort_nodup (G.ready remaining) (· ≤ ·))

Positive residual work guarantees that at least one vertex is ready.


theorem ready_nonempty_of_remainingWork_pos (G : CompDAG)
    (remaining : ℕ → ℕ) (hwork : 0 < G.remainingWork remaining) :
    (G.ready remaining).Nonempty := by
  by_contra hready
  have hempty : G.ready remaining = ∅ := Finset.not_nonempty_iff_eq_empty.mp hready
  have hexecute_empty : G.execute remaining ∅ = remaining := by
    funext v
    simp [execute]
  have hdrop := G.remainingSpan_execute_ready_add_one_le remaining hwork
  rw [hempty, hexecute_empty] at hdrop
  omega

With at least one processor, positive residual work makes the deterministic ready prefix nonempty. This is the progress fact used by the total scheduler.


theorem readyRun_nonempty (G : CompDAG) (remaining : ℕ → ℕ)
    (processors : ℕ) (hp : 0 < processors)
    (hwork : 0 < G.remainingWork remaining) :
    (G.readyRun remaining processors).Nonempty := by
  have hready : (G.ready remaining).Nonempty :=
    G.ready_nonempty_of_remainingWork_pos remaining hwork
  have hready_card : 0 < (G.ready remaining).card := Finset.card_pos.mpr hready
  apply Finset.card_pos.mp
  rw [G.readyRun_card remaining processors]
  exact lt_min hp hready_card

The deterministic ready prefix packaged as one certified greedy step.

def greedyStep (G : CompDAG) (remaining : ℕ → ℕ) (processors : ℕ) :
    DAGScheduleStep G processors where
  remaining := remaining
  run := G.readyRun remaining processors
  run_subset_ready := G.readyRun_subset_ready remaining processors
  run_card_eq_min := G.readyRun_card remaining processors

Every active deterministic greedy step strictly decreases residual work when at least one processor is available.

theorem remainingWork_greedyStep_after_lt (G : CompDAG)
    (remaining : ℕ → ℕ) (processors : ℕ) (hp : 0 < processors)
    (hwork : 0 < G.remainingWork remaining) :
    G.remainingWork (G.greedyStep remaining processors).after <
      G.remainingWork remaining := by
  have hrun : (G.readyRun remaining processors).Nonempty :=
    G.readyRun_nonempty remaining processors hp hwork
  have hcard : 0 < (G.readyRun remaining processors).card :=
    Finset.card_pos.mpr hrun
  have hbalance :
      G.remainingWork (G.greedyStep remaining processors).after +
          (G.readyRun remaining processors).card =
        G.remainingWork remaining :=
    (G.greedyStep remaining processors).remainingWork_after_add_card
  omega

Construct the terminating deterministic greedy schedule from any residual state. Recursion is well-founded because each active step strictly decreases the finite residual-work measure.

def greedyScheduleFrom (G : CompDAG) (processors : ℕ) (hp : 0 < processors) :
    (remaining : ℕ → ℕ) → DAGSchedule G processors remaining :=
  fun remaining =>
    if hcomplete : G.remainingWork remaining = 0 then
      DAGSchedule.done remaining hcomplete
    else
      have hactive : 0 < G.remainingWork remaining := Nat.pos_of_ne_zero hcomplete
      DAGSchedule.step (G.greedyStep remaining processors) hactive
        (G.greedyScheduleFrom processors hp
          (G.greedyStep remaining processors).after)
termination_by remaining => G.remainingWork remaining
decreasing_by
  exact G.remainingWork_greedyStep_after_lt remaining processors hp hactive

The terminating deterministic greedy schedule from the DAG's initial node work.

def greedySchedule (G : CompDAG) (processors : ℕ) (hp : 0 < processors) :
    DAGSchedule G processors G.node_work :=
  G.greedyScheduleFrom processors hp G.node_work

The constructed greedy schedule terminates only at a zero-work residual state.

theorem greedySchedule_final_work_eq_zero (G : CompDAG) (processors : ℕ)
    (hp : 0 < processors) :
    G.remainingWork (G.greedySchedule processors hp).finalState = 0 :=
  (G.greedySchedule processors hp).final_work_eq_zero

The constructed deterministic greedy schedule satisfies the CLRS Graham--Brent bound Tₚ ≤ T₁ / p + T∞.

theorem greedySchedule_time_le_work_div_add_span (G : CompDAG)
    (processors : ℕ) (hp : 0 < processors) :
    (G.greedySchedule processors hp).time ≤
      G.work / processors + G.span :=
  (G.greedySchedule processors hp).time_le_work_div_add_span hp

              end CompDAGend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_1_Multithreading_Model.S5_SpawnTreeAndLoops

26.1 S5. Spawn trees and parallel loops

Spawn/sync trees and the balanced parallel-loop model, with work, span, and depth bounds.

namespace CLRSnamespace Chapter27

Spawn trees

The spawn/sync structure of a parallel divide-and-conquer computation. A spawn node models one spawn/sync pair and contributes unit work and unit critical-path overhead; a seq node is sequential composition.

inductive SpawnTree : Type where
  | leaf (w : ℕ) : SpawnTree
  | seq (t1 t2 : SpawnTree) : SpawnTree
  | spawn (t1 t2 : SpawnTree) : SpawnTree
deriving Repr

namespace SpawnTree

The work of a spawn tree: leaf weights plus unit cost per spawn node.

def work : SpawnTree → ℕ
  | leaf w => w
  | seq t1 t2 => work t1 + work t2
  | spawn t1 t2 => work t1 + work t2 + 1

The span of a spawn tree: sequential spans add; spawned children run in parallel, so their spans take the maximum, plus unit spawn overhead.

def span : SpawnTree → ℕ
  | leaf w => w
  | seq t1 t2 => span t1 + span t2
  | spawn t1 t2 => max (span t1) (span t2) + 1

T∞ ≤ T₁ for spawn trees.

theorem span_le_work : ∀ t : SpawnTree, t.span ≤ t.work
  | leaf w => Nat.le_refl w
  | seq t1 t2 => Nat.add_le_add (span_le_work t1) (span_le_work t2)
  | spawn t1 t2 => by
      have h1 := span_le_work t1
      have h2 := span_le_work t2
      simp only [span, work]
      omega

end SpawnTree

Parallel loops

A parallel loop over n iterations is modeled as a balanced binary spawn tree, matching the textbook's Θ(log n) overhead analysis.

The spawn tree for a parallel loop with n iterations of weight w each: a balanced binary spawn tree with n leaves.

def parallelLoopTree (n w : ℕ) : SpawnTree :=
  if n ≤ 1 then
    .leaf (n * w)
  else
    .spawn (parallelLoopTree (n / 2) w) (parallelLoopTree (n - n / 2) w)
termination_by n
decreasing_by
  · exact Nat.div_lt_self (by omega) (by norm_num)
  · exact Nat.sub_lt (by omega) (Nat.div_pos (by omega) (by norm_num))



theorem parallelLoopTree_of_le_one {n w : ℕ} (hn : n ≤ 1) :
    parallelLoopTree n w = .leaf (n * w) := by
  rw [parallelLoopTree]
  simp [hn]



theorem parallelLoopTree_unfold {n w : ℕ} (hn : 2 ≤ n) :
    parallelLoopTree n w =
      .spawn (parallelLoopTree (n / 2) w) (parallelLoopTree (n - n / 2) w) := by
  rw [parallelLoopTree]
  simp [show ¬n ≤ 1 by omega]

The work of a parallel loop: n iterations of weight w plus one unit per internal spawn node (n - 1 of them).


theorem parallelLoop_work {n : ℕ} (hn : 1 ≤ n) (w : ℕ) :
    (parallelLoopTree n w).work + 1 = n * w + n := by
  revert hn w
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro hn w
      by_cases h1 : n ≤ 1
      · have : n = 1 := by omega
        subst this
        simp [parallelLoopTree_of_le_one, SpawnTree.work]
      · rw [parallelLoopTree_unfold (by omega), SpawnTree.work]
        have h1 := ih (n / 2) (by omega) (by omega) w
        have h2 := ih (n - n / 2) (by omega) (by omega) w
        have hsum : n / 2 * w + (n - n / 2) * w = n * w := by
          rw [← Nat.add_mul]
          congr 1
          omega
        omega

The spawn depth of the balanced parallel-loop tree: 0 for n ≤ 1, else one more than the deeper of the two halves.

def parallelLoopDepth (n : ℕ) : ℕ :=
  if n ≤ 1 then
    0
  else
    max (parallelLoopDepth (n / 2)) (parallelLoopDepth (n - n / 2)) + 1
termination_by n
decreasing_by
  · exact Nat.div_lt_self (by omega) (by norm_num)
  · exact Nat.sub_lt (by omega) (Nat.div_pos (by omega) (by norm_num))



theorem parallelLoopDepth_of_le_one {n : ℕ} (hn : n ≤ 1) :
    parallelLoopDepth n = 0 := by
  rw [parallelLoopDepth]
  simp [hn]



theorem parallelLoopDepth_unfold {n : ℕ} (hn : 2 ≤ n) :
    parallelLoopDepth n =
      max (parallelLoopDepth (n / 2)) (parallelLoopDepth (n - n / 2)) + 1 := by
  rw [parallelLoopDepth]
  simp [show ¬n ≤ 1 by omega]

Exact span of the parallel-loop tree: one iteration's weight plus the balanced halving depth.


theorem parallelLoop_span (n w : ℕ) :
    (parallelLoopTree n w).span =
      if n ≤ 1 then n * w else w + parallelLoopDepth n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · rw [parallelLoopTree_of_le_one hn, if_pos hn]
        rfl
      · rw [parallelLoopTree_unfold (by omega), if_neg hn, SpawnTree.span,
          parallelLoopDepth_unfold (by omega)]
        rw [ih (n / 2) (by omega), ih (n - n / 2) (by omega)]
        by_cases h1 : n / 2 ≤ 1 <;> by_cases h2 : n - n / 2 ≤ 1
        · rw [if_pos h1, if_pos h2, parallelLoopDepth_of_le_one h1,
            parallelLoopDepth_of_le_one h2]
          have e1 : n / 2 * w = w := by
            have : n / 2 = 1 := by omega
            rw [this, Nat.one_mul]
          have e2 : (n - n / 2) * w = w := by
            have : n - n / 2 = 1 := by omega
            rw [this, Nat.one_mul]
          rw [e1, e2]
          simp
        · rw [if_pos h1, if_neg h2, parallelLoopDepth_of_le_one h1]
          have e1 : n / 2 * w = w := by
            have : n / 2 = 1 := by omega
            rw [this, Nat.one_mul]
          rw [e1]
          omega
        · rw [if_neg h1, if_pos h2, parallelLoopDepth_of_le_one h2]
          have e2 : (n - n / 2) * w = w := by
            have : n - n / 2 = 1 := by omega
            rw [this, Nat.one_mul]
          rw [e2]
          omega
        · rw [if_neg h1, if_neg h2]
          omega

The depth is logarithmic: n ≤ 2 ^ depth.


theorem parallelLoopDepth_pow (n : ℕ) : n ≤ 2 ^ parallelLoopDepth n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · rw [parallelLoopDepth_of_le_one hn, pow_zero]
        omega
      · rw [parallelLoopDepth_unfold (by omega), pow_succ]
        have h1 := ih (n / 2) (by omega)
        have h2 := ih (n - n / 2) (by omega)
        have hmax :
            2 ^ max (parallelLoopDepth (n / 2)) (parallelLoopDepth (n - n / 2)) =
              max (2 ^ parallelLoopDepth (n / 2))
                (2 ^ parallelLoopDepth (n - n / 2)) := by
          rcases le_total (parallelLoopDepth (n / 2))
            (parallelLoopDepth (n - n / 2)) with h | h
          · rw [max_eq_right h,
              max_eq_right (Nat.pow_le_pow_right (by norm_num) h)]
          · rw [max_eq_left h,
              max_eq_left (Nat.pow_le_pow_right (by norm_num) h)]
        rw [hmax]
        rcases le_total (2 ^ parallelLoopDepth (n / 2))
          (2 ^ parallelLoopDepth (n - n / 2)) with h | h
        · rw [max_eq_right h]
          omega
        · rw [max_eq_left h]
          omega

The balanced parallel-loop depth is bounded by one more than the base-two floor logarithm on every input.


theorem parallelLoopDepth_le_log (n : ℕ) :
    parallelLoopDepth n ≤ Nat.log 2 n + 1 := by
  have hdepth_clog : parallelLoopDepth n ≤ Nat.clog 2 n := by
    induction n using Nat.strong_induction_on with
    | h n ih =>
        by_cases hn : n ≤ 1
        · rw [parallelLoopDepth_of_le_one hn]
          exact Nat.zero_le _
        · have hfloor := ih (n / 2) (by omega)
          have hceil := ih (n - n / 2) (by omega)
          have hfloor_le_ceil : n / 2 ≤ n - n / 2 := by omega
          have hhalf : (n + 2 - 1) / 2 = n - n / 2 := by omega
          rw [parallelLoopDepth_unfold (by omega),
            Nat.clog_of_two_le (by norm_num) (by omega), hhalf]
          exact Nat.add_le_add_right
            (max_le (hfloor.trans (Nat.clog_mono_right 2 hfloor_le_ceil)) hceil) 1
  apply hdepth_clog.trans
  rw [Nat.clog_le_iff_le_pow (by norm_num)]
  exact (Nat.lt_pow_succ_log_self (by norm_num) n).le

The balanced parallel-loop span is at most one iteration's weight plus one more than the base-two floor logarithm, on every input.


theorem parallelLoop_span_le_log (n w : ℕ) :
    (parallelLoopTree n w).span ≤ w + Nat.log 2 n + 1 := by
  rw [parallelLoop_span]
  by_cases hn : n ≤ 1
  · rw [if_pos hn]
    interval_cases n <;> simp
  · rw [if_neg hn]
    exact Nat.add_le_add_left (parallelLoopDepth_le_log n) w

              example : parallelLoopDepth 0 = 0 := by native_decideexample : parallelLoopDepth 1 = 0 := by native_decideexample : parallelLoopDepth 2 = 1 := by native_decideexample : parallelLoopDepth 3 = 2 := by native_decideexample : parallelLoopDepth 8 = 3 := by native_decideexample : parallelLoopDepth 9 = 4 := by native_decideexample : (parallelLoopTree 9 3).span ≤ 3 + Nat.log 2 9 + 1 :=
  parallelLoop_span_le_log 9 3end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Definitions

CLRS Section 26.2 — Parallel Matrix Algorithms

This module gives the main-text P-ADD and P-MATMUL algorithms executable interpretations. Each positive-depth addition runs four independent quadrant additions. Matrix multiplication runs eight independent recursive products, stores their values in two fresh functional temporary matrices, and then adds those matrices with P-ADD.

The returned CLRS.Chapter27.Costed value simultaneously records the ordinary result, total work, and critical-path span of the balanced execution.

              namespace CLRSnamespace Chapter27universe u

CLRS P-ADD on a depth-indexed 2^k × 2^k square matrix.

The value is the recursively assembled matrix sum. Each scalar leaf charges one unit of work and span, while each four-way level uses the fixed balanced fork/join structure of Costed.par4.

def pAdd (R : Type u) [Ring R] :
    ∀ k, Chapter04.SqMat R k → Chapter04.SqMat R k → Costed (Chapter04.SqMat R k)
  | 0, x, y => Costed.charge 1 1 (x + y)
  | k + 1, A, B =>
      Costed.map
        (fun q => !![q.1.1, q.1.2; q.2.1, q.2.2])
        (Costed.par4
          (pAdd R k (A 0 0) (B 0 0))
          (pAdd R k (A 0 1) (B 0 1))
          (pAdd R k (A 1 0) (B 1 0))
          (pAdd R k (A 1 1) (B 1 1)))

CLRS P-MATMUL on a depth-indexed 2^k × 2^k square matrix.

At a positive depth the eight recursive products run in one balanced parallel composition. The first four and last four results form fresh temporary matrices, which are then added sequentially. Because each branch produces an immutable value, the computation has no concurrent writes or data race.

def pMatMul (R : Type u) [Ring R] :
    ∀ k, Chapter04.SqMat R k → Chapter04.SqMat R k → Costed (Chapter04.SqMat R k)
  | 0, x, y => Costed.charge 1 1 (x * y)
  | k + 1, A, B =>
      Costed.seq
        (Costed.par8
          (pMatMul R k (A 0 0) (B 0 0))
          (pMatMul R k (A 0 0) (B 0 1))
          (pMatMul R k (A 1 0) (B 0 0))
          (pMatMul R k (A 1 0) (B 0 1))
          (pMatMul R k (A 0 1) (B 1 0))
          (pMatMul R k (A 0 1) (B 1 1))
          (pMatMul R k (A 1 1) (B 1 0))
          (pMatMul R k (A 1 1) (B 1 1)))
        (fun q =>
          let C : Chapter04.SqMat R (k + 1) :=
            !![q.1.1.1, q.1.1.2; q.1.2.1, q.1.2.2]
          let T : Chapter04.SqMat R (k + 1) :=
            !![q.2.1.1, q.2.1.2; q.2.2.1, q.2.2.2]
          pAdd R (k + 1) C T)

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Correctness

CLRS Section 26.2 — Correctness of Parallel Matrix Algorithms

The balanced execution structure affects only work and span: the value returned by P-ADD is exactly ordinary matrix addition, and P-MATMUL computes ordinary matrix multiplication. Both results hold over any ring, including a noncommutative one.

Main results:

Theorem pAdd_value: the executable result value is A + B.
Theorem pAdd_correct: reader-facing correctness of CLRS P-ADD.
Theorem pMatMul_value: the executable result value is A * B.
Theorem pMatMul_correct: reader-facing correctness of CLRS P-MATMUL.

              namespace CLRSnamespace Chapter27universe u

The value computed by P-ADD is ordinary matrix addition.

theorem pAdd_value (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) : (pAdd R k A B).value = A + B := by
  induction k with
  | zero => rfl
  | succ k ih =>
      funext i j
      change (pAdd R (k + 1) A B).value i j = A i j + B i j
      fin_cases i <;> fin_cases j <;>
        simp [pAdd, ih]

Reader-facing correctness theorem for CLRS P-ADD.

theorem pAdd_correct (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) : (pAdd R k A B).value = A + B :=
  pAdd_value R k A B

The value computed by P-MATMUL is ordinary matrix multiplication.


theorem pMatMul_value (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) : (pMatMul R k A B).value = A * B := by
  induction k with
  | zero => rfl
  | succ k ih =>
      funext i j
      have hmul : (A * B) i j = ∑ x : Fin 2, A i x * B x j :=
        Matrix.mul_apply
      rw [hmul]
      fin_cases i <;> fin_cases j <;>
        simp [pMatMul, pAdd, ih, Fin.sum_univ_two, pAdd_value]

Reader-facing correctness theorem for CLRS P-MATMUL.

theorem pMatMul_correct (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) : (pMatMul R k A B).value = A * B :=
  pMatMul_value R k A B

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Costs.Definitions

CLRS Section 26.2 — Exact Costs of Parallel Matrix Algorithms

This module defines the exact work and span recurrences induced by the executable P-ADD and P-MATMUL implementations. Their base cases charge one scalar operation. Recursive cases include the balanced fork/join costs recorded by Costed.par4 and Costed.par8.

The names pMatMulExecWork and pMatMulExecSpan deliberately distinguish these execution-attached costs from the earlier idealized recurrence model.

namespace CLRSnamespace Chapter27

P-ADD costs

Exact work recurrence induced by the balanced executable P-ADD.

def pAddWork (n : ℕ) : ℕ :=
  if n ≤ 1 then
    1
  else
    4 * pAddWork (n / 2) + 3
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)

Unfold the recursive branch of the exact P-ADD work recurrence.


@[simp] theorem pAddWork_unfold {n : ℕ} (hn : 2 ≤ n) :
    pAddWork n = 4 * pAddWork (n / 2) + 3 := by
  rw [pAddWork]
  simp [show ¬n ≤ 1 by omega]

Exact span recurrence induced by the balanced executable P-ADD.

def pAddSpan (n : ℕ) : ℕ :=
  if n ≤ 1 then
    1
  else
    pAddSpan (n / 2) + 2
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)

Unfold the recursive branch of the exact P-ADD span recurrence.


@[simp] theorem pAddSpan_unfold {n : ℕ} (hn : 2 ≤ n) :
    pAddSpan n = pAddSpan (n / 2) + 2 := by
  rw [pAddSpan]
  simp [show ¬n ≤ 1 by omega]

P-MATMUL execution costs

Exact work recurrence induced by executable P-MATMUL.

The recursive products contribute the eight-way parallel cost; the final term is the exact work of the subsequent P-ADD call.

def pMatMulExecWork (n : ℕ) : ℕ :=
  if n ≤ 1 then
    1
  else
    8 * pMatMulExecWork (n / 2) + 7 + pAddWork n
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)

Unfold the recursive branch of executable P-MATMUL work.


@[simp] theorem pMatMulExecWork_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMatMulExecWork n =
      8 * pMatMulExecWork (n / 2) + 7 + pAddWork n := by
  rw [pMatMulExecWork]
  simp [show ¬n ≤ 1 by omega]

Exact span recurrence induced by executable P-MATMUL.

The eight recursive products run in parallel, after which P-ADD runs sequentially on their two temporary matrices.

def pMatMulExecSpan (n : ℕ) : ℕ :=
  if n ≤ 1 then
    1
  else
    pMatMulExecSpan (n / 2) + 3 + pAddSpan n
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)

Unfold the recursive branch of executable P-MATMUL span.


@[simp] theorem pMatMulExecSpan_unfold {n : ℕ} (hn : 2 ≤ n) :
    pMatMulExecSpan n =
      pMatMulExecSpan (n / 2) + 3 + pAddSpan n := by
  rw [pMatMulExecSpan]
  simp [show ¬n ≤ 1 by omega]

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Costs.ExecutionEqualities

CLRS Section 26.2 — Matrix Execution Cost Equalities

This module connects the exact work and span carried by executable P-ADD and P-MATMUL results to their natural-number recurrences. The equalities hold at every matrix depth over any ring.

Main results:

Theorem pAdd_work_eq: executable P-ADD work equals pAddWork.
Theorem pAdd_span_eq: executable P-ADD span equals pAddSpan.
Theorem pMatMul_work_eq: executable P-MATMUL work equals pMatMulExecWork.
Theorem pMatMul_span_eq: executable P-MATMUL span equals pMatMulExecSpan.

              namespace CLRSnamespace Chapter27universe u

Halving the next power of two returns the preceding power.


private theorem two_pow_succ_div_two (k : ℕ) : 2 ^ (k + 1) / 2 = 2 ^ k := by
  rw [pow_succ]
  omega

Every non-base power of two has size at least two.


private theorem two_le_two_pow_succ (k : ℕ) : 2 ≤ 2 ^ (k + 1) := by
  rw [pow_succ]
  have := Nat.one_le_pow k 2 (by norm_num)
  omega

Exact work carried by executable P-ADD at matrix depth k.


theorem pAdd_work_eq (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) :
    (pAdd R k A B).work = pAddWork (2 ^ k) := by
  induction k with
  | zero => simp [pAdd, pAddWork]
  | succ k ih =>
      rw [pAddWork_unfold (two_le_two_pow_succ k), two_pow_succ_div_two]
      simp [pAdd, ih]
      omega

Exact span carried by executable P-ADD at matrix depth k.


theorem pAdd_span_eq (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) :
    (pAdd R k A B).span = pAddSpan (2 ^ k) := by
  induction k with
  | zero => simp [pAdd, pAddSpan]
  | succ k ih =>
      rw [pAddSpan_unfold (two_le_two_pow_succ k), two_pow_succ_div_two]
      simp [pAdd, ih]

Exact work carried by executable P-MATMUL at matrix depth k.


theorem pMatMul_work_eq (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) :
    (pMatMul R k A B).work = pMatMulExecWork (2 ^ k) := by
  induction k with
  | zero => simp [pMatMul, pMatMulExecWork]
  | succ k ih =>
      rw [pMatMulExecWork_unfold (two_le_two_pow_succ k),
        two_pow_succ_div_two]
      simp [pMatMul, ih, pAdd_work_eq]
      omega

Exact span carried by executable P-MATMUL at matrix depth k.


theorem pMatMul_span_eq (R : Type u) [Ring R] (k : ℕ)
    (A B : Chapter04.SqMat R k) :
    (pMatMul R k A B).span = pMatMulExecSpan (2 ^ k) := by
  induction k with
  | zero => simp [pMatMul, pMatMulExecSpan]
  | succ k ih =>
      rw [pMatMulExecSpan_unfold (two_le_two_pow_succ k),
        two_pow_succ_div_two]
      simp [pMatMul, ih, pAdd_span_eq]

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Costs.Monotonicity

CLRS Section 26.2 — Monotonicity of Matrix Execution Costs

The executable matrix recurrences use floor halving on arbitrary natural inputs. This module proves that all four costs are monotone and packages the adjacent-power sandwiches used by the all-input asymptotic analysis.

Main results:

Theorems pAddWork_monotone and pAddSpan_monotone.
Theorems pMatMulExecWork_monotone and pMatMulExecSpan_monotone.
The four corresponding *_power_sandwich theorems.

namespace CLRSnamespace Chapter27

Small base values

              

@[simp] private theorem pAddWork_zero : pAddWork 0 = 1 := by
  rw [pAddWork]
  norm_num

@[simp] private theorem pAddWork_one : pAddWork 1 = 1 := by
  rw [pAddWork]
  norm_num

@[simp] private theorem pAddWork_two : pAddWork 2 = 7 := by
  rw [pAddWork_unfold (n := 2) (by norm_num)]
  norm_num

@[simp] private theorem pAddSpan_zero : pAddSpan 0 = 1 := by
  rw [pAddSpan]
  norm_num

@[simp] private theorem pAddSpan_one : pAddSpan 1 = 1 := by
  rw [pAddSpan]
  norm_num

@[simp] private theorem pAddSpan_two : pAddSpan 2 = 3 := by
  rw [pAddSpan_unfold (n := 2) (by norm_num)]
  norm_num

@[simp] private theorem pMatMulExecWork_zero : pMatMulExecWork 0 = 1 := by
  rw [pMatMulExecWork]
  norm_num

@[simp] private theorem pMatMulExecWork_one : pMatMulExecWork 1 = 1 := by
  rw [pMatMulExecWork]
  norm_num

@[simp] private theorem pMatMulExecWork_two : pMatMulExecWork 2 = 22 := by
  rw [pMatMulExecWork_unfold (n := 2) (by norm_num)]
  norm_num

@[simp] private theorem pMatMulExecSpan_zero : pMatMulExecSpan 0 = 1 := by
  rw [pMatMulExecSpan]
  norm_num

@[simp] private theorem pMatMulExecSpan_one : pMatMulExecSpan 1 = 1 := by
  rw [pMatMulExecSpan]
  norm_num

@[simp] private theorem pMatMulExecSpan_two : pMatMulExecSpan 2 = 7 := by
  rw [pMatMulExecSpan_unfold (n := 2) (by norm_num)]
  norm_num

P-ADD

P-ADD work does not decrease at a successor input.


private theorem pAddWork_le_succ : ∀ n, pAddWork n ≤ pAddWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n <;> simp
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          rw [pAddWork_unfold (n := 2 * m) (by omega),
            pAddWork_unfold (n := 2 * m + 1) (by omega), hdiv0, hdiv1]
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pAddWork_unfold (n := 2 * m + 1) (by omega),
            pAddWork_unfold (n := 2 * m + 1 + 1) (by omega), hdiv0, hdiv1]
          exact Nat.add_le_add_right (Nat.mul_le_mul_left 4 (ih m (by omega))) 3

Exact P-ADD work is monotone in the input size.

theorem pAddWork_monotone : Monotone pAddWork :=
  monotone_nat_of_le_succ pAddWork_le_succ

Every positive P-ADD work cost lies between its adjacent power-of-two costs.

theorem pAddWork_power_sandwich (n : ℕ) (hn : 0 < n) :
    pAddWork (2 ^ Nat.log 2 n) ≤ pAddWork n ∧
      pAddWork n ≤ pAddWork (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pAddWork_monotone 2 n (by norm_num) hn.ne'

P-ADD span does not decrease at a successor input.


private theorem pAddSpan_le_succ : ∀ n, pAddSpan n ≤ pAddSpan (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n <;> simp
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          rw [pAddSpan_unfold (n := 2 * m) (by omega),
            pAddSpan_unfold (n := 2 * m + 1) (by omega), hdiv0, hdiv1]
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pAddSpan_unfold (n := 2 * m + 1) (by omega),
            pAddSpan_unfold (n := 2 * m + 1 + 1) (by omega), hdiv0, hdiv1]
          exact Nat.add_le_add_right (ih m (by omega)) 2

Exact P-ADD span is monotone in the input size.

theorem pAddSpan_monotone : Monotone pAddSpan :=
  monotone_nat_of_le_succ pAddSpan_le_succ

Every positive P-ADD span cost lies between its adjacent power-of-two costs.

theorem pAddSpan_power_sandwich (n : ℕ) (hn : 0 < n) :
    pAddSpan (2 ^ Nat.log 2 n) ≤ pAddSpan n ∧
      pAddSpan n ≤ pAddSpan (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pAddSpan_monotone 2 n (by norm_num) hn.ne'

P-MATMUL

Executable P-MATMUL work does not decrease at a successor input.


private theorem pMatMulExecWork_le_succ :
    ∀ n, pMatMulExecWork n ≤ pMatMulExecWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n <;> simp
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          rw [pMatMulExecWork_unfold (n := 2 * m) (by omega),
            pMatMulExecWork_unfold (n := 2 * m + 1) (by omega), hdiv0, hdiv1]
          exact Nat.add_le_add_left (pAddWork_monotone (by omega)) _
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pMatMulExecWork_unfold (n := 2 * m + 1) (by omega),
            pMatMulExecWork_unfold (n := 2 * m + 1 + 1) (by omega), hdiv0, hdiv1]
          have hrec := ih m (by omega)
          have hadd := pAddWork_monotone (show 2 * m + 1 ≤ 2 * m + 1 + 1 by omega)
          omega

Exact executable P-MATMUL work is monotone in the input size.

theorem pMatMulExecWork_monotone : Monotone pMatMulExecWork :=
  monotone_nat_of_le_succ pMatMulExecWork_le_succ

Every positive executable P-MATMUL work cost lies between its adjacent power-of-two costs.

theorem pMatMulExecWork_power_sandwich (n : ℕ) (hn : 0 < n) :
    pMatMulExecWork (2 ^ Nat.log 2 n) ≤ pMatMulExecWork n ∧
      pMatMulExecWork n ≤ pMatMulExecWork (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pMatMulExecWork_monotone 2 n
    (by norm_num) hn.ne'

Executable P-MATMUL span does not decrease at a successor input.


private theorem pMatMulExecSpan_le_succ :
    ∀ n, pMatMulExecSpan n ≤ pMatMulExecSpan (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n <;> simp
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          rw [pMatMulExecSpan_unfold (n := 2 * m) (by omega),
            pMatMulExecSpan_unfold (n := 2 * m + 1) (by omega), hdiv0, hdiv1]
          exact Nat.add_le_add_left (pAddSpan_monotone (by omega)) _
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [pMatMulExecSpan_unfold (n := 2 * m + 1) (by omega),
            pMatMulExecSpan_unfold (n := 2 * m + 1 + 1) (by omega), hdiv0, hdiv1]
          have hrec := ih m (by omega)
          have hadd := pAddSpan_monotone (show 2 * m + 1 ≤ 2 * m + 1 + 1 by omega)
          omega

Exact executable P-MATMUL span is monotone in the input size.

theorem pMatMulExecSpan_monotone : Monotone pMatMulExecSpan :=
  monotone_nat_of_le_succ pMatMulExecSpan_le_succ

Every positive executable P-MATMUL span cost lies between its adjacent power-of-two costs.

theorem pMatMulExecSpan_power_sandwich (n : ℕ) (hn : 0 < n) :
    pMatMulExecSpan (2 ^ Nat.log 2 n) ≤ pMatMulExecSpan n ∧
      pMatMulExecSpan n ≤ pMatMulExecSpan (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich pMatMulExecSpan_monotone 2 n
    (by norm_num) hn.ne'

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Costs.PowerBounds

CLRS Section 26.2 — Matrix Costs at Powers of Two

This module solves, or tightly bounds, the four execution recurrences at matrix sizes 2^k. Subtraction-free balance equations are used for the work recurrences so that the natural-number proofs remain stable.

Main results:

Theorems pAddWork_pow_two_bounds and pAddSpan_pow_two.
Theorems pMatMulExecWork_pow_two_bounds and pMatMulExecSpan_pow_two.
Exact-power big-Theta theorems for all four costs.

namespace CLRSnamespace Chapter27

Halving a non-base power of two returns the preceding power.


private theorem powerBounds_two_pow_succ_div_two (k : ℕ) :
    2 ^ (k + 1) / 2 = 2 ^ k := by
  rw [pow_succ]
  omega

A non-base power of two has size at least two.


private theorem powerBounds_two_le_two_pow_succ (k : ℕ) :
    2 ≤ 2 ^ (k + 1) := by
  rw [pow_succ]
  have := Nat.one_le_pow k 2 (by norm_num)
  omega

P-ADD exact powers

Subtraction-free closed form for P-ADD work at powers of two.


theorem pAddWork_pow_two_balance (k : ℕ) :
    pAddWork (2 ^ k) + 1 = 2 * 4 ^ k := by
  induction k with
  | zero =>
      rw [pAddWork]
      norm_num
  | succ k ih =>
      rw [pAddWork_unfold (powerBounds_two_le_two_pow_succ k),
        powerBounds_two_pow_succ_div_two,
        pow_succ]
      omega

P-ADD work at size 2^k is trapped within constant multiples of 4^k.


theorem pAddWork_pow_two_bounds (k : ℕ) :
    4 ^ k ≤ pAddWork (2 ^ k) ∧ pAddWork (2 ^ k) ≤ 2 * 4 ^ k := by
  have hbalance := pAddWork_pow_two_balance k
  have hpow : 1 ≤ 4 ^ k := Nat.one_le_pow k 4 (by norm_num)
  omega

Exact P-ADD span at powers of two.


theorem pAddSpan_pow_two (k : ℕ) : pAddSpan (2 ^ k) = 2 * k + 1 := by
  induction k with
  | zero =>
      rw [pAddSpan]
      norm_num
  | succ k ih =>
      rw [pAddSpan_unfold (powerBounds_two_le_two_pow_succ k),
        powerBounds_two_pow_succ_div_two, ih]
      omega

P-MATMUL exact powers

Subtraction-free closed form for executable P-MATMUL work at powers of two. It is equivalent to the usual closed form while avoiding truncated natural subtraction.


theorem pMatMulExecWork_pow_two_balance (k : ℕ) :
    7 * pMatMulExecWork (2 ^ k) + 14 * 4 ^ k + 6 = 27 * 8 ^ k := by
  induction k with
  | zero =>
      rw [pMatMulExecWork]
      norm_num
  | succ k ih =>
      rw [pMatMulExecWork_unfold (powerBounds_two_le_two_pow_succ k),
        powerBounds_two_pow_succ_div_two]
      have hadd := pAddWork_pow_two_balance (k + 1)
      rw [pow_succ] at hadd ⊢
      omega

Executable P-MATMUL work at size 2^k is trapped within constant multiples of 8^k.


theorem pMatMulExecWork_pow_two_bounds (k : ℕ) :
    8 ^ k ≤ pMatMulExecWork (2 ^ k) ∧
      pMatMulExecWork (2 ^ k) ≤ 4 * 8 ^ k := by
  constructor
  · induction k with
    | zero =>
        rw [pMatMulExecWork]
        norm_num
    | succ k ih =>
        rw [pMatMulExecWork_unfold (powerBounds_two_le_two_pow_succ k),
          powerBounds_two_pow_succ_div_two, pow_succ]
        omega
  · have hbalance := pMatMulExecWork_pow_two_balance k
    omega

Exact executable P-MATMUL span at powers of two.


theorem pMatMulExecSpan_pow_two (k : ℕ) :
    pMatMulExecSpan (2 ^ k) = k ^ 2 + 5 * k + 1 := by
  induction k with
  | zero =>
      rw [pMatMulExecSpan]
      norm_num
  | succ k ih =>
      rw [pMatMulExecSpan_unfold (powerBounds_two_le_two_pow_succ k),
        powerBounds_two_pow_succ_div_two, ih, pAddSpan_pow_two]
      ring

Executable P-MATMUL span at size 2^k is quadratic in k+1.


theorem pMatMulExecSpan_pow_two_bounds (k : ℕ) :
    (k + 1) ^ 2 ≤ pMatMulExecSpan (2 ^ k) ∧
      pMatMulExecSpan (2 ^ k) ≤ 3 * (k + 1) ^ 2 := by
  rw [pMatMulExecSpan_pow_two]
  constructor <;> nlinarith [Nat.zero_le k]

Exact-power asymptotics

P-ADD work is Theta of 4^k on exact powers of two.


theorem pAddWork_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pAddWork (2 ^ k) : ℝ))
      (fun k : ℕ => (4 : ℝ) ^ k) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨2, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hreal :
        (pAddWork (2 ^ k) : ℝ) ≤ ((2 * 4 ^ k : ℕ) : ℝ) := by
      exact_mod_cast (pAddWork_pow_two_bounds k).2
    simpa [Nat.cast_mul, Nat.cast_pow] using hreal
  · refine (Chapter03.isBigOmega_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ (4 : ℝ) ^ k),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hreal : ((4 ^ k : ℕ) : ℝ) ≤ (pAddWork (2 ^ k) : ℝ) := by
      exact_mod_cast (pAddWork_pow_two_bounds k).1
    simpa [Nat.cast_pow] using hreal

P-ADD span is Theta of k+1 on exact powers of two.


theorem pAddSpan_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pAddSpan (2 ^ k) : ℝ))
      (fun k : ℕ => (k : ℝ) + 1) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨2, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    rw [pAddSpan_pow_two]
    push_cast
    have hk : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k
    nlinarith
  · refine (Chapter03.isBigOmega_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ (k : ℝ) + 1),
      abs_of_nonneg (Nat.cast_nonneg _)]
    rw [pAddSpan_pow_two]
    push_cast
    have hk : (0 : ℝ) ≤ (k : ℝ) := Nat.cast_nonneg k
    nlinarith

Executable P-MATMUL work is Theta of 8^k on exact powers of two.


theorem pMatMulExecWork_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pMatMulExecWork (2 ^ k) : ℝ))
      (fun k : ℕ => (8 : ℝ) ^ k) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨4, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hreal :
        (pMatMulExecWork (2 ^ k) : ℝ) ≤ ((4 * 8 ^ k : ℕ) : ℝ) := by
      exact_mod_cast (pMatMulExecWork_pow_two_bounds k).2
    simpa [Nat.cast_mul, Nat.cast_pow] using hreal
  · refine (Chapter03.isBigOmega_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ (8 : ℝ) ^ k),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hreal : ((8 ^ k : ℕ) : ℝ) ≤ (pMatMulExecWork (2 ^ k) : ℝ) := by
      exact_mod_cast (pMatMulExecWork_pow_two_bounds k).1
    simpa [Nat.cast_pow] using hreal

Executable P-MATMUL span is Theta of (k+1)^2 on exact powers of two.


theorem pMatMulExecSpan_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (pMatMulExecSpan (2 ^ k) : ℝ))
      (fun k : ℕ => ((k : ℝ) + 1) ^ 2) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨3, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hreal :
        (pMatMulExecSpan (2 ^ k) : ℝ) ≤ ((3 * (k + 1) ^ 2 : ℕ) : ℝ) := by
      exact_mod_cast (pMatMulExecSpan_pow_two_bounds k).2
    norm_num [Nat.cast_mul, Nat.cast_pow] at hreal ⊢
    exact hreal
  · refine (Chapter03.isBigOmega_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ ((k : ℝ) + 1) ^ 2),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hreal : (((k + 1) ^ 2 : ℕ) : ℝ) ≤
        (pMatMulExecSpan (2 ^ k) : ℝ) := by
      exact_mod_cast (pMatMulExecSpan_pow_two_bounds k).1
    norm_num [Nat.cast_pow] at hreal ⊢
    exact hreal

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMatrix.Costs.AllInputBounds

CLRS Section 26.2 — All-Input Matrix Asymptotics

This module extends numerical cost recurrences from their exact-power analysis to every natural size. The actual P-ADD and P-MATMUL constructors remain indexed by depth and dimension 2^k; these numeric bounds do not supply an arbitrary-dimension padding/unpadding execution. The results distinguish the execution-attached P-MATMUL span, which includes its sequential P-ADD stage and therefore grows as Theta(log^2 n), from the earlier idealized recurrence.

Main results:

Theorem pAddWork_allInput_bigTheta: P-ADD work is quadratic.
Theorem pAddSpan_allInput_bigTheta: P-ADD span is logarithmic.
Theorem pMatMulExecWork_allInput_bigTheta: executable P-MATMUL work is cubic.
Theorem pMatMulExecSpan_allInput_bigTheta: executable P-MATMUL span is log-squared (Theta(log^2 n)).

namespace CLRSnamespace Chapter27

P-ADD has quadratic work on every positive input size.


theorem pAddWork_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pAddWork n : ℝ))
      (Chapter04.polynomialScale 2) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (pAddWork n : ℝ))
        (Chapter04.criticalPowerScale 4 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerScale 4 2
      (fun n : ℕ => (pAddWork n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast pAddWork_monotone)
      pAddWork_exactPower_bigTheta
  exact Chapter03.isBigTheta_trans hcritical (by
    simpa using Chapter04.criticalPowerScale_isBigTheta_polynomialScale 2 2
      (by norm_num))

P-ADD has logarithmic span on every positive input size.


theorem pAddSpan_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pAddSpan n : ℝ))
      (Chapter04.polynomialLogScale 2 0) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (pAddSpan n : ℝ))
        (Chapter04.criticalPowerLogScale 1 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerLogScale 1 2
      (fun n : ℕ => (pAddSpan n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast pAddSpan_monotone) (by
        simpa only [Nat.cast_one, one_pow, mul_one] using
          pAddSpan_exactPower_bigTheta)
  exact Chapter03.isBigTheta_trans hcritical (by
    simpa using Chapter04.criticalPowerLogScale_isBigTheta_polynomialLogScale
      2 0 (by norm_num))

Executable P-MATMUL has cubic work on every positive input size.


theorem pMatMulExecWork_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pMatMulExecWork n : ℝ))
      (Chapter04.polynomialScale 3) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (pMatMulExecWork n : ℝ))
        (Chapter04.criticalPowerScale 8 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerScale 8 2
      (fun n : ℕ => (pMatMulExecWork n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast pMatMulExecWork_monotone)
      pMatMulExecWork_exactPower_bigTheta
  exact Chapter03.isBigTheta_trans hcritical (by
    simpa using Chapter04.criticalPowerScale_isBigTheta_polynomialScale 2 3
      (by norm_num))

Executable P-MATMUL has log-squared span, Theta(log^2 n), on every positive input size. This is the actual span of the costed implementation, including the sequential P-ADD phase.


theorem pMatMulExecSpan_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (pMatMulExecSpan n : ℝ))
      (Chapter04.criticalPowerLogPolylogScale 1 2 1) := by
  have hpower :
      Chapter03.isBigTheta
        (fun i : ℕ => (pMatMulExecSpan (2 ^ i) : ℝ))
        (fun i : ℕ =>
          Chapter04.criticalPowerLogPolylogScale 1 2 1 (2 ^ i)) := by
    have hscale :
        (fun i : ℕ =>
          Chapter04.criticalPowerLogPolylogScale 1 2 1 (2 ^ i)) =
          (fun i : ℕ => ((i : ℝ) + 1) ^ 2) := by
      funext i
      simp [Chapter04.criticalPowerLogPolylogScale_exactPower]
    rw [hscale]
    exact pMatMulExecSpan_exactPower_bigTheta
  exact Chapter04.allInput_bigTheta_of_powerStep 2
    (fun n : ℕ => (pMatMulExecSpan n : ℝ))
    (Chapter04.criticalPowerLogPolylogScale 1 2 1) (by norm_num)
    (Chapter04.monotoneAbs_natCast pMatMulExecSpan_monotone)
    (Chapter04.criticalPowerLogPolylogScale_monotoneAbs 1 2 1 (by norm_num))
    (Chapter04.criticalPowerLogPolylogScale_powerStepBound 1 2 1
      (by norm_num) (by norm_num))
    hpower

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelStrassen.Recurrences.Definitions

Chapter 26 extension — parallel Strassen recurrences: definitions

This compatibility extension records the work/span recurrences and their exact power-of-two solutions for the parallelized form of Strassen's algorithm. It is deliberately separated from the Chapter 26 main-text recurrences.

              namespace CLRSnamespace Chapter27

private theorem pow_two_succ_eq (k : ℕ) : 2 ^ (k + 1) / 2 = 2 ^ k := by
  rw [pow_succ]
  omega

private theorem two_le_two_pow_succ (k : ℕ) : 2 ≤ 2 ^ (k + 1) := by
  rw [pow_succ]
  have := Nat.one_le_pow k 2 (by norm_num)
  omega

private theorem two_pow_succ_mul (k : ℕ) : 2 ^ (k + 1) * 2 ^ (k + 1) = 4 ^ (k + 1) := by
  have h42 : (4 : ℕ) = 2 ^ 2 := by norm_num
  rw [h42, ← pow_mul, ← pow_add]
  congr 1
  omega

Work recurrence for parallel Strassen: T₁(n) = 7 T₁(n/2) + n².

def strassenWork (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    7 * strassenWork (n / 2) + n * n
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)



theorem strassenWork_unfold {n : ℕ} (hn : 2 ≤ n) :
    strassenWork n = 7 * strassenWork (n / 2) + n * n := by
  rw [strassenWork]
  simp [show ¬n ≤ 1 by omega]

Exact work on powers of two: 3·T₁(2ᵏ) + 4ᵏ⁺¹ = 7ᵏ⁺¹ (work Θ(n^(log₂ 7))).


theorem strassenWork_pow_two (k : ℕ) :
    3 * strassenWork (2 ^ k) + 4 ^ (k + 1) = 7 ^ (k + 1) := by
  induction k with
  | zero =>
      rw [strassenWork]
      norm_num
  | succ k ih =>
      rw [strassenWork_unfold (two_le_two_pow_succ k), pow_two_succ_eq,
        two_pow_succ_mul]
      nlinarith [ih, pow_succ (4 : ℕ) (k + 1), pow_succ (7 : ℕ) (k + 1)]

Span recurrence for parallel Strassen: T∞(n) = T∞(n/2) + 1.

def strassenSpan (n : ℕ) : ℕ :=
  if n ≤ 1 then
    n
  else
    strassenSpan (n / 2) + 1
termination_by n
decreasing_by exact Nat.div_lt_self (by omega) (by norm_num)



theorem strassenSpan_unfold {n : ℕ} (hn : 2 ≤ n) :
    strassenSpan n = strassenSpan (n / 2) + 1 := by
  rw [strassenSpan]
  simp [show ¬n ≤ 1 by omega]

Exact span on powers of two: T∞(2ᵏ) = k + 1 (span Θ(log n)).


theorem strassenSpan_pow_two (k : ℕ) : strassenSpan (2 ^ k) = k + 1 := by
  induction k with
  | zero =>
      rw [strassenSpan]
      norm_num
  | succ k ih =>
      rw [strassenSpan_unfold (two_le_two_pow_succ k), pow_two_succ_eq, ih]

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelStrassen.Recurrences.Monotonicity

Chapter 26 extension — parallel Strassen recurrences: monotonicity

This module proves successor monotonicity and the adjacent-power sandwiches used to lift the compatibility extension's exact solutions to every input.

namespace CLRSnamespace Chapter27

The parallel Strassen work recurrence does not decrease at a successor step.


private theorem strassenWork_le_succ : ∀ n, strassenWork n ≤ strassenWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n
        · rw [show strassenWork 0 = 0 by rw [strassenWork]; norm_num]
          exact Nat.zero_le _
        · have hone : strassenWork 1 = 1 := by rw [strassenWork]; norm_num
          rw [hone, strassenWork_unfold (n := 2) (by norm_num)]
          norm_num [hone]
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          rw [strassenWork_unfold (n := 2 * m) (by omega),
            strassenWork_unfold (n := 2 * m + 1) (by omega), hdiv0, hdiv1]
          have hsquare : (2 * m) * (2 * m) ≤ (2 * m + 1) * (2 * m + 1) := by
            nlinarith
          omega
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [strassenWork_unfold (n := 2 * m + 1) (by omega),
            strassenWork_unfold (n := 2 * m + 1 + 1) (by omega), hdiv0, hdiv1]
          have ihm := ih m (by omega)
          have hsquare : (2 * m + 1) * (2 * m + 1) ≤
              (2 * m + 1 + 1) * (2 * m + 1 + 1) := by
            nlinarith
          omega

Parallel Strassen work is monotone in the input size.

theorem strassenWork_monotone : Monotone strassenWork :=
  monotone_nat_of_le_succ strassenWork_le_succ

Every positive parallel-Strassen work cost lies between its adjacent power-of-two costs.

theorem strassenWork_power_sandwich (n : ℕ) (hn : 0 < n) :
    strassenWork (2 ^ Nat.log 2 n) ≤ strassenWork n ∧
      strassenWork n ≤ strassenWork (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich strassenWork_monotone 2 n (by norm_num) hn.ne'

The parallel Strassen span recurrence does not decrease at a successor step.


private theorem strassenSpan_le_succ : ∀ n, strassenSpan n ≤ strassenSpan (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · interval_cases n
        · rw [show strassenSpan 0 = 0 by rw [strassenSpan]; norm_num]
          exact Nat.zero_le _
        · have hone : strassenSpan 1 = 1 := by rw [strassenSpan]; norm_num
          rw [hone, strassenSpan_unfold (n := 2) (by norm_num)]
          norm_num [hone]
      · obtain ⟨m, rfl | rfl⟩ : ∃ m, n = 2 * m ∨ n = 2 * m + 1 :=
          ⟨n / 2, by omega⟩
        · have hdiv0 : 2 * m / 2 = m := by omega
          have hdiv1 : (2 * m + 1) / 2 = m := by omega
          rw [strassenSpan_unfold (n := 2 * m) (by omega),
            strassenSpan_unfold (n := 2 * m + 1) (by omega), hdiv0, hdiv1]
        · have hdiv0 : (2 * m + 1) / 2 = m := by omega
          have hdiv1 : (2 * m + 1 + 1) / 2 = m + 1 := by omega
          rw [strassenSpan_unfold (n := 2 * m + 1) (by omega),
            strassenSpan_unfold (n := 2 * m + 1 + 1) (by omega), hdiv0, hdiv1]
          exact Nat.add_le_add_right (ih m (by omega)) 1

Parallel Strassen span is monotone in the input size.

theorem strassenSpan_monotone : Monotone strassenSpan :=
  monotone_nat_of_le_succ strassenSpan_le_succ

Every positive parallel-Strassen span cost lies between its adjacent power-of-two costs.

theorem strassenSpan_power_sandwich (n : ℕ) (hn : 0 < n) :
    strassenSpan (2 ^ Nat.log 2 n) ≤ strassenSpan n ∧
      strassenSpan n ≤ strassenSpan (2 ^ (Nat.log 2 n + 1)) :=
  Chapter04.monotone_power_sandwich strassenSpan_monotone 2 n (by norm_num) hn.ne'

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelStrassen.Recurrences.AllInputBounds

Chapter 26 extension — parallel Strassen recurrences: all-input bounds

This module lifts the compatibility extension's exact power-of-two work and span solutions to all positive input sizes.

              namespace CLRSnamespace Chapter27

private theorem strassenWork_exactPower_bounds (k : ℕ) :
    7 ^ k ≤ strassenWork (2 ^ k) ∧ strassenWork (2 ^ k) ≤ 3 * 7 ^ k := by
  have hexact := strassenWork_pow_two k
  rw [pow_succ (4 : ℕ) k, pow_succ (7 : ℕ) k] at hexact
  have hpow : 4 ^ k ≤ 7 ^ k := Nat.pow_le_pow_left (by norm_num) k
  constructor <;> omega

private theorem strassenWork_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (strassenWork (2 ^ k) : ℝ))
      (fun k : ℕ => (7 : ℝ) ^ k) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ⟨3, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (by positivity)]
    have hreal :
        (strassenWork (2 ^ k) : ℝ) ≤ ((3 * 7 ^ k : ℕ) : ℝ) := by
      exact_mod_cast (strassenWork_exactPower_bounds k).2
    simpa [Nat.cast_mul, Nat.cast_pow] using hreal
  · refine (Chapter03.isBigOmega_iff _ _).mpr ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [abs_of_nonneg (by positivity : 0 ≤ (7 : ℝ) ^ k),
      abs_of_nonneg (Nat.cast_nonneg _)]
    have hreal : ((7 ^ k : ℕ) : ℝ) ≤ (strassenWork (2 ^ k) : ℝ) := by
      exact_mod_cast (strassenWork_exactPower_bounds k).1
    simpa [Nat.cast_pow] using hreal

private theorem strassenSpan_exactPower_bigTheta :
    Chapter03.isBigTheta
      (fun k : ℕ => (strassenSpan (2 ^ k) : ℝ))
      (fun k : ℕ => (k : ℝ) + 1) := by
  have hfun :
      (fun k : ℕ => (strassenSpan (2 ^ k) : ℝ)) =
        (fun k : ℕ => (k : ℝ) + 1) := by
    funext k
    rw [strassenSpan_pow_two]
    push_cast
    norm_num
  rw [hfun]
  exact Chapter03.isBigTheta_refl _

Parallel Strassen has work n^(log₂ 7) on every positive input size.


theorem strassenWork_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (strassenWork n : ℝ))
      (Chapter04.realLogScale 7 2) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (strassenWork n : ℝ))
        (Chapter04.criticalPowerScale 7 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerScale 7 2
      (fun n : ℕ => (strassenWork n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast strassenWork_monotone)
      strassenWork_exactPower_bigTheta
  exact Chapter03.isBigTheta_trans hcritical
    (Chapter04.criticalPowerScale_isBigTheta_realLogScale 7 2
      (by norm_num) (by norm_num))

Parallel Strassen has logarithmic span on every positive input size.


theorem strassenSpan_allInput_bigTheta :
    Chapter03.isBigTheta (fun n : ℕ => (strassenSpan n : ℝ))
      (Chapter04.polynomialLogScale 2 0) := by
  have hcritical :
      Chapter03.isBigTheta (fun n : ℕ => (strassenSpan n : ℝ))
        (Chapter04.criticalPowerLogScale 1 2) :=
    Chapter04.allInput_bigTheta_of_criticalPowerLogScale 1 2
      (fun n : ℕ => (strassenSpan n : ℝ)) (by norm_num) (by norm_num)
      (Chapter04.monotoneAbs_natCast strassenSpan_monotone) (by
        simpa only [Nat.cast_one, one_pow, mul_one] using
          strassenSpan_exactPower_bigTheta)
  exact Chapter03.isBigTheta_trans hcritical (by
    simpa using Chapter04.criticalPowerLogScale_isBigTheta_polynomialLogScale 2 0
      (by norm_num))

end Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMerge.MergeSplit

CLRS Chapter 26.3 — P-MERGE Split Data

P-MERGE always chooses the midpoint of the longer input and locates that pivot in the shorter input by binary lower bound. MergeSplit records this normalization without a Boolean flag, together with the size and pivot facts needed by the recursive correctness and cost proofs.

              namespace CLRSnamespace Chapter27universe u

A normalized, nonempty P-MERGE split.

primary is one of the original inputs and is at least as long as secondary; inputOrder records whether normalization preserved or exchanged the inputs. The pivot is the midpoint element of primary, and search is exactly binary lower bound on secondary. The remaining fields expose the input-size and search-index invariants used by later proof modules.

structure MergeSplit (α : Type u) [LinearOrder α] where
  xs : List α
  ys : List α
  primary : List α
  secondary : List α
  inputOrder :
    (primary = xs ∧ secondary = ys) ∨ (primary = ys ∧ secondary = xs)
  secondary_length_le_primary : secondary.length ≤ primary.length
  total_positive : 0 < xs.length + ys.length
  normalized_total : primary.length + secondary.length = xs.length + ys.length
  pivotIndex_lt : primary.length / 2 < primary.length
  pivot : α
  pivot_eq : primary.get ⟨primary.length / 2, pivotIndex_lt⟩ = pivot
  search : Costed ℕ
  search_eq : search = binaryLowerBound secondary pivot
  search_index_le : search.value ≤ secondary.length

namespace MergeSplitvariable [LinearOrder α]

The midpoint chosen from the normalized primary input.

def pivotIndex (S : MergeSplit α) : ℕ := S.primary.length / 2

The canonical partition index returned by lower-bound search.

def splitIndex (S : MergeSplit α) : ℕ := S.search.value

The canonical lower-bound index lies within the secondary input.

theorem splitIndex_le_secondary (S : MergeSplit α) :
    S.splitIndex ≤ S.secondary.length := by
  simpa [splitIndex] using S.search_index_le

The primary prefix sent to the lower recursive call.

def lowerPrimary (S : MergeSplit α) : List α := S.primary.take S.pivotIndex

The secondary prefix sent to the lower recursive call.

def lowerSecondary (S : MergeSplit α) : List α := S.secondary.take S.splitIndex

The primary suffix strictly after the pivot.

def upperPrimary (S : MergeSplit α) : List α := S.primary.drop (S.pivotIndex + 1)

The secondary suffix beginning at the lower-bound index.

def upperSecondary (S : MergeSplit α) : List α := S.secondary.drop S.splitIndex

Total input size of the lower recursive call.

def leftSize (S : MergeSplit α) : ℕ :=
  S.lowerPrimary.length + S.lowerSecondary.length

Total input size of the upper recursive call.

def rightSize (S : MergeSplit α) : ℕ :=
  S.upperPrimary.length + S.upperSecondary.length

Total size of the original two inputs.

def totalSize (S : MergeSplit α) : ℕ := S.xs.length + S.ys.length

The two recursive inputs partition every element except the one primary pivot. This exact accounting uses both the lawful midpoint and the lower-bound index bound.


theorem childSizes_add_one (S : MergeSplit α) :
    S.leftSize + S.rightSize + 1 = S.totalSize := by
  have hiLt : S.pivotIndex < S.primary.length := by
    simpa [pivotIndex] using S.pivotIndex_lt
  have hi : S.pivotIndex ≤ S.primary.length := Nat.le_of_lt hiLt
  have hj := S.splitIndex_le_secondary
  have hiSucc : S.pivotIndex + 1 ≤ S.primary.length := by omega
  have hprimarySub := Nat.sub_add_cancel hiSucc
  have hsecondarySub := Nat.sub_add_cancel hj
  simp only [leftSize, rightSize, lowerPrimary, lowerSecondary, upperPrimary,
    upperSecondary, List.length_take, List.length_drop]
  rw [Nat.min_eq_left hi, Nat.min_eq_left hj]
  simp only [totalSize]
  rw [← S.normalized_total]
  omega

Removing the primary pivot makes the lower recursive problem strictly smaller, independently of the search result.

theorem leftSize_lt (S : MergeSplit α) : S.leftSize < S.totalSize := by
  have h := S.childSizes_add_one
  omega

Removing the primary pivot makes the upper recursive problem strictly smaller, independently of the search result.

theorem rightSize_lt (S : MergeSplit α) : S.rightSize < S.totalSize := by
  have h := S.childSizes_add_one
  omega

end MergeSplit

Normalize two nonempty-total inputs and build the midpoint/lower-bound data for one P-MERGE recursive step.


def mergeSplit [LinearOrder α] (xs ys : List α)
    (htotal : 0 < xs.length + ys.length) : MergeSplit α := by
  by_cases hxy : xs.length < ys.length
  · have hypos : 0 < ys.length := by omega
    have hidx : ys.length / 2 < ys.length := Nat.div_lt_self hypos (by omega)
    let pivot := ys.get ⟨ys.length / 2, hidx⟩
    let search := binaryLowerBound xs pivot
    exact
      { xs := xs
        ys := ys
        primary := ys
        secondary := xs
        inputOrder := Or.inr ⟨rfl, rfl⟩
        secondary_length_le_primary := Nat.le_of_lt hxy
        total_positive := htotal
        normalized_total := by omega
        pivotIndex_lt := hidx
        pivot := pivot
        pivot_eq := rfl
        search := search
        search_eq := rfl
        search_index_le := by
          dsimp [search]
          exact binaryLowerBound_index_le_length xs pivot }
  · have hyx : ys.length ≤ xs.length := Nat.le_of_not_gt hxy
    have hxpos : 0 < xs.length := by omega
    have hidx : xs.length / 2 < xs.length := Nat.div_lt_self hxpos (by omega)
    let pivot := xs.get ⟨xs.length / 2, hidx⟩
    let search := binaryLowerBound ys pivot
    exact
      { xs := xs
        ys := ys
        primary := xs
        secondary := ys
        inputOrder := Or.inl ⟨rfl, rfl⟩
        secondary_length_le_primary := hyx
        total_positive := htotal
        normalized_total := rfl
        pivotIndex_lt := hidx
        pivot := pivot
        pivot_eq := rfl
        search := search
        search_eq := rfl
        search_index_le := by
          dsimp [search]
          exact binaryLowerBound_index_le_length ys pivot }

              @[simp] theorem mergeSplit_xs [LinearOrder α] (xs ys : List α)
    (htotal : 0 < xs.length + ys.length) : (mergeSplit xs ys htotal).xs = xs := by
  unfold mergeSplit
  split <;> rfl@[simp] theorem mergeSplit_ys [LinearOrder α] (xs ys : List α)
    (htotal : 0 < xs.length + ys.length) : (mergeSplit xs ys htotal).ys = ys := by
  unfold mergeSplit
  split <;> rflend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.Span.MapInvariance

CLRS Chapter 26.3 — Order-Embedding Cost Invariance

Strictly monotone key transformations preserve every comparison made by binary lower bound, P-MERGE, and P-MERGE-SORT. Consequently they preserve the attached work and span while mapping only the returned values.

              namespace CLRSnamespace Chapter27namespace ParallelMergeSortnamespace Costsnamespace Spanvariable [LinearOrder α] [LinearOrder β]

private theorem loop_map (f : α → β) (hf : StrictMono f)
    (xs : List α) (pivot : α) (lo hi : ℕ) :
    ParallelMerge.Internal.loop (xs.map f) (f pivot) lo hi =
      Costed.map id (ParallelMerge.Internal.loop xs pivot lo hi) := by
  induction lo, hi using ParallelMerge.Internal.loop.induct xs with
  | case1 lo hi hlt mid hnone =>
      rw [ParallelMerge.Internal.loop, ParallelMerge.Internal.loop]
      simp only [hlt, if_true, mid, List.getElem?_map,
        hnone, Option.map_none]
      rfl
  | case2 lo hi hlt mid x hget ihRight ihLeft =>
      rw [ParallelMerge.Internal.loop, ParallelMerge.Internal.loop]
      simp only [hlt, if_true, mid, List.getElem?_map,
        hget, Option.map_some, Costed.seq, Costed.charge, Costed.map]
      by_cases hx : x < pivot
      · have hfx : f x < f pivot := hf hx
        simp only [hx, hfx, if_true]
        rw [ihRight]
        rfl
      · have hfx : ¬ f x < f pivot := by
          intro hcontra
          exact hx (hf.lt_iff_lt.mp hcontra)
        simp only [hx, hfx, if_false]
        rw [ihLeft]
        rfl
  | case3 lo hi hnlt =>
      rw [ParallelMerge.Internal.loop, ParallelMerge.Internal.loop]
      simp [hnlt, Costed.pure, Costed.map]private theorem binaryLowerBound_map (f : α → β) (hf : StrictMono f)
    (xs : List α) (pivot : α) :
    binaryLowerBound (xs.map f) (f pivot) =
      Costed.map id (binaryLowerBound xs pivot) := by
  simpa [binaryLowerBound] using loop_map f hf xs pivot 0 xs.lengthprivate theorem mergeSplit_map_data (f : α → β) (hf : StrictMono f)
    (xs ys : List α) (htotal : 0 < xs.length + ys.length) :
    let S := mergeSplit xs ys htotal
    let T := mergeSplit (xs.map f) (ys.map f) (by simpa using htotal)
    T.search = Costed.map id S.search ∧
      T.lowerPrimary = S.lowerPrimary.map f ∧
      T.lowerSecondary = S.lowerSecondary.map f ∧
      T.upperPrimary = S.upperPrimary.map f ∧
      T.upperSecondary = S.upperSecondary.map f ∧
      T.pivot = f S.pivot := by
  dsimp only
  by_cases hxy : xs.length < ys.length
  · simp [mergeSplit, hxy, binaryLowerBound_map f hf,
      MergeSplit.lowerPrimary, MergeSplit.lowerSecondary,
      MergeSplit.upperPrimary, MergeSplit.upperSecondary,
      MergeSplit.pivotIndex, MergeSplit.splitIndex,
      List.map_take, List.map_drop]
  · simp [mergeSplit, hxy, binaryLowerBound_map f hf,
      MergeSplit.lowerPrimary, MergeSplit.lowerSecondary,
      MergeSplit.upperPrimary, MergeSplit.upperSecondary,
      MergeSplit.pivotIndex, MergeSplit.splitIndex,
      List.map_take, List.map_drop]

private theorem pMerge_map (f : α → β) (hf : StrictMono f) (n : ℕ) :
    ∀ (xs ys : List α), xs.length + ys.length = n →
      pMerge (xs.map f) (ys.map f) =
        Costed.map (List.map f) (pMerge xs ys) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs ys htotal
      by_cases hzero : xs.length + ys.length = 0
      · rw [pMerge, pMerge]
        simp [hzero, Costed.pure, Costed.map]
      · let S := mergeSplit xs ys (Nat.pos_of_ne_zero hzero)
        let T := mergeSplit (xs.map f) (ys.map f) (by
          simpa using (Nat.pos_of_ne_zero hzero))
        obtain ⟨hsearch, hlowerP, hlowerS, hupperP, hupperS, hpivot⟩ :=
          mergeSplit_map_data f hf xs ys (Nat.pos_of_ne_zero hzero)
        have hleft_lt : S.leftSize < n := by
          calc
            S.leftSize < S.totalSize := S.leftSize_lt
            _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have hright_lt : S.rightSize < n := by
          calc
            S.rightSize < S.totalSize := S.rightSize_lt
            _ = xs.length + ys.length := by simp [S, MergeSplit.totalSize]
            _ = n := htotal
        have ihlower := ih S.leftSize hleft_lt
          S.lowerPrimary S.lowerSecondary rfl
        have ihupper := ih S.rightSize hright_lt
          S.upperPrimary S.upperSecondary rfl
        rw [pMerge, pMerge]
        simp only [List.length_map, hzero]
        change Costed.seq T.search (fun _ =>
            Costed.seq
              (Costed.par (pMerge T.lowerPrimary T.lowerSecondary)
                (pMerge T.upperPrimary T.upperSecondary))
              (fun parts => Costed.charge 1 1
                (parts.1 ++ T.pivot :: parts.2))) =
          Costed.map (List.map f)
            (Costed.seq S.search (fun _ =>
              Costed.seq
                (Costed.par (pMerge S.lowerPrimary S.lowerSecondary)
                  (pMerge S.upperPrimary S.upperSecondary))
                (fun parts => Costed.charge 1 1
                  (parts.1 ++ S.pivot :: parts.2))))
        rw [hsearch, hlowerP, hlowerS, hupperP, hupperS, hpivot,
          ihlower, ihupper]
        simp [Costed.seq, Costed.par, Costed.charge, Costed.map, S]

P-MERGE-SORT's complete cost annotation is invariant under a strict order embedding; only its returned list is mapped.


theorem pMergeSort_map (f : α → β) (hf : StrictMono f) (n : ℕ) :
    ∀ (xs : List α), xs.length = n →
      pMergeSort (xs.map f) = Costed.map (List.map f) (pMergeSort xs) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs hlength
      by_cases hsmall : xs.length ≤ 1
      · rw [pMergeSort, pMergeSort]
        simp [hsmall, Costed.charge, Costed.map]
      · let mid := xs.length / 2
        let left := xs.take mid
        let right := xs.drop mid
        have hn : 2 ≤ n := by omega
        have hleft_lt : left.length < n := by
          simp [left, mid, hlength]
          omega
        have hright_lt : right.length < n := by
          simp [right, mid, hlength]
          omega
        have hleft := ih left.length hleft_lt left rfl
        have hright := ih right.length hright_lt right rfl
        have hmerge := pMerge_map f hf
          ((pMergeSort left).value.length + (pMergeSort right).value.length)
          (pMergeSort left).value (pMergeSort right).value rfl
        rw [pMergeSort, pMergeSort]
        simp only [List.length_map]
        simp only [hsmall]
        rw [← List.map_take, ← List.map_drop]
        change Costed.seq
            (Costed.par (pMergeSort (left.map f)) (pMergeSort (right.map f)))
            (fun sorted => pMerge sorted.1 sorted.2) =
          Costed.map (List.map f)
            (Costed.seq (Costed.par (pMergeSort left) (pMergeSort right))
              (fun sorted => pMerge sorted.1 sorted.2))
        rw [hleft, hright]
        simp only [Costed.seq, Costed.par, Costed.map]
        rw [hmerge]
        rfl

              end Spanend Costsend ParallelMergeSortend Chapter27end CLRS

CLRSLean.FourthEdition.Chapter_26.Section_26_2_4_Algorithms.ParallelMergeSort.Costs.Span.WitnessInput

CLRS Chapter 26.3 — Worst-Family P-MERGE-SORT Inputs

At each level the witness places all even keys in the left half and all odd keys in the right half. Recursive sorting therefore feeds the interleaved P-MERGE lower-bound family into the final merge.

namespace CLRSnamespace Chapter27

Power-of-two P-MERGE-SORT witness: recursively generated even keys occupy the left half and recursively generated odd keys occupy the right half.

def worstMergeSortInput : ℕ → List ℕ
  | 0 => [0]
  | k + 1 =>
      (worstMergeSortInput k).map (fun x => 2 * x) ++
        (worstMergeSortInput k).map (fun x => 2 * x + 1)

              @[simp] theorem worstMergeSortInput_length (k : ℕ) :
    (worstMergeSortInput k).length = 2 ^ k := by
  induction k with
  | zero => simp [worstMergeSortInput]
  | succ k ih =>
      simp [worstMergeSortInput, ih, pow_succ]
      omeganamespace ParallelMergeSortnamespace Costsnamespace Span

private theorem evenOddKeys_perm_range (n : ℕ) :
    (evenKeys n ++ oddKeys n).Perm (List.range (2 * n)) := by
  have heven : (evenKeys n).Nodup := by
    exact List.nodup_range.map (by
      intro a b h
      change 2 * a = 2 * b at h
      omega)
  have hodd : (oddKeys n).Nodup := by
    exact List.nodup_range.map (by
      intro a b h
      change 2 * a + 1 = 2 * b + 1 at h
      omega)
  have hdisjoint : List.Disjoint (evenKeys n) (oddKeys n) := by
    rw [List.disjoint_left]
    intro x hx hxo
    simp only [evenKeys, List.mem_map, List.mem_range] at hx
    simp only [oddKeys, List.mem_map, List.mem_range] at hxo
    omega
  apply (List.perm_ext_iff_of_nodup
    (heven.append hodd hdisjoint) List.nodup_range).2
  intro x
  simp only [List.mem_append, evenKeys, oddKeys, List.mem_map,
    List.mem_range]
  constructor
  · rintro (⟨i, hi, rfl⟩ | ⟨i, hi, rfl⟩) <;> omega
  · intro hx
    obtain ⟨i, hxi⟩ : ∃ i, x = 2 * i ∨ x = 2 * i + 1 := by
      exact ⟨x / 2, by omega⟩
    rcases hxi with hxi | hxi
    · left
      exact ⟨i, by omega, hxi.symm⟩
    · right
      exact ⟨i, by omega, hxi.symm⟩

The recursively generated witness contains exactly 0, ..., 2^k - 1.

theorem witness_perm_range (k : ℕ) :
    (worstMergeSortInput k).Perm (List.range (2 ^ k)) := by
  induction k with
  | zero => simp [worstMergeSortInput]
  | succ k ih =>
      have heven := ih.map (fun x => 2 * x)
      have hodd := ih.map (fun x => 2 * x + 1)
      have happ := heven.append hodd
      simpa [worstMergeSortInput, evenKeys, oddKeys, pow_succ,
        Nat.mul_comm] using happ.trans (evenOddKeys_perm_range (2 ^ k))

@[simp] theorem witness_take_half (k : ℕ) :
    (worstMergeSortInput (k + 1)).take (2 ^ k) =
      (worstMergeSortInput k).map (fun x => 2 * x) := by
  simp [worstMergeSortInput, worstMergeSortInput_length]

@[simp] theorem witness_drop_half (k : ℕ) :
    (worstMergeSortInput (k + 1)).drop (2 ^ k) =
      (worstMergeSortInput k).map (fun x => 2 * x + 1) := by
  simp [worstMergeSortInput, worstMergeSortInput_length]

Sorting the witness's even half produces the canonical even-key list.

theorem sorted_even_half (k : ℕ) :
    (pMergeSort ((worstMergeSortInput k).map (fun x => 2 * x))).value =
      evenKeys (2 ^ k) := by
  exact List.Perm.eq_of_pairwise' (r := (· ≤ ·))
    (pMergeSort_value_sorted _) (evenKeys_sorted _)
    ((pMergeSort_value_perm _).trans
      ((witness_perm_range k).map (fun x => 2 * x)))

Sorting the witness's odd half produces the canonical odd-key list.

theorem sorted_odd_half (k : ℕ) :
    (pMergeSort ((worstMergeSortInput k).map (fun x => 2 * x + 1))).value =
      oddKeys (2 ^ k) := by
  exact List.Perm.eq_of_pairwise' (r := (· ≤ ·))
    (pMergeSort_value_sorted _) (oddKeys_sorted _)
    ((pMergeSort_value_perm _).trans
      ((witness_perm_range k).map (fun x => 2 * x + 1)))

              end Spanend Costsend ParallelMergeSortend Chapter27end CLRS

26.3. Parallel Merge Sort

Formalized content

Definitions and proofs

CLRS Chapter 26 — Execution-Attached Work and Span

26.2–26.3. Parallel Recurrences

§26.2: Parallel matrix multiplication (P-MATMUL)

§26.3: Parallel merge (P-MERGE)

§26.3: Parallel merge sort (P-MERGE-SORT)

26.2–26.3. All-Input Bounds

All-input work and span bounds

CLRS Chapter 26.3 — Binary Lower-Bound Definitions

CLRS Chapter 26.3 — Executable P-MERGE

CLRS Chapter 26.3 — Binary Lower-Bound Correctness

Public theorems

CLRS Chapter 26.3 — Binary Lower-Bound Costs

Public theorems

CLRS Chapter 26.3 — P-MERGE Order Boundaries

CLRS Chapter 26.3 — P-MERGE Permutation Accounting

CLRS Chapter 26.3 — P-MERGE Correctness

Public theorems

CLRS Chapter 26.3 — P-MERGE Structural Cost Bounds

CLRS Chapter 26.3 — One P-MERGE Cost Step

CLRS Chapter 26.3 — P-MERGE Work Potential

CLRS Chapter 26.3 — P-MERGE Linear Work

Public theorems

CLRS Chapter 26.3 — A Three-Quarter Span Envelope

CLRS Chapter 26.3 — Pointwise P-MERGE Span Upper Bound

Public theorem

CLRS Chapter 26.3 — Interleaved P-MERGE Witness Lists

CLRS Chapter 26.3 — Interleaved Span Lower Witness

Public theorem

CLRS Chapter 26.3 — Executable P-MERGE-SORT

CLRS Chapter 26.3 — P-MERGE-SORT Specification

CLRS Chapter 26.3 — P-MERGE-SORT Correctness

Public theorems

CLRS Chapter 26.3 — P-MERGE-SORT Step Costs

CLRS Chapter 26.3 — P-MERGE-SORT Work Recurrence Links

CLRS Chapter 26.3 — Executable P-MERGE-SORT Work Bounds

Public theorems

CLRS Chapter 26.3 — Executable P-MERGE-SORT Span Upper Bound

Public theorem

CLRS Chapter 26.3 — P-MERGE-SORT Cubic-Log Span Witness

Public theorem

26.1 S1. Computation DAGs

Strands and computation DAGs

26.1 S2. Ready execution

Residual computation states

26.1 S3. Greedy accounting

Greedy-scheduler accounting

Greedy-schedule traces

Per-step greedy-schedule accounting

Concrete computation-DAG steps

Chained computation-DAG schedules

26.1 S4. Executable scheduler

26.1 S5. Spawn trees and parallel loops

Spawn trees

Parallel loops

CLRS Section 26.2 — Parallel Matrix Algorithms

CLRS Section 26.2 — Correctness of Parallel Matrix Algorithms

CLRS Section 26.2 — Exact Costs of Parallel Matrix Algorithms

P-ADD costs

P-MATMUL execution costs

CLRS Section 26.2 — Matrix Execution Cost Equalities

CLRS Section 26.2 — Monotonicity of Matrix Execution Costs

Small base values

P-ADD

P-MATMUL

CLRS Section 26.2 — Matrix Costs at Powers of Two

P-ADD exact powers

P-MATMUL exact powers

Exact-power asymptotics

CLRS Section 26.2 — All-Input Matrix Asymptotics

Chapter 26 extension — parallel Strassen recurrences: definitions

Chapter 26 extension — parallel Strassen recurrences: monotonicity

Chapter 26 extension — parallel Strassen recurrences: all-input bounds

CLRS Chapter 26.3 — P-MERGE Split Data

CLRS Chapter 26.3 — Order-Embedding Cost Invariance

CLRS Chapter 26.3 — Worst-Family P-MERGE-SORT Inputs