Sweep-line segment intersection detection

42 fully proved

Non-vertical segments as graphs

DefinitionHeight of a line at an abscissa#✓fully proved

For points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) in \(K^2\), \(K\) a field, and \(x \in K\), this is \(p_2 + (x - p_1)(q_2 - p_2)/(q_1 - p_1)\), with division by zero read as \(0\). When \(p_1 \ne q_1\) it is the height at \(x\) of the line through \(p\) and \(q\).

def lineY (p q : 𝕜 × 𝕜) (x : 𝕜) : 𝕜 := p.2 + (x - p.1) * (q.2 - p.2) / (q.1 - p.1)

Used by 12

Used byDIRECTION as a scaled vertical offset · Leftmost point of the intersection of two segments · Crossing of two non-vertical segments · A non-vertical segment is the graph of its line · The sweep order holds weakly at the leftmost intersection · The sweep order persists before the leftmost intersection · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events

TheoremA non-vertical segment is the graph of its line#✓fully proved

Let \(p\) and \(q\) be points of the plane over a linearly ordered field, where a point \(z\) has coordinates \((z_1, z_2)\), and suppose \(p_1 < q_1\). A point \(z\) lies on the segment from \(p\) to \(q\) if and only if \(p_1 \le z_1 \le q_1\) and \(z_2\) is the height at abscissa \(z_1\) of the line through \(p\) and \(q\).

theorem mem_segment_iff_lineY {p q z : 𝕜 × 𝕜} (hpq : p.1 < q.1) :
    z ∈ segment 𝕜 p q ↔ p.1 ≤ z.1 ∧ z.1 ≤ q.1 ∧ z.2 = lineY p q z.1

Uses 1 · Used by 6

Statement usesHeight of a line at an abscissa

Used byLeftmost point of the intersection of two segments · Crossing of two non-vertical segments · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Phase one: the status list is strictly sorted between the processed and remaining events

TheoremDIRECTION as a scaled vertical offset#✓fully proved

Let \(\Bbbk\) be a field with a linear order, let \(p, q, r \in \Bbbk^2\), writing \(p = (p_x, p_y)\) and likewise for \(q\) and \(r\), with \(p_x < q_x\), and let \(y_{pq}(x)\) be the height at \(x\) of the line through \(p\) and \(q\). Then \(\mathrm{DIRECTION}(p, q, r) = (q_x - p_x)\,(y_{pq}(r_x) - r_y)\).

theorem direction_eq_lineY {p q : 𝕜 × 𝕜} (hpq : p.1 < q.1) (r : 𝕜 × 𝕜) :
    direction p q r = (q.1 - p.1) * (lineY p q r.1 - r.2)

Uses 2 · Used by 3

Statement usesDirection of three points · Height of a line at an abscissa

Used bySweep completeness when the leftmost intersection is a left endpoint · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · Phase one: the status list is strictly sorted between the processed and remaining events

TheoremCrossing of two non-vertical segments#✓fully proved

Let \(K\) be a linearly ordered field, write \(z_1\) for the first coordinate of a point \(z \in K^2\), and let \([p, q]\) and \([p', q']\) be segments in \(K^2\) with \(p_1 < q_1\) and \(p'_1 < q'_1\). For \(t \in K\) let \(y(t)\) be the height at \(t\) of the line through \(p\) and \(q\), and \(y'(t)\) that of the line through \(p'\) and \(q'\). Let \(a < b\) with \(p_1 \le a\), \(p'_1 \le a\), \(b \le q_1\) and \(b \le q'_1\). If \(y(a) < y'(a)\) and \(y'(b) \le y(b)\), then some \(z \in [p, q] \cap [p', q']\) has \(a < z_1 \le b\), and \(z_1 < b\) if moreover \(y'(b) < y(b)\).

theorem exists_mem_inter_of_cross {p q p' q' : 𝕜 × 𝕜} (hpq : p.1 < q.1) (hpq' : p'.1 < q'.1)
    {x₀ x₁ : 𝕜} (hx : x₀ < x₁) (hp : p.1 ≤ x₀) (hq : x₁ ≤ q.1) (hp' : p'.1 ≤ x₀)
    (hq' : x₁ ≤ q'.1) (h₀ : lineY p q x₀ < lineY p' q' x₀)
    (h₁ : lineY p' q' x₁ ≤ lineY p q x₁) :
    ∃ z ∈ segment 𝕜 p q ∩ segment 𝕜 p' q', x₀ < z.1 ∧ z.1 ≤ x₁ ∧
      (lineY p' q' x₁ < lineY p q x₁ → z.1 < x₁)

Uses 2 · Used by 2

Statement usesHeight of a line at an abscissa

Proof usesA non-vertical segment is the graph of its line

Used byThe sweep order holds weakly at the leftmost intersection · The sweep order persists before the leftmost intersection

TheoremLeftmost point of the intersection of two segments#✓fully proved

Let \(K\) be a linearly ordered field, write \(x_1\) for the first coordinate of a point \(x \in K^2\), and let \([p, q]\) and \([p', q']\) be segments in \(K^2\) with \(p_1 < q_1\) and \(p'_1 < q'_1\). If \([p, q] \cap [p', q']\) is nonempty, then it contains a point \(m\) with \(m_1 \le w_1\) for every \(w \in [p, q] \cap [p', q']\).

theorem exists_leftmost_mem_inter {p q p' q' z : 𝕜 × 𝕜} (hpq : p.1 < q.1) (hpq' : p'.1 < q'.1)
    (hz : z ∈ segment 𝕜 p q ∩ segment 𝕜 p' q') :
    ∃ m ∈ segment 𝕜 p q ∩ segment 𝕜 p' q', ∀ w ∈ segment 𝕜 p q ∩ segment 𝕜 p' q', m.1 ≤ w.1

Uses 2 · Used by 1

Proof usesHeight of a line at an abscissa · A non-vertical segment is the graph of its line

Used byA leftmost intersection point

Sorted lists of graphs

TheoremInserting into a strictly sorted list#✓fully proved

Let \(f\) map a type \(\alpha\) to a linearly ordered set, let \(T\) be a list over \(\alpha\) with \(f(j) < f(k)\) whenever \(j\) occurs before \(k\), let \(i \in \alpha\) be such that \(f(j) \ne f(i)\) for every \(j\) in \(T\), and let \(P\) be a predicate that holds for an element \(j\) of \(T\) exactly when \(f(j) < f(i)\). Insert \(i\) just before the first element of \(T\) not satisfying \(P\): the list made of the longest prefix of \(T\) satisfying \(P\), then \(i\), then the rest of \(T\). In this list, \(f(j) < f(k)\) whenever \(j\) occurs before \(k\).

theorem pairwise_takeWhile_append_cons_dropWhile_lt {T : List α} {i : α} (p : α → Bool)
    (hp : ∀ j ∈ T, p j = true ↔ f j < f i) (hT : T.Pairwise (fun j k => f j < f k))
    (hne : ∀ j ∈ T, f j ≠ f i) :
    (T.takeWhile p ++ i :: T.dropWhile p).Pairwise (fun j k => f j < f k)

Used by 1

Used byPhase one: the status list is strictly sorted between the processed and remaining events

TheoremInserting into a weakly sorted list#✓fully proved

Let \(f\) map a type \(\alpha\) to a linearly ordered set, let \(T\) be a list over \(\alpha\) with \(f(j) \le f(k)\) whenever \(j\) occurs before \(k\), let \(i \in \alpha\), and let \(P\) be a predicate that holds for an element \(j\) of \(T\) exactly when \(f(j) < f(i)\). Insert \(i\) just before the first element of \(T\) not satisfying \(P\): the list made of the longest prefix of \(T\) satisfying \(P\), then \(i\), then the rest of \(T\). In this list, \(f(j) \le f(k)\) whenever \(j\) occurs before \(k\).

theorem pairwise_takeWhile_append_cons_dropWhile_le {T : List α} {i : α} (p : α → Bool)
    (hp : ∀ j ∈ T, p j = true ↔ f j < f i) (hT : T.Pairwise (fun j k => f j ≤ f k)) :
    (T.takeWhile p ++ i :: T.dropWhile p).Pairwise (fun j k => f j ≤ f k)

Used by 1

Used byPhase two: inserting left endpoints on a vertical line keeps the status weakly sorted

TheoremFirst element at or above a uniquely attained height#✓fully proved

Let \(f\) map a type to a linearly ordered set, let \(y\) be a value, and let \(T\) be a list sorted non-strictly by \(f\), that is, \(f(j) \le f(k)\) whenever \(j\) occurs before \(k\) in \(T\). Suppose \(b\) lies in \(T\) with \(f(b) = y\), and every element \(c \ne b\) of \(T\) has \(f(c) \ne y\). Then removing from \(T\) its longest prefix of elements \(j\) with \(f(j) < y\) leaves a list whose first element is \(b\).

theorem head?_dropWhile_eq_of_unique {T : List α} {b : α} (p : α → Bool)
    (hp : ∀ j ∈ T, p j = true ↔ f j < y) (hT : T.Pairwise (fun j k => f j ≤ f k)) (hb : b ∈ T)
    (hfb : f b = y) (huniq : ∀ c ∈ T, c ≠ b → f c ≠ y) :
    (T.dropWhile p).head? = some b

Used by 1

Used bySweep completeness when the leftmost intersection is a left endpoint

TheoremSplitting a list at two distinct members#✓fully proved

If \(a\) and \(b\) are distinct members of a list \(T\), then there are elements \(u\), \(w\) with either \(u = a\) and \(w = b\), or \(u = b\) and \(w = a\), and lists \(A\), \(M\), \(B\) such that \(T\) is the concatenation of \(A\), the element \(u\), \(M\), the element \(w\) and \(B\), in this order.

theorem exists_append_of_mem_of_mem {T : List α} {a b : α} (ha : a ∈ T) (hb : b ∈ T)
    (hab : a ≠ b) :
    ∃ u w A M B, (u = a ∧ w = b ∨ u = b ∧ w = a) ∧ T = A ++ u :: (M ++ w :: B)

Used by 1

Used bySweep completeness when the leftmost intersection is inside both segments

The algorithm

DefinitionLeft endpoint of a segment#✓fully proved

Let \(K\) be a linearly ordered set and \(S\) a family of segments in \(K^2\), segment \(i\) being given by its two endpoints \((a, b)\) in either order. The left endpoint of segment \(i\) is \(a\) if \(a_1 \le b_1\) and \(b\) otherwise, where \(a_1\) and \(b_1\) are the first coordinates.

def left (i : Fin n) : 𝕜 × 𝕜 := if (S i).1.1 ≤ (S i).2.1 then (S i).1 else (S i).2

Used by 21

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Segment strictly below a point · A leftmost intersection point · Soundness of the any-segments-intersect sweep · Left endpoint events precede right endpoint events · Meeting segments · The sweep order holds weakly at the leftmost intersection · The sweep order persists before the leftmost intersection · Endpoint of an event · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events · One step of the sweep · The any-segments-intersect sweep · Intersection test for two input segments

DefinitionRight endpoint of a segment#✓fully proved

Write \(z_1\) for the abscissa of a point \(z\). If segment \(i\) is given by the endpoints \(u\) and \(v\), in this order, its right endpoint is \(v\) when \(u_1 \le v_1\) and \(u\) otherwise.

def right (i : Fin n) : 𝕜 × 𝕜 := if (S i).1.1 ≤ (S i).2.1 then (S i).2 else (S i).1

Used by 18

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Segment strictly below a point · A leftmost intersection point · Soundness of the any-segments-intersect sweep · Left endpoint events precede right endpoint events · Meeting segments · The sweep order holds weakly at the leftmost intersection · The sweep order persists before the leftmost intersection · Endpoint of an event · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events · Intersection test for two input segments

AbbreviationSweep event#✓fully proved

For \(n\) segments indexed by \(0, \dots, n-1\), an event is a pair \((i, b)\) of a segment index \(i\) and a Boolean \(b\); it stands for the left endpoint of segment \(i\) when \(b\) is true and for its right endpoint when \(b\) is false.

abbrev Event (n : ℕ) := Fin n × Bool

Used by 19

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Cost charged to a sweep event · Sorted sweep events · Soundness of the any-segments-intersect sweep · Sweep order on endpoint events · A sweep prefix with a right endpoint has its left endpoint · Endpoint of an event · Running the sweep over a list of events · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events · One step of the sweep · The any-segments-intersect sweep

DefinitionEndpoint of an event#✓fully proved

The point of the sweep event \((i, b)\) is the left endpoint of segment \(i\) when \(b\) is true (a left-endpoint event) and the right endpoint of segment \(i\) when \(b\) is false.

def point (e : Event n) : 𝕜 × 𝕜 := if e.2 then left S e.1 else right S e.1

Uses 3 · Used by 8

Statement usesSweep event · Left endpoint of a segment · Right endpoint of a segment

Used bySweep order on endpoint events · Left endpoint events precede right endpoint events · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events

DefinitionSweep order on endpoint events#✓fully proved

Let \(K\) be a linearly ordered set and \(S\) a family of segments in \(K^2\), each given by its two endpoints. An endpoint event \(e\) of \(S\) standing for the point \((x, y)\) gets the key \((x, \varepsilon, y)\), compared lexicographically, where \(\varepsilon = 0\) if \(e\) is a left endpoint and \(\varepsilon = 1\) if it is a right endpoint. So events are ordered by \(x\); at equal \(x\), left endpoints come first; then by \(y\). This is the endpoint order of CLRS.

def key (e : Event n) : 𝕜 ×ₗ (ℕ ×ₗ 𝕜) :=
  toLex ((point S e).1, toLex (if e.2 then 0 else 1, (point S e).2))

Uses 2 · Used by 12

Statement usesSweep event · Endpoint of an event

Used byRunning time of ANY-SEGMENTS-INTERSECT · Sorted sweep events · Soundness of the any-segments-intersect sweep · Left endpoint events precede right endpoint events · A sweep prefix with a right endpoint has its left endpoint · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events

DefinitionSorted sweep events#✓fully proved

For \(n\) segments, each given by its two endpoints, the left endpoint of a segment is its endpoint with the smaller \(x\)-coordinate, or its first given endpoint when both \(x\)-coordinates agree, and the right endpoint is the other one. The event list consists of the \(2n\) events, the left and the right endpoint of each segment, sorted by the \(x\)-coordinate of the endpoint, with left endpoints before right endpoints at equal \(x\), and then by the \(y\)-coordinate of the endpoint; events that tie appear in increasing order of segment index. This is line 2 of CLRS ANY-SEGMENTS-INTERSECT.

def events : List (Event n) :=
  ((List.finRange n).map (·, true) ++ (List.finRange n).map (·, false)).mergeSort
    fun e f => decide (key S e ≤ key S f)

Uses 2 · Used by 13

Statement usesSweep event · Sweep order on endpoint events

Used byANY-SEGMENTS-INTERSECT · Correctness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · A sweep prefix with a right endpoint has its left endpoint · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events

DefinitionSegment strictly below a point#✓fully proved

For a segment \(j\), write \(l_j\) for its endpoint with the smaller \(x\)-coordinate, or for its first given endpoint when both \(x\)-coordinates agree, and \(r_j\) for its other endpoint. For a point \(q\), segment \(j\) is below \(q\) when \(\mathrm{DIRECTION}(l_j, r_j, q) < 0\).

For a non-vertical segment this says that the line through \(l_j\) and \(r_j\) passes strictly below \(q\) at the abscissa of \(q\).

def below (j : Fin n) (q : 𝕜 × 𝕜) : Bool := decide (direction (left S j) (right S j) q < 0)

Uses 3 · Used by 10

Statement usesLeft endpoint of a segment · Right endpoint of a segment · Direction of three points

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Sweep completeness when the leftmost intersection is a left endpoint · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · Phase one: the status list is strictly sorted between the processed and remaining events · One step of the sweep · The any-segments-intersect sweep

DefinitionIntersection test for two input segments#✓fully proved

Given \(n\) segments in the plane over a linearly ordered field, each given by its two endpoints, and indices \(i, j < n\), this runs CLRS SEGMENTS-INTERSECT on the left and right endpoints of segment \(i\) and the left and right endpoints of segment \(j\). It returns that procedure's Boolean answer together with its cost in DIRECTION and ON-SEGMENT evaluations.

def test (i j : Fin n) : TimeM ℕ Bool :=
  segmentsIntersect (left S i) (right S i) (left S j) (right S j)

Uses 3 · Used by 6

Statement usesLeft endpoint of a segment · Right endpoint of a segment · The SEGMENTS-INTERSECT procedure

Used byRunning time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Sweep completeness when the leftmost intersection is a left endpoint · Neighbours on the sweep status are disjoint · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment

DefinitionTesting a segment against an optional neighbour#✓fully proved

Given a segment \(i\) and possibly a neighbour \(j\), return the result of SEGMENTS-INTERSECT on segments \(i\) and \(j\), with its cost, when \(j\) is given, and return false at no cost when there is no neighbour.

def testOpt (i : Fin n) : Option (Fin n) → TimeM ℕ Bool
  | none => pure false
  | some j => test S i j

Uses 1 · Used by 10

Statement usesIntersection test for two input segments

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Sweep completeness when the leftmost intersection is a left endpoint · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · Phase one: the status list is strictly sorted between the processed and remaining events · One step of the sweep · The any-segments-intersect sweep

DefinitionTesting the neighbours of a deleted segment#✓fully proved

Given \(n\) segments in the plane over a linearly ordered field and two optional segment indices \(a\) and \(b\) (in the sweep, the segments just below and just above a deleted segment, when they exist), this runs the intersection test of segments \(a\) and \(b\) when both indices are present, and otherwise returns false at no cost.

def testPair : Option (Fin n) → Option (Fin n) → TimeM ℕ Bool
  | some a, some b => test S a b
  | _, _ => pure false

Uses 1 · Used by 8

Statement usesIntersection test for two input segments

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase one: the status list is strictly sorted between the processed and remaining events · One step of the sweep · The any-segments-intersect sweep

DefinitionThe any-segments-intersect sweep#✓fully proved

CLRS ANY-SEGMENTS-INTERSECT, lines 3-11: the sweep processes a list of events with a status list \(T\) of segments ordered from bottom to top, returns true as soon as an intersection test succeeds, and returns false once the events run out. At the left endpoint \(p\) of segment \(i\), split \(T\) as \(A\) followed by \(B\), where \(A\) is the longest initial part of \(T\) whose segments pass strictly below \(p\) by the DIRECTION test; this scan costs \(\min(|A| + 1, |T|)\), one DIRECTION per segment scanned. Segment \(i\) is tested with SEGMENTS-INTERSECT against the first segment of \(B\) and then against the last segment of \(A\) (when these exist), and the sweep continues with \(A\), then \(i\), then \(B\). At the right endpoint of segment \(i\), with \(A\) the part of \(T\) before the first occurrence of \(i\) and \(B\) the part after it, the last segment of \(A\) is tested against the first segment of \(B\) when both exist, and the sweep continues with \(A\) followed by \(B\).

def sweep : List (Event n) → List (Fin n) → TimeM ℕ Bool
  | [], _ => pure false
  | (i, true) :: es, T => do
      ✓[min ((T.takeWhile (below S · (left S i))).length + 1) T.length]
      let b₁ ← testOpt S i (T.dropWhile (below S · (left S i))).head?
      if b₁ then pure true else do
      let b₂ ← testOpt S i (T.takeWhile (below S · (left S i))).getLast?
      if b₂ then pure true else
      sweep es (T.takeWhile (below S · (left S i)) ++ i :: T.dropWhile (below S · (left S i)))
  | (i, false) :: es, T => do
      let b ← testPair S (T.takeWhile (· != i)).getLast? (T.dropWhile (· != i)).tail.head?
      if b then pure true else sweep es (T.takeWhile (· != i) ++ (T.dropWhile (· != i)).tail)

Uses 5 · Used by 3

Statement usesSweep event · Segment strictly below a point · Left endpoint of a segment · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment

Used byANY-SEGMENTS-INTERSECT · Correctness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT

DefinitionOne step of the sweep#✓fully proved

A step takes an event and a status list \(T\) of segments, ordered from bottom to top, and returns a new status list, or no result when an intersection is reported. At the left endpoint \(p\) of segment \(i\), split \(T\) as \(A\) followed by \(B\), where \(A\) is the longest initial part of \(T\) whose segments pass strictly below \(p\) by the DIRECTION test. If SEGMENTS-INTERSECT reports that \(i\) meets the first segment of \(B\) or the last segment of \(A\) (when these exist), there is no result; otherwise the new status list is \(A\), then \(i\), then \(B\). At the right endpoint of segment \(i\), let \(A\) be the part of \(T\) before the first occurrence of \(i\) and \(B\) the part after it (so \(A\) is all of \(T\) and \(B\) is empty when \(i\) does not occur). If both the last segment of \(A\) and the first segment of \(B\) exist and SEGMENTS-INTERSECT reports that they meet, there is no result; otherwise the new status list is \(A\) followed by \(B\).

def step : Event n → List (Fin n) → Option (List (Fin n))
  | (i, true), T =>
      if (testOpt S i (T.dropWhile (below S · (left S i))).head?).ret ||
          (testOpt S i (T.takeWhile (below S · (left S i))).getLast?).ret then none
      else some (T.takeWhile (below S · (left S i)) ++ i :: T.dropWhile (below S · (left S i)))
  | (i, false), T =>
      if (testPair S (T.takeWhile (· != i)).getLast? (T.dropWhile (· != i)).tail.head?).ret then
        none
      else some (T.takeWhile (· != i) ++ (T.dropWhile (· != i)).tail)

Uses 5 · Used by 9

Statement usesSweep event · Segment strictly below a point · Left endpoint of a segment · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment

Used byRunning time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Running the sweep over a list of events · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · Phase one: the status list is strictly sorted between the processed and remaining events

DefinitionRunning the sweep over a list of events#✓fully proved

Starting from a status list \(T\), the sweep steps are applied to the events in order, each to the status list left by the previous one. The result is the final status list, or no result as soon as some step reports an intersection; on the empty list of events the result is \(T\).

def run : List (Event n) → List (Fin n) → Option (List (Fin n))
  | [], T => some T
  | e :: es, T => (step S e T).bind (run es)

Uses 2 · Used by 11

Statement usesSweep event · One step of the sweep

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events

Endpoints and events

TheoremLeft endpoint events precede right endpoint events#✓fully proved

Let \(K\) be a linearly ordered set and \(S\) a family of segments in \(K^2\), each given by its two endpoints. For every segment \(i\) of \(S\), the left endpoint event of \(i\) is strictly smaller than its right endpoint event in the sweep order on events (by \(x\)-coordinate, then left endpoints before right endpoints, then by \(y\)-coordinate).

theorem key_left_lt_right (i : Fin n) : key S (i, true) < key S (i, false)

Uses 4 · Used by 1

Statement usesSweep order on endpoint events

Proof usesLeft endpoint of a segment · Endpoint of an event · Right endpoint of a segment

Used byA sweep prefix with a right endpoint has its left endpoint

TheoremA sweep prefix with a right endpoint has its left endpoint#✓fully proved

Let \(K\) be a linearly ordered set and \(S\) a family of \(n\) segments in \(K^2\), each given by its two endpoints. If the sorted sweep event list of \(S\) is a list \(P\) followed by a list \(Q\), and \(P\) contains the right endpoint event of a segment \(j\), then \(P\) also contains the left endpoint event of \(j\).

theorem left_mem_of_right_mem {P Q : List (Event n)} (hE : events S = P ++ Q) {j : Fin n}
    (hj : (j, false) ∈ P) : (j, true) ∈ P

Uses 4 · Used by 4

Statement usesSweep event · Sorted sweep events

Proof usesSweep order on endpoint events · Left endpoint events precede right endpoint events

Used bySoundness of the any-segments-intersect sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase one: the status list is strictly sorted between the processed and remaining events

Invariants of the status list

TheoremSplitting a list at the first occurrence of a member#✓fully proved

If \(i\) occurs in a list \(T\) of indices in \(\{0, \dots, n-1\}\), then \(T\) is the longest initial part of \(T\) not containing \(i\), followed by \(i\), followed by the part of \(T\) after the first occurrence of \(i\).

theorem takeWhile_append_cons_tail_dropWhile {T : List (Fin n)} {i : Fin n} (hi : i ∈ T) :
    T.takeWhile (· != i) ++ i :: (T.dropWhile (· != i)).tail = T

Used by 4

Used bySoundness of the any-segments-intersect sweep · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · Phase one: the status list is strictly sorted between the processed and remaining events

TheoremThe sweep status holds the active segments#✓fully proved

Let \(P\) be an initial part of the sorted list of events. If running the sweep over \(P\) from the empty status list reports no intersection and ends with status list \(T\), then \(T\) has no repeated entries, and a segment \(j\) belongs to \(T\) exactly when the left endpoint event of \(j\) is in \(P\) and the right endpoint event of \(j\) is not.

theorem run_mem_iff {P Q : List (Event n)} (hE : events S = P ++ Q) {T : List (Fin n)}
    (hT : run S P [] = some T) : T.Nodup ∧ ∀ j, j ∈ T ↔ (j, true) ∈ P ∧ (j, false) ∉ P

Uses 11 · Used by 7

Statement usesSweep event · Sorted sweep events · Running the sweep over a list of events

Proof usesSegment strictly below a point · Sweep order on endpoint events · Left endpoint of a segment · A sweep prefix with a right endpoint has its left endpoint · One step of the sweep · Splitting a list at the first occurrence of a member · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment

Used byRunning time of ANY-SEGMENTS-INTERSECT · Soundness of the any-segments-intersect sweep · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Neighbours on the sweep status are disjoint · The status list is weakly sorted after the events left of a vertical line · Phase one: the status list is strictly sorted between the processed and remaining events

DefinitionMeeting segments#✓fully proved

Let \(K\) be a field with a linear order and \(S\) a family of segments in \(K^2\), each given by its two endpoints. Segments \(i\) and \(j\) of \(S\) meet when the closed segment between the endpoints of \(i\) and the closed segment between the endpoints of \(j\) have a point in common.

def Meets (S : Fin n → (𝕜 × 𝕜) × (𝕜 × 𝕜)) (i j : Fin n) : Prop :=
  (segment 𝕜 (left S i) (right S i) ∩ segment 𝕜 (left S j) (right S j)).Nonempty

Uses 2 · Used by 7

Statement usesLeft endpoint of a segment · Right endpoint of a segment

Used byCorrectness of ANY-SEGMENTS-INTERSECT · A leftmost intersection point · Soundness of the any-segments-intersect sweep · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Completeness of the segment-intersection sweep · Neighbours on the sweep status are disjoint

TheoremNeighbours on the sweep status are disjoint#✓fully proved

Let \(P\) be an initial part of the sorted list of events. If running the sweep over \(P\) from the empty status list reports no intersection and ends with status list \(T\), then no two consecutive segments of \(T\) meet.

theorem run_isChain {P Q : List (Event n)} (hE : events S = P ++ Q) {T : List (Fin n)}
    (hT : run S P [] = some T) : T.IsChain fun j k => ¬ Meets S j k

Uses 16 · Used by 1

Statement usesSweep event · Meeting segments · Sorted sweep events · Running the sweep over a list of events

Proof usesSegment strictly below a point · Sweep order on endpoint events · Left endpoint of a segment · A sweep prefix with a right endpoint has its left endpoint · Right endpoint of a segment · The sweep status holds the active segments · One step of the sweep · Splitting a list at the first occurrence of a member · Intersection test for two input segments · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment · Correctness of SEGMENTS-INTERSECT

Used bySweep completeness when the leftmost intersection is inside both segments

TheoremSoundness of the any-segments-intersect sweep#✓fully proved

Let \(S\) be a family of \(n\) segments in \(K^2\), \(K\) a linearly ordered field, and split the sorted list of their \(2n\) endpoint events as \(P\) followed by \(Q\). If running the sweep over \(P\) from the empty status list succeeds with status list \(T\), and running it over \(Q\) from \(T\) reports an intersection, then there are two distinct indices \(i \ne j\) such that segments \(i\) and \(j\) meet.

In particular, when the sweep over all the events reports an intersection, two distinct segments meet.

theorem exists_meets_of_run_eq_none {P Q : List (Event n)} (hE : events S = P ++ Q)
    {T : List (Fin n)} (hT : run S P [] = some T) (hQ : run S Q T = none) :
    ∃ i j, i ≠ j ∧ Meets S i j

Uses 16 · Used by 1

Statement usesSweep event · Meeting segments · Sorted sweep events · Running the sweep over a list of events

Proof usesSegment strictly below a point · Sweep order on endpoint events · Left endpoint of a segment · A sweep prefix with a right endpoint has its left endpoint · Right endpoint of a segment · The sweep status holds the active segments · One step of the sweep · Splitting a list at the first occurrence of a member · Intersection test for two input segments · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment · Correctness of SEGMENTS-INTERSECT

Used byCorrectness of ANY-SEGMENTS-INTERSECT

Completeness

TheoremThe sweep order persists before the leftmost intersection#✓fully proved

Let finitely many segments in the plane over a linearly ordered field be given, where a point \(z\) has coordinates \((z_1, z_2)\) and segment \(j\) has left endpoint \(l_j\) and right endpoint \(r_j\) with \((l_j)_1 < (r_j)_1\). Write \(y_j(t)\) for the height at abscissa \(t\) of the line through \(l_j\) and \(r_j\). Let \(p_x\) be such that every point shared by two distinct segments has abscissa at least \(p_x\), let \(x \le x' < p_x\), and let \(T\) be a list of segments such that \((l_j)_1 \le x\) and \(x' \le (r_j)_1\) for every \(j\) in \(T\). If \(y_j(x) < y_k(x)\) whenever \(j\) occurs before \(k\) in \(T\), then \(y_j(x') < y_k(x')\) whenever \(j\) occurs before \(k\) in \(T\).

theorem pairwise_lt_of_pairwise_lt {T : List (Fin n)} {x x' : 𝕜} (hxx : x ≤ x') (hx' : x' < px)
    (hact : ∀ j ∈ T, (left S j).1 ≤ x ∧ x' ≤ (right S j).1)
    (hT : T.Pairwise fun j k => lineY (left S j) (right S j) x < lineY (left S k) (right S k) x) :
    T.Pairwise fun j k => lineY (left S j) (right S j) x' < lineY (left S k) (right S k) x'

Uses 4 · Used by 1

Statement usesLeft endpoint of a segment · Right endpoint of a segment · Height of a line at an abscissa

Proof usesCrossing of two non-vertical segments

Used byPhase one: the status list is strictly sorted between the processed and remaining events

TheoremThe sweep order holds weakly at the leftmost intersection#✓fully proved

Let finitely many segments in the plane over a linearly ordered field be given, where a point \(z\) has coordinates \((z_1, z_2)\) and segment \(j\) has left endpoint \(l_j\) and right endpoint \(r_j\) with \((l_j)_1 < (r_j)_1\). Write \(y_j(t)\) for the height at abscissa \(t\) of the line through \(l_j\) and \(r_j\). Let \(p_x\) be such that every point shared by two distinct segments has abscissa at least \(p_x\), let \(x < p_x\), and let \(T\) be a list of segments such that \((l_j)_1 \le x\) and \(p_x \le (r_j)_1\) for every \(j\) in \(T\). If \(y_j(x) < y_k(x)\) whenever \(j\) occurs before \(k\) in \(T\), then \(y_j(p_x) \le y_k(p_x)\) whenever \(j\) occurs before \(k\) in \(T\).

theorem pairwise_le_of_pairwise_lt {T : List (Fin n)} {x : 𝕜} (hx : x < px)
    (hact : ∀ j ∈ T, (left S j).1 ≤ x ∧ px ≤ (right S j).1)
    (hT : T.Pairwise fun j k => lineY (left S j) (right S j) x < lineY (left S k) (right S k) x) :
    T.Pairwise fun j k => lineY (left S j) (right S j) px ≤ lineY (left S k) (right S k) px

Uses 4 · Used by 1

Statement usesLeft endpoint of a segment · Right endpoint of a segment · Height of a line at an abscissa

Proof usesCrossing of two non-vertical segments

Used byThe status list is weakly sorted after the events left of a vertical line

TheoremPhase one: the status list is strictly sorted between the processed and remaining events#✓fully proved

Fix a number \(p_x\) in the field of coordinates. Suppose no segment is vertical (each segment's left endpoint has smaller \(x\)-coordinate than its right endpoint) and every point common to two distinct segments has \(x\)-coordinate at least \(p_x\). Split the sorted list of events as \(P\) followed by \(Q\), where the endpoint of every event of \(P\) has \(x\)-coordinate less than \(p_x\), and suppose running the sweep over \(P\) from the empty status list reports no intersection and ends with status list \(T\). Let \(x < p_x\) be at least the \(x\)-coordinate of the endpoint of every event of \(P\) and at most that of every event of \(Q\). Then whenever segment \(j\) comes before segment \(k\) in \(T\), the height at \(x\) of the line through the endpoints of \(j\) is less than that of the line through the endpoints of \(k\).

theorem run_pairwise_lt {P Q : List (Event n)} (hE : events S = P ++ Q)
    (hP : ∀ e ∈ P, (point S e).1 < px) {T : List (Fin n)} (hT : run S P [] = some T) {x : 𝕜}
    (hxP : ∀ e ∈ P, (point S e).1 ≤ x) (hxQ : ∀ e ∈ Q, x ≤ (point S e).1) (hx : x < px) :
    T.Pairwise fun j k => lineY (left S j) (right S j) x < lineY (left S k) (right S k) x

Uses 20 · Used by 1

Statement usesSweep event · Sorted sweep events · Left endpoint of a segment · Endpoint of an event · Right endpoint of a segment · Running the sweep over a list of events · Height of a line at an abscissa

Proof usesSegment strictly below a point · Sweep order on endpoint events · A sweep prefix with a right endpoint has its left endpoint · The sweep order persists before the leftmost intersection · The sweep status holds the active segments · One step of the sweep · Splitting a list at the first occurrence of a member · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment · Direction of three points · DIRECTION as a scaled vertical offset · A non-vertical segment is the graph of its line · Inserting into a strictly sorted list

Used byThe status list is weakly sorted after the events left of a vertical line

TheoremThe status list is weakly sorted after the events left of a vertical line#✓fully proved

Fix a number \(p_x\) in the field of coordinates. Suppose no segment is vertical (each segment's left endpoint has smaller \(x\)-coordinate than its right endpoint) and every point common to two distinct segments has \(x\)-coordinate at least \(p_x\). Split the sorted list of events as \(P\) followed by \(Q\), where the endpoint of every event of \(P\) has \(x\)-coordinate less than \(p_x\) and that of every event of \(Q\) has \(x\)-coordinate at least \(p_x\). If running the sweep over \(P\) from the empty status list reports no intersection and ends with status list \(T\), then whenever segment \(j\) comes before segment \(k\) in \(T\), the height at \(p_x\) of the line through the endpoints of \(j\) is at most that of the line through the endpoints of \(k\).

theorem run_pairwise_le_of_lt {P Q : List (Event n)} (hE : events S = P ++ Q)
    (hP : ∀ e ∈ P, (point S e).1 < px) (hQ : ∀ e ∈ Q, px ≤ (point S e).1) {T : List (Fin n)}
    (hT : run S P [] = some T) :
    T.Pairwise fun j k => lineY (left S j) (right S j) px ≤ lineY (left S k) (right S k) px

Uses 11 · Used by 2

Statement usesSweep event · Sorted sweep events · Left endpoint of a segment · Endpoint of an event · Right endpoint of a segment · Running the sweep over a list of events · Height of a line at an abscissa

Proof usesSweep order on endpoint events · The sweep order holds weakly at the leftmost intersection · The sweep status holds the active segments · Phase one: the status list is strictly sorted between the processed and remaining events

Used bySweep completeness when the leftmost intersection is inside both segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted

TheoremPhase two: inserting left endpoints on a vertical line keeps the status weakly sorted#✓fully proved

Fix a number \(p_x\) in the field of coordinates. Suppose no segment is vertical (each segment's left endpoint has smaller \(x\)-coordinate than its right endpoint) and every point common to two distinct segments has \(x\)-coordinate at least \(p_x\). Split the sorted list of events as \(P_1\), then \(P_2\), then \(Q\), where the endpoint of every event of \(P_1\) has \(x\)-coordinate less than \(p_x\), every event of \(P_2\) is a left endpoint with \(x\)-coordinate equal to \(p_x\), and the endpoint of every event of \(Q\) has \(x\)-coordinate at least \(p_x\). If running the sweep over \(P_1\) followed by \(P_2\) from the empty status list reports no intersection and ends with status list \(T\), then whenever segment \(j\) comes before segment \(k\) in \(T\), the height at \(p_x\) of the line through the endpoints of \(j\) is at most that of the line through the endpoints of \(k\).

theorem run_pairwise_le {P₁ P₂ Q : List (Event n)} (hE : events S = P₁ ++ P₂ ++ Q)
    (hP₁ : ∀ e ∈ P₁, (point S e).1 < px) (hP₂ : ∀ e ∈ P₂, e.2 = true ∧ (point S e).1 = px)
    (hQ : ∀ e ∈ Q, px ≤ (point S e).1) {T : List (Fin n)} (hT : run S (P₁ ++ P₂) [] = some T) :
    T.Pairwise fun j k => lineY (left S j) (right S j) px ≤ lineY (left S k) (right S k) px

Uses 14 · Used by 1

Statement usesSweep event · Sorted sweep events · Left endpoint of a segment · Endpoint of an event · Right endpoint of a segment · Running the sweep over a list of events · Height of a line at an abscissa

Proof usesSegment strictly below a point · The status list is weakly sorted after the events left of a vertical line · One step of the sweep · Testing a segment against an optional neighbour · Direction of three points · DIRECTION as a scaled vertical offset · Inserting into a weakly sorted list

Used bySweep completeness when the leftmost intersection is a left endpoint

TheoremSweep completeness when the leftmost intersection is inside both segments#✓fully proved

Let \(n\) segments in the plane over a linearly ordered field be given, where \(z_1\) is the abscissa of a point \(z\) and segment \(i\) has left endpoint \(l_i\) and right endpoint \(r_i\) with \((l_i)_1 < (r_i)_1\), and suppose no point lies on three distinct segments. Let \(a \ne b\) be segments that share a point \(p\) such that every point shared by two distinct segments has abscissa at least \(p_1\), and suppose \((l_a)_1 < p_1\) and \((l_b)_1 < p_1\). Then the sweep, run on the sorted list of endpoint events from the empty status list, reports an intersection.

Just before the sweep line reaches \(p\), the segments \(a\) and \(b\) are neighbours on the status list, so they were tested.

theorem run_eq_none_of_lt {a b : Fin n} (hab : a ≠ b) {p : 𝕜 × 𝕜}
    (hpa : p ∈ segment 𝕜 (left S a) (right S a)) (hpb : p ∈ segment 𝕜 (left S b) (right S b))
    (hmin : ∀ i j z, i ≠ j → z ∈ segment 𝕜 (left S i) (right S i) →
      z ∈ segment 𝕜 (left S j) (right S j) → p.1 ≤ z.1)
    (hla : (left S a).1 < p.1) (hlb : (left S b).1 < p.1) : run S (events S) [] = none

Uses 15 · Used by 1

Statement usesSorted sweep events · Left endpoint of a segment · Right endpoint of a segment · Running the sweep over a list of events

Proof usesSweep event · Meeting segments · Sweep order on endpoint events · Endpoint of an event · Neighbours on the sweep status are disjoint · The sweep status holds the active segments · The status list is weakly sorted after the events left of a vertical line · One step of the sweep · Splitting a list at two distinct members · Height of a line at an abscissa · A non-vertical segment is the graph of its line

Used byCompleteness of the segment-intersection sweep

TheoremSweep completeness when the leftmost intersection is a left endpoint#✓fully proved

Let \(n\) segments in the plane over a linearly ordered field be given, where \(z_1\) is the abscissa of a point \(z\) and segment \(i\) has left endpoint \(l_i\) and right endpoint \(r_i\) with \((l_i)_1 < (r_i)_1\), and suppose no point lies on three distinct segments. Let \(a \ne b\) be segments such that \(l_a\) lies on segment \(b\) and every point shared by two distinct segments has abscissa at least \((l_a)_1\). If the left endpoint of \(b\) comes before the left endpoint of \(a\) in the sorted list of endpoint events, then the sweep, run on that list from the empty status list, reports an intersection.

Inserting \(a\) places it right next to \(b\), so the two are tested.

theorem run_eq_none_of_left {a b : Fin n} (hab : a ≠ b)
    (hpb : left S a ∈ segment 𝕜 (left S b) (right S b))
    (hmin : ∀ i j z, i ≠ j → z ∈ segment 𝕜 (left S i) (right S i) →
      z ∈ segment 𝕜 (left S j) (right S j) → (left S a).1 ≤ z.1)
    {P Q : List (Event n)} (hE : events S = P ++ (a, true) :: Q) (hbP : (b, true) ∈ P) :
    run S (events S) [] = none

Uses 20 · Used by 1

Statement usesSweep event · Sorted sweep events · Left endpoint of a segment · Right endpoint of a segment · Running the sweep over a list of events

Proof usesMeeting segments · Segment strictly below a point · Sweep order on endpoint events · Endpoint of an event · The sweep status holds the active segments · Phase two: inserting left endpoints on a vertical line keeps the status weakly sorted · One step of the sweep · Intersection test for two input segments · Testing a segment against an optional neighbour · Direction of three points · DIRECTION as a scaled vertical offset · First element at or above a uniquely attained height · Height of a line at an abscissa · A non-vertical segment is the graph of its line · Correctness of SEGMENTS-INTERSECT

Used byCompleteness of the segment-intersection sweep

TheoremA leftmost intersection point#✓fully proved

Let \(\Bbbk\) be a linearly ordered field, let \(s_0, \dots, s_{n-1}\) be closed segments in \(\Bbbk^2\), none of them vertical, and write \(z_x\) for the \(x\)-coordinate of a point \(z\). If some \(s_i\) and \(s_j\) with \(i \ne j\) meet, then there are indices \(a \ne b\) and a point \(p \in s_a \cap s_b\) such that \(p_x \le z_x\) for all indices \(k \ne l\) and every point \(z \in s_k \cap s_l\).

theorem exists_leftmost_meet (h : ∃ i j, i ≠ j ∧ Meets S i j) :
    ∃ a b p, a ≠ b ∧ p ∈ segment 𝕜 (left S a) (right S a) ∧
      p ∈ segment 𝕜 (left S b) (right S b) ∧
      ∀ i j z, i ≠ j → z ∈ segment 𝕜 (left S i) (right S i) →
        z ∈ segment 𝕜 (left S j) (right S j) → p.1 ≤ z.1

Uses 4 · Used by 1

Statement usesMeeting segments · Left endpoint of a segment · Right endpoint of a segment

Proof usesLeftmost point of the intersection of two segments

Used byCompleteness of the segment-intersection sweep

TheoremCompleteness of the segment-intersection sweep#✓fully proved

Let \(n\) segments in the plane over a linearly ordered field be given, none of them vertical (the left endpoint of each has strictly smaller abscissa than its right endpoint), and assume, as CLRS does, that no point lies on three distinct segments. If two distinct segments meet, then the sweep, run on the sorted list of endpoint events from the empty status list, reports an intersection.

theorem run_eq_none_of_meets
    (h3 : ∀ i j k, i ≠ j → j ≠ k → i ≠ k → ∀ z, z ∈ segment 𝕜 (left S i) (right S i) →
      z ∈ segment 𝕜 (left S j) (right S j) → z ∉ segment 𝕜 (left S k) (right S k))
    (h : ∃ i j, i ≠ j ∧ Meets S i j) : run S (events S) [] = none

Uses 13 · Used by 1

Statement usesMeeting segments · Sorted sweep events · Left endpoint of a segment · Right endpoint of a segment · Running the sweep over a list of events

Proof usesSweep event · A leftmost intersection point · Sweep order on endpoint events · Endpoint of an event · Sweep completeness when the leftmost intersection is a left endpoint · Sweep completeness when the leftmost intersection is inside both segments · Height of a line at an abscissa · A non-vertical segment is the graph of its line

Used byCorrectness of ANY-SEGMENTS-INTERSECT

Cost

DefinitionCost charged to a sweep event#✓fully proved

For \(n\) segments, the charge of an event is \(n + 16\) if it is the left endpoint of a segment and \(8\) if it is the right endpoint of a segment.

These charges bound the actual costs: a left endpoint scans at most \(n\) segments of the status list and runs two SEGMENTS-INTERSECT tests, and a right endpoint runs one test.

def eventCost (n : ℕ) : Event n → ℕ
  | (_, true) => n + 16
  | (_, false) => 8

Uses 1 · Used by 1

Statement usesSweep event

Used byRunning time of ANY-SEGMENTS-INTERSECT

DefinitionANY-SEGMENTS-INTERSECT#✓fully proved

Let \(\Bbbk\) be a linearly ordered field. Given \(n\) segments \(s_0, \dots, s_{n-1}\) in \(\Bbbk^2\), each given by its two endpoints, write \(l_t\), the left endpoint of \(s_t\), for its endpoint with the smaller \(x\)-coordinate, or for its first given endpoint when both \(x\)-coordinates agree, and \(r_t\), the right endpoint, for the other one. The procedure sorts the \(2n\) endpoints by \(x\)-coordinate, left endpoints before right endpoints at equal \(x\), then by \(y\)-coordinate, with remaining ties in increasing order of segment index. It then sweeps a vertical line across them, starting with an empty status list of segments, kept from bottom to top. At the left endpoint \(l_i\) of \(s_i\), let \(P\) be the longest initial part of the status list consisting of segments \(s_t\) with \(\mathrm{DIRECTION}(l_t, r_t, l_i) < 0\). Then \(s_i\) is tested with SEGMENTS-INTERSECT first against the segment just after \(P\) and then against the last segment of \(P\), when these exist, and is inserted directly after \(P\). At the right endpoint of \(s_i\), the segments just before and just after \(s_i\) in the status list, when both exist, are tested against each other and \(s_i\) is deleted. The procedure returns true as soon as a test succeeds and false after the last event. Cost counts one unit per evaluation of DIRECTION or ON-SEGMENT (CLRS, third edition, Section 33.2).

The status is kept in a list rather than CLRS's red-black tree.

def anySegmentsIntersect {n : ℕ} (S : Fin n → (𝕜 × 𝕜) × (𝕜 × 𝕜)) : TimeM ℕ Bool :=
  AnySegments.sweep S (AnySegments.events S) []

Uses 2 · Used by 2

Statement usesSorted sweep events · The any-segments-intersect sweep

Used byCorrectness of ANY-SEGMENTS-INTERSECT · Running time of ANY-SEGMENTS-INTERSECT

TheoremCorrectness of ANY-SEGMENTS-INTERSECT#✓fully proved

Let \(\Bbbk\) be a linearly ordered field and let \(s_0, \dots, s_{n-1}\) be closed segments in \(\Bbbk^2\), each given by its two endpoints in either order. Suppose no segment is vertical (its two endpoints have different \(x\)-coordinates) and no point lies on three segments \(s_i\), \(s_j\), \(s_k\) with \(i\), \(j\), \(k\) pairwise distinct. Then ANY-SEGMENTS-INTERSECT returns true on these segments if and only if there are indices \(i \ne j\) such that \(s_i\) and \(s_j\) intersect (CLRS, third edition, Theorem 33.1).

theorem anySegmentsIntersect_ret_eq_true_iff {n : ℕ} (S : Fin n → (𝕜 × 𝕜) × (𝕜 × 𝕜))
    (hv : ∀ i, (S i).1.1 ≠ (S i).2.1)
    (h3 : ∀ i j k, i ≠ j → j ≠ k → i ≠ k →
      segment 𝕜 (S i).1 (S i).2 ∩ segment 𝕜 (S j).1 (S j).2 ∩ segment 𝕜 (S k).1 (S k).2 = ∅) :
    (anySegmentsIntersect S).ret = true ↔
      ∃ i j, i ≠ j ∧ (segment 𝕜 (S i).1 (S i).2 ∩ segment 𝕜 (S j).1 (S j).2).Nonempty

Uses 13

Statement usesANY-SEGMENTS-INTERSECT

Proof usesSweep event · Meeting segments · Segment strictly below a point · Sorted sweep events · Soundness of the any-segments-intersect sweep · Left endpoint of a segment · Right endpoint of a segment · Running the sweep over a list of events · Completeness of the segment-intersection sweep · The any-segments-intersect sweep · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment

TheoremRunning time of ANY-SEGMENTS-INTERSECT#✓fully proved

Let \(\Bbbk\) be a field with a linear order. For every \(n\) segments in \(\Bbbk^2\), each given by its two endpoints, ANY-SEGMENTS-INTERSECT costs at most \(n^2 + 24n\), so it runs in time \(O(n^2)\). Cost counts one unit per evaluation of DIRECTION or ON-SEGMENT.

The bound comes from at most \(n\) DIRECTION evaluations to place each segment in the list-based status and at most three SEGMENTS-INTERSECT tests per segment.

theorem anySegmentsIntersect_time_le {n : ℕ} (S : Fin n → (𝕜 × 𝕜) × (𝕜 × 𝕜)) :
    (anySegmentsIntersect S).time ≤ n * n + 24 * n

Uses 17

Statement usesANY-SEGMENTS-INTERSECT

Proof usesSweep event · Segment strictly below a point · Cost charged to a sweep event · Sorted sweep events · Sweep order on endpoint events · Left endpoint of a segment · Right endpoint of a segment · Running the sweep over a list of events · The sweep status holds the active segments · One step of the sweep · The any-segments-intersect sweep · Intersection test for two input segments · Testing a segment against an optional neighbour · Testing the neighbours of a deleted segment · The SEGMENTS-INTERSECT procedure · Running time of SEGMENTS-INTERSECT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.