Library mathcomp.algebra.matrix

Basic concrete linear algebra : definition of type for matrices, and all basic matrix operations including determinant, trace and support for block decomposition. Matrices are represented by a row-major list of their coefficients but this implementation is hidden by three levels of wrappers (Matrix/Finfun/Tuple) so the matrix type should be treated as abstract and handled using only the operations described below: 'M[R](m, n) == the type of m rows by n columns matrices with 'M(m, n) coefficients in R; the [R] is optional and is usually omitted. 'M[R]_n, 'M_n == the type of n x n square matrices. 'rV[R]_n, 'rV_n == the type of 1 x n row vectors. 'cV[R]_n, 'cV_n == the type of n x 1 column vectors. \matrix(i < m, j < n) Expr(i, j) == the m x n matrix with general coefficient Expr(i, j), with i : 'I_m and j : 'I_n. the < m bound can be omitted if it is equal to n, though usually both bounds are omitted as they can be inferred from the context. \row(j < n) Expr(j), \col(i < m) Expr(i) the row / column vectors with general term Expr; the parentheses can be omitted along with the bound. \matrix(i < m) RowExpr(i) == the m x n matrix with row i given by RowExpr(i) : 'rV_n. A i j == the coefficient of matrix A : 'M(m, n) in column j of row i, where i : 'I_m, and j : 'I_n (via the coercion fun_of_matrix : matrix >-> Funclass). const_mx a == the constant matrix whose entries are all a (dimensions should be determined by context). map_mx f A == the pointwise image of A by f, i.e., the matrix Af congruent to A with Af i j = f (A i j) for all i and j. A^T == the matrix transpose of A. row i A == the i'th row of A (this is a row vector). col j A == the j'th column of A (a column vector). row' i A == A with the i'th row spliced out. col' i A == A with the j'th column spliced out. xrow i1 i2 A == A with rows i1 and i2 interchanged. xcol j1 j2 A == A with columns j1 and j2 interchanged. row_perm s A == A : 'M(m, n) with rows permuted by s : 'S_m. col_perm s A == A : 'M(m, n) with columns permuted by s : 'S_n. row_mx Al Ar == the row block matrix <Al Ar> obtained by contatenating two matrices Al and Ar of the same height. col_mx Au Ad == the column block matrix / Au \ (Au and Ad must have the same width). \ Ad / block_mx Aul Aur Adl Adr == the block matrix / Aul Aur \ \ Adl Adr / \mxblock(i < m, j < n) B i j == the block matrix of type 'M(\sum_i p i, \sum_j q j) / (B 0 0) ⋯ (B 0 j) ⋯ (B 0 n) \ | ... ... ... | | (B i 0) ⋯ (B i j) ⋯ (B i n) | | ... ... ... | \ (B m 0) ⋯ (B m j) ⋯ (B m n) / where each block (B i j) has type 'M(p i, q j). \mxdiag(i < n) B i == the block square matrix of type 'M(\sum_i p i) / (B 0) 0 \ | ... ... | | 0 (B i) 0 | | ... ... | \ 0 (B n) / where each block (B i) has type 'M(p i). \mxrow(j < n) B j == the block matrix of type 'M(m, \sum_j q j). < (B 0) ... (B n) > where each block (B j) has type 'M(m, q j). \mxcol(i < m) B i == the block matrix of type 'M(\sum_i p i, n) / (B 0) \ | ... | \ (B m) / where each block (B i) has type 'M(p i, n). [l|r]submx A == the left/right submatrices of a row block matrix A. Note that the type of A, 'M(m, n1 + n2) indicates how A should be decomposed. [u|d]submx A == the up/down submatrices of a column block matrix A. [u|d] [l|r]submx A == the upper left, etc submatrices of a block matrix A. submxblock A i j == the block submatrix of type 'M(p i, q j) of A. The type of A, 'M(\sum_i p i, \sum_i q i) indicates how A should be decomposed. There is no analogous for mxdiag since one can use submxblock A i i to extract a diagonal block. submxrow A j == the submatrix of type 'M(m, q j) of A. The type of A, 'M(m, \sum_j q j) indicates how A should be decomposed. submxrow A j == the submatrix of type 'M(p i, n) of A. The type of A, 'M(\sum_i p i, n) indicates how A should be decomposed. mxsub f g A == generic reordered submatrix, given by functions f and g which specify which subset of rows and columns to take and how to reorder them, e.g. picking f and g to be increasing yields traditional submatrices. := \matrix(i, j) A (f i) (g i) rowsub f A := mxsub f id A colsub g A := mxsub id g A castmx eq_mn A == A : 'M(m, n) cast to 'M(m', n') using the equation pair eq_mn : (m = m') * (n = n'). This is the usual workaround for the syntactic limitations of dependent types in Coq, and can be used to introduce a block decomposition. It simplifies to A when eq_mn is the pair (erefl m, erefl n) (using rewrite /castmx /=). conform_mx B A == A if A and B have the same dimensions, else B. mxvec A == a row vector of width m * n holding all the entries of the m x n matrix A. mxvec_index i j == the index of A i j in mxvec A. vec_mx v == the inverse of mxvec, reshaping a vector of width m * n back into into an m x n rectangular matrix. In 'M[R](m, n), R can be any type, but 'M[R](m, n) inherits the eqType, choiceType, countType, finType, zmodType structures of R; 'M[R](m, n) also has a natural lmodType R structure when R has a ringType structure. Because the type of matrices specifies their dimension, only non-trivial square matrices (of type 'M[R]_n.+1) can inherit the ring structure of R; indeed they then have an algebra structure (lalgType R, or algType R if R is a comRingType, or even unitAlgType if R is a comUnitRingType). We thus provide separate syntax for the general matrix multiplication, and other operations for matrices over a ringType R: A *m B == the matrix product of A and B; the width of A must be equal to the height of B. a%:M == the scalar matrix with a's on the main diagonal; in particular 1%:M denotes the identity matrix, and is is equal to 1%R when n is of the form n'.+1 (e.g., n >= 1). is_scalar_mx A <=> A is a scalar matrix (A = a%:M for some A). diag_mx d == the diagonal matrix whose main diagonal is d : 'rV_n. is_diag_mx A <=> A is a diagonal matrix: forall i j, i != j -> A i j = 0 is_trig_mx A <=> A is a triangular matrix: forall i j, i < j -> A i j = 0 delta_mx i j == the matrix with a 1 in row i, column j and 0 elsewhere. pid_mx r == the partial identity matrix with 1s only on the r first coefficients of the main diagonal; the dimensions of pid_mx r are determined by the context, and pid_mx r can be rectangular. copid_mx r == the complement to 1%:M of pid_mx r: a square diagonal matrix with 1s on all but the first r coefficients on its main diagonal. perm_mx s == the n x n permutation matrix for s : 'S_n. tperm_mx i1 i2 == the permutation matrix that exchanges i1 i2 : 'I_n. is_perm_mx A == A is a permutation matrix. lift0_mx A == the 1 + n square matrix block_mx 1 0 0 A when A : 'M_n. \tr A == the trace of a square matrix A. \det A == the determinant of A, using the Leibnitz formula. cofactor i j A == the i, j cofactor of A (the signed i, j minor of A), \adj A == the adjugate matrix of A (\adj A i j = cofactor j i A). A \in unitmx == A is invertible (R must be a comUnitRingType). invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. A \is a mxOver S == the matrix A has its coefficients in S. comm_mx A B := A *m B = B *m A comm_mxb A B := A *m B == B *m A all_comm_mx As fs := all2rel comm_mxb fs The following operations provide a correspondence between linear functions and matrices: lin1_mx f == the m x n matrix that emulates via right product a (linear) function f : 'rV_m -> 'rV_n on ROW VECTORS lin_mx f == the (m1 * n1) x (m2 * n2) matrix that emulates, via the right multiplication on the mxvec encodings, a linear function f : 'M(m1, n1) -> 'M(m2, n2) lin_mul_row u := lin1_mx (mulmx u \o vec_mx) (applies a row-encoded function to the row-vector u). mulmx A == partially applied matrix multiplication (mulmx A B is displayed as A *m B), with, for A : 'M(m, n), a canonical {linear 'M(n, p) -> 'M(m, p}} structure. mulmxr A == self-simplifying right-hand matrix multiplication, i.e., mulmxr A B simplifies to B *m A, with, for A : 'M(n, p), a canonical {linear 'M(m, n) -> 'M(m, p}} structure. lin_mulmx A := lin_mx (mulmx A). lin_mulmxr A := lin_mx (mulmxr A). We also extend any finType structure of R to 'M[R](m, n), and define: {'GL_n[R]} == the finGroupType of units of 'M[R]_n.-1.+1. 'GL_n[R] == the general linear group of all matrices in {'GL_n(R)}. 'GL_n(p) == 'GL_n['F_p], the general linear group of a prime field. GLval u == the coercion of u : {'GL_n(R)} to a matrix. In addition to the lemmas relevant to these definitions, this file also proves several classic results, including :

• The determinant is a multilinear alternate form.
• The Laplace determinant expansion formulas: expand_det [row|col].
• The Cramer rule : mul_mx_adj & mul_adj_mx.

Finally, as an example of the use of block products, we program and prove the correctness of a classical linear algebra algorithm: cormen_lup A == the triangular decomposition (L, U, P) of a nontrivial square matrix A into a lower triagular matrix L with 1s on the main diagonal, an upper matrix U, and a permutation matrix P, such that P * A = L * U. This is example only; we use a different, more precise algorithm to develop the theory of matrix ranks and row spaces in mxalgebra.v

Type Definition*********************************

Basic linear algebra (matrices). We use dependent types (ordinals) for the indices so that ranges are mostly inferred automatically

Matrix structural operations (transpose, permutation, blocks) *******

Constant matrix

Definitions and properties for which we can work with fixed dimensions.

Reshape a matrix, to accomodate the block functions for instance.

Transpose a matrix

Permute a matrix vertically (rows) or horizontally (columns)

Exchange two rows/columns of a matrix

Row/Column sub matrices of a matrix

Removing a row/column from a matrix

reindexing/subindex a matrix

This can be use to reverse an equation that involves a cast.

Concatenating two matrices, in either direction.

Left/Right | Up/Down submatrices of a rows | columns matrix. The shape of the (dependent) width parameters of the type of A determines which submatrix is selected.

This lemma has Prenex Implicits to help RL rewrititng with castmx_sym.

This lemma has Prenex Implicits to help RL rewrititng with castmx_sym.