Monotone chain convex hull algorithm

DefinitionPop step of the monotone-chain scan#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field, let \(p \in \Bbbk^2\), and write \(u \times v = u_1 v_2 - v_1 u_2\) for the cross product. Given a stack of points of \(\Bbbk^2\) listed top first, while the stack has at least two points, with top \(a\) and next point \(b\), and \((a - b) \times (p - b) \le 0\) (so \(b \to a \to p\) is not a strict left turn), remove \(a\). The result is the first stack reached that has fewer than two points or whose top two points \(a, b\) satisfy \((a - b) \times (p - b) > 0\); that stack is returned unchanged. Each test of the sign of \((a - b) \times (p - b)\) costs one unit, and nothing else is charged.

def popNonLeft (p : π•œ Γ— π•œ) : List (π•œ Γ— π•œ) β†’ TimeM β„• (List (π•œ Γ— π•œ))
  | a :: b :: rest => do
      βœ“
      if cross (a - b) (p - b) ≀ 0 then popNonLeft p (b :: rest) else pure (a :: b :: rest)
  | st => pure st
Uses 1 Β· Used by 8
Statement usesCross product of plane vectors
Used byMonotone chain scan Β· The lower chain ends at the last point Β· The lower chain starts at the first point Β· Every input point lies on or left of each lower-chain edge Β· The lower chain is a sublist of the input Β· The lower-chain scan makes linearly many tests Β· The lower chain turns strictly left Β· The upper chain is a reflected lower chain

DefinitionMonotone chain scan#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. Given a stack \(S\) of points of \(\Bbbk^2\), listed top first, and a list of points \(p_1, \dots, p_n\) of \(\Bbbk^2\), the scan processes \(p_1, \dots, p_n\) in order: for each point \(p = p_i\) it removes the top \(a\) of the stack as long as the stack has a second element \(b\) with \((a_x - b_x)(p_y - b_y) - (p_x - b_x)(a_y - b_y) \le 0\), and then pushes \(p\). Starting from \(S\), the result is the final stack, top first. Each evaluation of this inequality costs one unit; nothing else is counted.

def chainScan : List (π•œ Γ— π•œ) β†’ List (π•œ Γ— π•œ) β†’ TimeM β„• (List (π•œ Γ— π•œ))
  | st, [] => pure st
  | st, p :: ps => do
      let st' ← popNonLeft p st
      chainScan (p :: st') ps
Uses 1 Β· Used by 8
Statement usesPop step of the monotone-chain scan
Used byLower chain Β· The lower chain ends at the last point Β· The lower chain starts at the first point Β· Every input point lies on or left of each lower-chain edge Β· The lower chain is a sublist of the input Β· The lower-chain scan makes linearly many tests Β· The lower chain turns strictly left Β· The upper chain is a reflected lower chain

DefinitionLower chain#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. The lower chain of a list of points \(p_1, \dots, p_n\) of \(\Bbbk^2\) is computed by Andrew's monotone chain scan: start with an empty stack and process \(p_1, \dots, p_n\) in order; for each point \(p = p_i\), remove the top \(a\) of the stack as long as the stack has a second element \(b\) with \((a_x - b_x)(p_y - b_y) - (p_x - b_x)(a_y - b_y) \le 0\), then push \(p\). The lower chain is the final stack read from bottom to top. Each evaluation of the inequality costs one unit; nothing else is counted.

The scan is meant for points sorted strictly in lexicographic \((x, y)\) order; the chain then runs from left to right.

def lowerHull (ps : List (π•œ Γ— π•œ)) : TimeM β„• (List (π•œ Γ— π•œ)) := do
  let st ← chainScan [] ps
  pure st.reverse
Uses 1 Β· Used by 21
Statement usesMonotone chain scan
Used byConvex hull by the monotone chain algorithm Β· The hull polygon contains every input point Β· The hull's vertices are input points Β· The monotone chain hull makes at most \(4n\) orientation tests Β· The monotone chain hull of non-collinear points turns strictly left at every vertex Β· The lower chain ends at the last point Β· The lower chain starts at the first point Β· Every input point lies on or left of each lower-chain edge Β· Lower chain of unsorted points Β· Correctness of the lower chain for unsorted input Β· The lower chain is a sublist of the input Β· The lower-chain scan makes linearly many tests Β· The lower chain turns strictly left Β· Upper chain Β· The upper chain is a reflected lower chain Β· The upper chain ends at the first point Β· The upper chain starts at the last point Β· Every input point lies left of the upper chain Β· The upper chain is a subsequence of the reversed input Β· Running time of the upper chain scan Β· The upper chain turns strictly left

DefinitionLower chain of unsorted points#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. For a list \(P\) of points of \(\Bbbk^2\), sort \(P\) by merge sort into nondecreasing lexicographic \((x, y)\) order and return the lower chain of the sorted list. Only the orientation tests of the lower chain are counted; sorting costs nothing.

def lowerHullOfPoints (ps : List (π•œ Γ— π•œ)) : TimeM β„• (List (π•œ Γ— π•œ)) :=
  lowerHull (ps.mergeSort fun a b => decide (toLex a ≀ toLex b))
Uses 1 Β· Used by 1
Statement usesLower chain
Used byCorrectness of the lower chain for unsorted input

TheoremThe lower chain is a sublist of the input#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field and let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\) that are strictly increasing in lexicographic \((x, y)\) order. Then the lower chain of \(p_1, \dots, p_n\) is a sublist of \(p_1, \dots, p_n\): it is \(p_{i_1}, \dots, p_{i_m}\) for some indices \(i_1 < \dots < i_m\).

theorem lowerHull_sublist (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    (lowerHull ps).ret <+ ps
Uses 4 Β· Used by 4
Statement usesLower chain
Proof usesMonotone chain scan Β· Cross product of plane vectors Β· Pop step of the monotone-chain scan
Used byThe hull's vertices are input points Β· The monotone chain hull of non-collinear points turns strictly left at every vertex Β· Correctness of the lower chain for unsorted input Β· The upper chain is a subsequence of the reversed input

TheoremThe lower chain starts at the first point#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field and let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\) that are strictly increasing in lexicographic \((x, y)\) order. If \(n \ge 1\), the lower chain of \(p_1, \dots, p_n\) starts at \(p_1\); if \(n = 0\), the lower chain is empty.

theorem lowerHull_head? (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    (lowerHull ps).ret.head? = ps.head?
Uses 4 Β· Used by 4
Statement usesLower chain
Proof usesMonotone chain scan Β· Cross product of plane vectors Β· Pop step of the monotone-chain scan
Used byThe hull polygon contains every input point Β· The monotone chain hull of non-collinear points turns strictly left at every vertex Β· Correctness of the lower chain for unsorted input Β· The upper chain starts at the last point

TheoremThe lower chain ends at the last point#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field and let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\) that are strictly increasing in lexicographic \((x, y)\) order. If \(n \ge 1\), the lower chain of \(p_1, \dots, p_n\) ends at \(p_n\); if \(n = 0\), the lower chain is empty.

theorem lowerHull_getLast? (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    (lowerHull ps).ret.getLast? = ps.getLast?
Uses 4 Β· Used by 4
Statement usesLower chain
Proof usesMonotone chain scan Β· Cross product of plane vectors Β· Pop step of the monotone-chain scan
Used byThe hull polygon contains every input point Β· The monotone chain hull of non-collinear points turns strictly left at every vertex Β· Correctness of the lower chain for unsorted input Β· The upper chain ends at the first point

TheoremThe lower chain turns strictly left#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field and let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\) that are strictly increasing in lexicographic \((x, y)\) order, with lower chain \(c_0, \dots, c_{m-1}\). Writing \(\operatorname{cross}(u, v) = u_x v_y - v_x u_y\), for every \(i\) with \(i + 2 < m\) we have \(\operatorname{cross}(c_{i+1} - c_i, c_{i+2} - c_i) > 0\).

theorem lowerHull_turn_left (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b)
    (i : β„•) (h : i + 2 < (lowerHull ps).ret.length) :
    0 < cross ((lowerHull ps).ret[i + 1] - (lowerHull ps).ret[i])
      ((lowerHull ps).ret[i + 2] - (lowerHull ps).ret[i])
Uses 4 Β· Used by 3
Statement usesCross product of plane vectors Β· Lower chain
Proof usesMonotone chain scan Β· Pop step of the monotone-chain scan
Used byThe monotone chain hull of non-collinear points turns strictly left at every vertex Β· Correctness of the lower chain for unsorted input Β· The upper chain turns strictly left

TheoremEvery input point lies on or left of each lower-chain edge#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field and let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\) that are strictly increasing in lexicographic \((x, y)\) order, and write \(\operatorname{cross}(u, v) = u_x v_y - v_x u_y\). For every \(s \in \{p_1, \dots, p_n\}\) and every pair of consecutive vertices \(a, b\) of the lower chain of \(p_1, \dots, p_n\) we have \(\operatorname{cross}(b - a, s - a) \ge 0\): the point \(s\) lies on or to the left of the directed edge from \(a\) to \(b\).

theorem lowerHull_left_of_edges (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b)
    {s : π•œ Γ— π•œ} (hsps : s ∈ ps) :
    (lowerHull ps).ret.IsChain fun a b => 0 ≀ cross (b - a) (s - a)
Uses 4 Β· Used by 4
Statement usesCross product of plane vectors Β· Lower chain
Proof usesMonotone chain scan Β· Pop step of the monotone-chain scan
Used byThe hull polygon contains every input point Β· The monotone chain hull of non-collinear points turns strictly left at every vertex Β· Correctness of the lower chain for unsorted input Β· Every input point lies left of the upper chain

TheoremThe lower-chain scan makes linearly many tests#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. For every list of \(n\) points of \(\Bbbk^2\), computing its lower chain makes at most \(2n\) orientation tests (cross-product evaluations).

theorem lowerHull_time_le (ps : List (π•œ Γ— π•œ)) : (lowerHull ps).time ≀ 2 * ps.length
Uses 4 Β· Used by 2
Statement usesLower chain
Proof usesMonotone chain scan Β· Cross product of plane vectors Β· Pop step of the monotone-chain scan
Used byThe monotone chain hull makes at most \(4n\) orientation tests Β· Running time of the upper chain scan

TheoremCorrectness of the lower chain for unsorted input#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field, let \(P\) be a list of pairwise distinct points of \(\Bbbk^2\) in any order, write \(\preceq\) for the lexicographic \((x, y)\) order on \(\Bbbk^2\), and let \(C = c_0, \dots, c_{m-1}\) be the lower chain of the list obtained by sorting \(P\) into \(\preceq\)-increasing order. Write \(\operatorname{cross}(u, v) = u_x v_y - v_x u_y\). Then every \(c_j\) is a point of \(P\); if \(P\) is nonempty then \(m \ge 1\); if \(m \ge 1\) then \(c_0 \preceq s \preceq c_{m-1}\) for every \(s \in P\); for every \(i\) with \(i + 2 < m\) we have \(\operatorname{cross}(c_{i+1} - c_i, c_{i+2} - c_i) > 0\); and for every \(s \in P\) and every pair of consecutive vertices \(a, b\) of \(C\) we have \(\operatorname{cross}(b - a, s - a) \ge 0\).

theorem lowerHullOfPoints_spec (ps : List (π•œ Γ— π•œ)) (hnd : ps.Nodup) :
    let C := (lowerHullOfPoints ps).ret
    (βˆ€ c ∈ C, c ∈ ps) ∧ (ps β‰  [] β†’ C β‰  []) ∧
    (βˆ€ c ∈ C.head?, βˆ€ s ∈ ps, toLex c ≀ toLex s) ∧
    (βˆ€ c ∈ C.getLast?, βˆ€ s ∈ ps, toLex s ≀ toLex c) ∧
    (βˆ€ i (h : i + 2 < C.length), 0 < cross (C[i + 1] - C[i]) (C[i + 2] - C[i])) ∧
    βˆ€ s ∈ ps, C.IsChain fun a b => 0 ≀ cross (b - a) (s - a)
Uses 8
Statement usesCross product of plane vectors Β· Lower chain of unsorted points
Proof usesLower chain Β· The lower chain ends at the last point Β· The lower chain starts at the first point Β· Every input point lies on or left of each lower-chain edge Β· The lower chain is a sublist of the input Β· The lower chain turns strictly left

DefinitionUpper chain#βœ“fully proved

Let \(K\) be a field with a linear order. The upper chain of a list of points \(p_1, \dots, p_n \in K^2\) is the lower chain of the reversed list \(p_n, \dots, p_1\), together with its cost: the same scan, counting the same orientation tests. For points sorted by \((x, y)\) it runs from the last point back to the first.

def upperHull (ps : List (π•œ Γ— π•œ)) : TimeM β„• (List (π•œ Γ— π•œ)) := lowerHull ps.reverse
Uses 1 Β· Used by 12
Statement usesLower chain
Used byConvex hull by the monotone chain algorithm Β· The hull polygon contains every input point Β· The hull's vertices are input points Β· The monotone chain hull makes at most \(4n\) orientation tests Β· The monotone chain hull of non-collinear points turns strictly left at every vertex Β· The upper chain is a reflected lower chain Β· The upper chain ends at the first point Β· The upper chain starts at the last point Β· Every input point lies left of the upper chain Β· The upper chain is a subsequence of the reversed input Β· Running time of the upper chain scan Β· The upper chain turns strictly left

DefinitionConvex hull by the monotone chain algorithm#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. The convex hull of a list \(P\) of points of \(\Bbbk^2\) is the lower chain of \(P\) followed by the upper chain of \(P\) with its first and last points removed, together with its cost: the cost of computing the lower chain plus the cost of computing the upper chain.

For points sorted strictly in lexicographic \((x, y)\) order, the result runs counterclockwise from the first point.

def convexHull (ps : List (π•œ Γ— π•œ)) : TimeM β„• (List (π•œ Γ— π•œ)) := do
  let lower ← lowerHull ps
  let upper ← upperHull ps
  pure (lower ++ upper.tail.dropLast)
Uses 2 Β· Used by 4
Statement usesLower chain Β· Upper chain
Used byThe hull polygon contains every input point Β· The hull's vertices are input points Β· The monotone chain hull makes at most \(4n\) orientation tests Β· The monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremThe upper chain is a reflected lower chain#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. For every list \(p_1, \dots, p_n\) of points of \(\Bbbk^2\), the upper chain of the list is the image under \(p \mapsto -p\) of the lower chain of \(-p_n, \dots, -p_1\), and the two computations have the same cost.

theorem upperHull_eq (ps : List (π•œ Γ— π•œ)) :
    (upperHull ps).ret = (lowerHull (ps.reverse.map Neg.neg)).ret.map Neg.neg ∧
      (upperHull ps).time = (lowerHull (ps.reverse.map Neg.neg)).time
Uses 5 Β· Used by 6
Statement usesLower chain Β· Upper chain
Proof usesMonotone chain scan Β· Cross product of plane vectors Β· Pop step of the monotone-chain scan
Used byThe upper chain ends at the first point Β· The upper chain starts at the last point Β· Every input point lies left of the upper chain Β· The upper chain is a subsequence of the reversed input Β· Running time of the upper chain scan Β· The upper chain turns strictly left

TheoremThe upper chain is a subsequence of the reversed input#βœ“fully proved

Let \(K\) be an ordered field and let \(p_1, \dots, p_n \in K^2\) be strictly increasing in the lexicographic \((x, y)\) order. Then the upper chain of \(p_1, \dots, p_n\) is a sublist of the reversed list \(p_n, \dots, p_1\): it is obtained from \(p_n, \dots, p_1\) by deleting some of the entries.

theorem upperHull_sublist (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    (upperHull ps).ret <+ ps.reverse
Uses 4 Β· Used by 2
Statement usesUpper chain
Proof usesLower chain Β· The lower chain is a sublist of the input Β· The upper chain is a reflected lower chain
Used byThe hull's vertices are input points Β· The monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremThe upper chain starts at the last point#βœ“fully proved

Let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\), for an ordered field \(\Bbbk\), strictly increasing in the lexicographic order on \((x, y)\). If \(n = 0\) the upper chain is empty; otherwise its first vertex is \(p_n\).

theorem upperHull_head? (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    (upperHull ps).ret.head? = ps.getLast?
Uses 4 Β· Used by 2
Statement usesUpper chain
Proof usesLower chain Β· The lower chain starts at the first point Β· The upper chain is a reflected lower chain
Used byThe hull polygon contains every input point Β· The monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremThe upper chain ends at the first point#βœ“fully proved

Let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\), for an ordered field \(\Bbbk\), strictly increasing in the lexicographic order on \((x, y)\). If \(n = 0\) the upper chain is empty; otherwise its last vertex is \(p_1\).

theorem upperHull_getLast? (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    (upperHull ps).ret.getLast? = ps.head?
Uses 4 Β· Used by 2
Statement usesUpper chain
Proof usesLower chain Β· The lower chain ends at the last point Β· The upper chain is a reflected lower chain
Used byThe hull polygon contains every input point Β· The monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremThe upper chain turns strictly left#βœ“fully proved

Let \(K\) be an ordered field, let \(p_1, \dots, p_n \in K^2\) be strictly increasing in the lexicographic \((x, y)\) order, and let \(c_0, c_1, \dots, c_{m-1}\) be the upper chain of \(p_1, \dots, p_n\). Then for every \(i\) with \(i + 2 < m\), we have \((c_{i+1} - c_i) \times (c_{i+2} - c_i) > 0\), where \((u_1, u_2) \times (v_1, v_2) = u_1 v_2 - v_1 u_2\) is the cross product: the vertices \(c_i\), \(c_{i+1}\), \(c_{i+2}\) make a strict left turn.

theorem upperHull_turn_left (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b)
    (i : β„•) (h : i + 2 < (upperHull ps).ret.length) :
    0 < cross ((upperHull ps).ret[i + 1] - (upperHull ps).ret[i])
      ((upperHull ps).ret[i + 2] - (upperHull ps).ret[i])
Uses 5 Β· Used by 1
Statement usesCross product of plane vectors Β· Upper chain
Proof usesLower chain Β· The lower chain turns strictly left Β· The upper chain is a reflected lower chain
Used byThe monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremEvery input point lies left of the upper chain#βœ“fully proved

Let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\), for an ordered field \(\Bbbk\), strictly increasing in the lexicographic order on \((x, y)\). Then for every input point \(s\) and every two consecutive vertices \(a, b\) of the upper chain, the cross product \((b - a) \times (s - a)\) is nonnegative: \(s\) lies on or to the left of the edge from \(a\) to \(b\).

theorem upperHull_left_of_edges (ps : List (π•œ Γ— π•œ))
    (hs : ps.Pairwise fun a b => toLex a < toLex b) {s : π•œ Γ— π•œ} (hsps : s ∈ ps) :
    (upperHull ps).ret.IsChain fun a b => 0 ≀ cross (b - a) (s - a)
Uses 5 Β· Used by 2
Statement usesCross product of plane vectors Β· Upper chain
Proof usesLower chain Β· Every input point lies on or left of each lower-chain edge Β· The upper chain is a reflected lower chain
Used byThe hull polygon contains every input point Β· The monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremRunning time of the upper chain scan#βœ“fully proved

Let \(K\) be a field with a linear order and let \(p_1, \dots, p_n \in K^2\) be any \(n\) points, sorted or not. Computing the upper chain of \(p_1, \dots, p_n\) costs at most \(2n\), where the cost counts one unit per orientation test (one cross-product comparison) and nothing else.

theorem upperHull_time_le (ps : List (π•œ Γ— π•œ)) : (upperHull ps).time ≀ 2 * ps.length
Uses 4 Β· Used by 1
Statement usesUpper chain
Proof usesLower chain Β· The lower-chain scan makes linearly many tests Β· The upper chain is a reflected lower chain
Used byThe monotone chain hull makes at most \(4n\) orientation tests

TheoremThe hull's vertices are input points#βœ“fully proved

Let \(p_1, \dots, p_n\) be points of \(\Bbbk^2\), for an ordered field \(\Bbbk\), strictly increasing in the lexicographic order on \((x, y)\). Then every vertex of their convex hull computed by the monotone chain algorithm is one of the \(p_i\).

theorem convexHull_subset (ps : List (π•œ Γ— π•œ)) (hs : ps.Pairwise fun a b => toLex a < toLex b) :
    βˆ€ c ∈ (convexHull ps).ret, c ∈ ps
Uses 5
Statement usesConvex hull by the monotone chain algorithm
Proof usesLower chain Β· The lower chain is a sublist of the input Β· Upper chain Β· The upper chain is a subsequence of the reversed input

TheoremThe hull polygon contains every input point#βœ“fully proved

Let \(p_1, \dots, p_n\) be \(n \ge 2\) points of \(\Bbbk^2\), for an ordered field \(\Bbbk\), strictly increasing in the lexicographic order on \((x, y)\), and let \(v_1, \dots, v_m\) be the vertices of their convex hull computed by the monotone chain algorithm. Then for every input point \(s\) and every edge \((a, b)\) of the closed polygon \(v_1, \dots, v_m, v_1\) (that is, \(a, b\) consecutive in this sequence), the cross product \((b - a) \times (s - a)\) is nonnegative: \(s\) lies on or to the left of the edge from \(a\) to \(b\).

theorem convexHull_left_of_edges (ps : List (π•œ Γ— π•œ))
    (hs : ps.Pairwise fun a b => toLex a < toLex b) (hlen : 2 ≀ ps.length) {s : π•œ Γ— π•œ}
    (hsps : s ∈ ps) :
    ((convexHull ps).ret ++ (convexHull ps).ret.take 1).IsChain fun a b =>
      0 ≀ cross (b - a) (s - a)
Uses 10
Statement usesConvex hull by the monotone chain algorithm Β· Cross product of plane vectors
Proof usesLower chain Β· The lower chain ends at the last point Β· The lower chain starts at the first point Β· Every input point lies on or left of each lower-chain edge Β· Upper chain Β· The upper chain ends at the first point Β· The upper chain starts at the last point Β· Every input point lies left of the upper chain

TheoremThe monotone chain hull makes at most \(4n\) orientation tests#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order. For every list of \(n\) points of \(\Bbbk^2\), computing their convex hull by the monotone chain algorithm costs at most \(4n\), where each orientation test costs one unit.

theorem convexHull_time_le (ps : List (π•œ Γ— π•œ)) : (convexHull ps).time ≀ 4 * ps.length
Uses 5
Statement usesConvex hull by the monotone chain algorithm
Proof usesLower chain Β· The lower-chain scan makes linearly many tests Β· Upper chain Β· Running time of the upper chain scan

DefinitionLists of points turning strictly left#βœ“fully proved

Let \(\Bbbk\) be a field with a linear order and write \((u_1, u_2) \times (v_1, v_2) = u_1 v_2 - v_1 u_2\) for the cross product on \(\Bbbk^2\). A list \(q_1, \dots, q_k\) of points of \(\Bbbk^2\) turns strictly left when every three consecutive points do: \((q_{i+1} - q_i) \times (q_{i+2} - q_i) > 0\) for every \(i\) with \(1 \le i \le k - 2\). In particular, every list of fewer than three points turns strictly left.

def TurnsLeft : List (π•œ Γ— π•œ) β†’ Prop
  | a :: b :: c :: rest => 0 < cross (b - a) (c - a) ∧ TurnsLeft (b :: c :: rest)
  | _ => True
Uses 1 Β· Used by 1
Statement usesCross product of plane vectors
Used byThe monotone chain hull of non-collinear points turns strictly left at every vertex

TheoremThe monotone chain hull of non-collinear points turns strictly left at every vertex#βœ“fully proved

Let \(\Bbbk\) be a linearly ordered field and write \((u_1, u_2) \times (v_1, v_2) = u_1 v_2 - v_1 u_2\) for the cross product on \(\Bbbk^2\). Let \(P\) be a list of points of \(\Bbbk^2\) that is strictly increasing in the lexicographic order on \((x, y)\), and suppose the points of \(P\) are not all collinear: there are points \(a, b, c\) of \(P\) with \((b - a) \times (c - a) \ne 0\). Let \(H\) be the list of points returned by the monotone chain convex hull algorithm on \(P\). Then the list obtained from \(H\) by appending its first two points (all of \(H\) if \(H\) has fewer than two points) turns strictly left: any three consecutive points \(q, r, s\) of it satisfy \((r - q) \times (s - q) > 0\).

Read cyclically, this says the hull polygon turns strictly left at every vertex, including the two vertices where the lower and upper chains meet.

theorem convexHull_turnsLeft (ps : List (π•œ Γ— π•œ))
    (hs : ps.Pairwise fun a b => toLex a < toLex b)
    (hncol : βˆƒ a ∈ ps, βˆƒ b ∈ ps, βˆƒ c ∈ ps, cross (b - a) (c - a) β‰  0) :
    TurnsLeft ((convexHull ps).ret ++ (convexHull ps).ret.take 2)
Uses 15
Statement usesLists of points turning strictly left Β· Convex hull by the monotone chain algorithm Β· Cross product of plane vectors
Proof usesLower chain Β· The lower chain ends at the last point Β· The lower chain starts at the first point Β· Every input point lies on or left of each lower-chain edge Β· The lower chain is a sublist of the input Β· The lower chain turns strictly left Β· Upper chain Β· The upper chain ends at the first point Β· The upper chain starts at the last point Β· Every input point lies left of the upper chain Β· The upper chain is a subsequence of the reversed input Β· The upper chain turns strictly left
25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.