Orientation and segment intersection tests
DefinitionCross product of plane vectors#βfully proved
For \(p = (x_p, y_p)\) and \(q = (x_q, y_q)\) in \(K^2\), where \(K\) is a linearly ordered field, the cross product is \(p \times q = x_p y_q - x_q y_p\) (CLRS equation (33.1)).
def cross (p q : π Γ π) : π := p.1 * q.2 - q.1 * p.2Used by 15
DefinitionDirection of three points#βfully proved
For points \(p_i, p_j, p_k \in K^2\), where \(K\) is a linearly ordered field, CLRS's DIRECTION\((p_i, p_j, p_k)\) is the cross product \((p_k - p_i) \times (p_j - p_i)\).
It is positive when \(p_k\) is clockwise from \(p_j\) about \(p_i\), negative when counterclockwise, and zero when the three points are collinear.
def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)def cross (p q : π Γ π) : π := p.1 * q.2 - q.1 * p.2CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:51
Uses 1 Β· Used by 15
DefinitionThe ON-SEGMENT test#βfully proved
For points \(p_i = (x_i, y_i)\), \(p_j = (x_j, y_j)\) and \(p_k = (x_k, y_k)\) in \(K^2\), where \(K\) is a linearly ordered field, CLRS's ON-SEGMENT\((p_i, p_j, p_k)\) is the Boolean that is true exactly when \(p_k\) lies in the bounding box of \(p_i\) and \(p_j\), that is, \(\min(x_i, x_j) \le x_k \le \max(x_i, x_j)\) and \(\min(y_i, y_j) \le y_k \le \max(y_i, y_j)\).
DefinitionValues of opposite sign#βfully proved
Two elements \(d\) and \(e\) of a field with a linear order straddle zero when \(d > 0\) and \(e < 0\), or \(d < 0\) and \(e > 0\); that is, \(d\) and \(e\) are nonzero with opposite signs.
def Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eUsed by 10
DefinitionCollinear-endpoint step of SEGMENTS-INTERSECT#βfully proved
Let \(K\) be a linearly ordered field, \(d \in K\) and \(p_i, p_j, p_k \in K^2\). When \(d = 0\), this step costs one unit and returns the value of ON-SEGMENT\((p_i, p_j, p_k)\); when \(d \neq 0\), it costs nothing and returns false.
In SEGMENTS-INTERSECT, \(d\) is the direction of \(p_k\) relative to \(p_i\) and \(p_j\).
def collinearBranch (d : π) (pi pj pk : π Γ π) : TimeM β Bool :=
if d = 0 then do
β
pure (onSegment pi pj pk)
else pure falsedef onSegment (pi pj pk : π Γ π) : Bool :=
decide (min pi.1 pj.1 β€ pk.1 β§ pk.1 β€ max pi.1 pj.1 β§
min pi.2 pj.2 β€ pk.2 β§ pk.2 β€ max pi.2 pj.2)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:58
Uses 1 Β· Used by 3
DefinitionThe SEGMENTS-INTERSECT procedure#βfully proved
Let \(K\) be a field with a linear order and let \(p_1, p_2, p_3, p_4 \in K^2\). CLRS's procedure SEGMENTS-INTERSECT\((p_1, p_2, p_3, p_4)\), which tests whether the segments \(p_1p_2\) and \(p_3p_4\) meet, first computes, at a cost of \(4\), the directions \(d_1 = \mathrm{DIRECTION}(p_3, p_4, p_1)\), \(d_2 = \mathrm{DIRECTION}(p_3, p_4, p_2)\), \(d_3 = \mathrm{DIRECTION}(p_1, p_2, p_3)\) and \(d_4 = \mathrm{DIRECTION}(p_1, p_2, p_4)\). If \(d_1\) and \(d_2\) are nonzero with opposite signs and so are \(d_3\) and \(d_4\), it returns true. Otherwise it tries in order the cases \(d_1 = 0\) with ON-SEGMENT\((p_3, p_4, p_1)\), \(d_2 = 0\) with ON-SEGMENT\((p_3, p_4, p_2)\), \(d_3 = 0\) with ON-SEGMENT\((p_1, p_2, p_3)\), and \(d_4 = 0\) with ON-SEGMENT\((p_1, p_2, p_4)\): in each case it runs the ON-SEGMENT test, at a cost of \(1\), only when the direction is \(0\), and it returns true as soon as a test succeeds. If none succeeds it returns false.
Cslib.Algorithms.Lean.Geometry.segmentsIntersect Β· 15 lines
def segmentsIntersect (p1 p2 p3 p4 : π Γ π) : TimeM β Bool := do
β[4]
let d1 := direction p3 p4 p1
let d2 := direction p3 p4 p2
let d3 := direction p1 p2 p3
let d4 := direction p1 p2 p4
if Straddles d1 d2 β§ Straddles d3 d4 then pure true
else do
let b1 β collinearBranch d1 p3 p4 p1
if b1 then pure true else do
let b2 β collinearBranch d2 p3 p4 p2
if b2 then pure true else do
let b3 β collinearBranch d3 p1 p2 p3
if b3 then pure true else
collinearBranch d4 p1 p2 p4def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
def Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
def collinearBranch (d : π) (pi pj pk : π Γ π) : TimeM β Bool :=
if d = 0 then do
β
pure (onSegment pi pj pk)
else pure falseCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:69
Uses 3 Β· Used by 5
Cost
TheoremRunning time of SEGMENTS-INTERSECT#βfully proved
Let \(K\) be a field with a linear order and let \(p_1, p_2, p_3, p_4 \in K^2\). In the cost model that charges one unit per DIRECTION computation and one per ON-SEGMENT test, SEGMENTS-INTERSECT\((p_1, p_2, p_3, p_4)\) costs at least \(4\) and at most \(8\).
The four directions are always computed, and at most four ON-SEGMENT tests run.
theorem segmentsIntersect_time (p1 p2 p3 p4 : π Γ π) :
4 β€ (segmentsIntersect p1 p2 p3 p4).time β§ (segmentsIntersect p1 p2 p3 p4).time β€ 8def segmentsIntersect (p1 p2 p3 p4 : π Γ π) : TimeM β Bool := do
β[4]
let d1 := direction p3 p4 p1
let d2 := direction p3 p4 p2
let d3 := direction p1 p2 p3
let d4 := direction p1 p2 p4
if Straddles d1 d2 β§ Straddles d3 d4 then pure true
else do
let b1 β collinearBranch d1 p3 p4 p1
if b1 then pure true else do
let b2 β collinearBranch d2 p3 p4 p2
if b2 then pure true else do
β―CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:76
Uses 5 Β· Used by 1
Geometry of the tests
TheoremSEGMENTS-INTERSECT as a Boolean formula#βfully proved
Let \(K\) be a field with a linear order, let \(p_1, p_2, p_3, p_4 \in K^2\), and write \(d_1 = \mathrm{DIRECTION}(p_3, p_4, p_1)\), \(d_2 = \mathrm{DIRECTION}(p_3, p_4, p_2)\), \(d_3 = \mathrm{DIRECTION}(p_1, p_2, p_3)\) and \(d_4 = \mathrm{DIRECTION}(p_1, p_2, p_4)\). The value returned by SEGMENTS-INTERSECT\((p_1, p_2, p_3, p_4)\) is true if and only if at least one of the following holds: \(d_1\) and \(d_2\) are nonzero with opposite signs and \(d_3\) and \(d_4\) are nonzero with opposite signs; \(d_1 = 0\) and ON-SEGMENT\((p_3, p_4, p_1)\) is true; \(d_2 = 0\) and ON-SEGMENT\((p_3, p_4, p_2)\) is true; \(d_3 = 0\) and ON-SEGMENT\((p_1, p_2, p_3)\) is true; or \(d_4 = 0\) and ON-SEGMENT\((p_1, p_2, p_4)\) is true.
theorem segmentsIntersect_ret (p1 p2 p3 p4 : π Γ π) :
(segmentsIntersect p1 p2 p3 p4).ret =
(decide (Straddles (direction p3 p4 p1) (direction p3 p4 p2) β§
Straddles (direction p1 p2 p3) (direction p1 p2 p4)) ||
(decide (direction p3 p4 p1 = 0) && onSegment p3 p4 p1) ||
(decide (direction p3 p4 p2 = 0) && onSegment p3 p4 p2) ||
(decide (direction p1 p2 p3 = 0) && onSegment p1 p2 p3) ||
(decide (direction p1 p2 p4 = 0) && onSegment p1 p2 p4))def segmentsIntersect (p1 p2 p3 p4 : π Γ π) : TimeM β Bool := do
β[4]
let d1 := direction p3 p4 p1
let d2 := direction p3 p4 p2
let d3 := direction p1 p2 p3
let d4 := direction p1 p2 p4
if Straddles d1 d2 β§ Straddles d3 d4 then pure true
else do
let b1 β collinearBranch d1 p3 p4 p1
if b1 then pure true else do
let b2 β collinearBranch d2 p3 p4 p2
if b2 then pure true else do
β―CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:76
def Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
def onSegment (pi pj pk : π Γ π) : Bool :=
decide (min pi.1 pj.1 β€ pk.1 β§ pk.1 β€ max pi.1 pj.1 β§
min pi.2 pj.2 β€ pk.2 β§ pk.2 β€ max pi.2 pj.2)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:58
Uses 5 Β· Used by 1
TheoremPoints of a segment lie in its bounding box#βfully proved
Let \(K\) be a linearly ordered field and \(p, q, r \in K^2\). If \(r\) lies on the closed segment from \(p\) to \(q\), then ON-SEGMENT\((p, q, r)\) is true, that is, \(r\) lies in the bounding box of \(p\) and \(q\).
theorem onSegment_of_mem {p q r : π Γ π} (h : r β segment π p q) : onSegment p q r = truedef onSegment (pi pj pk : π Γ π) : Bool :=
decide (min pi.1 pj.1 β€ pk.1 β§ pk.1 β€ max pi.1 pj.1 β§
min pi.2 pj.2 β€ pk.2 β§ pk.2 β€ max pi.2 pj.2)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:58
Uses 1 Β· Used by 1
TheoremPoints of a segment have direction zero#βfully proved
Let \(K\) be a linearly ordered field and \(p, q, r \in K^2\). If \(r\) lies on the closed segment from \(p\) to \(q\), then the direction \((r - p) \times (q - p)\) is zero, that is, \(r\) is collinear with \(p\) and \(q\).
theorem direction_eq_zero_of_mem {p q r : π Γ π} (h : r β segment π p q) :
direction p q r = 0def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
Uses 1 Β· Used by 1
TheoremA collinear point in the bounding box lies on the segment#βfully proved
Let \(K\) be a linearly ordered field, write \((u_1, u_2) \times (v_1, v_2) = u_1 v_2 - v_1 u_2\) for the cross product on \(K^2\), and let \(p, q, r \in K^2\). If \(r\) is collinear with \(p\) and \(q\), that is, the direction \((r - p) \times (q - p)\) is zero, and ON-SEGMENT\((p, q, r)\) is true, that is, \(r\) lies in the bounding box of \(p\) and \(q\), then \(r\) lies on the closed segment from \(p\) to \(q\).
This is the fact behind CLRS's use of ON-SEGMENT.
theorem mem_segment_of_direction_eq_zero {p q r : π Γ π} (hd : direction p q r = 0)
(hb : onSegment p q r = true) : r β segment π p qdef direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
def onSegment (pi pj pk : π Γ π) : Bool :=
decide (min pi.1 pj.1 β€ pk.1 β§ pk.1 β€ max pi.1 pj.1 β§
min pi.2 pj.2 β€ pk.2 β§ pk.2 β€ max pi.2 pj.2)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:58
Uses 2 Β· Used by 1
Straddling
TheoremValues of opposite sign have nonzero difference#βfully proved
If \(d\) and \(e\) are elements of a linearly ordered field that straddle zero, that is, they are nonzero with opposite signs, then \(d - e \ne 0\).
theorem Straddles.sub_ne_zero {d e : π} (h : Straddles d e) : d - e β 0def Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
Uses 1 Β· Used by 2
TheoremZero-crossing parameter of values of opposite sign#βfully proved
If \(d\) and \(e\) are elements of a linearly ordered field that straddle zero, that is, they are nonzero with opposite signs, then \(0 \le d / (d - e) \le 1\).
theorem Straddles.param_mem {d e : π} (h : Straddles d e) : 0 β€ d / (d - e) β§ d / (d - e) β€ 1def Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
Uses 1 Β· Used by 2
TheoremA vanishing convex combination of nonzero values forces opposite signs#βfully proved
Let \(d\) and \(e\) be nonzero elements of a linearly ordered field. If \(a d + b e = 0\) for some \(a, b \ge 0\) in the field with \(a + b = 1\), then \(d\) and \(e\) have opposite signs.
theorem straddles_of_combo {a b d e : π} (ha : 0 β€ a) (hb : 0 β€ b) (hab : a + b = 1)
(hd : d β 0) (he : e β 0) (h : a * d + b * e = 0) : Straddles d edef Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
Uses 1 Β· Used by 1
TheoremProperly crossing segments meet#βfully proved
Let \(K\) be a linearly ordered field and \(p_1, p_2, p_3, p_4 \in K^2\). Suppose the directions \((p_1 - p_3) \times (p_4 - p_3)\) and \((p_2 - p_3) \times (p_4 - p_3)\) are nonzero with opposite signs, and so are \((p_3 - p_1) \times (p_2 - p_1)\) and \((p_4 - p_1) \times (p_2 - p_1)\). Then the closed segments \(p_1 p_2\) and \(p_3 p_4\) have a common point.
theorem inter_nonempty_of_straddles {p1 p2 p3 p4 : π Γ π}
(h12 : Straddles (direction p3 p4 p1) (direction p3 p4 p2))
(h34 : Straddles (direction p1 p2 p3) (direction p1 p2 p4)) :
(segment π p1 p2 β© segment π p3 p4).Nonemptydef Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
Uses 4 Β· Used by 1
Completeness
TheoremPoints with direction zero lie on the line#βfully proved
Let \(K\) be a linearly ordered field and \(p, q, r \in K^2\) with \(p \neq q\). If \((r - p) \times (q - p) = 0\), then \(r = p + \mu (q - p)\) for some \(\mu \in K\).
One can take \(\mu = \frac{(r - p) \cdot (q - p)}{(q - p) \cdot (q - p)}\), a quotient of dot products.
theorem eq_param_of_direction_eq_zero {p q r : π Γ π} (hpq : p β q) (hd : direction p q r = 0) :
β ΞΌ : π, r.1 = p.1 + ΞΌ * (q.1 - p.1) β§ r.2 = p.2 + ΞΌ * (q.2 - p.2)def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
Uses 1 Β· Used by 1
TheoremCollinear case of segment intersection#βfully proved
Let \(K\) be a linearly ordered field and \(p_1, p_2, p_3, p_4 \in K^2\). Suppose the directions \((p_1 - p_3) \times (p_4 - p_3)\) and \((p_2 - p_3) \times (p_4 - p_3)\) are both zero and the closed segments \(p_1 p_2\) and \(p_3 p_4\) have a common point. Then \(p_1\) or \(p_2\) lies on the segment \(p_3 p_4\), or \(p_3\) or \(p_4\) lies on the segment \(p_1 p_2\).
theorem endpoint_mem_of_collinear {p1 p2 p3 p4 z : π Γ π} (h1 : direction p3 p4 p1 = 0)
(h2 : direction p3 p4 p2 = 0) (hA : z β segment π p1 p2) (hB : z β segment π p3 p4) :
p1 β segment π p3 p4 β¨ p2 β segment π p3 p4 β¨ p3 β segment π p1 p2 β¨
p4 β segment π p1 p2def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
Uses 5 Β· Used by 1
TheoremMeeting segments cross properly or an endpoint lies on the other#βfully proved
Let \(K\) be a linearly ordered field and \(p_1, p_2, p_3, p_4 \in K^2\), and suppose the closed segments \([p_1, p_2]\) and \([p_3, p_4]\) have a common point. Then either \(\mathrm{DIRECTION}(p_3, p_4, p_1)\) and \(\mathrm{DIRECTION}(p_3, p_4, p_2)\) are nonzero with opposite signs and \(\mathrm{DIRECTION}(p_1, p_2, p_3)\) and \(\mathrm{DIRECTION}(p_1, p_2, p_4)\) are nonzero with opposite signs, or \(p_1 \in [p_3, p_4]\), or \(p_2 \in [p_3, p_4]\), or \(p_3 \in [p_1, p_2]\), or \(p_4 \in [p_1, p_2]\).
theorem straddles_or_endpoint_mem {p1 p2 p3 p4 z : π Γ π} (hA : z β segment π p1 p2)
(hB : z β segment π p3 p4) :
(Straddles (direction p3 p4 p1) (direction p3 p4 p2) β§
Straddles (direction p1 p2 p3) (direction p1 p2 p4)) β¨
p1 β segment π p3 p4 β¨ p2 β segment π p3 p4 β¨ p3 β segment π p1 p2 β¨
p4 β segment π p1 p2def Straddles (d e : π) : Prop := 0 < d β§ e < 0 β¨ d < 0 β§ 0 < eCSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:63
def direction (pi pj pk : π Γ π) : π := cross (pk - pi) (pj - pi)CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:55
Uses 4 Β· Used by 1
Correctness
TheoremCorrectness of SEGMENTS-INTERSECT#βfully proved
Let \(K\) be a linearly ordered field and let \(p_1, p_2, p_3, p_4 \in K^2\). The procedure SEGMENTS-INTERSECT\((p_1, p_2, p_3, p_4)\) returns true if and only if the closed segments \([p_1, p_2]\) and \([p_3, p_4]\) have a common point.
theorem segmentsIntersect_ret_eq_true_iff (p1 p2 p3 p4 : π Γ π) :
(segmentsIntersect p1 p2 p3 p4).ret = true β
(segment π p1 p2 β© segment π p3 p4).Nonemptydef segmentsIntersect (p1 p2 p3 p4 : π Γ π) : TimeM β Bool := do
β[4]
let d1 := direction p3 p4 p1
let d2 := direction p3 p4 p2
let d3 := direction p1 p2 p3
let d4 := direction p1 p2 p4
if Straddles d1 d2 β§ Straddles d3 d4 then pure true
else do
let b1 β collinearBranch d1 p3 p4 p1
if b1 then pure true else do
let b2 β collinearBranch d2 p3 p4 p2
if b2 then pure true else do
β―CSLibExt/Algorithms/Lean/Geometry/SegmentIntersection.lean:76
Sources
- CLRS Section 33.1.
Uses 10 Β· Used by 3
Loading dependency explorerβ¦
The dependency explorer needs JavaScript and its graph data.