List-based matrix representation and computation

An implementation of a list-based matrix representation and computation for tactics that certify facts about matrix literals.

Implementation notes

dotProduct is sealed, and its expansion into the sum of products is reached only through the rewrite lemmas. Checking that expansion by kernel unfolding would make the kernel unfold + and * as well. For computable rings it then wastefully evaluates the entries, and for noncomputable rings it probes many nodes of opaque operations, which brings a worse constant.

ListMatrix namespace is used to avoid accidental collision with other downstream definitions.

Lean's Array is essentially a List within the kernel, so random access is slow; the List carrier is chosen for easier inductive operations. Reading an entry by position costs the kernel a walk of that length. Therefore, operations on this representation need to be mindful of traversing the structure in an efficient order.

def Mathlib.Tactic.Matrix.ListMatrix.dotProduct {α : Type u_1} [Mul α] [Add α] [Zero α] : Nat → List α → List α → α

A term for the sum of exactly n pointwise products of l₁ and l₂ padded with 0. This allows its bridge lemma to be provable without zero_mul, which minimises the instance strength.

Equations

• Mathlib.Tactic.Matrix.ListMatrix.dotProduct 0 x✝¹ x✝ = 0
• Mathlib.Tactic.Matrix.ListMatrix.dotProduct n.succ x✝¹ x✝ = x✝¹.headD 0 * x✝.headD 0 + Mathlib.Tactic.Matrix.ListMatrix.dotProduct n x✝¹.tail x✝.tail

theorem Mathlib.Tactic.Matrix.ListMatrix.dotProduct_zero {α : Type u_1} [Mul α] [Add α] [Zero α] (l₁ l₂ : List α) : dotProduct 0 l₁ l₂ = 0

theorem Mathlib.Tactic.Matrix.ListMatrix.dotProduct_add_one {α : Type u_1} [Mul α] [Add α] [Zero α] (n : Nat) (l₁ l₂ : List α) : dotProduct (n + 1) l₁ l₂ = l₁.headD 0 * l₂.headD 0 + dotProduct n l₁.tail l₂.tail

theorem Mathlib.Tactic.Matrix.ListMatrix.dotProduct_add_one_cons_cons {α : Type u_1} [Mul α] [Add α] [Zero α] {n : Nat} (a b : α) {l₁ l₂ : List α} {c : α} (h : dotProduct n l₁ l₂ = c) : dotProduct (n + 1) (a :: l₁) (b :: l₂) = a * b + c

def Mathlib.Tactic.Matrix.ListMatrix.consPad {α : Type u_1} [Zero α] : List α → List (List α) → List (List α)

A one-pass recursion that prepends the entries of row to the rows of cols, with row padded with 0 when it is shorter. This can be done using List.zipWith + row.rightpad, but that version requires 3 traversals.

Equations

• Mathlib.Tactic.Matrix.ListMatrix.consPad x✝ [] = []
• Mathlib.Tactic.Matrix.ListMatrix.consPad (a :: row) (col :: cols) = (a :: col) :: Mathlib.Tactic.Matrix.ListMatrix.consPad row cols
• Mathlib.Tactic.Matrix.ListMatrix.consPad [] (col :: cols) = (0 :: col) :: Mathlib.Tactic.Matrix.ListMatrix.consPad [] cols

theorem Mathlib.Tactic.Matrix.ListMatrix.consPad_eq_zipWith {α : Type u_1} [Zero α] (row : List α) (cols : List (List α)) : consPad row cols = List.zipWith List.cons (List.rightpad cols.length 0 row) cols

def Mathlib.Tactic.Matrix.ListMatrix.transpose {α : Type u_1} [Zero α] (n : Nat) : List (List α) → List (List α)

The transpose of a list of rows as n rows, where row j collects the j-th entries of the input rows padded with 0. Defined by recursion on the rows with explicit padding rather than through Batteries' List.transpose, so that it reduces in the kernel. This is also more efficient as it gives an O(nm) transposition without any random access.

Equations

• Mathlib.Tactic.Matrix.ListMatrix.transpose n [] = List.replicate n []
• Mathlib.Tactic.Matrix.ListMatrix.transpose n (row :: rows) = Mathlib.Tactic.Matrix.ListMatrix.consPad row (Mathlib.Tactic.Matrix.ListMatrix.transpose n rows)

@[simp]

theorem Mathlib.Tactic.Matrix.ListMatrix.length_transpose {α : Type u_1} [Zero α] (n : Nat) (rows : List (List α)) : (transpose n rows).length = n

theorem Mathlib.Tactic.Matrix.ListMatrix.getD_transpose {α : Type u_1} [Zero α] {n j : Nat} (rows : List (List α)) (i : Nat) (hj : j < n) : ((transpose n rows).getD j []).getD i 0 = (rows.getD i []).getD j 0

def Mathlib.Tactic.Matrix.ListMatrix.mul {α : Type u_1} [Mul α] [Add α] [Zero α] (l m n : Nat) (A B : List (List α)) : List (List α)

The product of two lists of rows as l rows of n entries. Each entry is a dot product of m terms, with A and B read as an l × m and an m × n matrix respectively.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Tactic.Matrix.ListMatrix.getD_mul {α : Type u_1} [Mul α] [Add α] [Zero α] {l m n i j : Nat} (A B : List (List α)) (hi : i < l) (hj : j < n) : ((mul l m n A B).getD i []).getD j 0 = dotProduct m (A.getD i []) ((transpose n B).getD j [])