Simple planar geometry

Stream: Is there code for X?

[Michael George]

I'm interested in implementing some computational geometry algorithms (like polygon union and intersection or determining whether a point is in a polygon) and proving their correctness. To do so, I need basic primitives like adding a vector to a point, comparing the distances between points, sorting line segments by angle, determining which side of a line a point is on, and so on.

Since I care about computation, everything needs to be decidable (and ideally, fast!). I also want to parameterize on the ground field so that I can have coordinates in $\Q[\sqrt{2}}$ for example.

The linear algebra and euclidean geometry machinery in mathlib seems too heavy for this task (but maybe not?). These primitives shouldn't be too hard to implement by hand, just representing a point as a pair of coordinates, but I'm imagining that the proofs might require machinery that would be tedious and/or difficult to implement.

Any suggestions on how I should proceed? Are there simple 2D geometry libraries that I could use?

[Yaël Dillies]

Hey!

The linear algebra and euclidean geometry machinery in mathlib seems too heavy for this task

I don't think so, at least for the basic operations. You can use docs#AddTorsor to add vectors to points and that will be computationally nice and all. Sorting lines by angles will be annoying and noncomputable) with the mathlib machinery though, so you'll have to do that yourself.

Are there simple 2D geometry libraries that I could use?

Not really, no. There's the very general geometry development in mathlib and then some axiomatic geometry developments outside it, like geolean which is meant to be a port of geocoq.

[Siddhartha Gadgil]

Where is geolean? I could not find it with a google search

[Yaël Dillies]

See eg https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/tarski.20axiom.20geometry/near/391771428

[Yaël Dillies]

cc @Jovan Gerbscheid because I'm sure you will find this interesting

[Jovan Gerbscheid]

I haven't dabbled into computational geometry myself, just geometry proving without a model.