Hi. I'd like to prove something about points in the 2D plane. The mathcomp library looks promising, but I can't make heads or tails out of how I can just declare, say a point named x with coordinates (0,0): https://math-comp.github.io/htmldoc/mathcomp.algebra.vector.html

Or am I overcomplicating things if I just want a bit of vector math?

If you wish to reason about concrete 2-dimensional row and column vectors, see matrix.v. https://math-comp.github.io/htmldoc/mathcomp.algebra.matrix.html

Ah, so I was supposed to use the matrix module. Thanks!

Pinging @Cyril Cohen and @Yves Bertot , who might have more to say on the matter. Using mathcomp is probably the right direction though, given that the 2D/3D geometry work of the aforementioned people is based on mathcomp.

this stuff (and the whole project) looks relevant: https://github.com/affeldt-aist/coq-robot/blob/master/euclidean3.v

Last updated: Sep 26 2023 at 11:01 UTC