Imports

import CLRSLean.Chapter_04.Section_04_2_Strassen_Algorithm

4.1. Multiplying Square Matrices

This section formalizes the naive square-matrix-multiplication algorithm of CLRS §4.1 (fourth edition). On the depth-indexed power-of-two squares CLRS.Chapter04.SqMat it defines the recursive eight-product SQUARE-MATRIX-MULTIPLY-RECURSIVE, proves it computes the ordinary matrix product at every depth, and shows the work recurrence T(n) = 8 T(⌊n/2⌋) + n² is Θ(n³) by Master-theorem case 1.

The representation and Master-theorem infrastructure are shared with §4.2 (Section_04_2_Strassen_Algorithm), where SqMat R k is a 2^k × 2^k block matrix and the recursive runtime analysis discharges the floor/ceiling Master-theorem case 1 wrapper.

The companion MatrixExecution module, exported by the chapter guide, computes both value and scalar work in one recursion. Its MatrixExecution.mulWithCost_work_eq identifies that count with this budget on side lengths 2^k, and MatrixExecution.mulWithCost_theta proves cubic scalar work for arbitrary input families. padOne is only a one-level embedding of a power-of-two square.

Main results:

Definition mulRec: the recursive eight-product multiplication on SqMat (CLRS SQUARE-MATRIX-MULTIPLY-RECURSIVE).
Theorem mulRec_correct: mulRec R k A B = A * B at every depth.
Theorem mulRec_padOne_corner: zero-padding into the next power of two preserves the top-left product.
Theorem mul_runtime_bigTheta: the work recurrence T(n) = 8 T(⌊n/2⌋) + n² is Θ(n^(log₂ 8)).
Theorem realLogScale_eight_two: the comparison scale at a = 8, b = 2 is the polynomial n³, so the runtime bound is exactly Θ(n³).

Notation conventions used in this section:

R : the scalar ring
SqMat R k : a 2^k × 2^k square matrix over R
mulWork, T : the recursive work/cost function

namespace CLRSnamespace Chapter04

The naive 2 × 2 block product

section Naive2variable {S : Type*} [Ring S]

The naive 2 × 2 block product (the combine step of the recursive algorithm): each output block is the sum of two block products, eight in total. This is the straightforward SQUARE-MATRIX-MULTIPLY block arithmetic that Strassen's seven products optimize away.

def mul2 (M N : Matrix (Fin 2) (Fin 2) S) : Matrix (Fin 2) (Fin 2) S :=
  !![M 0 0 * N 0 0 + M 0 1 * N 1 0, M 0 0 * N 0 1 + M 0 1 * N 1 1;
     M 1 0 * N 0 0 + M 1 1 * N 1 0, M 1 0 * N 0 1 + M 1 1 * N 1 1]

The naive block product computes the ordinary 2 × 2 matrix product.

theorem mul2_eq_mul (M N : Matrix (Fin 2) (Fin 2) S) : mul2 M N = M * N := by
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [mul2, Matrix.mul_apply, Fin.sum_univ_two]

end Naive2

Recursive naive multiplication on power-of-two squares

The recursive SQUARE-MATRIX-MULTIPLY-RECURSIVE algorithm. mulRec R 0 is the scalar base case (conventional multiplication); mulRec R (k+1) partitions both factors into four depth-k blocks and forms the eight recursive block products (CLRS §4.1): each output block is the sum of two of them.

def mulRec (R : Type u) [Ring R] : ∀ k, SqMat R k → SqMat R k → SqMat R k
  | 0, x, y => x * y
  | (k + 1), A, B =>
      !![mulRec R k (A 0 0) (B 0 0) + mulRec R k (A 0 1) (B 1 0),
         mulRec R k (A 0 0) (B 0 1) + mulRec R k (A 0 1) (B 1 1);
         mulRec R k (A 1 0) (B 0 0) + mulRec R k (A 1 1) (B 1 0),
         mulRec R k (A 1 0) (B 0 1) + mulRec R k (A 1 1) (B 1 1)]

Correctness of the recursive naive multiplication: at every depth it returns the ordinary matrix product A * B. The proof is induction on depth; each step rewrites the eight recursive products by the induction hypothesis and then applies the 2 × 2 identity CLRS.Chapter04.mul2_eq_mul.


theorem mulRec_eq_mul (R : Type u) [Ring R] :
    ∀ (k : ℕ) (A B : SqMat R k), mulRec R k A B = A * B
  | 0, x, y => rfl
  | (k + 1), A, B => by
      have IH : ∀ X Y : SqMat R k, mulRec R k X Y = X * Y := mulRec_eq_mul R k
      have hstep : mulRec R (k + 1) A B = mul2 A B := by
        simp only [mulRec, mul2, IH]
      rw [hstep]
      exact mul2_eq_mul A B

Reader-facing correctness theorem for the recursive algorithm: on a 2^k × 2^k square, CLRS.Chapter04.mulRec produces the true matrix product.

theorem mulRec_correct (R : Type u) [Ring R] (k : ℕ) (A B : SqMat R k) :
    mulRec R k A B = A * B :=
  mulRec_eq_mul R k A B

Running the recursive naive multiplication on two zero-padded inputs recovers the padded product: padding to the next power of two does not change the meaningful top-left product. This composes CLRS.Chapter04.mulRec_correct with CLRS.Chapter04.padOne_mul.


theorem mulRec_padOne (R : Type u) [Ring R] (k : ℕ) (x y : SqMat R k) :
    mulRec R (k + 1) (padOne R k x) (padOne R k y) = padOne R k (x * y) := by
  rw [mulRec_correct, padOne_mul]

Extracting the corner after a padded naive multiplication returns the original product x * y.


theorem mulRec_padOne_corner (R : Type u) [Ring R] (k : ℕ) (x y : SqMat R k) :
    (mulRec R (k + 1) (padOne R k x) (padOne R k y)) 0 0 = x * y := by
  rw [mulRec_padOne]
  show (!![x * y, 0; 0, 0] : Matrix (Fin 2) (Fin 2) (SqMat R k)) 0 0 = x * y
  simp

Runtime: `T(n) = 8 T(⌊n/2⌋) + n²` is `Θ(n³)`

The naive work recurrence T(n) = 8 T(⌊n/2⌋) + n²: eight recursive subproblems of half size plus quadratic block-combination work, with base value T(0) = 0. This is the CLRS cost recurrence whose solution is the running time of CLRS.Chapter04.mulRec.

noncomputable def mulWork : ℕ → ℝ
  | 0 => 0
  | (n + 1) => 8 * mulWork ((n + 1) / 2) + ((n + 1 : ℕ) : ℝ) ^ 2
  decreasing_by exact Nat.div_lt_self (Nat.succ_pos n) (by norm_num)

Base value of the work recurrence.


theorem mulWork_zero : mulWork 0 = 0 := by
  rw [mulWork]

One recursion step of the work recurrence at a successor argument.


theorem mulWork_succ (n : ℕ) :
    mulWork (n + 1) = 8 * mulWork ((n + 1) / 2) + ((n + 1 : ℕ) : ℝ) ^ 2 := by
  rw [mulWork]

One recursion step of the work recurrence at any positive argument.

theorem mulWork_pos_step (n : ℕ) (hn : 0 < n) :
    mulWork n = 8 * mulWork (n / 2) + ((n : ℕ) : ℝ) ^ 2 := by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'
  exact mulWork_succ m

The forcing term f(n) = T(n) - 8 T(⌊n/2⌋) of the recurrence. Choosing f as this defect makes the CLRS floor recurrence T(n) = 8 T(⌊n/2⌋) + f(n) hold definitionally at every input.

noncomputable def mulForcing (n : ℕ) : ℝ :=
  mulWork n - 8 * mulWork (n / 2)

The work function satisfies the Chapter 4 floor-division Master recurrence with a = 8, b = 2.

theorem mulWork_floorRec :
    FloorDivideRecurrence 8 2 mulForcing mulWork := by
  refine ⟨fun n => ?_⟩
  simp only [mulForcing]
  push_cast
  ring

The work function is nonnegative.


theorem mulWork_nonneg : ∀ n, 0 ≤ mulWork n := by
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    rcases Nat.eq_zero_or_pos n with hn | hn
    · subst hn; simp [mulWork_zero]
    · rw [mulWork_pos_step n hn]
      have hlt : n / 2 < n := Nat.div_lt_self hn (by norm_num)
      have hrec := ih (n / 2) hlt
      nlinarith [hrec, sq_nonneg ((n : ℕ) : ℝ)]

The work function is nondecreasing across one step.


theorem mulWork_le_succ : ∀ n, mulWork n ≤ mulWork (n + 1) := by
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    rcases Nat.eq_zero_or_pos n with hn | hn
    · subst hn; rw [mulWork_zero]; exact mulWork_nonneg _
    · rw [mulWork_pos_step n hn, mulWork_pos_step (n + 1) (Nat.succ_pos n)]
      have hcast : ((n : ℕ) : ℝ) ^ 2 ≤ ((n + 1 : ℕ) : ℝ) ^ 2 := by
        have h1 : ((n : ℕ) : ℝ) ≤ ((n + 1 : ℕ) : ℝ) := by push_cast; linarith
        have hn_nonneg : (0 : ℝ) ≤ (n : ℕ) := Nat.cast_nonneg _
        nlinarith [hn_nonneg, h1]
      rcases (by omega : (n + 1) / 2 = n / 2 ∨ (n + 1) / 2 = n / 2 + 1) with h | h
      · rw [h]; linarith [hcast]
      · rw [h]
        have hj : n / 2 < n := Nat.div_lt_self hn (by norm_num)
        have hstep := ih (n / 2) hj
        linarith [hstep, hcast]

The work function is monotone.

theorem mulWork_monotone : Monotone mulWork :=
  monotone_nat_of_le_succ mulWork_le_succ

The work function satisfies the absolute-value monotonicity interface.


theorem mulWork_monotoneAbs : MonotoneAbs mulWork := by
  intro m n hmn
  rw [abs_of_nonneg (mulWork_nonneg m), abs_of_nonneg (mulWork_nonneg n)]
  exact mulWork_monotone hmn

The normalized forcing on exact powers is the convergent geometric sequence (1/2)^(k+1): on n = 2^(k+1) the forcing is exactly the block-work (2^(k+1))² = 4^(k+1), so dividing by 8^(k+1) gives (4/8)^(k+1) = (1/2)^(k+1). This is what places the naive recurrence in Master case 1 (the forcing n² is polynomially smaller than the critical n^(log₂ 8) = n³).


theorem mul_normForcing (k : ℕ) :
    normalizedForcing 8 2 mulForcing k = (1 / 2 : ℝ) ^ (k + 1) := by
  have hpos : 0 < 2 ^ (k + 1) := pow_pos (by norm_num) _
  have hdiv : 2 ^ (k + 1) / 2 = 2 ^ k := by rw [pow_succ]; omega
  have hcast : ((2 ^ (k + 1) : ℕ) : ℝ) ^ 2 = (4 : ℝ) ^ (k + 1) := by
    push_cast
    rw [show (4 : ℝ) = 2 ^ 2 by norm_num, ← pow_mul, ← pow_mul, Nat.mul_comm 2 (k + 1)]
  have hforcing : mulForcing (2 ^ (k + 1)) = (4 : ℝ) ^ (k + 1) := by
    unfold mulForcing
    rw [mulWork_pos_step (2 ^ (k + 1)) hpos, hdiv]
    linarith [hcast]
  unfold normalizedForcing
  rw [hforcing, ← div_pow]
  norm_num

Case-1 hypothesis: the normalized forcing is nonnegative.


theorem mul_term_nonneg (k : ℕ) : 0 ≤ normalizedForcing 8 2 mulForcing k := by
  rw [mul_normForcing]; positivity

Case-1 hypothesis: the normalized forcing is bounded by a geometric sequence.


theorem mul_term_upper (k : ℕ) :
    normalizedForcing 8 2 mulForcing k ≤ (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ k := by
  rw [mul_normForcing, pow_succ]
  exact le_of_eq (mul_comm _ _)

Value of the work recurrence at the base input 1.


theorem mulWork_one : mulWork 1 = 1 := by
  rw [show (1 : ℕ) = 0 + 1 from rfl, mulWork_succ]
  norm_num [mulWork_zero]

Positivity of the normalized base value, a case-1 hypothesis.

theorem mul_base_pos : 0 < normalizedValue 8 2 mulWork 0 := by
  unfold normalizedValue
  norm_num [mulWork_one]

Runtime of the naive matrix-multiplication algorithm. The recurrence T(n) = 8 T(⌊n/2⌋) + n² is Θ(n^(log₂ 8)). This is the CLRS Θ(n³) bound, obtained by discharging Master-theorem case 1 (the forcing n² is polynomially smaller than the critical n^(log₂ 8)) through the Chapter 4 wrapper CLRS.Chapter04.floorDivide_allInput_masterCase1_realLogScale.

theorem mul_runtime_bigTheta :
    Chapter03.isBigTheta mulWork (realLogScale 8 2) :=
  floorDivide_allInput_masterCase1_realLogScale 8 2 mulForcing mulWork
    mulWork_floorRec (by norm_num) (by norm_num) mulWork_monotoneAbs
    mul_base_pos mul_term_nonneg (r := 1 / 2) (C := 1 / 2)
    (by norm_num) (by norm_num) (by norm_num) mul_term_upper

The comparison scale CLRS.Chapter04.realLogScale at a = 8, b = 2 is the polynomial n³, since log₂ 8 = 3. So CLRS.Chapter04.mul_runtime_bigTheta is exactly the CLRS Θ(n³) statement.

Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
theorem realLogScale_eight_two (n : ℕ) :
    realLogScale 8 2 n = (n : ℝ) ^ 3 := by
  rw [realLogScale, realLogExponent]
  have h : Real.log (((8 : ℕ) : ℝ)) / Real.log (((2 : ℕ) : ℝ)) = 3 := by
    rw [show (((8 : ℕ) : ℝ)) = (2 : ℝ) ^ 3 by norm_num, Real.log_pow]
    have hlog : Real.log (2 : ℝ) ≠ 0 := by
      exact Real.log_ne_zero.mpr ⟨by norm_num, by norm_num, by norm_num⟩
    field_simp [hlog]
    Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
  rw [h]
  simp

end Chapter04end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_04.MatrixExecution.Asymptotics

Asymptotic scalar work on power-of-two squares

The functions below read counters from arbitrary families of input matrices. The asymptotic variable is depth k; the comparison functions use their actual side length 2^k. Consequently these statements do not extend the input type to all natural dimensions.

              namespace CLRS.Chapter04.MatrixExecution

private theorem cubic_side (k : Nat) : ((2 ^ k : Nat) : ℝ) ^ 3 = (8 : ℝ) ^ k := by
  rw [Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, Nat.mul_comm k 3, pow_mul]
  norm_num

private theorem strassen_side (k : Nat) :
    ((2 ^ k : Nat) : ℝ) ^ Real.logb 2 7 = (7 : ℝ) ^ k := by
  rw [Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_pow_comm (by norm_num)]
  rw [Real.rpow_logb (by norm_num) (by norm_num) (by norm_num)]

Every input family has cubic scalar work in its power-of-two side length.


theorem mulWithCost_theta (R : Type u) [Ring R] (A B : ∀ k, SqMat R k) :
    Chapter03.isBigTheta (fun k => ((mulWithCost R k (A k) (B k)).work : ℝ))
      (fun k => ((2 ^ k : Nat) : ℝ) ^ 3) := by
  constructor
  · rw [Chapter03.isBigO_iff]
    refine ⟨2, by norm_num, 0, ?_⟩
    intro k _
    rw [mulWithCost_work, cubic_side, abs_of_nonneg (by positivity),
      abs_of_nonneg (by positivity)]
    exact_mod_cast (mulCount_bounds k).2
  · rw [Chapter03.isBigOmega_iff]
    refine ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [mulWithCost_work, cubic_side, abs_of_nonneg (by positivity),
      abs_of_nonneg (by positivity), one_mul]
    exact_mod_cast (mulCount_bounds k).1

Every input family has Strassen's scalar-work exponent on its side length.


theorem strassenWithCost_theta (R : Type u) [Ring R] (A B : ∀ k, SqMat R k) :
    Chapter03.isBigTheta (fun k => ((strassenWithCost R k (A k) (B k)).work : ℝ))
      (fun k => ((2 ^ k : Nat) : ℝ) ^ Real.logb 2 7) := by
  constructor
  · rw [Chapter03.isBigO_iff]
    refine ⟨7, by norm_num, 0, ?_⟩
    intro k _
    rw [strassenWithCost_work, strassen_side, abs_of_nonneg (by positivity),
      abs_of_nonneg (by positivity)]
    exact_mod_cast (strassenCount_bounds k).2
  · rw [Chapter03.isBigOmega_iff]
    refine ⟨1, by norm_num, 0, ?_⟩
    intro k _
    rw [strassenWithCost_work, strassen_side, abs_of_nonneg (by positivity),
      abs_of_nonneg (by positivity), one_mul]
    exact_mod_cast (strassenCount_bounds k).1

end CLRS.Chapter04.MatrixExecution

CLRSLean.FourthEdition.Chapter_04.MatrixExecution.Algorithms

Matrix multiplication with scalar work

Both algorithms obtain their value and work from the same recursion. Every matrix sum/difference is itself evaluated by the counted leaf traversal. Strassen's seven product results are shared; each result is computed and charged once, even when it contributes to more than one output block.

namespace CLRS.Chapter04.MatrixExecution

Eight recursive products and four counted output-block sums.

def mulWithCost (R : Type u) [Ring R] :
    ∀ k, SqMat R k → SqMat R k → Result R k
  | 0, x, y => ⟨x * y, 1⟩
  | k + 1, A, B =>
      let p1 := mulWithCost R k (A 0 0) (B 0 0)
      let p2 := mulWithCost R k (A 0 1) (B 1 0)
      let p3 := mulWithCost R k (A 0 0) (B 0 1)
      let p4 := mulWithCost R k (A 0 1) (B 1 1)
      let p5 := mulWithCost R k (A 1 0) (B 0 0)
      let p6 := mulWithCost R k (A 1 1) (B 1 0)
      let p7 := mulWithCost R k (A 1 0) (B 0 1)
      let p8 := mulWithCost R k (A 1 1) (B 1 1)
      let c11 := zipWithCost R (· + ·) k p1.value p2.value
      let c12 := zipWithCost R (· + ·) k p3.value p4.value
      let c21 := zipWithCost R (· + ·) k p5.value p6.value
      let c22 := zipWithCost R (· + ·) k p7.value p8.value
      ⟨!![c11.value, c12.value; c21.value, c22.value],
        p1.work + p2.work + p3.work + p4.work + p5.work + p6.work + p7.work + p8.work +
        c11.work + c12.work + c21.work + c22.work⟩

Strassen with all ten preparation and eight reassembly sums/differences counted.

def strassenWithCost (R : Type u) [Ring R] :
    ∀ k, SqMat R k → SqMat R k → Result R k
  | 0, x, y => ⟨x * y, 1⟩
  | k + 1, A, B =>
      let t1 := zipWithCost R (· - ·) k (B 0 1) (B 1 1)
      let t2 := zipWithCost R (· + ·) k (A 0 0) (A 0 1)
      let t3 := zipWithCost R (· + ·) k (A 1 0) (A 1 1)
      let t4 := zipWithCost R (· - ·) k (B 1 0) (B 0 0)
      let t5 := zipWithCost R (· + ·) k (A 0 0) (A 1 1)
      let t6 := zipWithCost R (· + ·) k (B 0 0) (B 1 1)
      let t7 := zipWithCost R (· - ·) k (A 0 1) (A 1 1)
      let t8 := zipWithCost R (· + ·) k (B 1 0) (B 1 1)
      let t9 := zipWithCost R (· - ·) k (A 0 0) (A 1 0)
      let t10 := zipWithCost R (· + ·) k (B 0 0) (B 0 1)
      let p1 := strassenWithCost R k (A 0 0) t1.value
      let p2 := strassenWithCost R k t2.value (B 1 1)
      let p3 := strassenWithCost R k t3.value (B 0 0)
      let p4 := strassenWithCost R k (A 1 1) t4.value
      let p5 := strassenWithCost R k t5.value t6.value
      let p6 := strassenWithCost R k t7.value t8.value
      let p7 := strassenWithCost R k t9.value t10.value
      let c11a := zipWithCost R (· + ·) k p5.value p4.value
      let c11b := zipWithCost R (· - ·) k c11a.value p2.value
      let c11 := zipWithCost R (· + ·) k c11b.value p6.value
      let c12 := zipWithCost R (· + ·) k p1.value p2.value
      let c21 := zipWithCost R (· + ·) k p3.value p4.value
      let c22a := zipWithCost R (· + ·) k p5.value p1.value
      let c22b := zipWithCost R (· - ·) k c22a.value p3.value
      let c22 := zipWithCost R (· - ·) k c22b.value p7.value
      ⟨!![c11.value, c12.value; c21.value, c22.value],
        t1.work + t2.work + t3.work + t4.work + t5.work + t6.work + t7.work + t8.work +
        t9.work + t10.work + p1.work + p2.work + p3.work + p4.work + p5.work + p6.work +
        p7.work + c11a.work + c11b.work + c11.work + c12.work + c21.work + c22a.work +
        c22b.work + c22.work⟩

Erasing work recovers the existing eight-product algorithm.

theorem mulWithCost_value (R : Type u) [Ring R] :
    ∀ (k : Nat) (A B : SqMat R k), (mulWithCost R k A B).value = mulRec R k A B := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      simp only [mulWithCost, addWithCost_value, ih, mulRec]

Erasing work recovers the existing seven-product algorithm.

theorem strassenWithCost_value (R : Type u) [Ring R] :
    ∀ (k : Nat) (A B : SqMat R k),
      (strassenWithCost R k A B).value = strassenRec R k A B := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      simp only [strassenWithCost, addWithCost_value, subWithCost_value, ih, strassenRec]

Depth recurrence proved below to be the eight-product execution's work.

def mulCount : Nat → Nat
  | 0 => 1
  | k + 1 => 8 * mulCount k + 4 * 4 ^ k

Depth recurrence including Strassen's eighteen block sums/differences.

def strassenCount : Nat → Nat
  | 0 => 1
  | k + 1 => 7 * strassenCount k + 18 * 4 ^ k

              theorem mulWithCost_work (R : Type u) [Ring R] :
    ∀ (k : Nat) (A B : SqMat R k), (mulWithCost R k A B).work = mulCount k := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      simp only [mulWithCost, zipWithCost_work, ih, mulCount]
      omegatheorem strassenWithCost_work (R : Type u) [Ring R] :
    ∀ (k : Nat) (A B : SqMat R k),
      (strassenWithCost R k A B).work = strassenCount k := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      simp only [strassenWithCost, zipWithCost_work, ih, strassenCount]
      omegaend CLRS.Chapter04.MatrixExecution

CLRSLean.FourthEdition.Chapter_04.MatrixExecution.Basic

Scalar-operation execution for block matrices

The counter charges one scalar addition, subtraction, or multiplication. Matrix addition/subtraction visits all four child blocks recursively; it is not charged as one scalar operation. Indexing, immutable representation, allocation, and forming the four output blocks are outside this arithmetic model. Local results are shared when a later expression uses them more than once.

namespace CLRS.Chapter04.MatrixExecution

A returned matrix and the scalar arithmetic operations used to obtain it.

structure Result (R : Type u) (k : Nat) where
  value : SqMat R k
  work : Nat

Apply one scalar operation at every corresponding pair of leaves.

def zipWithCost (R : Type u) (op : R → R → R) :
    ∀ k, SqMat R k → SqMat R k → Result R k
  | 0, x, y => ⟨op x y, 1⟩
  | k + 1, A, B =>
      let a := zipWithCost R op k (A 0 0) (B 0 0)
      let b := zipWithCost R op k (A 0 1) (B 0 1)
      let c := zipWithCost R op k (A 1 0) (B 1 0)
      let d := zipWithCost R op k (A 1 1) (B 1 1)
      ⟨!![a.value, b.value; c.value, d.value], a.work + b.work + c.work + d.work⟩

The count comes from visiting the scalar leaves of the returned matrix.

theorem zipWithCost_work (R : Type u) (op : R → R → R) :
    ∀ (k : Nat) (A B : SqMat R k), (zipWithCost R op k A B).work = 4 ^ k := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      simp only [zipWithCost, ih, pow_succ]
      omega

              theorem addWithCost_value (R : Type u) [Ring R] :
    ∀ (k : Nat) (A B : SqMat R k),
      (zipWithCost R (· + ·) k A B).value = A + B := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      funext i j
      fin_cases i <;> fin_cases j <;> simp [zipWithCost, ih] <;> rfltheorem subWithCost_value (R : Type u) [Ring R] :
    ∀ (k : Nat) (A B : SqMat R k),
      (zipWithCost R (· - ·) k A B).value = A - B := by
  intro k
  induction k with
  | zero => intros; rfl
  | succ k ih =>
      intro A B
      funext i j
      fin_cases i <;> fin_cases j <;> simp [zipWithCost, ih] <;> rflend CLRS.Chapter04.MatrixExecution

CLRSLean.FourthEdition.Chapter_04.MatrixExecution.Bounds

Bounds for executed scalar arithmetic

These results concern matrices of side length 2^k. The eight-product counter equals the existing work recurrence on that domain. Strassen's eighteen block sums give a different exact count, bounded by constant multiples of the existing recurrence. Neither result claims an arbitrary-dimension padding API or a machine-time bound for ring operations of nonconstant cost.

              namespace CLRS.Chapter04.MatrixExecution

private theorem side_square (k : Nat) : ((2 ^ k : Nat) : ℝ) ^ 2 = (4 ^ k : Nat) := by
  norm_cast
  rw [← pow_mul, Nat.mul_comm k 2, pow_mul]
  norm_num

theorem mulCount_eq_budget (k : Nat) : (mulCount k : ℝ) = mulWork (2 ^ k) := by
  induction k with
  | zero => simp [mulCount, mulWork_one]
  | succ k ih =>
      rw [mulCount, Nat.cast_add, Nat.cast_mul, ih,
        mulWork_pos_step (2 ^ (k + 1)) (by positivity)]
      have hdiv : 2 ^ (k + 1) / 2 = 2 ^ k := by rw [pow_succ]; omega
      rw [hdiv, side_square]
      simp only [pow_succ 4 k,
        Nat.cast_mul, Nat.cast_ofNat]
      norm_num
      ring

theorem strassenCount_budget_bounds (k : Nat) :
    strassenWork (2 ^ k) ≤ (strassenCount k : ℝ) ∧
      (strassenCount k : ℝ) ≤ 5 * strassenWork (2 ^ k) := by
  induction k with
  | zero => norm_num [strassenCount, strassenWork_one]
  | succ k ih =>
      rw [strassenCount, Nat.cast_add, Nat.cast_mul,
        strassenWork_pos_step (2 ^ (k + 1)) (by positivity)]
      have hdiv : 2 ^ (k + 1) / 2 = 2 ^ k := by rw [pow_succ]; omega
      rw [hdiv, side_square]
      simp only [pow_succ 4 k,
        Nat.cast_mul, Nat.cast_ofNat]
      have hnonneg : (0 : ℝ) ≤ (4 ^ k : Nat) := by positivity
      constructor <;> nlinarith [ih.1, ih.2]

Equality with the budget is proved from the returned execution counter.


theorem mulWithCost_work_eq (R : Type u) [Ring R] (k : Nat) (A B : SqMat R k) :
    ((mulWithCost R k A B).work : ℝ) = mulWork (2 ^ k) := by
  rw [mulWithCost_work, mulCount_eq_budget]

Strassen's actual arithmetic count is within a factor of five of the budget.


theorem strassenWithCost_work_bounds (R : Type u) [Ring R]
    (k : Nat) (A B : SqMat R k) :
    strassenWork (2 ^ k) ≤ ((strassenWithCost R k A B).work : ℝ) ∧
      ((strassenWithCost R k A B).work : ℝ) ≤ 5 * strassenWork (2 ^ k) := by
  rw [strassenWithCost_work]
  exact strassenCount_budget_bounds k

              theorem mulCount_closed (k : Nat) : mulCount k + 4 ^ k = 2 * 8 ^ k := by
  induction k with
  | zero => norm_num [mulCount]
  | succ k ih => simp only [mulCount, pow_succ]; omegatheorem strassenCount_closed (k : Nat) : strassenCount k + 6 * 4 ^ k = 7 * 7 ^ k := by
  induction k with
  | zero => norm_num [strassenCount]
  | succ k ih => simp only [strassenCount, pow_succ]; omega

theorem mulCount_bounds (k : Nat) : 8 ^ k ≤ mulCount k ∧ mulCount k ≤ 2 * 8 ^ k := by
  have h := mulCount_closed k
  have hpow : 4 ^ k ≤ 8 ^ k := Nat.pow_le_pow_left (by norm_num) k
  have hnonneg := Nat.zero_le (4 ^ k)
  omega

theorem strassenCount_bounds (k : Nat) :
    7 ^ k ≤ strassenCount k ∧ strassenCount k ≤ 7 * 7 ^ k := by
  have h := strassenCount_closed k
  have hpow : 4 ^ k ≤ 7 ^ k := Nat.pow_le_pow_left (by norm_num) k
  omega

Value correctness and work for the same eight-product run.


theorem mulWithCost_correct (R : Type u) [Ring R] (k : Nat) (A B : SqMat R k) :
    (mulWithCost R k A B).value = A * B ∧
      ((mulWithCost R k A B).work : ℝ) = mulWork (2 ^ k) :=
  ⟨by rw [mulWithCost_value, mulRec_correct], mulWithCost_work_eq R k A B⟩

Value correctness and work bounds for the same seven-product run.


theorem strassenWithCost_correct (R : Type u) [Ring R] (k : Nat) (A B : SqMat R k) :
    (strassenWithCost R k A B).value = A * B ∧
      strassenWork (2 ^ k) ≤ ((strassenWithCost R k A B).work : ℝ) ∧
      ((strassenWithCost R k A B).work : ℝ) ≤ 5 * strassenWork (2 ^ k) :=
  ⟨by rw [strassenWithCost_value, strassenRec_correct], strassenWithCost_work_bounds R k A B⟩

end CLRS.Chapter04.MatrixExecution

CLRSLean.FourthEdition.Chapter_04.Section_04_2_Strassen_Algorithm

Zero-padded factors multiply block-diagonally: the top-left corner of the product of two padded matrices is the product of the two originals, with the rest still zero.

theorem padOne_mul (R : Type u) [Ring R] (k : ℕ) (x y : SqMat R k) :
    padOne R k x * padOne R k y = padOne R k (x * y) := by
  show (!![x, 0; 0, 0] : Matrix (Fin 2) (Fin 2) (SqMat R k)) * !![y, 0; 0, 0]
      = !![x * y, 0; 0, 0]
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [Matrix.mul_apply, Fin.sum_univ_two]

CLRSLean.Chapter_04.Section_04_6_Master_Theorem_All_Input

The real-log comparison scale n^(log_b a). This is the textbook scale used in the standard CLRS statement of the Master theorem: the homogeneous-solution growth rate without floors and ceilings.

For integer exponents it coincides with the ordinary polynomial scale polynomialScale.

noncomputable def realLogScale (a b : ℕ) (n : ℕ) : ℝ :=
  (n : ℝ) ^ (realLogExponent a b)

Floor-division all-input Master case 1 stated in the textbook real-log scale n^(log_b a).

theorem floorDivide_allInput_masterCase1_realLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (realLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (floorDivide_allInput_masterCase1_criticalPowerScale a b f T h_rec
      ha hb hT_mono h_base_pos h_term_nonneg hr_nonneg hr_lt_one hC_pos
      h_term_upper)
    (criticalPowerScale_isBigTheta_realLogScale a b ha hb)