The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Ben,

Ben Grange 
<lagrange123 AT gmail.com>
 writes:

> I'm going through a linear algebra book (Linear Algebra Done Wrong, for
> anyone curious), and would like to verify my proofs with Coq. This would
> involve heavy use of matrices, of course.
> I've found the Mathematical Components library, (which has a matrix.v), but
> this seems like overkill for my humble purposes. Initially, I only went
> there because I was curious, "how did they implement this kind of
> polymorphism?"

Personally, I do recommend math-comp; even if a bit steep at the
beginning, getting into it will greatly pay off IMO.

> Indeed, what is the best way to quantify over all field-types? Would
> it be a typeclass? What would be the best way to leverage the existing
> Coq standard library?  Hopefully this makes sense.

These are very interesting questions without a definitive answer yet.

I suggest you check recent threads such as [1], but in all cases, this
kind of packaging is a significant amount work.

Thus, using a mature, proven library such as math-comp will allow you to
get things done much quicker (especially when talking about linear
algebra!), and at the same time learn their approach for packaging
mathematical structures [2].

Kind regards,
Emilio

[1] 
https://coq.discourse.group/t/how-to-represent-mathematical-structures-in-coq/188/8
[2] https://hal.inria.fr/inria-00368403v1/document