Supplied planar orthogonal drawings of finite incidence graphs

Drawing data are a finite list of integer vertex positions and a finite list of polygonal routes. Positions follow the declared vertex list and routes follow the edge list, including parallel edge occurrences. All geometric conditions refer to complete real segment supports. The drawing predicate uses loopless graphs with distinct declared vertex labels.

Edge orientation in the input list is immaterial: an incidence route may be listed in either direction. Its endpoints must be the actual incident vertices. Routes are simple, orthogonal, avoid nonincident vertices, and meet other routes only at shared incident vertices.

Main definitions

• Cslib.Complexity.Graph.OrthogonalDrawing: finite position and route data.
• Cslib.Complexity.Graph.drawingPosition: the displayed point of a declared vertex.
• Cslib.Complexity.Graph.IsPlanarOrthogonalDrawing: the geometric embedding certificate.
• Cslib.Complexity.Graph.drawingFits: bounds on all listed integer coordinates.
• Cslib.Complexity.Graph.drawingWireLength, Cslib.Complexity.Graph.drawingSegmentCount: explicit geometric output costs.

References

These are the ordinary finite drawing conditions, expressed using Mathlib real segments and the existing listed graph representation.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.OrthogonalDrawing : Type

Vertex positions and edge routes, in their graph-list orders. No graph data are duplicated.

def Cslib.Complexity.Graph.drawingPosition (G : Graph) (d : OrthogonalDrawing) (v : ℕ) : Orthogonal.Point

Displayed position of a declared vertex, using its first position in the vertex list.

structure Cslib.Complexity.Graph.IsPlanarOrthogonalDrawing (G : Graph) (d : OrthogonalDrawing) : Prop

A supplied planar orthogonal embedding of the loopless listed graph. Parallel listed edges have distinct simple routes; all contacts are tested in the real plane.

• vertexCount : d.1.length = G.vertices.length

  Exactly one position per declared vertex.

• edgeCount : d.2.length = G.edges.length

  Exactly one route per listed edge occurrence.

• labelsNodup : G.vertices.Nodup

  Labels describe distinct vertices.

• positionsNodup : d.1.Nodup

  Distinct declared vertices have distinct positions.

• endpointsDeclared (e : ℕ × ℕ) : e ∈ G.edges → e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices

  Both endpoints of every edge are declared.

• loopless (e : ℕ × ℕ) : e ∈ G.edges → e.1 ≠ e.2

  This interface concerns loopless graphs.

• endpoints (i : ℕ) (hi : i < G.edges.length) : let r := d.2.getD i []; let a := G.drawingPosition d G.edges[i].1; let b := G.drawingPosition d G.edges[i].2; List.head? r = some a ∧ List.getLast? r = some b ∨ List.head? r = some b ∧ List.getLast? r = some a

  Route endpoints are the incident vertices, in either order.

• orthogonal (i : ℕ) : i < G.edges.length → Orthogonal.IsOrthogonal (d.2.getD i [])

  Every segment is nondegenerate and axis aligned.

• simple (i : ℕ) : i < G.edges.length → Orthogonal.IsSimple (d.2.getD i [])

  Every route has no retracing, repeated points, or self-crossing.

• avoidsVertices (i : ℕ) (hi : i < G.edges.length) (v : ℕ) : v ∈ G.vertices → Orthogonal.realPoint (G.drawingPosition d v) ∈ Orthogonal.support (d.2.getD i []) → v = G.edges[i].1 ∨ v = G.edges[i].2

  A route visits only its incident graph vertices.

• contacts (i : ℕ) (hi : i < G.edges.length) (j : ℕ) (hj : j < G.edges.length) : i ≠ j → ∀ p ∈ Orthogonal.support (d.2.getD i []), p ∈ Orthogonal.support (d.2.getD j []) → ∃ v ∈ G.vertices, (v = G.edges[i].1 ∨ v = G.edges[i].2) ∧ (v = G.edges[j].1 ∨ v = G.edges[j].2) ∧ p = Orthogonal.realPoint (G.drawingPosition d v)

  Distinct routes intersect only at common graph endpoints.

def Cslib.Complexity.Graph.drawingFits (d : OrthogonalDrawing) (width height : ℕ) : Prop

Every listed position and route point lies in the nonnegative integer rectangle.

theorem Cslib.Complexity.Graph.drawingFits_mono {d : OrthogonalDrawing} {w h w' h' : ℕ} (hd : drawingFits d w h) (hw : w ≤ w') (hh : h ≤ h') : drawingFits d w' h'

A larger rectangle preserves bounds on every displayed vertex and route point.

def Cslib.Complexity.Graph.drawingWireLength (d : OrthogonalDrawing) : ℕ

The sum of Manhattan lengths of all incidence routes.

def Cslib.Complexity.Graph.drawingSegmentCount (d : OrthogonalDrawing) : ℕ

The number of consecutive segments in all incidence routes.