Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Dear Georges,

Thank you very much for your detailed answer. We now understand better 
the foundations of the modules mxalgebra and vector and the way they are 
organized.

Yesterday we wrote an entire proof using Vector. In fact, it helped us 
to design the statement and its proof in a more readable way. For 
information, this statement establishes the existence of a certain free 
family of vectors satisfying certain properties.
We fully agree that we can rewrite everything using mxalgebra only. But 
we were missing a few (completely trivial) definitions and lemmas 
relating matrices and their sequence of rows. This connection is more 
apparent in the module Vector, via the functions span, lbasis, etc. This 
is why we were initially more comfortable with Vector.

As you may imagine, we wanted to mix \rank and \dim to make a connection 
with some other statements we already proved and which use \rank. Those 
statements could be rewritten using Vector, substituting the rank by 
\dim \limg, as you suggested.
Nevertheless, according to your message, it seems that it is more 
reasonable to rely on mxalgebra only (all the dimensions are explicit in 
our case).

Best regards.
Xavier and Ricardo

Le 16/06/2016 à 18:33, Georges Gonthier a écrit :
>    Dear Xavier,
>       Indeed, the vectType instance for the matrix type is fairly rudimentary 
> and doesn't readily provide the transparent encoding of the (fun v => A *m v) 
> function you seem to be expecting. Breaking the vectType abstractions doesn't 
> help all that much proving the \dim (ker A) lemma, because the
> 'cV_n <-> 'rV_n isomorphism provided by the matrix_vectType instance is 
> opaque, and thus need not be transposition.
>    It is actually unclear whether you need to use vector at all: mxalgebra 
> support a full theory of vector spaces with explicit dimensions, covering all 
> the results you cite. Using the same matrix type to represent vectors, 
> subspaces and linear functions (though usually with different dimensions) 
> simplifies considerably many formal proofs. This usually compensates for a 
> few quirks of the theory, such as  the non-unique representation of subspaces 
> and their relational equality (U :=: V)%MS.
>    The bottom line is that mxalgebra is better when working with explicit 
> matrices or in a space with an explicit dimension, while vector is better 
> when the dimension is implicit or when working with multiple spaces. So for 
> example MathComp uses matrices in representation theory, including for the 
> group ring, but vector for characters and Galois field extensions.
>    Assuming you nevertheless need to mix matrix and vector, the reason your 
> lemma is hard to prove
> Is because you need to tie the mxalgebra notion of rank to the vector 
> dimensions. With
>       Definition rng A := limg (linfun_mx A).
>       Lemma dim_rng A : \dim (rng A) = \rank A.
> Your lemma follows easily from limg_ker_dim
>    Lemma dim_ker A : \dim (ker A) = (n - \rank A)%N.
>    Proof.
>    apply/(canRL (addnK _)); rewrite -[ker A]capfv -dim_rng limg_ker_dim.
>    by rewrite dimvf /= [Vector.dim Vn]muln1.
>    Qed.
> Admittedly, dim_rng is somewhat painful to prove. One has to exhibit a basis 
> for rng A:
>   Lemma dim_rng A : \dim (rng A) = \rank A.
>   Proof.
>   pose X := mktuple (fun i => (row i (row_base A^T))^T).
>   suffices /size_basis->: basis_of (rng A) X by rewrite mxrank_tr.
>   rewrite /basis_of eqEsubv -andbA; apply/and3P; split.
>   - apply/span_subvP=> _ /codomP[i ->]; set u := row i _.
>      have /submxP[v ->]: (u <= A^T)%MS.
>         by rewrite (submx_trans (row_sub i _)) ?eq_row_base.
>      by apply/memv_imgP; exists v^T; rewrite ?memvf // trmx_mul trmxK lfunE.
>   - apply/subvP=> _ /memv_imgP[v _ ->].
>      rewrite lfunE /= -[A *m v]trmxK trmx_mul -[At in _ *m At]mulmx_base.
>      rewrite mulmxA mulmx_sum_row linear_sum rpred_sum // => i _.
>      by rewrite linearZZ rpredZ //=; apply/memv_span/codom_f.
>   apply/freeP=> a aA_0; pose u := \row_i a i.
>   suffices u0: u = 0 by move=> i; have /rowP/(_ i) := u0; rewrite !mxE.
>   apply/(row_free_inj (row_base_free A^T)); rewrite mul0mx -trmx0 -{}aA_0.
>   rewrite linear_sum mulmx_sum_row; apply/eq_bigr=> i _.
>   by rewrite mxE nth_mktuple linearZZ /= trmxK.
>   Qed.
> Do note that the proof is slightly complicated by a sprinkling of transposes 
> because you've chosen to use French-style column vectors instead of the 
> US-style row vectors favoured in mxalgebra (indeed, you get the type of 
> linfun_mx A wrong below: it's 'Hom(Vn, Vm)).
>    Finally, it's not clear why you need to relate to the mxalgebra definition 
> of rank: couldn't you avoid dim_rng altogether by defining rank A := \dim 
> (rng A) ?
>
>    Best,
> Georges
>
> -----Original Message-----
> From: 
>
>  
> [mailto:]
>  On Behalf Of Xavier Allamigeon
> Sent: 16 June 2016 09:27
> To: 
>
> Cc: Ricardo D. Katz 
> <>
> Subject: [ssreflect] Connection between mxalgebra and vector
>
> Dear SSReflect-list,
>
> Ricardo Katz (cc'ed) and myself are currently working on polyhedra and 
> polyhedral cones within SSReflect. For this purpose, we need some basic 
> linear algebra operations and statements.
> So far, we used matrices and vectors through the module Matrix, but now comes 
> the time make some proof involving the dimension of some subspaces, kernel of 
> linear maps, completion of free families of vectors, etc.
>
> As far as we can see, mxalgebra provides several useful constructions.
> However, the more abstract interface provided by the module Vector would 
> better suited for our needs (and proofs would be more elegant).
> Even though the implementation of Vector is based on matrices, this part is 
> supposed to be hidden, according to the documentation of 
> Vector.InternalTheory. In consequence, we don't understand how to easily make 
> the connections between the two layers.
>
> As an example, we would like to define the kernel of the linear map 
> associated with a matrix A: 'M_(m,n), and relate its dimension with the rank 
> of the matrix A. For this purpose, we introduced the linear map linfun_mx A 
> := linfun (mulmx A): 'Hom(Vm, Vn) where Vm and Vn are matrix_vectType of 
> dimension m 1 and n 1 respectively. Then, we defined ker A := lker (linfun_mx 
> A) and we could  straightforwardly check that it consists the vectors x:
> 'cV_n such that A *m x == 0.
> But now, we don't see how to prove that
> \dim ker A = n - \rank A
> unless going into the internal representation of the module Vector (which we 
> would like to avoid...).
>
> Which is the best approach for this problem?
>
> Thanks in advance,
>
> Best regards.
> Xavier