structure Hex.Matrix.Winograd {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] (A₁₁ A₁₂ A₂₁ A₂₂ : Matrix R n m) (B₁₁ B₁₂ B₂₁ B₂₂ : Matrix R m k) : Type u

The Winograd seven-product schedule over eight blocks of a 2×2 product.

The eight base blocks are the structure parameters; the fifteen operand and result sums S₁…S₄, T₁…T₄, U₁…U₇ and the seven products P₁…P₇ are fields, each pinned to the schedule by a defining equation. A consumer (the mulStrassen correctness proof) instantiates the fields with its recursively-computed intermediates and discharges the equations, then reads off the four output-block identities c11, c12, c21, c22.

• S₁ : Matrix R n m

  S₁ = A₂₁ + A₂₂.

• S₂ : Matrix R n m

  S₂ = S₁ − A₁₁.

• S₃ : Matrix R n m

  S₃ = A₁₁ − A₂₁.

• S₄ : Matrix R n m

  S₄ = A₁₂ − S₂.

• T₁ : Matrix R m k

  T₁ = B₁₂ − B₁₁.

• T₂ : Matrix R m k

  T₂ = B₂₂ − T₁.

• T₃ : Matrix R m k

  T₃ = B₂₂ − B₁₂.

• T₄ : Matrix R m k

  T₄ = T₂ − B₂₁.

• P₁ : Matrix R n k

  P₁ = A₁₁ · B₁₁.

• P₂ : Matrix R n k

  P₂ = A₁₂ · B₂₁.

• P₃ : Matrix R n k

  P₃ = S₄ · B₂₂.

• P₄ : Matrix R n k

  P₄ = A₂₂ · T₄.

• P₅ : Matrix R n k

  P₅ = S₁ · T₁.

• P₆ : Matrix R n k

  P₆ = S₂ · T₂.

• P₇ : Matrix R n k

  P₇ = S₃ · T₃.

• U₁ : Matrix R n k

  U₁ = P₁ + P₂ (output block C₁₁).

• U₂ : Matrix R n k

  U₂ = P₁ + P₆.

• U₃ : Matrix R n k

  U₃ = U₂ + P₇.

• U₄ : Matrix R n k

  U₄ = U₂ + P₅.

• U₅ : Matrix R n k

  U₅ = U₄ + P₃ (output block C₁₂).

• U₆ : Matrix R n k

  U₆ = U₃ − P₄ (output block C₂₁).

• U₇ : Matrix R n k

  U₇ = U₃ + P₅ (output block C₂₂).

• hS₁ : self.S₁ = A₂₁ + A₂₂
• hS₂ : self.S₂ = self.S₁ - A₁₁
• hS₃ : self.S₃ = A₁₁ - A₂₁
• hS₄ : self.S₄ = A₁₂ - self.S₂
• hT₁ : self.T₁ = B₁₂ - B₁₁
• hT₂ : self.T₂ = B₂₂ - self.T₁
• hT₃ : self.T₃ = B₂₂ - B₁₂
• hT₄ : self.T₄ = self.T₂ - B₂₁
• hP₁ : self.P₁ = A₁₁ * B₁₁
• hP₂ : self.P₂ = A₁₂ * B₂₁
• hP₃ : self.P₃ = self.S₄ * B₂₂
• hP₄ : self.P₄ = A₂₂ * self.T₄
• hP₅ : self.P₅ = self.S₁ * self.T₁
• hP₆ : self.P₆ = self.S₂ * self.T₂
• hP₇ : self.P₇ = self.S₃ * self.T₃
• hU₁ : self.U₁ = self.P₁ + self.P₂
• hU₂ : self.U₂ = self.P₁ + self.P₆
• hU₃ : self.U₃ = self.U₂ + self.P₇
• hU₄ : self.U₄ = self.U₂ + self.P₅
• hU₅ : self.U₅ = self.U₄ + self.P₃
• hU₆ : self.U₆ = self.U₃ - self.P₄
• hU₇ : self.U₇ = self.U₃ + self.P₅

theorem Hex.Matrix.Winograd.c11 {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] {A₁₁ A₁₂ A₂₁ A₂₂ : Matrix R n m} {B₁₁ B₁₂ B₂₁ B₂₂ : Matrix R m k} (w : A₁₁.Winograd A₁₂ A₂₁ A₂₂ B₁₁ B₁₂ B₂₁ B₂₂) : w.U₁ = A₁₁ * B₁₁ + A₁₂ * B₂₁

Output block C₁₁ = U₁ of the Winograd schedule equals A₁₁·B₁₁ + A₁₂·B₂₁.

theorem Hex.Matrix.Winograd.c12 {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] {A₁₁ A₁₂ A₂₁ A₂₂ : Matrix R n m} {B₁₁ B₁₂ B₂₁ B₂₂ : Matrix R m k} (w : A₁₁.Winograd A₁₂ A₂₁ A₂₂ B₁₁ B₁₂ B₂₁ B₂₂) : w.U₅ = A₁₁ * B₁₂ + A₁₂ * B₂₂

Output block C₁₂ = U₅ of the Winograd schedule equals A₁₁·B₁₂ + A₁₂·B₂₂.

theorem Hex.Matrix.Winograd.c21 {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] {A₁₁ A₁₂ A₂₁ A₂₂ : Matrix R n m} {B₁₁ B₁₂ B₂₁ B₂₂ : Matrix R m k} (w : A₁₁.Winograd A₁₂ A₂₁ A₂₂ B₁₁ B₁₂ B₂₁ B₂₂) : w.U₆ = A₂₁ * B₁₁ + A₂₂ * B₂₁

Output block C₂₁ = U₆ of the Winograd schedule equals A₂₁·B₁₁ + A₂₂·B₂₁.

theorem Hex.Matrix.Winograd.c22 {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] {A₁₁ A₁₂ A₂₁ A₂₂ : Matrix R n m} {B₁₁ B₁₂ B₂₁ B₂₂ : Matrix R m k} (w : A₁₁.Winograd A₁₂ A₂₁ A₂₂ B₁₁ B₁₂ B₂₁ B₂₂) : w.U₇ = A₂₁ * B₁₂ + A₂₂ * B₂₂

Output block C₂₂ = U₇ of the Winograd schedule equals A₂₁·B₁₂ + A₂₂·B₂₂.