(Credits ITP 2013 tutorial: The Mathematical Components library by Enrico Tassi and Assia Mahboubi material here)
A matrix is encoded as a 2-dimension array
Some notations : size inside parentheses, type of coefficients inside square brackets. NB: In the library, the type of coefficients can also be ommitted.
matrix is just a tag over ffun: it inherits from its structure. We can transfer automatically all structures from the type of finite functions by trivial subTyping.
Test overloaded "_ == _" notation, given by the eqType canonical structure.
Since matrices over nat are comparable with _ == _, matrices over matrices over nat are also comparable.
We define a coercion in order to access elements as if matrices were functions.
We provide a notation to build matrices from a general term. This is the best way to define a matrix. One can also assemble blocks using row_mx, col_mx and block_mx, but most of the time, this might be a bad idea.
Main Theorems
We now show the most used theorems for matrix manipulation.
mxE
mxE is an equation to compute a term in the matrix at given coordinates: it extracts the general term of the matrix and compute the substitution of indexes. It is generally the right move when you have
(A complicated matrix) i j
in your goal.
matrixP
matrixP is the extensionality theorem for matrices, it says two matrices are equal if and only if all their coefficients are pairwise equal.
Ring operations on matrices
Matrices on rings are provided with a R-module canonical structure.
Mathematical components includes a library for many standard algebaric structures. This library provides generic operations (0, 1, +, *, ...) and theorems depending on how rich the structure is.
However, the library does not contain heterogeneous multiplication, so we have a specific operation for that.
square matrices with non zero size have a ring canonical structure.
The generic ring product is available on square matrices with explicit nonzero size (ie size is convertible to n.+1). This ring product coincides with the matrix product (definitionally).
Specific matrix operations
There are scalar_mx, trace, transpose and determinant operations, that are specific to matrices.
Builds a diagonal matrix from any element
rewrite /mxtrace (eq_bigr (fun i => \sum_j A i j * B j i)); last first.
by move=> i _; rewrite mxE.
rewrite exchange_big /=; apply: eq_bigr => i _.
by rewrite mxE; apply: eq_bigr => j _; rewrite mulrC.
Naming conventions.
The two most important things to get your way out of a situation:
Knowing your math
Searching the library for what you think you know
For that you have the ssreflect Search command. To use its full power, one should combine seach by identifier (Coq definition), pattern (partial terms) and name (a string contained in the name of the theorem).
The two first methods are straightforward to use (except if you instanciate your patterns more than necessary), but searching by name requires to be aware of naming conventions.
Names in the library are usually obeying one of following the convention
(condition_)?mainSymbol_suffixes
mainSymbol_suffixes(_condition)?
Or in the presence of a property denoted by a nary or unary predicate:
naryPredicate_mainSymbol+
mainSymbol_unaryPredicate
Where :
mainSymbol is the most meaningful part of the lemma. It generally
is the head symbol of the right-hand side of an equation or the
head symbol of a theorem. It can also simply be the main object of
study, head symbol or not. It is usually either
one of the main symbols of the theory at hand. For example, it will be opp, add, mul, etc...
or a special canonical operation, such as a ring morphism or a
subtype predicate. e.g. linear, raddf, rmorph, rpred, etc ...
condition is used when the lemma applies under some hypothesis.
suffixes are there to refine what shape and/or what other symbols the lemma has. It can either be the name of a symbol (add, mul, etc...), or the (short) name of a predicate (inj for injectivity, id for identity, ...) or an abbreviation.
Abbreviations are in the header of the file which introduce them. We list here the main abbreviations.
A -- associativity, as in andbA : associative andb.
AC -- right commutativity.
ACA -- self-interchange (inner commutativity), e.g.,
orbACA : (a || b) || (c || d) = (a || c) || (b || d).
b -- a boolean argument, as in andbb : idempotent andb.
C -- commutativity, as in andbC : commutative andb,
or predicate complement, as in predC.
CA -- left commutativity.
D -- predicate difference, as in predD.
E -- elimination, as in negbFE : ~~ b = false -> b.
F or f -- boolean false, as in andbF : b && false = false.
I -- left/right injectivity, as in addbI : right_injective addb or predicate intersection, as in predI.
l -- a left-hand operation, as andb_orl : left_distributive andb orb.
N or n -- boolean negation, as in andbN : a && (~~ a) = false.
n -- alternatively, it is a natural number argument
P -- a characteristic property, often a reflection lemma, as in
andP : reflect (a /\ b) (a && b).
r -- a right-hand operation, as orb_andr : right_distributive orb andb.
- alternatively, it is a ring argument
T or t -- boolean truth, as in andbT: right_id true andb.
U -- predicate union, as in predU.
W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P.
0 -- ring 0, as in addr0 : x + 0 = x.
1 -- ring 1, as in mulr1 : x * 1 = x.
D -- ring addition, as in linearD : f (u + v) = f u + f v.
B -- ring subtraction, as in opprB : - (x - y) = y - x.
M -- ring multiplication, as in invfM : (x * y)^-1 = x^-1 * y^-1.
Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n.
mx -- a matrix argument
N -- ring opposite, as in mulNr : (- x) * y = - (x * y).
V -- ring inverse, as in mulVr : x^-1 * x = 1.
X -- ring exponentiation, as in rmorphX : f (x ^+ n) = f x ^+ n.
Z -- (left) module scaling, as in linearZ : f (a *: v) = s *: f v.
z -- a int operation
My most used search pattern
Search _ "prefix" "suffix"* (symbol|pattern)* in library.
Examples
Toy application to graph theory
We now illustrate the use of matrices on simple example of graph. For simplicity, we take graphs on ordinal (type representing initial segments of natural numbers : 0,..,i-1)
In order to compare elements from a field with total order, we use the structure real field type from the library numeric hierarchy. In practice this can be instanciated to rational numbers.
Definition of the adjacency matrix and partial inverse
Transposing the adjacency matrix reverses the graph
by move=> x y; rewrite /adjrel !mxE; case: g; rewrite ?ltr01.
Graph paths
We define the set of paths in g from x to y of size k by comprehension, as the set of lists of size k, that end with y. Hence a path of size k goes through k+1 points, and in particular a path of size 0 starts and ends at the same point.
We start by posing a notation on the set of graphs.
We can exhibit what are paths of size 0 and prove how many there are.
We can exhibit what are paths of size 1 and prove how many there are.
This proof is left as an exercise in finite types and finite sets, but contains nothing about matrices. You may as well skip it if you want to focus on matrices.
We can exhibit what are paths of size n+1 and prove how many there are.
The cardinality proof is left as an exercise in finite types and finite sets, but contains nothing about matrices. You may as well skip it if you want to focus on matrices.
rewrite (eq_bigr (fun z : T => \sum_(p : k.-tuple T)
if [&& g x z, path g z p & last z p == y] then 1 else 0)%N);
last first.
move=> z _; rewrite -sum1dep_card big_distrr /= big_mkcond.
by apply: eq_bigr=> p _; case: path; case: eqP; case: g.
rewrite pair_big_dep /= -big_mkcond sum1dep_card.
rewrite -(@card_imset _ _
(fun p : T * k.-tuple T => [tuple of p.1 :: p.2]));
last by move=> [a p] [b q] /= [->/val_inj->].
rewrite gSpath; apply: eq_card=> p; rewrite !inE /=.
apply/idP/imsetP=> [|[[q z /=]]]; last by rewrite inE /= => ? ->.
exists (thead p, [tuple of behead p]); rewrite ?inE //=.
by case: (tupleP p) => //= ??; apply/val_inj.
Counting the number of path using the adjacency matrix.
We show the correspondance between the kth power of the adjacency matrix and the number of paths of size k.
elim: k=> [|k IHk] in x y *; first by rewrite expr0 mxE card_g0path.
rewrite exprS mxE card_gSpath natr_sum; apply: eq_bigr => i _.
by rewrite natrM IHk mxE.
Definition of stochastic matrices
First, we define the boolean definition, then the reflection lemma (which might be automated using Enrico and Benjamin's work on automated views.
Then we can start proving intersting properties, like the product of two stochastic matrices is stochastic.
move=> u_stoc M_stoc; apply/stochasticP => i.
rewrite (eq_bigr _ (fun j _ => (mxE _ _ i j))) exchange_big /=.
rewrite (eq_bigr (fun j => N i j)) ?(stochasticP _) //.
by move=> l _; rewrite -mulr_sumr (stochasticP _) ?mulr1.
Page rank
We define the page rank matrix and show it is stochastic.
move=> g_connects; apply/stochasticP => i.
rewrite (eq_bigr _ (fun j _ => (mxE _ _ i j))).
rewrite -mulr_suml divff //= -natr_sum pnatr_eq0 -big_mkcond /=.
rewrite sum1dep_card cards_eq0; apply/set0Pn.
by have [j ?] := g_connects i; exists j; rewrite inE.
Polynomial adjacency matrix
We define the polynomial adjacency matrix of a graph with no edges from vertices to themselves, as the matrix with 1 on the diagonal, polynomial X when there is an edge, and 0 if there is no connexion (between two different vertices).
First we show it is a generalisation of the adjacency matrix, as taking the degree of each polynomial in the matrix results in the previously define adjacency matrix.
Polynomial adjacency matrix
Then one can prove that there is a link beween the number of path of size i, and the ith coefficient of the polynomial in the corresponding coefficient of the matrix.
I was not aware of this result, does anyone know where one could find it in the litterature?
Warning: my own proof of this fact is currently 31 lines...
wlog -> : k i g x y / k = 1%N => [hwlog|]; last first.
move=> gNrefl; rewrite expr1 !mxE !(fun_if (fun p : {poly _} => p`_i)).
rewrite !coefC !coefX ?if_same.
case: i => [|[|i]]; rewrite ?(binS, bin0, bin0n, muln0, muln1, if_same) //=.
by rewrite card_g0path; case: eqP => [|]//; rewrite ?if_same.
rewrite card_g1path; case: eqP => [->|] //; last by case: (g).
by rewrite (negPf (gNrefl y)).
elim: k {-2}k (leqnn k) => [|K IHK] k le_k // in i g x y *.
move: le_k; rewrite leqn0 => /eqP -> gNrefl.
rewrite bin0n mxE coefMn coef1.
have [->|_] := altP eqP; last by rewrite ?mul0rn ?muln0 ?mul0n.
rewrite !muln1 mulr1n -sum1dep_card big_mkcond (bigD1 [tuple]) //=.
by rewrite big1 ?addn0; [case: eqP|move=> t; rewrite tuple0 /= ?eqxx].
move=> gNrefl; case: k => [//|k] in le_k *; first by apply: IHK.
rewrite [_ ^+ _.+1](exprD _ 1) mxE coef_sum ?ltnS in le_k *.
case: i => [|i].
evar (F : 'I_n -> R); rewrite !muln1 (eq_bigr F)=> [|z _]; last first.
rewrite coefM big_ord1 subnn hwlog // bin0 IHK // bin0 !muln1 -!natrM.
by rewrite !card_g0path /F.
rewrite /F {F} -natr_sum card_g0path ?(maxn_idPr _) ?subn0 //.
rewrite (bigD1 x) //= ?eqxx ?mul1n big1 ?addn0 -?natrM // => i.
by rewrite eq_sym => /negPf->; rewrite mul0n.
evar (F : 'I_n -> R); rewrite (eq_bigr F)=> [|z _]; last first.
rewrite coefM !big_ord_recl //.
rewrite big1 ?addr0; last by move=> l; rewrite hwlog // muln0 mul0r.
rewrite subn0 subSS subn0 [_`_(i.+1)]IHK // [_`_(i)]IHK//.
rewrite !hwlog //= card_g0path card_g1path ?mulr1 ?expn1 ?muln1.
by rewrite -!natrM !mulnA /F.
rewrite big_split /= (bigD1 x) // big1 /= ?addr0 ?eqxx ?mul1n; last first.
by move=> z; rewrite eq_sym => /negPf->; rewrite ?mul0r.
by rewrite -natr_sum -!big_distrl /= -card_gSpath /= -natrD binS mulnDr.