Stream: math-comp users

Topic: Linear Algebra Basics


view this post on Zulip William Spencer (Oct 15 2023 at 16:44):

Hi,

I'm a close-to-beginner formalizing some (basic) combinatorial results for fun and to get a better hold on coq. I want to use linear-algebraic methods for some of this (in particular, Berlekamp's oddtown theorem). So far I've been using mathcomp's matrix.v, but it doesn't seem to have some basic-ish results I need. In particular:
1) (under some algebraic conditions on the base ring) The determinant of A is 0 <-> there is a nontrivial linear relation among the cols, equivalently rows
2) (under some conditions) The matrix A has full row-rank (row-full A) <-> there is not a nontrivial linear relation among the rows; in particular, if v^T A = 0, then v = 0 (this is the 'right' way to state it, I think)

It's entirely possible that both of these and more are present in mathcomp in a form I didn't recognize. There is one direction of (2) (row_full_inj in matrix.v) giving that v => A . v is injective if A has full row rank, but I couldn't find the other.

I only really need these results for integer matrices, and eventually for matrices over a finite field (really just F_2, actually), and I don't know enough algebra to say what rings they hold on in general, so I wonder if I need to somehow specialize from mathcomp's framework of working over a generic ring to my specific domain.

Am I missing results mathcomp already has? Is there another library that has more robust linear algebra of this sort?

Or does it sound feasible to build up these results myself with what mathcomp has? I.e., define linear independence and use mathcomp's results to springboard to this type of thing. I don't have a sense of the feasibility of that sort of thing.

Thanks for any help!

view this post on Zulip Karl Palmskog (Oct 15 2023 at 16:47):

Did you look at CoqEAL? It has various matrix-related results for MathComp: https://github.com/coq-community/coqeal

view this post on Zulip Notification Bot (Oct 15 2023 at 16:48):

This topic was moved here from #Coq users > Linear Algebra Basics by Karl Palmskog.

view this post on Zulip Karl Palmskog (Oct 15 2023 at 16:49):

(I think this fits better here due to the many MathComp references)

view this post on Zulip William Spencer (Oct 15 2023 at 16:51):

I will look into CoqEAL, thank you! Also, I just found (1) in matrix.v (det0P), so that's half of it solved as well.

view this post on Zulip Karl Palmskog (Oct 15 2023 at 16:53):

this may be of interest w.r.t. linear algebra: https://github.com/VeriNum/LAProof


Last updated: Jul 25 2024 at 15:02 UTC