Stream: Coq users

Topic: Where do I get points and vectors from?


view this post on Zulip 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

view this post on Zulip WKroneman (Aug 29 2020 at 19:43):

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

view this post on Zulip 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

view this post on Zulip WKroneman (Aug 30 2020 at 16:05):

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

view this post on Zulip 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.

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC