Merge pull request #9 from bsubercaseaux/fixup-hole6thm

Match hole_6_theorem with paper

ITP/geometry.tex

@@ -12,22 +12,29 @@
 def ConvexIndep (S : Set Point) : Prop :=
     ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a})
 
+/-- `ConvexEmptyIn S P' means that `S' forms a convex empty polygon in `P' -/
 def ConvexEmptyIn (S P : Set Point) : Prop :=
     ConvexIndep S ∧ EmptyShapeIn S P
 
-def HasEmptyKGon (k : Nat) (S : Set Point) : Prop :=
-    ∃ s : Finset Point, s.card = k ∧ ↑s ⊆ S ∧ ConvexEmptyIn s S
+/-- `HasEmptyKGon k P' means that `P' has a convex, empty `k'-gon -/
+def HasEmptyKGon (k : Nat) (P : Set Point) : Prop :=
+    ∃ S : Finset Point, S.card = k ∧ ↑S ⊆ P ∧ ConvexEmptyIn S P
 \end{lstlisting}
 
-Let \lstinline|ListInGenPos| be a predicate that states that a list of points is in \emph{general position}, i.e., no three points lie on a common line (made precise in~\Cref{sec:triple-orientations}).
-With this we can already state the main theorem of our paper.
+Let \lstinline|SetInGenPos| be a predicate that states that a set of points is in \emph{general position}, i.e., no three points lie on a common line (made precise in~\Cref{sec:triple-orientations}).
+With this we can already state the core theorem.
 
 \begin{lstlisting}
-theorem hole_6_theorem (pts : List Point) (gp : ListInGenPos pts)
-    (h : pts.length ≥ 30) : HasEmptyKGon 6 pts.toFinset
+theorem hole_6_theorem : ∀ (pts : Finset Point),
+    SetInGenPos pts → pts.card = 30 → HasEmptyKGon 6 pts
 \end{lstlisting}
 
-At the root  of the encoding of Heule and Scheucher is the idea that the~\lstinline|ConvexEmptyIn| predicate can be determined by analyzing only triangles. In particular, that a set $s$ of $k$ points in a pointset $S$ form an empty convex $k$-gon if and only if all the ${k \choose 3}$ triangles induced by vertices in $s$ are empty with respect to $S$. This is discussed informally in~\cite[Section 3, Eq.~4]{emptyHexagonNumber}.
+At the root  of the encoding of Heule and Scheucher is the idea that
+the~\lstinline|ConvexEmptyIn| predicate can be determined by analyzing only triangles.
+In particular, that a set $s$ of $k$ points in a pointset $S$ form an empty convex $k$-gon
+if and only if all the ${k \choose 3}$ triangles induced by vertices in $s$
+are empty with respect to $S$.
+This is discussed informally in~\cite[Section 3, Eq.~4]{emptyHexagonNumber}.
 Concretely, we prove the following theorem:
 \begin{lstlisting}
 theorem ConvexEmptyIn.iff_triangles {s : Finset Point} {S : Set Point}

ITP/intro.tex

@@ -89,7 +89,7 @@
 In the 1930s,
 Erd\H{o}s and Szekeres, inspired by Esther Klein, showed that for any $k \geq 3$,
 one can find a sufficiently large number $n$
-such that every $n$ points in \emph{general position}
+such that every $n$ points in the plane in \emph{general position}
 (i.e., with no three points collinear)
 contain a convex \emph{$k$-gon}, i.e., a convex polygon with $k$ vertices~\cite{35erdos_combinatorial_problem_geometry}.
 The minimal such $n$ is denoted $g(k)$.

ITP/related-work.tex

@@ -13,7 +13,7 @@
 Rather than devise a new SAT encoding,
 we use essentially the same encoding presented by Heule and Scheucher~\cite{emptyHexagonNumber}.
 Interestingly,
-a (verified) proof of $g(6) \leq 17$ can be obtained
+a formal proof of $g(6) \leq 17$ can be obtained
 as a corollary of our development.
 We can assert the hole variables $\hvar_{a,b,c}$ as true
 while leaving the remainder of the encoding in~\Cref{fig:full-encoding} unchanged,
@@ -29,8 +29,8 @@
 We checked this formula to be unsatisfiable for $n = 17$,
 giving the same result as Marić:
 \begin{lstlisting}
-theorem gon_6_theorem (pts : List Point) (gp : ListInGenPos pts)
-    (h : pts.length ≥ 17) : HasConvexKGon 6 pts.toFinset
+theorem gon_6_theorem : ∀ (pts : Finset Point),
+  SetInGenPos pts → pts.card = 17 → HasConvexKGon 6 pts
 \end{lstlisting}
 
 Since both formalizations can be executed,

ITP/symmetry-breaking.tex

@@ -30,16 +30,20 @@
 \input{fig-sigma-equiv}
 
 Third, the lex-order property breaks symmetry due to \emph{reflection}.
-Reflecting a set of points~$S$ through a line (e.g., with the map $(x, y) \mapsto (-x, y)$)
+Reflecting a set of points~$S$ over a line (e.g., with the map $(x, y) \mapsto (-x, y)$)
 preserves the presence of $k$-holes and convex $k$-gons.
-Such reflected point sets are almost $\sigma$-equivalent to $S$,
-but their orientations have all changed sign.
-Consider the point sets in \Cref{fig:sigma-equiv}.
-As a result,
-we included the \emph{parity} flag in our Lean definition of $\sigma$-equivalence
-to capture changes in orientations due to reflection,
-where \lstinline|parity := true| changes sign of all orientations.
-The lex-order property ensures that the point set is the lexicographically-larger reflection.
+This operation does not quite preserve orientations, but rather flips them
+(clockwise orientations become counterclockwise and vice versa).
+Our definition of $\sigma$-equivalence includes a \emph{parity} flag for this purpose:
+\lstinline|parity := false| corresponds to the case that orientations are the same,
+and \lstinline|parity := true| corresponds to the case that all orientations have been flipped.
+See the point sets in \Cref{fig:sigma-equiv} for an example.
+
+The lex-order property, then, picks between a set of points and its reflection over \(x=0\).
+The vector of consecutive orientations from the middle to the left
+is assumed to be at least as big as the vector of consecutive orientations from the middle to the right.
+This constraint is not geometrically meaningful,
+but is easy to implement in the SAT encoding.
 
 We prove that there always exists a $\sigma$-equivalent point set in canonical position.
 
@@ -54,22 +58,42 @@
 
 
 \begin{proof}[Proof Sketch]
-The proof proceeds in 6 steps, illustrated in~\Cref{fig:symmetry-breaking}. In each of the steps, we will construct a new list of points that is $\sigma$-equivalent to the previous one, and the last one will be in canonical position.\footnote{Even though we defined $\sigma$-equivalence for sets of points, our formalization goes back and forth between sets and lists. Given that symmetry breaking distinguishes between the order of the points e.g., $x$-order, this proof proceeds over lists. All permutations of a list are immediately $\sigma$-equivalent.}
-The main justification for each step is that, given that the function $\sigma$ is defined as a sign of the determinant, applying transformations that preserve (or, when \lstinline|parity := true|, uniformly reverse) the sign of the determinant will preserve (or uniformly reverse) the values of $\sigma$. In particular, given the identity $\det(AB) = \det(A)\det(B)$, if we apply a transformation to the points that corresponds to multiplying by a matrix $B$ such that $\det(B) > 0$, then $\sign(\det(A)) = \sign(\det(AB))$, and thus orientations will be preserved.
-In step 1, we transform the list of points so that no two points share the same $x$-coordinate. This can be done by applying a rotation to the list of points, which corresponds to multiplying by a rotation matrix.
-Rotations always have determinant $1$. 
-In step 2, we translate all points by a constant vector $t$, by multiplying by a translation matrix, so that the left most point gets position $(0, 0)$, and naturally every other point will have a positive $x$-coordinate.
-Let $L_2$ be the list of points after this transformation, excluding $(0,0)$ which we will denote by $p_1$.
-Then, in step 3, we  apply the projective transformation $f: (x, y) \mapsto (y/x, 1/x)$ to every point in $L_2$, showing that this preserves orientations within $L_2$.
-To see that this mapping is a $\sigma$-equivalence consider that 
+The proof proceeds in 6 steps, illustrated in~\Cref{fig:symmetry-breaking}.
+In each of the steps, we construct a new list of points that is $\sigma$-equivalent to the previous one,
+with the last one being in canonical position.\footnote{
+Even though we defined $\sigma$-equivalence for sets of points,
+our formalization goes back and forth between sets and lists.
+Given that symmetry breaking distinguishes between the order of the points
+e.g., $x$-order, this proof proceeds over lists.
+All permutations of a list are immediately $\sigma$-equivalent.}
+The main justification for each step is that,
+given that the function $\sigma$ is defined as a sign of the determinant,
+applying transformations that preserve (or, when \lstinline|parity := true|, uniformly reverse)
+the sign of the determinant will preserve (or uniformly reverse) the values of $\sigma$.
+
+For example, given the identity $\det(AB) = \det(A)\det(B)$,
+if we apply a transformation to the points that corresponds to multiplying by a matrix $B$ such that $\det(B) > 0$,
+then $\sign(\det(A)) = \sign(\det(AB))$, and thus orientations will be preserved.
+\textbf{Step 1}: we transform the list of points so that no two points share the same $x$-coordinate.
+This can be done by applying a rotation to the list of points, which corresponds to multiplying by a rotation matrix.
+Rotations always have determinant $1$.
+\textbf{Step 2}: we translate all points by a constant vector $t$, which corresponds to multiplying by a translation matrix,
+to bring the leftmost point~$p_1$ to position $(0, 0)$.
+As a result, every other point has a positive $x$-coordinate.
+
+Let $L_2$ be the list of points excluding $p_1$ after Step 2.
+\textbf{Step 3}: we apply the projective transformation $f: (x, y) \mapsto (y/x, 1/x)$ to every point in $L_2$,
+showing that this preserves orientations within $L_2$.
+To see that this mapping is a $\sigma$-equivalence consider that
 \[
 \begin{multlined}
  \sign \det \begin{pmatrix} p_x & q_x & r_x \\ p_y & q_y & r_y \\ 1 & 1 & 1 \end{pmatrix} =  \sign \det \left( \begin{pmatrix} 0 & 0 & 1 \\ 1 & 0 & 0\\ 0 & 1 & 0 \end{pmatrix}  \begin{pmatrix} \nicefrac{p_y}{p_x} & \nicefrac{q_y}{q_x} & \nicefrac{r_y}{r_x} \\ \nicefrac{1}{p_x} & \nicefrac{1}{q_x} & \nicefrac{1}{r_x} \\ 1 & 1 & 1 \end{pmatrix}  \begin{pmatrix} p_x & 0 & 0 \\ 0 & q_x & 0\\ 0 & 0 & r_x \end{pmatrix} \right)\\
                         = \sign \left(1 \cdot \det  \begin{pmatrix} \nicefrac{p_y}{p_x} & \nicefrac{q_y}{q_x} & \nicefrac{r_y}{r_x} \\ \nicefrac{1}{p_x} & \nicefrac{1}{q_x} & \nicefrac{1}{r_x} \\ 1 & 1 & 1 \end{pmatrix} \cdot  p_x q_x r_x  \right) = \sign \det \begin{pmatrix} p_y/p_x & q_y/q_x & r_y/r_x \\ 1/p_x & 1/q_x & 1/r_x \\ 1 & 1 & 1 \end{pmatrix}.
                         %  \tag{As $p_x q_x r_x > 0$ by step 2}
 \end{multlined}
 \]
-To preserve orientations with respect to the leftmost point $(0, 0)$, we set $f( (0, 0)) = (0, \infty)$, a special point that is treated separately as follows.
+To preserve orientations with respect to the leftmost point $(0, 0)$, we set $f( (0, 0)) = (0, \infty)$,
+a special point that is treated separately as follows.
 As the function $\sigma$ takes points in $\mathbb{R}^2$ as arguments,
 we need to define an extension
 \(
@@ -79,13 +103,25 @@
   \end{cases},
 \)
 We then show that $\sigma((0, 0), q, r) = \sigma_{(0, \infty)}(f(q), f(r))$ for all points $q, r \in L_2$. 
-In step 4, we sort the list $L_2$ by $x$-coordinate in increasing order, thus obtaining a list $L_3$.
-This can be done while preserving $\sigma$-equivalence because sorting corresponds to a permutation, and all permutations of a list are $\sigma$-equivalent by definition.
-In step 5, we check whether the \textsf{Lex order} condition above is satisfied in $L_3$, and if it is not, we reflect the pointset, which preserves $\sigma$-equivalence with \lstinline|parity := true|.
+
+\textbf{Step 4}: we sort the list~$L_2$ by $x$-coordinate in increasing order,
+thus obtaining a list~$L_3$.
+This can be done while preserving $\sigma$-equivalence because sorting corresponds to a permutation,
+and all permutations of a list are $\sigma$-equivalent by definition.
+\textbf{Step 5}: we check whether the \textsf{Lex order} condition above is satisfied in $L_3$,
+and if it is not, we reflect the pointset,
+which preserves $\sigma$-equivalence with \lstinline|parity := true|.
 Note that in such a case we need to relabel the points from left to right again.
-In step 6, we bring point $(0, \infty)$ back into the range by first finding a constant $c$ such that all points in $L_3$ are to the right of the line $y=c$, and then finding a large enough value $M$ such that $(c, M)$ has the same orientation with respect to the other points as $(0, \infty)$ did, meaning that 
+
+\textbf{Step 6}: we bring point $(0, \infty)$ back into the range
+by first finding a constant $c$ such that all points in $L_3$ are to the right of the line $y=c$,
+and then finding a large enough value $M$ such that $(c, M)$ has the same orientation
+with respect to the other points as $(0, \infty)$ did,
+meaning that 
 \(\sigma((c, M), q, r) = \sigma_{(0, \infty)}(q, r)\) for every $q, r \in L_3$.
-Finally, we note that the list of points obtained in step 6 satisfies the \text{CCW-order} property by the following reasoning:
+
+Finally, we note that the list of points obtained in step 6
+satisfies the \text{CCW-order} property by the following reasoning:
 if $1 < i < j \leq n$ are indices, then 
 \begin{align*}
   \sigma(p_1, p_i, p_j) = 1 &\iff \sigma((c, M), p_i, p_j) = 1\\
@@ -95,4 +131,3 @@
 \end{align*}
 This concludes the proof.
 \end{proof}
-

ITP/triple-orientations.tex

@@ -128,13 +128,18 @@
 structure σEquiv (S T : Set Point) where
   f : Point → Point
   bij : Set.BijOn f S T
-  parity : Bool -- See Section 4 for details on this field
+  parity : Bool
   σ_eq : ∀ (p ∈ S) (q ∈ S) (r ∈ S), σ p q r = parity ^^^ σ (f p) (f q) (f r)
 
 def OrientationProperty (P : Set Point → Prop) :=
   ∀ {{S T}}, S ≃σ T → P S → P T -- `≃σ` is infix notation for `σEquiv`
 \end{lstlisting}
 
+Our notion of \(\sigma\) equivalence allows for all orientations to be flipped.
+The \lstinline{^^^} (xor) operation does nothing when \lstinline{parity} is false,
+and negates the orientation when \lstinline{parity} is true.
+See~\Cref{sec:symmetry-breaking} for more details.
+
 To illustrate how these notions will be used, let us consider the property
 \(
   \pi_k(S) \triangleq \text{\em ``pointset } S \text{ contains an empty convex } k\text{-gon''}
@@ -184,17 +189,17 @@
   ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ∀ (a ∈ s) (b ∈ s) (c ∈ s), 
   a ≠ b → a ≠ c → b ≠ c → σIsEmptyTriangleFor a b c S
 
-theorem σHasEmptyKGon_iff_HasEmptyKGon (gp : ListInGenPos pts) :
-      σHasEmptyKGon n pts.toFinset ↔ HasEmptyKGon n pts.toFinset
+theorem σHasEmptyKGon_iff_HasEmptyKGon {n : Nat} (gp : ListInGenPos pts) :
+    σHasEmptyKGon n pts.toFinset ↔ HasEmptyKGon n pts.toFinset
 \end{lstlisting}
 
 Then, because \lstinline|σHasEmptyKGon| is ultimately defined in terms of $\sigma$, we can prove
 \begin{lstlisting}
-lemma OrientationProperty_σHasEmptyKGon : OrientationProperty (σHasEmptyKGon n)
+lemma OrientationProperty_σHasEmptyKGon {n : Nat} : OrientationProperty (σHasEmptyKGon n)
 \end{lstlisting}
 Which in combination with \lstinline|theorem σHasEmptyKGon_iff_HasEmptyKGon|, provides
 \begin{lstlisting}
-theorem OrientationProperty_HasEmptyKGon : OrientationProperty (HasEmptyKGon n)
+theorem OrientationProperty_HasEmptyKGon {n : Nat} : OrientationProperty (HasEmptyKGon n)
 \end{lstlisting}
 
 The previous theorem is important for two reasons.
@@ -239,15 +244,25 @@ \subsection{Properties of orientations}\label{sec:sigma-props}
     σ p q r = cw → σ q r s = cw → σ p r s = cw
 \end{lstlisting}
 
-They will be used in justifying the addition of clauses~\labelcref{eq:signotopeClauses11,eq:signotopeClauses12};
-clauses like these or the one below are easily added,
-and are commonly used to reduce the search space in SAT encodings~\cite{emptyHexagonNumber,scheucherTwoDisjoint5holes2020,subercaseaux2023minimizing, szekeres_peters_2006}.
-
-\begin{align}
-  &\left(\neg \orvar_{a, b, c} \lor \neg \orvar_{a, c, d} \lor \orvar_{a, b, d}\right) \land \left(\orvar_{a, b, c} \lor \orvar_{a, c, d} \lor  \neg \orvar_{a, b, d}\right)
-\end{align}
+Our proofs of these properties are based on an equivalence between
+the orientation of a triple of points
+and the \emph{slopes} of the lines that connect them.
+Namely, if $p, q, r$  are sorted from left to right,
+then (i) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pq}) < \textsf{slope}(\overrightarrow{pr})$
+and (ii) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pr}) < \textsf{slope}(\overrightarrow{qr})$.
+By first proving these \emph{slope-orientation} equivalences
+we can then easily prove \lstinline|σ_prop₁| and others,
+as illustrated in~\Cref{fig:orientation-implication}.
+
+These properties will be used in~\Cref{sec:encoding}
+to justify clauses~\labelcref{eq:signotopeClauses11,eq:signotopeClauses12} of the SAT encoding;
+these clauses are commonly added in orientation-based SAT encodings
+to reduce the search space by removing some ``unrealizable'' orientations~\cite{emptyHexagonNumber,scheucherTwoDisjoint5holes2020,subercaseaux2023minimizing, szekeres_peters_2006}.
+\[
+  \left(\neg \orvar_{a, b, c} \lor \neg \orvar_{a, c, d} \lor \orvar_{a, b, d}\right) \land
+  \left(\orvar_{a, b, c} \lor \orvar_{a, c, d} \lor  \neg \orvar_{a, b, d}\right)
+\]
 
-Our proofs of these properties are based on an equivalence between the orientation of a triple of points and the \emph{slopes} of the lines that connect them. Namely, if $p, q, r$  are sorted from left to right, then (i) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pq}) < \textsf{slope}(\overrightarrow{pr})$  and (ii) $\sigma(p,q,r)=1 \iff \textsf{slope}(\overrightarrow{pr}) < \textsf{slope}(\overrightarrow{qr})$. By first proving these \emph{slope-orientation} equivalences we can then easily prove \lstinline|σ_prop₁| and others, as illustrated in~\Cref{fig:orientation-implication}.
 
 \begin{figure}
   \centering

Lean/Geo.lean

@@ -19,11 +19,11 @@ i.e. the point set encloses a convex polygon. Also known as a "convex-independen
 recall Geo.ConvexIndep (S : Set Point) : Prop :=
   ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a})
 
-recall Geo.HasConvexKGon (n : Nat) (S : Set Point) : Prop :=
-  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s
+recall Geo.HasConvexKGon (n : Nat) (P : Set Point) : Prop :=
+  ∃ S : Finset Point, S.card = n ∧ ↑S ⊆ P ∧ ConvexIndep S
 
-recall Geo.HasEmptyKGon (n : Nat) (S : Set Point) : Prop :=
-  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s ∧ EmptyShapeIn s S
+recall Geo.HasEmptyKGon (n : Nat) (P : Set Point) : Prop :=
+  ∃ S : Finset Point, S.card = n ∧ ↑S ⊆ P ∧ ConvexIndep S ∧ EmptyShapeIn S P
 
 /- `gonNumber k` is the smallest number `n` such that every set of `n` or more points
 in general position contains a convex-independent set of size `k`. -/
@@ -98,7 +98,7 @@ axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1) (holes := true)).isUnsat
 (and no fewer) contains an empty hexagon.
 -/
 theorem holeNumber_6 : holeNumber 6 = 30 :=
-  le_antisymm (hole_6_theorem unsat_6hole_cnf) (hole_lower_bound [
+  le_antisymm (hole_6_theorem' unsat_6hole_cnf) (hole_lower_bound [
     (1, 1260), (16, 743), (22, 531), (37, 0), (306, 592), (310, 531), (366, 552), (371, 487),
     (374, 525), (392, 575), (396, 613), (410, 539), (416, 550), (426, 526), (434, 552), (436, 535),
     (446, 565), (449, 518), (450, 498), (453, 542), (458, 526), (489, 537), (492, 502), (496, 579),

Lean/Geo/Canonicalization/SymmetryBreaking.lean

@@ -150,7 +150,7 @@ theorem HasEmptyKGon_extension' :
     (∀ l : List Point, l.length = n → l.Nodup → Point.ListInGenPos l → HasEmptyKGon k l.toFinset) →
     l.Nodup → n ≤ l.length → HasEmptyKGon k l.toFinset := by
   intro H nodup llength
-  rw [← σHasEmptyKGon_iff_HasEmptyKGon gp]
+  rw [← σHasEmptyKGon_iff_HasEmptyKGon gp.toFinset]
 
   have ⟨l₁, σ₁, distinct⟩ := σEmbed_rotate l nodup
   replace gp := (OrientationProperty'.gp σ₁).mp gp
@@ -172,7 +172,7 @@ theorem HasEmptyKGon_extension' :
   suffices σHasEmptyKGon k l₂.toFinset by
     rwa [List.toFinset_eq_of_perm _ _ l₂l₁] at this
 
-  rw [σHasEmptyKGon_iff_HasEmptyKGon gp]
+  rw [σHasEmptyKGon_iff_HasEmptyKGon gp.toFinset]
   let left := l₂.take n
   let right := l₂.drop n
   have leftl₂ : left <+ l₂ := List.take_sublist ..