Convex Polygons

This file defines convex polygons as ordered lists of rational vertices.

structure NondegenPolygon : Type

A polygon represented by its vertices.

we require that all vertices are distinct, and that there are 3 or more vertices.

Operations that would return a degenerate polygon (fewer than 3 vertices) return none instead.

Note we do not extend mathlib's Polygon, because we want to bundle the vertex count.

• vertex_count : ℕ

  The number of vertices in the polygon.

• vertex_count_pos : NeZero self.vertex_count

  vertex_count must be positive

• three_le_vertex_count : 3 ≤ self.vertex_count

  Vertex count must be at least 3

• vertices : Fin self.vertex_count → RationalPoint

  The vertices of the polygon, in counterclockwise order

• nodup : Function.Injective self.vertices

  All vertices are distinct

def instReprNondegenPolygon.repr : NondegenPolygon → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instReprNondegenPolygon : Repr NondegenPolygon

Equations

• instReprNondegenPolygon = { reprPrec := instReprNondegenPolygon.repr }

def instDecidableEqNondegenPolygon.decEq (x✝ x✝¹ : NondegenPolygon) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instDecidableEqNondegenPolygon : DecidableEq NondegenPolygon

Equations

• instDecidableEqNondegenPolygon = instDecidableEqNondegenPolygon.decEq

instance instNeZeroNatVertex_count (poly : NondegenPolygon) : NeZero poly.vertex_count

def NondegenPolygon.getStrictlyLeftHalfspace (ng : NondegenPolygon) (i : Fin ng.vertex_count) : OpenHalfSpace

The open half-space strictly to the left of the directed edge from vertex i to vertex i+1.

Equations

• ng.getStrictlyLeftHalfspace i = (ng.vertices i).toStrictlyLeft (ng.vertices (i + 1)) ⋯

structure ConvexPolygonextends NondegenPolygon : Type

A convex polygon.

Convexity is enforced by the condition that for each edge i→i+1, all other vertices lie strictly to the left of that edge.

The strictness enforces that there can be no collinear triples of vertices, which in turn ensures that all vertices are extreme points of the convex hull.

• vertex_count : ℕ
• vertex_count_pos : NeZero self.vertex_count
• three_le_vertex_count : 3 ≤ self.vertex_count
• vertices : Fin self.vertex_count → RationalPoint
• nodup : Function.Injective self.vertices
• vertices_extremeRationalPoints (i j : Fin self.vertex_count) : j ≠ i → j ≠ i + 1 → (self.getStrictlyLeftHalfspace i).contains (self.vertices j) = true

  For all edges i→i+1, all other vertices lie on or to the left (closed half-space)

def instReprConvexPolygon.repr : ConvexPolygon → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instReprConvexPolygon : Repr ConvexPolygon

Equations

• instReprConvexPolygon = { reprPrec := instReprConvexPolygon.repr }

def instDecidableEqConvexPolygon.decEq (x✝ x✝¹ : ConvexPolygon) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instDecidableEqConvexPolygon : DecidableEq ConvexPolygon

Equations

• instDecidableEqConvexPolygon = instDecidableEqConvexPolygon.decEq

def ConvexPolygon.vertex_list (poly : ConvexPolygon) : List RationalPoint

The vertex list of a convex polygon, in counterclockwise order.

Equations

• poly.vertex_list = List.map poly.vertices (List.finRange poly.vertex_count)

def grahamScanStep (stack : List RationalPoint) (p : RationalPoint) : List RationalPoint

Graham scan helper: process remaining points to build upper/lower hull

Equations

• grahamScanStep [] p = [p]
• grahamScanStep [q] p = [p, q]
• grahamScanStep (q :: r :: rest) p = if r.ccw q p = true then p :: q :: r :: rest else grahamScanStep (r :: rest) p

def convexHullRationalPoints (points : List RationalPoint) : List RationalPoint

Compute the convex hull of a list of points using a Graham-scan-like algorithm. Should return a list of vertices such that:

• All points in the returned list are in the input list (no new points).
• The returned list has no duplicates.
• The returned list starts with the lowest x-coordinate point (lowest y-coordinate to tiebreak) and then goes in counterclockwise order.
• All input points are in the convex hull defined by the returned vertices.
• The returned vertices are extreme points of the convex hull (no vertex is a convex combination of others).

Equations

• convexHullRationalPoints points = sorry

theorem convexHullRationalPoints_nodup (points : List RationalPoint) : (convexHullRationalPoints points).Nodup

def ConvexPolygon.ofList (vertices : List RationalPoint) : Option ConvexPolygon

Construct a ConvexPolygon from a list of points by removing duplicates and keeping only extreme points of the convex hull. returns none if there are fewer than 3 extreme points.

Equations

• ConvexPolygon.ofList vertices = sorry

def ConvexPolygon.toHalfSpaces (poly : ConvexPolygon) : Option (List ClosedHalfSpace)

Returns a list of closed half-spaces corresponding to the edges of the convex polygon. If there are fewer than 3 vertices, returns none.

Equations

• One or more equations did not get rendered due to their size.

def ConvexPolygon.ofHalfSpaces (halfSpaces : List ClosedHalfSpace) : Option ConvexPolygon

Given a collection of half-spaces, construct the convex polygon defined by their intersection. This is determined by taking all intersections of the boundary lines of pairs of half-spaces, and then filtering to those that satisfy all half-space constraints.

Equations

• One or more equations did not get rendered due to their size.

def ConvexPolygon.contains (poly : ConvexPolygon) (p : RationalPoint) : Bool

Decide whether the point p lies in the convex polygon poly.

Equations

• poly.contains p = match poly.toHalfSpaces with | none => false | some halfSpaces => halfSpaces.all fun (h : ClosedHalfSpace) => h.contains p

def ConvexPolygon.isSubsetOf (p q : ConvexPolygon) : Bool

Decide whether every vertex of p lies in q, witnessing p ⊆ q for convex polygons.

Equations

• p.isSubsetOf q = p.vertex_list.all fun (v : RationalPoint) => q.contains v

def ConvexPolygon.shrink (poly : ConvexPolygon) (dist tolerance : ℚ) (hdist : 0 < dist) (htol : 0 < tolerance) : Option ConvexPolygon

Shrink a convex polygon by moving each edge inward by at least dist (in the normal direction). and at most dist + tolerance (to account for numerical issues).

Equations

• One or more equations did not get rendered due to their size.