WKroneman (Aug 29 2020 at 19:41): WKroneman (Aug 29 2020 at 19:41):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
WKroneman (Aug 29 2020 at 19:43):Or am I overcomplicating things if I just want a bit of vector math?
Kazuhiko Sakaguchi (Aug 30 2020 at 09:59):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
WKroneman (Aug 30 2020 at 16:05):Ah, so I was supposed to use the matrix module. Thanks!
Christian Doczkal (Aug 31 2020 at 09:00):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.
Karl Palmskog (Aug 31 2020 at 09:06):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