Integer points and local neighborhoods of orthogonal unit paths

Main definitions

• Cslib.Orthogonal.StraightThrough: a consecutive three-point neighborhood in either direction.

Main results

• Cslib.Orthogonal.mem_iff_realPoint_mem_support: for unit paths, integer support membership is exactly membership in the finite listed-point data.
• Cslib.Orthogonal.StraightThrough.getD_neighbors: exact indexed predecessor/successor lookups.
• Cslib.Orthogonal.subdivide_horizontal, .subdivide_vertical: strict interior grid points retain consecutive straight neighborhoods after subdivision.
• Cslib.Orthogonal.point_bounds_of_mem_support: listed-point bounds hold on all integer support.

References

These are original finite-list proofs of elementary lattice-segment facts.

def Cslib.Orthogonal.StraightThrough (r : Route) (p d : Point) : Prop

A unit path passes straight through p, with its two immediate neighbors p-d and p+d. The three points occur consecutively, in either orientation.

theorem Cslib.Orthogonal.eq_endpoint_of_mem_unit_segment {a b p : Point} (hab : length a b = 1) (hp : realPoint p ∈ segment a b) : p = a ∨ p = b

An integer point on a unit segment is one of its endpoints.

theorem Cslib.Orthogonal.mem_iff_realPoint_mem_support {r : Route} (hr : ∀ e ∈ List.consecutivePairs r, length e.1 e.2 = 1) (p : Point) : p ∈ r ↔ realPoint p ∈ support r

A finite unit path lists every integer point in its continuous real support.

theorem Cslib.Orthogonal.point_bounds_of_mem_support {r : Route} (hr : IsOrthogonal r) {w h : ℤ} (hb : ∀ p ∈ r, 0 ≤ p.1 ∧ p.1 ≤ w ∧ 0 ≤ p.2 ∧ p.2 ≤ h) {p : Point} (hp : realPoint p ∈ support r) : 0 ≤ p.1 ∧ p.1 ≤ w ∧ 0 ≤ p.2 ∧ p.2 ≤ h

A rectangle containing every listed point also contains every integer point of the continuous orthogonal support.

theorem Cslib.Orthogonal.StraightThrough.neg {r : Route} {p d : Point} (h : StraightThrough r p d) : StraightThrough r p (-d)

Changing the sign only interchanges the two orientations of a straight neighborhood.

theorem Cslib.Orthogonal.StraightThrough.infix {r s : Route} {p d : Point} (h : StraightThrough r p d) (hrs : r <:+: s) : StraightThrough s p d

A straight neighborhood remains consecutive inside any larger list containing the path.

theorem Cslib.Orthogonal.StraightThrough.getD_neighbors {r : Route} {p d : Point} (ht : StraightThrough r p d) (hn : List.Nodup r) {k : ℕ} (hk : k < List.length r) (heq : r[k] = p) : 0 < k ∧ k + 1 < List.length r ∧ (List.getD r (k - 1) p = p - d ∧ List.getD r (k + 1) p = p + d ∨ List.getD r (k - 1) p = p + d ∧ List.getD r (k + 1) p = p - d)

The consecutive neighborhood gives the exact predecessor/successor lookups used by finite wire compilers, at every valid occurrence index of the middle point.

theorem Cslib.Orthogonal.walk_triple (a d : Point) {i k : ℕ} (hi : i + 2 ≤ k) : [a + i • d, a + (i + 1) • d, a + (i + 2) • d] <:+: walk a d k

Three successive steps of a finite walk form a consecutive sublist.

theorem Cslib.Orthogonal.walk_straight (a d : Point) {i k : ℕ} (hi : 0 < i) (hik : i < k) : StraightThrough (walk a d k) (a + i • d) d

Every non-endpoint index of a walk has its two immediately neighboring steps.

theorem Cslib.Orthogonal.segmentWalk_straight {a b p : Point} (haxis : a.1 = b.1 ∨ a.2 = b.2) (hp : realPoint p ∈ segment a b) (hpa : p ≠ a) (hpb : p ≠ b) : StraightThrough (segmentWalk a b) p (direction a b)

A strict interior integer point of an axis-aligned segment has both neighboring unit points consecutively present in that segment's subdivision.

theorem Cslib.Orthogonal.segmentWalk_horizontal {a b p : Point} (hab : a.2 = b.2) (hp : p.2 = a.2) (hx : min a.1 b.1 < p.1 ∧ p.1 < max a.1 b.1) : StraightThrough (segmentWalk a b) p (1, 0)

A horizontal segment is traversed horizontally at every strict interior grid point.

theorem Cslib.Orthogonal.segmentWalk_vertical {a b p : Point} (hab : a.1 = b.1) (hp : p.1 = a.1) (hy : min a.2 b.2 < p.2 ∧ p.2 < max a.2 b.2) : StraightThrough (segmentWalk a b) p (0, 1)

A vertical segment is traversed vertically at every strict interior grid point.

theorem Cslib.Orthogonal.segmentWalk_infix_subdivide {r : Route} (hr : IsOrthogonal r) {e : Point × Point} (he : e ∈ List.consecutivePairs r) : segmentWalk e.1 e.2 <:+: subdivide r

Every original segment's complete unit walk occurs consecutively in the subdivided route.

theorem Cslib.Orthogonal.subdivide_horizontal {r : Route} (hr : IsOrthogonal r) {e : Point × Point} (he : e ∈ List.consecutivePairs r) {p : Point} (hab : e.1.2 = e.2.2) (hp : p.2 = e.1.2) (hx : min e.1.1 e.2.1 < p.1 ∧ p.1 < max e.1.1 e.2.1) : StraightThrough (subdivide r) p (1, 0)

Horizontal strict interior neighborhoods survive subdivision of an entire route.

theorem Cslib.Orthogonal.subdivide_vertical {r : Route} (hr : IsOrthogonal r) {e : Point × Point} (he : e ∈ List.consecutivePairs r) {p : Point} (hab : e.1.1 = e.2.1) (hp : p.1 = e.1.1) (hy : min e.1.2 e.2.2 < p.2 ∧ p.2 < max e.1.2 e.2.2) : StraightThrough (subdivide r) p (0, 1)

Vertical strict interior neighborhoods survive subdivision of an entire route.