match hole_6_theorem with paper, make it about sets

ITP/geometry.tex

@@ -19,15 +19,20 @@
     ∃ s : Finset Point, s.card = k ∧ ↑s ⊆ S ∧ ConvexEmptyIn s S
 \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),
+    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}

Lean/Geo.lean

@@ -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 ..

Lean/Geo/Definitions/OrientationProperties.lean

@@ -67,14 +67,14 @@ theorem σIsEmptyTriangleFor_iff' {a b c : Point} (gp : Point.ListInGenPos S)
   have ss := hs.subset; have nd := hs.nodup (gp.nodup hs.length_le); simp [not_or] at ss nd
   rw [σIsEmptyTriangleFor_iff] <;> simp [*]
 
-theorem σHasEmptyKGon_iff_HasEmptyKGon (gp : Point.ListInGenPos pts) :
-    σHasEmptyKGon n pts.toFinset ↔ HasEmptyKGon n pts.toFinset := by
+theorem σHasEmptyKGon_iff_HasEmptyKGon {pts : Finset Point} (gp : Point.SetInGenPos ↑pts) :
+    σHasEmptyKGon n pts ↔ HasEmptyKGon n pts := by
   unfold σHasEmptyKGon HasEmptyKGon
   refine exists_congr fun s => and_congr_right' <| and_congr_right fun spts => ?_
   rw [ConvexEmptyIn.iff_triangles'' spts gp]
   simp [Set.subset_def] at spts
   iterate 9 refine forall_congr' fun _ => ?_
-  rw [σIsEmptyTriangleFor_iff gp] <;> simp [EmptyShapeIn, PtInTriangle, *]
+  rw [σIsEmptyTriangleFor_iff'' gp] <;> simp [EmptyShapeIn, PtInTriangle, *]
 
 theorem σHasConvexKGon_iff_HasConvexKGon (gp : Point.ListInGenPos pts) :
     σHasConvexKGon n pts.toFinset ↔ HasConvexKGon n pts.toFinset := by
@@ -228,7 +228,7 @@ theorem σCCWPoints.cycle (H : σCCWPoints (l₁ ++ l₂)) : σCCWPoints (l₂ +
     fun a ha => (H3 a ha).imp <| Eq.trans (by rw [σ_perm₂, ← σ_perm₁])⟩
 
 theorem σCCWPoints.convex (H : σCCWPoints l) : ConvexIndep l.toFinset := by
-  refine ((ConvexEmptyIn.iff_triangles'' subset_rfl H.gp).2 ?_).1
+  refine ((ConvexEmptyIn.iff_triangles'' subset_rfl H.gp.toFinset).2 ?_).1
   simp only [mem_toFinset, Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton,
     not_or, and_imp]
   intro a ha b hb c hc ab ac bc p hp pa pb pc hn
@@ -353,7 +353,7 @@ theorem σCCWPoints.emptyHexagon
     gp ((@perm_append_comm _ [c,d,e,f] [a, b']).subperm.trans sp)
   have ⟨f', sp, H, efa⟩ := σCCWPoints.flatten (H.cycle (l₁ := [c, d']) (l₂ := [e,f,a,b']))
     gp ((@perm_append_comm _ [e,f,a,b'] [c, d']).subperm.trans sp)
-  refine (σHasEmptyKGon_iff_HasEmptyKGon gp).2
+  refine (σHasEmptyKGon_iff_HasEmptyKGon gp.toFinset).2
     ⟨[e, f', a, b', c, d'].toFinset, ?_, by simpa [Set.subset_def] using sp.subset, H.convex, ?_⟩
   · exact congrArg length (dedup_eq_self.2 (H.gp.nodup (by show 3 ≤ 6; decide)))
   · refine σCCWPoints.split_emptyShapeIn e [f'] a [b', c, d'] H efa ?_

Lean/Geo/Definitions/Structures.lean

@@ -55,16 +55,18 @@ theorem ConvexIndep.lt_3 {s : Finset Point} (hs : s.card < 3) : ConvexIndep s :=
     subst eq; simp at hn; subst b
     simpa using congrArg (a ∈ ·) e1
 
-theorem ConvexIndep.triangle' {s : Finset Point} {S : List Point}
-    (hs : s.card ≤ 3) (sS : s ⊆ S.toFinset) (gp : Point.ListInGenPos S) :
+theorem ConvexIndep.triangle' {s : Finset Point} {S : Finset Point}
+    (hs : s.card ≤ 3) (sS : s ⊆ S) (gp : Point.SetInGenPos S) :
     ConvexIndep s := by
   cases lt_or_eq_of_le hs with
   | inl hs => exact ConvexIndep.lt_3 hs
   | inr hs =>
     match s, s.exists_mk with | _, ⟨[a,b,c], h1, rfl⟩ => ?_
     rw [ConvexIndep.triangle_iff]
-    apply Point.ListInGenPos.subperm.1 gp
-    exact List.subperm_of_subset h1 (by simpa [Finset.subset_iff] using sS)
+    refine gp ?_ h1
+    intro _ _
+    simp [Finset.subset_iff] at *
+    aesop
 
 theorem ConvexIndep.antitone {S₁ S₂ : Set Point} (S₁S₂ : S₁ ⊆ S₂)
     (convex : ConvexIndep S₂) : ConvexIndep S₁ := by
@@ -115,12 +117,12 @@ theorem ConvexEmptyIn.iff_triangles {s : Finset Point} {S : Set Point}
     refine this.2 _ ⟨pS, fun pu => ?_⟩ (convexHull_mono tu ht)
     exact this.1 p pu (convexHull_mono (Set.subset_diff_singleton tu (mt (tS' ·) pn)) ht)
 
-theorem ConvexEmptyIn.iff_triangles' {s : Finset Point} {S : List Point}
-    (sS : s ⊆ S.toFinset) (gp : Point.ListInGenPos S) :
-    ConvexEmptyIn s S.toFinset ↔
-    ∀ (t : Finset Point), t.card = 3 → t ⊆ s → EmptyShapeIn t S.toFinset := by
+theorem ConvexEmptyIn.iff_triangles' {s : Finset Point} {S : Finset Point}
+    (sS : s ⊆ S) (gp : Point.SetInGenPos S) :
+    ConvexEmptyIn s S ↔
+    ∀ (t : Finset Point), t.card = 3 → t ⊆ s → EmptyShapeIn t S := by
   if sz : 3 ≤ s.card then
-    have' sS' : (s:Set _) ⊆ S.toFinset := sS
+    have' sS' : (s:Set _) ⊆ S := sS
     rw [ConvexEmptyIn.iff_triangles sS' sz]
     simp (config := {contextual := true}) [ConvexEmptyIn,
       fun a b => ConvexIndep.triangle' a (subset_trans b sS) gp]
@@ -134,16 +136,17 @@ theorem ConvexEmptyIn.iff_triangles' {s : Finset Point} {S : List Point}
       | ⟨[a], _, (eq : s = {a})⟩, _ => subst eq; simpa using pS'
       | ⟨[a,b], h1, eq⟩, _ =>
         have : s = {a, b} := eq ▸ by ext; simp
-        have gp' := Point.ListInGenPos.subperm.1 gp <|
-          List.subperm_of_subset (.cons (a := p) (by simpa [this] using pn) h1) <|
-          List.cons_subset.2 ⟨by simpa using pS, by simpa [this, Finset.insert_subset_iff] using sS⟩
+        have gp' : Point.InGenPos₃ p a b := by
+          apply gp
+          · intro _ _; aesop
+          · aesop
         cases gp'.not_mem_seg (by simpa [this] using pS')
 
-theorem ConvexEmptyIn.iff_triangles'' {s : Finset Point} {S : List Point}
-    (sS : s ⊆ S.toFinset) (gp : Point.ListInGenPos S) :
-    ConvexEmptyIn s S.toFinset ↔
+theorem ConvexEmptyIn.iff_triangles'' {s : Finset Point} {S : Finset Point}
+    (sS : s ⊆ S) (gp : Point.SetInGenPos S) :
+    ConvexEmptyIn s S ↔
     ∀ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a ≠ b → a ≠ c → b ≠ c →
-      ∀ p ∈ S.toFinset \ {a,b,c}, ¬PtInTriangle p a b c := by
+      ∀ p ∈ S \ {a,b,c}, ¬PtInTriangle p a b c := by
   simp_rw [iff_triangles' sS gp, Finset.card_eq_three, EmptyShapeIn, PtInTriangle]
   constructor
   . intro H a ha b hb c hc ab ac bc p hp
@@ -165,20 +168,15 @@ theorem ConvexEmptyIn.iff_triangles'' {s : Finset Point} {S : List Point}
 theorem ConvexIndep.iff_triangles' {s : Finset Point} (gp : Point.SetInGenPos s) :
     ConvexIndep s ↔ ∀ (t : Finset Point), t.card = 3 → t ⊆ s → EmptyShapeIn t s := by
   have : s = s.toList.toFinset := s.toList_toFinset.symm
-  rw [← ConvexEmptyIn.refl_iff, this, ← ConvexEmptyIn.iff_triangles' subset_rfl]
-  apply Point.SetInGenPos.of_nodup
-  simp [gp]
-  exact Finset.nodup_toList s
+  rw [← ConvexEmptyIn.refl_iff, ← ConvexEmptyIn.iff_triangles' subset_rfl]
+  exact gp
 
 theorem ConvexIndep.iff_triangles'' {s : Finset Point} (gp : Point.SetInGenPos s) :
     ConvexIndep s ↔
     ∀ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a ≠ b → a ≠ c → b ≠ c →
       ∀ p ∈ s \ {a,b,c}, ¬PtInTriangle p a b c := by
-  have : s = s.toList.toFinset := s.toList_toFinset.symm
-  rw [← ConvexEmptyIn.refl_iff, this, ← ConvexEmptyIn.iff_triangles'' subset_rfl]
-  apply Point.SetInGenPos.of_nodup
-  simp [gp]
-  exact Finset.nodup_toList s
+  rw [← ConvexEmptyIn.refl_iff, ← ConvexEmptyIn.iff_triangles'' subset_rfl]
+  exact gp
 
 open Point in
 theorem split_convexHull (cvx : ConvexIndep S) :

Lean/Geo/Hexagon/TheMainTheorem.lean

@@ -6,34 +6,27 @@ import Geo.Hexagon.Encoding
 namespace Geo
 open Classical LeanSAT Model
 
--- /-- This asserts that the CNF produced by `lake exe encode gon 6 17` is UNSAT -/
--- axiom unsat_6gon_cnf : (Geo.hexagonCNF (rlen := 17-1) (holes := false)).isUnsat
+variable (unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1) (holes := true)).isUnsat)
 
--- theorem gon_6_theorem (pts : List Point) (gp : Point.ListInGenPos pts)
---     (h : pts.length ≥ 17) : HasConvexKGon 6 pts.toFinset := by
---   refine HasConvexKGon_extension gp (fun pts gp h => ?_) h
---   by_contra h'
---   have noσgon : ¬σHasConvexKGon 6 pts.toFinset := mt (σHasConvexKGon_iff_HasConvexKGon gp).1 h'
---   have ⟨w, ⟨hw⟩⟩ := @symmetry_breaking pts (h ▸ by decide) gp
---   have noσgon' : ¬σHasEmptyKGonIf 6 (holes := false) w.toFinset :=
---     OrientationProperty_σHasConvexKGon.not (hw.toEquiv w.nodup) noσgon
---   have rlen_eq : w.rlen = 16 := Nat.succ_inj.1 <| hw.length_eq.symm.trans h
---   apply unsat_6gon_cnf
---   with_reducible
---     have := (PropForm.toICnf_sat _).2 ⟨w.toPropAssn false, w.satisfies_hexagonEncoding noσgon'⟩
---     rw [rlen_eq] at this
---     rwa [hexagonCNF]
-
-variable (unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1) (holes := true)).isUnsat) in
-theorem hole_6_theorem : holeNumber 6 ≤ 30 := by
-  refine holeNumber_le.2 fun pts h _ gp => by_contra fun h' => ?_
-  have noσtri : ¬σHasEmptyKGon 6 pts.toFinset := mt (σHasEmptyKGon_iff_HasEmptyKGon gp).1 h'
-  have ⟨w, ⟨hw⟩⟩ := @symmetry_breaking pts (h ▸ by decide) gp
+theorem hole_6_theorem : ∀ (pts : Finset Point),
+    Point.SetInGenPos pts → pts.card = 30 → HasEmptyKGon 6 pts := by
+  intro pts gp h
+  by_contra h'
+  have noσtri : ¬σHasEmptyKGon 6 pts := mt (σHasEmptyKGon_iff_HasEmptyKGon gp).1 h'
+  have ⟨w, ⟨hw⟩⟩ := @symmetry_breaking pts.toList (by simp [h]) gp.toList
   have noσtri' : ¬σHasEmptyKGonIf 6 (holes := true) w.toFinset :=
-    OrientationProperty_σHasEmptyKGon.not (hw.toEquiv w.nodup) noσtri
-  have rlen29 : w.rlen = 29 := Nat.succ_inj.1 <| hw.length_eq.symm.trans h
+    OrientationProperty_σHasEmptyKGon.not (hw.toEquiv w.nodup) (by simpa using noσtri)
+  have rlen29 : w.rlen = 29 := Nat.succ_inj.1 <| hw.length_eq.symm.trans (by simp; simpa using h)
   apply unsat_6hole_cnf
   with_reducible
     have := (PropForm.toICnf_sat _).2 ⟨w.toPropAssn, w.satisfies_hexagonEncoding noσtri'⟩
     rw [rlen29] at this
     rwa [hexagonCNF]
+
+theorem hole_6_theorem' : holeNumber 6 ≤ ↑(30 : Nat) := by
+  rw [holeNumber_le]
+  intro pts h nodup genpos
+  apply hole_6_theorem
+  · exact unsat_6hole_cnf
+  · apply genpos.toFinset
+  · rw [List.toFinset_card_of_nodup nodup]; exact h

Lean/Geo/LowerBound/HoleCheckerProof.lean

@@ -795,4 +795,4 @@ theorem hole_lower_bound {r : Nat} (points : List NPoint)
     points.length + 1 ≤ holeNumber (r+3) := by
   let ⟨(), eq⟩ := Option.isSome_iff_exists.1 checkIt
   let ⟨H1, H2, H3⟩ := of_holeCheck' MaybeHoles.yes_wf eq
-  simpa using holeNumber_lower_bound (↑'points) H1 H2 (mt (σHasEmptyKGon_iff_HasEmptyKGon H2).2 H3)
+  simpa using holeNumber_lower_bound (↑'points) H1 H2 (mt (σHasEmptyKGon_iff_HasEmptyKGon H2.toFinset).2 H3)

Lean/Geo/Naive/TheMainTheorem.lean

@@ -8,7 +8,7 @@ open Classical LeanSAT Model
 
 theorem empty_kgon_naive (unsat : (Geo.naiveCNF k (r+2)).isUnsat) : holeNumber k ≤ r + 3 := by
   refine holeNumber_le.2 fun pts h _ gp => by_contra fun h' => ?_
-  have noσtri : ¬σHasEmptyKGon k pts.toFinset := mt (σHasEmptyKGon_iff_HasEmptyKGon gp).1 h'
+  have noσtri : ¬σHasEmptyKGon k pts.toFinset := mt (σHasEmptyKGon_iff_HasEmptyKGon gp.toFinset).1 h'
   have ⟨w, ⟨hw⟩⟩ := @symmetry_breaking pts (h ▸ Nat.le_add_left ..) gp
   have noσtri' : ¬σHasEmptyKGon k w.toFinset :=
     OrientationProperty_σHasEmptyKGon.not (hw.toEquiv w.nodup) noσtri