Working Set Invariants

This file defines the WorkingSet type with its three invariants.

structure Moser.WorkingSet : Type

The working set of polygons maintained during the algorithm

• polygons : List ConvexPolygon

  The set of candidate polygons

def Moser.WorkingSet.initial : WorkingSet

Create initial working set with just the InitialWorm

Equations

• Moser.WorkingSet.initial = { polygons := [Moser.InitialWorm] }

def Moser.WorkingSet.isEmpty (s : WorkingSet) : Bool

Check if the working set is empty

Equations

• s.isEmpty = s.polygons.isEmpty

def Moser.WorkingSet.minAreaPolygon (s : WorkingSet) : Option ConvexPolygon

Get the polygon with minimum area

Equations

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

def Moser.WorkingSet.minArea (s : WorkingSet) : ℚ

Get the minimum area in the working set

Equations

• s.minArea = match s.minAreaPolygon with | none => 0 | some p => p.area

def Moser.WorkingSet.size (s : WorkingSet) : ℕ

Count the number of polygons

Equations

• s.size = s.polygons.length