CoqEAL seqmatrix multiplication refinement — List (List R) row-col product

This file extends the CoqEAL seqmatrix add-refinement of SeqMatrix.lean from addition to multiplication.

CoqEAL's seqmatrix refines MathComp matrices 'M[R]_(m,n) to lists of lists. SeqMatrix.lean ported the Radd_seqmx square (concrete row-wise addMx refines the abstract entrywise add). Matrix multiplication is the next refinement: it is a foldl-shaped dot-product of rows against columns. Here we build the concrete row-major multiply mulMx and prove the multiplication refinement square

entry (mulMx p ncols m n) i j = ∑ k : Fin p, entry m i k * entry n k j

(the sum runs over the shared/contraction dimension p), under the well-formed rectangular hypotheses that the row index is in range and the contracted row has length p. This is the CoqEAL Rmul_seqmx-shaped square restricted to the dimension-matching case — a correct restricted statement, as opposed to an unproven fully-general one.

A matrix-vector product A · v is mulMx with a single-column right operand, recorded as the specialization matVec / getD_matVec. The suite's frontier — fast matrix multiply (Strassen), and the linear-solve, determinant, and normal-form developments — is in the CoqEAL aggregator.

def Transfer.Examples.CoqEAL.SeqMatrixMul.entry {R : Type u_1} [NonUnitalNonAssocSemiring R] (m : List (List R)) (i j : ℕ) : R

The CoqEAL seqmatrix refinement relation (re-stated here matching SeqMatrix.entry): a row-major list of lists denotes the abstract entry function ℕ → ℕ → R, with absent rows and entries 0.

Equations

• Transfer.Examples.CoqEAL.SeqMatrixMul.entry m i j = (m.getD i []).getD j 0

def Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd {R : Type u_1} [NonUnitalNonAssocSemiring R] : List R → List R → R

List dot product Σ pᵢ·qᵢ, truncating at the shorter length. This is the inner fold that matrix multiplication contracts over.

Equations

• Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd [] x✝ = 0
• Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd x✝ [] = 0
• Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd (a :: p) (b :: q) = a * b + Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd p q

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd_eq_sum {R : Type u_1} [NonUnitalNonAssocSemiring R] (p : ℕ) (u v : List R) (hu : u.length = p) (hv : v.length = p) : dotProd u v = ∑ k : Fin p, u.getD (↑k) 0 * v.getD (↑k) 0

Dot-product refinement. Over two length-p lists, the concrete dotProd equals the abstract finite sum of pointwise products. This is the induction-on-the-shared-dimension core that the multiply square reuses.

def Transfer.Examples.CoqEAL.SeqMatrixMul.column {R : Type u_1} [NonUnitalNonAssocSemiring R] (n : List (List R)) (p j : ℕ) : List R

Column j (first p rows) of a matrix n: the length-p list [entry n 0 j, …, entry n (p-1) j]. Materializing the column lets the row-col product reuse the row-shaped dotProd.

Equations

• Transfer.Examples.CoqEAL.SeqMatrixMul.column n p j = List.map (fun (k : ℕ) => Transfer.Examples.CoqEAL.SeqMatrixMul.entry n k j) (List.range p)

@[simp]

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.column_length {R : Type u_1} [NonUnitalNonAssocSemiring R] (n : List (List R)) (p j : ℕ) : (column n p j).length = p

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.getD_column {R : Type u_1} [NonUnitalNonAssocSemiring R] (n : List (List R)) (p j k : ℕ) (hk : k < p) : (column n p j).getD k 0 = entry n k j

def Transfer.Examples.CoqEAL.SeqMatrixMul.mulMx {R : Type u_1} [NonUnitalNonAssocSemiring R] (p ncols : ℕ) (m n : List (List R)) : List (List R)

Concrete (computational) row-major matrix multiply. Row i of the product is the length-ncols list whose j-th entry is the dot product of row i of m with column j of n; p is the shared (contraction) dimension and ncols the column count of the result.

Equations

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

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.getD_mulMx_row {R : Type u_1} [NonUnitalNonAssocSemiring R] (p ncols : ℕ) (m n : List (List R)) (i : ℕ) (hi : i < m.length) : (mulMx p ncols m n).getD i [] = List.map (fun (j : ℕ) => dotProd (m.getD i []) (column n p j)) (List.range ncols)

Row i of mulMx (in range) is the explicit map of dot products.

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.entry_mulMx {R : Type u_1} [NonUnitalNonAssocSemiring R] (p ncols : ℕ) (m n : List (List R)) (i j : ℕ) (hi : i < m.length) (hj : j < ncols) (hrow : (m.getD i []).length = p) : entry (mulMx p ncols m n) i j = ∑ k : Fin p, entry m i ↑k * entry n (↑k) j

The CoqEAL Rmul_seqmx refinement square (well-formed case). The concrete row-col list multiply mulMx refines the abstract entrywise matrix product: entry (i,j) is the sum over the shared dimension p of entry m i k * entry n k j. Hypotheses pin the well-formed rectangular shape — the result row i is present (hi), the output has a j-th column (hj), and the contracted row i of m has length p (hrow).

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.entry_mulMx_fun {R : Type u_1} [NonUnitalNonAssocSemiring R] (p ncols : ℕ) (m n : List (List R)) (i : ℕ) (hi : i < m.length) (hrow : (m.getD i []).length = p) (j : ℕ) : j < ncols → entry (mulMx p ncols m n) i j = ∑ k : Fin p, entry m i ↑k * entry n (↑k) j

Functional form of the multiply square (over the fixed in-range row i, in-bounds columns, well-formed contracted row) — the commuting square the ReprTransfer registry consumes (concrete mulMx ↦ abstract entrywise product).

Specialization: matrix-vector product

A matrix-vector product A · v is mulMx with a single-column right operand. We give the direct form: the concrete matVec maps each row of A to its dot product with v, and refines the abstract matrix-vector product (A·v)_i = ∑_k A_{i,k} v_k.

def Transfer.Examples.CoqEAL.SeqMatrixMul.matVec {R : Type u_1} [NonUnitalNonAssocSemiring R] (A : List (List R)) (v : List R) : List R

Concrete matrix-vector product: each row of A dotted with v.

Equations

• Transfer.Examples.CoqEAL.SeqMatrixMul.matVec A v = List.map (fun (r : List R) => Transfer.Examples.CoqEAL.SeqMatrixMul.dotProd r v) A

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.getD_matVec {R : Type u_1} [NonUnitalNonAssocSemiring R] (p : ℕ) (A : List (List R)) (v : List R) (i : ℕ) (hi : i < A.length) (hrow : (A.getD i []).length = p) (hv : v.length = p) : (matVec A v).getD i 0 = ∑ k : Fin p, (A.getD i []).getD (↑k) 0 * v.getD (↑k) 0

Matrix-vector refinement square (well-formed case). The i-th entry of the concrete A · v equals the abstract sum ∑ k, A_{i,k} v_k over the shared dimension p, given the row is in range, the row has length p, and v has length p.

Agreement with Mathlib Matrix.mulVec

The matrix-vector refinement square above (getD_matVec) relates the concrete List-rep matVec to a raw Finset sum ∑ k, A_{i,k} v_k. This section relates that sum to the linear-algebra operation: the abstract matrix-vector product Matrix.mulVec of Mathlib, under the canonical conversion from the seq-matrix representation to a Matrix (Fin m) (Fin p) R and from the coefficient List to a Fin p → R vector.

This certifies the concrete matrix-vector product as Mathlib's Matrix.mulVec under the canonical conversions — the data refinement carried up to the real linear-algebra operation.

def Transfer.Examples.CoqEAL.SeqMatrixMul.toMatrix {R : Type u_1} [NonUnitalNonAssocSemiring R] (A : List (List R)) (m p : ℕ) : Matrix (Fin m) (Fin p) R

Convert a seq-matrix A : List (List R) to an abstract Matrix (Fin m) (Fin p) R via the entry function.

Equations

• Transfer.Examples.CoqEAL.SeqMatrixMul.toMatrix A m p = Matrix.of fun (i : Fin m) (j : Fin p) => Transfer.Examples.CoqEAL.SeqMatrixMul.entry A ↑i ↑j

def Transfer.Examples.CoqEAL.SeqMatrixMul.toVec {R : Type u_1} [NonUnitalNonAssocSemiring R] (v : List R) (p : ℕ) : Fin p → R

Convert a coefficient List R to an abstract column vector Fin p → R.

Equations

• Transfer.Examples.CoqEAL.SeqMatrixMul.toVec v p j = v.getD (↑j) 0

theorem Transfer.Examples.CoqEAL.SeqMatrixMul.getD_matVec_eq_mulVec {R : Type u_1} [NonUnitalNonAssocSemiring R] (m p : ℕ) (A : List (List R)) (v : List R) (i : ℕ) (hi : i < A.length) (hrow : (A.getD i []).length = p) (hv : v.length = p) (him : i < m) : (matVec A v).getD i 0 = (toMatrix A m p).mulVec (toVec v p) ⟨i, him⟩

Matrix-vector refinement = Mathlib Matrix.mulVec. Under the canonical seq-matrix → Matrix and List → Fin p → R conversions, the i-th entry of the concrete matVec A v equals the abstract Matrix.mulVec of the converted matrix applied to the converted vector — the data refinement carried up to the real linear-algebra operation.