Finite certificates for contacts of polygonal routes

Two axis-aligned closed segments have rectangular bounding boxes whose intersection is empty, a singleton, or an overlapping segment. The Boolean checker accepts the first two cases when the singleton is an allowed contact point. Its soundness refers to the entire real segments. In fact, the sufficient bounding-box criterion is sound even for diagonal segments.

The route checker includes a degenerate segment for every listed point, so its soundness also covers empty and singleton routes. In particular, checking against a singleton route certifies that an incidence route avoids a nonincident vertex.

Main definitions

• Cslib.Orthogonal.consecutiveContact: permitted shared bend between two segments.
• Cslib.Orthogonal.segmentContactCheck: check permitted contacts between two closed segments.
• Cslib.Orthogonal.routeBoxDisjoint: check whether two route bounding boxes are disjoint.
• Cslib.Orthogonal.routeContactCheck: check permitted contacts between continuous route supports.

Main results

• Cslib.Orthogonal.segmentContactCheck_sound: every real intersection is an allowed grid point.
• Cslib.Orthogonal.isSimple_of_segmentContactCheck: consecutive-bend checks prove simplicity.
• Cslib.Orthogonal.disjoint_support_of_routeBoxDisjoint: disjoint route boxes have disjoint continuous supports.
• Cslib.Orthogonal.routeContactCheck_sound: the corresponding certificate for route supports.
• Cslib.Orthogonal.disjoint_support_of_routeContactCheck: an empty contact list proves disjointness.
• Cslib.Orthogonal.not_mem_support_of_routeContactCheck: a singleton check excludes a vertex.
• Cslib.Orthogonal.routeContactCheck_ite_sound: a conditional single-contact check identifies the only possible contact.

References

This finite bounding-box certificate is an elementary geometric construction.

def Cslib.Orthogonal.consecutiveContact (a b : Point × Point) : List Point

A pair of different segments may meet only at a consecutive shared bend.

def Cslib.Orthogonal.segmentContactCheck (allowed : List Point) (a b c d : Point) : Bool

A finite sufficient test that two segments meet only at listed grid points. It accepts disjoint bounding boxes or a singleton intersection belonging to allowed.

theorem Cslib.Orthogonal.segmentContactCheck_sound {allowed : List Point} {a b c d : Point} (h : segmentContactCheck allowed a b c d = true) {p : ℝ × ℝ} (hab : p ∈ segment a b) (hcd : p ∈ segment c d) : ∃ q ∈ allowed, p = realPoint q

The finite checker controls every real intersection, not only lattice intersections.

theorem Cslib.Orthogonal.isSimple_of_segmentContactCheck {r : Route} (hnodup : List.Nodup r) (h : ∀ a ∈ List.consecutivePairs r, ∀ b ∈ List.consecutivePairs r, a ≠ b → segmentContactCheck (consecutiveContact a b) a.1 a.2 b.1 b.2 = true) : IsSimple r

A route without repeated listed points is simple when every pair of distinct segments passes the contact check whose only allowed contact is their consecutive shared bend.

def Cslib.Orthogonal.segmentPieces (r : Route) : List (Point × Point)

Segment pieces for a route, including degenerate pieces for isolated listed points.

theorem Cslib.Orthogonal.mem_support_iff_segmentPieces {r : Route} {p : ℝ × ℝ} : p ∈ support r ↔ ∃ e ∈ segmentPieces r, p ∈ segment e.1 e.2

Continuous route support is exactly the union of its finite segment pieces.

def Cslib.Orthogonal.coordMin (f : Point → ℤ) (p : Point) : Route → ℤ

Minimum of a coordinate projection along a nonempty route p :: r.

def Cslib.Orthogonal.coordMax (f : Point → ℤ) (p : Point) : Route → ℤ

Maximum of a coordinate projection along a nonempty route p :: r.

def Cslib.Orthogonal.routeBoxDisjoint : Route → Route → Bool

Check whether the integer coordinate bounding boxes of two routes are disjoint. Empty routes have empty support, so their bounding boxes are treated as disjoint.

theorem Cslib.Orthogonal.disjoint_support_of_routeBoxDisjoint {r s : Route} (h : routeBoxDisjoint r s = true) : Disjoint (support r) (support s)

Disjoint integer route bounding boxes certify disjoint continuous supports.

def Cslib.Orthogonal.routeContactCheck (allowed : List Point) (r s : Route) : Bool

Check whether two routes have disjoint bounding boxes or all finite segment-piece pairs have only permitted contacts.

theorem Cslib.Orthogonal.routeContactCheck_sound {allowed : List Point} {r s : Route} (h : routeContactCheck allowed r s = true) {p : ℝ × ℝ} (hr : p ∈ support r) (hs : p ∈ support s) : ∃ q ∈ allowed, p = realPoint q

Every real intersection of the route supports is one of the allowed grid points.

theorem Cslib.Orthogonal.disjoint_support_of_routeContactCheck {r s : Route} (h : routeContactCheck [] r s = true) : Disjoint (support r) (support s)

An empty permitted-contact list certifies disjoint continuous supports.

theorem Cslib.Orthogonal.not_mem_support_of_routeContactCheck {r : Route} {q : Point} (h : routeContactCheck [] r [q] = true) : realPoint q ∉ support r

Testing against a singleton route certifies that a route avoids a specified vertex.

theorem Cslib.Orthogonal.routeContactCheck_ite_sound {P : Prop} [Decidable P] {q : Point} {r s : Route} (h : routeContactCheck (if P then [q] else []) r s = true) {p : ℝ × ℝ} (hr : p ∈ support r) (hs : p ∈ support s) : P ∧ p = realPoint q

A check that allows the single contact q exactly when P holds: any real contact proves P and is q. This is the usual form of an access-to-terminal certificate.