rename ConvexPoints -> ConvexIndep

ITP/encoding.tex

@@ -133,7 +133,7 @@
 of points on either side of $\overleftrightarrow{ab}$.
 That is:
 \begin{lstlisting}
-theorem split_convexHull (cvx : ConvexPoints S) :
+theorem split_convexHull (cvx : ConvexIndep S) :
   ∀ {a b}, a ∈ S → b ∈ S →
     convexHull ℝ S ⊆ convexHull ℝ {x ∈ S | σ a b x ≠ ccw}
                     ∪ convexHull ℝ {x ∈ S | σ a b x ≠ cw}

ITP/fig_triangulation.tex

@@ -66,5 +66,5 @@
         \end{tikzpicture}
         \caption{}\label{fig:triangulation-b}
     \end{subfigure}
-    \caption{Illustration of the proof for \lstinline|ConvexEmptyIn.iff_triangles|. The left subfigure shows how a point in $S \setminus s$ that lies inside  $s$ will be inside one of the triangles induced by the convex hull of $s$ (orange triangle). The right subfigure shows how if the $\textsf{ConvexPoints}$ predicate does not hold of $s$, then some point $a \in s$ will be inside one of the triangles induced by the convex hull of $s \setminus \{a\}$.}\label{fig:triangulation}
+    \caption{Illustration of the proof for \lstinline|ConvexEmptyIn.iff_triangles|. The left subfigure shows how a point in $S \setminus s$ that lies inside  $s$ will be inside one of the triangles induced by the convex hull of $s$ (orange triangle). The right subfigure shows how if the $\textsf{ConvexIndep}$ predicate does not hold of $s$, then some point $a \in s$ will be inside one of the triangles induced by the convex hull of $s \setminus \{a\}$.}\label{fig:triangulation}
 \end{figure}

ITP/geometry.tex

@@ -7,13 +7,13 @@
 def EmptyShapeIn (S P : Set Point) : Prop :=
     ∀ p ∈ P \ S, p ∉ convexHull ℝ S
 
-/-- `ConvexPoints S' means that `S' consists of extremal points of its convex hull,
+/-- `ConvexIndep S' means that `S' consists of extremal points of its convex hull,
 i.e., the point set encloses a convex polygon. -/
-def ConvexPoints (S : Set Point) : Prop :=
+def ConvexIndep (S : Set Point) : Prop :=
     ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a})
 
 def ConvexEmptyIn (S P : Set Point) : Prop :=
-    ConvexPoints S ∧ EmptyShapeIn S P
+    ConvexIndep S ∧ EmptyShapeIn S P
 
 def HasEmptyKGon (k : Nat) (S : Set Point) : Prop :=
     ∃ s : Finset Point, s.card = k ∧ ↑s ⊆ S ∧ ConvexEmptyIn s S
@@ -37,10 +37,10 @@
 \end{lstlisting}
 \input{fig_triangulation.tex}
 \begin{proof}[Proof sketch]
-    We first prove a simple monotonicity lemma: if $\textsf{ConvexPoints}(s)$, then $\textsf{ConvexPoints}(s')$ for every $s' \subseteq s$, and similarly $\textsf{EmptyShapeIn}(s, S) \Rightarrow \textsf{EmptyShapeIn}(s', S)$ for every set of points $S$.
+    We first prove a simple monotonicity lemma: if $\textsf{ConvexIndep}(s)$, then $\textsf{ConvexIndep}(s')$ for every $s' \subseteq s$, and similarly $\textsf{EmptyShapeIn}(s, S) \Rightarrow \textsf{EmptyShapeIn}(s', S)$ for every set of points $S$.
     By instantiating this monotonicity lemma over all subsets $t \subseteq s$ with $|t| = 3$ we get the forward direction of the theorem.
-    For the backward direction it is easier to reason contrapositively: if the~$\textsf{ConvexPoints}$ predicate does not hold of $s$, or if $s$ is not empty w.r.t.~$S$, then we want to show that there is a triangle $t \subseteq s$ that is also not empty w.r.t.~$S$. To see this, let $H$ be the convex hull of $s$, and then by Carath\'eodory's theorem (cf. \lstinline|theorem convexHull_eq_union| from \textsf{mathlib}), every point in $H$ is a convex combination of at most $3$ points in $s$, and consequently, of exactly $3$ points in $s$.
-    If $s$ is non-empty w.r.t.~$S$, then there is a point $p \in S \setminus s$ that belongs to $H$, and by Carath\'eodory, $p$ is a convex combination of $3$ points in $s \setminus \{a\}$, and thus lies inside a triangle $t \subseteq s$ (\Cref{fig:triangulation-a}). If $s$ does not hold $\textsf{ConvexPoints}$, then there is a point $a \in s$ such that $a \in \textsf{convexHull}(s \setminus \{a\})$, and by Carath\'eodory again, $a$ is a convex combination of $3$ points in $s$, and thus lies inside a triangle $t \subseteq s \setminus \{a\}$ (\Cref{fig:triangulation-b}).
+    For the backward direction it is easier to reason contrapositively: if the~$\textsf{ConvexIndep}$ predicate does not hold of $s$, or if $s$ is not empty w.r.t.~$S$, then we want to show that there is a triangle $t \subseteq s$ that is also not empty w.r.t.~$S$. To see this, let $H$ be the convex hull of $s$, and then by Carath\'eodory's theorem (cf. \lstinline|theorem convexHull_eq_union| from \textsf{mathlib}), every point in $H$ is a convex combination of at most $3$ points in $s$, and consequently, of exactly $3$ points in $s$.
+    If $s$ is non-empty w.r.t.~$S$, then there is a point $p \in S \setminus s$ that belongs to $H$, and by Carath\'eodory, $p$ is a convex combination of $3$ points in $s \setminus \{a\}$, and thus lies inside a triangle $t \subseteq s$ (\Cref{fig:triangulation-a}). If $s$ does not hold $\textsf{ConvexIndep}$, then there is a point $a \in s$ such that $a \in \textsf{convexHull}(s \setminus \{a\})$, and by Carath\'eodory again, $a$ is a convex combination of $3$ points in $s$, and thus lies inside a triangle $t \subseteq s \setminus \{a\}$ (\Cref{fig:triangulation-b}).
 %     The
 %     The forward direction is easy to see, as triangles are always convex, and if $s$ is empty w.r.t.~$S$, then so are the triangles induced by vertices of $s$.
 %     Let $T = \{t_1, \ldots, t_{{k \choose 3}}\}$ be all the triangles induced by vertices of $s$.

Lean/Geo.lean

@@ -14,16 +14,16 @@ other than those already in `S`. -/
 recall Geo.EmptyShapeIn (S P : Set Point) : Prop :=
   ∀ p ∈ P \ S, p ∉ convexHull ℝ S
 
-/- `ConvexPoints S` means that `S` consists of extremal points of its convex hull,
+/- `ConvexIndep S` means that `S` consists of extremal points of its convex hull,
 i.e. the point set encloses a convex polygon. Also known as a "convex-independent set". -/
-recall Geo.ConvexPoints (S : Set Point) : Prop :=
+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 ∧ ConvexPoints s
+  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s
 
 recall Geo.HasEmptyKGon (n : Nat) (S : Set Point) : Prop :=
-  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexPoints s ∧ EmptyShapeIn s S
+  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s ∧ EmptyShapeIn s S
 
 /- `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`. -/

Lean/Geo/Definitions/OrientationProperties.lean

@@ -81,7 +81,7 @@ theorem σHasConvexKGon_iff_HasConvexKGon (gp : Point.ListInGenPos pts) :
   unfold σHasConvexKGon HasConvexKGon
   refine exists_congr fun s => and_congr_right' <| and_congr_right fun spts => ?_
   have gp' := gp.toFinset
-  rw [ConvexPoints.iff_triangles'' (gp'.mono spts)]
+  rw [ConvexIndep.iff_triangles'' (gp'.mono spts)]
   iterate 9 refine forall_congr' fun _ => ?_
   rw [σIsEmptyTriangleFor_iff'' (gp'.mono spts)] <;> simp [EmptyShapeIn, PtInTriangle, *]
 
@@ -227,7 +227,7 @@ theorem σCCWPoints.cycle (H : σCCWPoints (l₁ ++ l₂)) : σCCWPoints (l₂ +
     fun c hc => (H4 c hc).imp <| Eq.trans (by rw [σ_perm₁, ← σ_perm₂]),
     fun a ha => (H3 a ha).imp <| Eq.trans (by rw [σ_perm₂, ← σ_perm₁])⟩
 
-theorem σCCWPoints.convex (H : σCCWPoints l) : ConvexPoints l.toFinset := by
+theorem σCCWPoints.convex (H : σCCWPoints l) : ConvexIndep l.toFinset := by
   refine ((ConvexEmptyIn.iff_triangles'' subset_rfl H.gp).2 ?_).1
   simp only [mem_toFinset, Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton,
     not_or, and_imp]

Lean/Geo/Definitions/Structures.lean

@@ -21,14 +21,14 @@ theorem emptyShapeIn_congr_right {S : Set Point} (h : ∀ p ∉ S, p ∈ P₁ 
     EmptyShapeIn S P₁ ↔ EmptyShapeIn S P₂ :=
   forall_congr' fun _ => imp_congr_left <| and_congr_left (h _)
 
-/-- `ConvexPoints S` means that `S` consists of extremal points of its convex hull,
+/-- `ConvexIndep S` means that `S` consists of extremal points of its convex hull,
 i.e. the point set encloses a convex polygon. Also known as a "convex-independent set". -/
-def ConvexPoints (S : Set Point) : Prop :=
+def ConvexIndep (S : Set Point) : Prop :=
   ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a})
 
 open Classical
-theorem ConvexPoints.triangle_iff {a b c : Point} {h : [a, b, c].Nodup} :
-    ConvexPoints (Finset.mk (α := Point) [a,b,c] h) ↔ Point.InGenPos₃ a b c := by
+theorem ConvexIndep.triangle_iff {a b c : Point} {h : [a, b, c].Nodup} :
+    ConvexIndep (Finset.mk (α := Point) [a,b,c] h) ↔ Point.InGenPos₃ a b c := by
   constructor <;> intro h2
   · simp [not_or, Set.subset_def] at h ⊢
     refine Point.InGenPos₃.iff_not_mem_seg.2 ⟨?_, ?_, ?_⟩ <;>
@@ -44,7 +44,7 @@ theorem ConvexPoints.triangle_iff {a b c : Point} {h : [a, b, c].Nodup} :
     · exact h2.2.1 (convexHull_mono (by simp [Set.subset_def]) hp2)
     · exact h2.2.2 (convexHull_mono (by simp [Set.subset_def]) hp2)
 
-theorem ConvexPoints.lt_3 {s : Finset Point} (hs : s.card < 3) : ConvexPoints s := by
+theorem ConvexIndep.lt_3 {s : Finset Point} (hs : s.card < 3) : ConvexIndep s := by
   intro a ha hn
   rw [← Finset.coe_erase] at hn
   have := Nat.le_of_lt_succ <| (Finset.card_erase_lt_of_mem ha).trans_le (Nat.le_of_lt_succ hs)
@@ -55,25 +55,25 @@ theorem ConvexPoints.lt_3 {s : Finset Point} (hs : s.card < 3) : ConvexPoints s
     subst eq; simp at hn; subst b
     simpa using congrArg (a ∈ ·) e1
 
-theorem ConvexPoints.triangle' {s : Finset Point} {S : List Point}
+theorem ConvexIndep.triangle' {s : Finset Point} {S : List Point}
     (hs : s.card ≤ 3) (sS : s ⊆ S.toFinset) (gp : Point.ListInGenPos S) :
-    ConvexPoints s := by
+    ConvexIndep s := by
   cases lt_or_eq_of_le hs with
-  | inl hs => exact ConvexPoints.lt_3 hs
+  | inl hs => exact ConvexIndep.lt_3 hs
   | inr hs =>
     match s, s.exists_mk with | _, ⟨[a,b,c], h1, rfl⟩ => ?_
-    rw [ConvexPoints.triangle_iff]
+    rw [ConvexIndep.triangle_iff]
     apply Point.ListInGenPos.subperm.1 gp
     exact List.subperm_of_subset h1 (by simpa [Finset.subset_iff] using sS)
 
-theorem ConvexPoints.antitone {S₁ S₂ : Set Point} (S₁S₂ : S₁ ⊆ S₂)
-    (convex : ConvexPoints S₂) : ConvexPoints S₁ := by
+theorem ConvexIndep.antitone {S₁ S₂ : Set Point} (S₁S₂ : S₁ ⊆ S₂)
+    (convex : ConvexIndep S₂) : ConvexIndep S₁ := by
   intro a aS₁ aCH
   have : S₁ \ {a} ⊆ S₂ \ {a} := Set.diff_subset_diff S₁S₂ (le_refl _)
   apply convex a (S₁S₂ aS₁) (convexHull_mono this aCH)
 
 def ConvexEmptyIn (S P : Set Point) : Prop :=
-  ConvexPoints S ∧ EmptyShapeIn S P
+  ConvexIndep S ∧ EmptyShapeIn S P
 
 theorem ConvexEmptyIn.antitone_left {S₁ S₂ P : Set Point} (S₁S₂ : S₁ ⊆ S₂) :
     ConvexEmptyIn S₂ P → ConvexEmptyIn S₁ P := by
@@ -84,7 +84,7 @@ theorem ConvexEmptyIn.antitone_left {S₁ S₂ P : Set Point} (S₁S₂ : S₁ 
 
 @[simp]
 theorem ConvexEmptyIn.refl_iff {S : Set Point} :
-    ConvexEmptyIn S S ↔ ConvexPoints S :=
+    ConvexEmptyIn S S ↔ ConvexIndep S :=
   ⟨(·.left), (⟨·, EmptyShapeIn.rfl⟩)⟩
 
 theorem ConvexEmptyIn.iff {S P : Set Point} (SP : S ⊆ P) :
@@ -123,11 +123,11 @@ theorem ConvexEmptyIn.iff_triangles' {s : Finset Point} {S : List Point}
     have' sS' : (s:Set _) ⊆ S.toFinset := sS
     rw [ConvexEmptyIn.iff_triangles sS' sz]
     simp (config := {contextual := true}) [ConvexEmptyIn,
-      fun a b => ConvexPoints.triangle' a (subset_trans b sS) gp]
+      fun a b => ConvexIndep.triangle' a (subset_trans b sS) gp]
   else
     constructor <;> intro
     · intro _ h1 h2; cases sz (h1 ▸ Finset.card_le_card h2)
-    · refine ⟨ConvexPoints.lt_3 (not_le.1 sz), fun p ⟨pS, pn⟩ pS' => pn ?_⟩
+    · refine ⟨ConvexIndep.lt_3 (not_le.1 sz), fun p ⟨pS, pn⟩ pS' => pn ?_⟩
       have := Nat.le_of_lt_succ <| not_le.1 sz
       match s.exists_mk, this with
       | ⟨[], _, (eq : s = ∅)⟩, _ => subst eq; simp at pS'
@@ -162,16 +162,16 @@ theorem ConvexEmptyIn.iff_triangles'' {s : Finset Point} {S : List Point}
     simp at hp ⊢
     assumption
 
-theorem ConvexPoints.iff_triangles' {s : Finset Point} (gp : Point.SetInGenPos s) :
-    ConvexPoints s ↔ ∀ (t : Finset Point), t.card = 3 → t ⊆ s → EmptyShapeIn t s := by
+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
 
-theorem ConvexPoints.iff_triangles'' {s : Finset Point} (gp : Point.SetInGenPos s) :
-    ConvexPoints s ↔
+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
@@ -181,7 +181,7 @@ theorem ConvexPoints.iff_triangles'' {s : Finset Point} (gp : Point.SetInGenPos
   exact Finset.nodup_toList s
 
 open Point in
-theorem split_convexHull (cvx : ConvexPoints S) :
+theorem split_convexHull (cvx : ConvexIndep S) :
   ∀ {a b}, a ∈ S → b ∈ S →
     convexHull ℝ S ⊆
     convexHull ℝ {x ∈ S | σ a b x ≠ .ccw} ∪
@@ -254,7 +254,7 @@ theorem split_convexHull (cvx : ConvexPoints S) :
   right; refine (convex_convexHull ..).segment_subset hv ?_ this
   simp at zab; refine segment_subset_convexHull ?_ ?_ zab <;> simp [S2, ha, hb, σ_self₁, σ_self₂]
 
-theorem EmptyShapeIn.split (cvx : ConvexPoints S) (ha : a ∈ S) (hb : b ∈ S)
+theorem EmptyShapeIn.split (cvx : ConvexIndep S) (ha : a ∈ S) (hb : b ∈ S)
     (H1 : EmptyShapeIn {x ∈ S | σ a b x ≠ .ccw} P)
     (H2 : EmptyShapeIn {x ∈ S | σ a b x ≠ .cw} P) : EmptyShapeIn S P := fun _ ⟨pP, pS⟩ hn =>
   (split_convexHull cvx ha hb hn).elim (H1 _ ⟨pP, mt And.left pS⟩) (H2 _ ⟨pP, mt And.left pS⟩)
@@ -263,6 +263,6 @@ def HasEmptyKGon (n : Nat) (S : Set Point) : Prop :=
   ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexEmptyIn s S
 
 def HasConvexKGon (n : Nat) (S : Set Point) : Prop :=
-  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexPoints s
+  ∃ s : Finset Point, s.card = n ∧ ↑s ⊆ S ∧ ConvexIndep s
 
 end Geo

Lean/attic/Triangle/TheMainTheorem.lean

@@ -19,12 +19,12 @@ theorem HasEmptyTriangle.iff (S : Set Point) :
     match s, s.exists_mk with | _, ⟨[a,b,c], h1, rfl⟩ => ?_
     have s_eq : (Finset.mk (Multiset.ofList [a,b,c]) h1 : Set _) = {a, b, c} := by ext; simp
     simp [not_or, Set.subset_def] at h1 h2 h3 ⊢
-    refine ⟨a, h2.1, b, h2.2.1, c, h2.2.2, ConvexPoints.triangle_iff.1 h3, ?_⟩
+    refine ⟨a, h2.1, b, h2.2.1, c, h2.2.2, ConvexIndep.triangle_iff.1 h3, ?_⟩
     simpa [not_or, EmptyShapeIn, s_eq] using h4
   · intro ⟨a, ha, b, hb, c, hc, h1, h2⟩
     let s : Finset Point := ⟨[a,b,c], by simp [h1.ne₁, h1.ne₂, h1.ne₃]⟩
     have s_eq : s = {a,b,c} := by ext; simp
-    refine ⟨s, rfl, ?_, ConvexPoints.triangle_iff.2 h1, ?_⟩
+    refine ⟨s, rfl, ?_, ConvexIndep.triangle_iff.2 h1, ?_⟩
     · simp [Set.subset_def, ha, hb, hc]
     · simpa [s_eq, EmptyShapeIn] using h2