diff --git a/ITP/geometry.tex b/ITP/geometry.tex index 690340e..f185c62 100644 --- a/ITP/geometry.tex +++ b/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} diff --git a/Lean/Geo.lean b/Lean/Geo.lean index dfc57a3..0335fc7 100644 --- a/Lean/Geo.lean +++ b/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), diff --git a/Lean/Geo/Canonicalization/SymmetryBreaking.lean b/Lean/Geo/Canonicalization/SymmetryBreaking.lean index 448fecf..6c4c2b3 100644 --- a/Lean/Geo/Canonicalization/SymmetryBreaking.lean +++ b/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 .. diff --git a/Lean/Geo/Definitions/OrientationProperties.lean b/Lean/Geo/Definitions/OrientationProperties.lean index ec28338..512f03a 100644 --- a/Lean/Geo/Definitions/OrientationProperties.lean +++ b/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 ?_ diff --git a/Lean/Geo/Definitions/Structures.lean b/Lean/Geo/Definitions/Structures.lean index cc1d29c..586508d 100644 --- a/Lean/Geo/Definitions/Structures.lean +++ b/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) : diff --git a/Lean/Geo/Hexagon/TheMainTheorem.lean b/Lean/Geo/Hexagon/TheMainTheorem.lean index bf5b5e7..52d89ff 100644 --- a/Lean/Geo/Hexagon/TheMainTheorem.lean +++ b/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 diff --git a/Lean/Geo/LowerBound/HoleCheckerProof.lean b/Lean/Geo/LowerBound/HoleCheckerProof.lean index 15f0e1b..378603a 100644 --- a/Lean/Geo/LowerBound/HoleCheckerProof.lean +++ b/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) diff --git a/Lean/Geo/Naive/TheMainTheorem.lean b/Lean/Geo/Naive/TheMainTheorem.lean index 62df626..33df68c 100644 --- a/Lean/Geo/Naive/TheMainTheorem.lean +++ b/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