beginning of pf of brooks' theorem, procedure to extend path maximally

1 files changed, 171 insertions, 52 deletions

diff --git a/Brooks.lean b/Brooks.lean
index 24c6daa..669ecc7 100644
--- a/Brooks.lean
+++ b/Brooks.lean
@@ -9,6 +9,7 @@ import Mathlib.Order.Disjoint
 import Mathlib.Data.List.Basic
 import Mathlib.Data.List.Lemmas
 import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Fintype.Card
 import Mathlib.Data.Fintype.Sets
 import Mathlib.Data.Set.Basic
 import Mathlib.Tactic.Linarith
@@ -19,13 +20,7 @@ open Classical
 variable
   {α : Type}
   {V : Type} [Fintype V]
-  (G : SimpleGraph V)  [DecidableRel G.Adj]
-
-namespace List
-  abbrev toSet (l : List α) := { x | x ∈ l }
-
-  lemma toSet_nil : ([] : List α).toSet = ∅ := by
-    simp_all only [toSet, not_mem_nil, Set.setOf_false]
+  (G : SimpleGraph V) [DecidableRel G.Adj]
 
 noncomputable def extend_coloring
   (S : Set V) (S_coloring : Coloring (G.induce S) α)
@@ -61,7 +56,7 @@ noncomputable def extend_coloring
       simp_all only [comap_adj, Function.Embedding.coe_subtype]
       simp_all only [Set.union_singleton, Set.mem_insert_iff, or_false, SimpleGraph.irrefl]
 
-lemma preimage_val_card {A B : Set V} : (A ↓∩ B).toFinset.card = (A ∩ B).toFinset.card := by
+lemma preimage_val_card (A B : Set V) : (A ↓∩ B).toFinset.card = (A ∩ B).toFinset.card := by
   apply Finset.card_bij'
   case i => exact fun a _ => ↑a
   case j =>
@@ -83,29 +78,70 @@ lemma preimage_val_card {A B : Set V} : (A ↓∩ B).toFinset.card = (A ∩ B).t
     intro a ha
     simp_all only [not_false_eq_true, true_and]
 
+lemma extend_coloring'
+  {k : ℕ}
+  (S : Set V) (S_colorable : Colorable (G.induce S) k)
+  (v : V) (h : (G.neighborSet v ∩ S).toFinset.card < k)
+  : Colorable (G.induce (S ∪ {v})) k := by
+  have S_coloring := S_colorable.some
+  let N := G.neighborSet v
+
+  have card_fact : (S ↓∩ N).toFinset.card = (S ∩ N).toFinset.card := by
+    -- without "convert" this gives a timeout error
+    have foo := preimage_val_card S N
+    convert foo
+
+  have unused_color : ∃ c : Fin k, c ∉ S_coloring '' (S ↓∩ N) := by
+    suffices (S_coloring '' (S ↓∩ N)).toFinset.card < (Set.univ : Set (Fin k)).toFinset.card from by
+      have ⟨c, hc⟩ := Finset.exists_mem_not_mem_of_card_lt_card this
+      simp only [Set.mem_toFinset] at hc
+      exact ⟨c, hc.right⟩
+    simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin]
+    calc
+      (Finset.image (⇑S_coloring) (S ↓∩ N).toFinset).card ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le
+      _ = (S ∩ N).toFinset.card := card_fact
+      _ = (N ∩ S).toFinset.card := by simp only [Set.inter_comm]
+      _ < k := h
+  have ⟨c, hc⟩ := unused_color
+  exact Nonempty.intro (extend_coloring G S S_coloring v c hc)
+
+lemma extend_coloring''
+  {k : ℕ}
+  (S : Set V) (S_colorable : Colorable (G.induce S) k)
+  (v : V) (h : G.degree v < k)
+  : Colorable (G.induce (S ∪ {v})) k := by
+  apply extend_coloring'
+  · assumption
+  · calc
+    (G.neighborSet v ∩ S).toFinset.card ≤ (G.neighborSet v).toFinset.card := by
+      simp only [Set.toFinset_inter]
+      apply Finset.card_le_card
+      simp only [Set.subset_toFinset, Finset.coe_inter, Set.coe_toFinset, Set.inter_subset_left]
+    _ = G.degree v := by simp only [Set.toFinset_card, G.card_neighborSet_eq_degree]
+    _ < k := h
+
 theorem color_path
     (k : ℕ) (maxDeg_le_k : G.maxDegree ≤ k)
     {u v : V} (P : G.Path u v)
     (S : Set V)
     (P_outside_S : ∀ x ∈ P.val.support, x ∉ S)
     (S_colorable : Colorable (G.induce S) k)
-    : Colorable (G.induce (S ∪ P.val.support.tail.toSet)) k := by
+    : Colorable (G.induce (S ∪ P.val.support.tail.toFinset)) k := by
   classical
   let ⟨W, W_is_path⟩ := P
   cases W with
   | nil =>
     simp
-    rw [List.toSet_nil, Set.union_empty]
+    rw [Finset.coe_empty, Set.union_empty]
     exact S_colorable
   | @cons u w v adj W' =>
     simp at *
     let P' : G.Path w v := ⟨W', IsPath.of_cons W_is_path⟩
     have P'_colorable := color_path k maxDeg_le_k P' S (P_outside_S.right) S_colorable
-    let P'_coloring := P'_colorable.some
 
     let N := G.neighborSet w
     -- set of vertices already colored by P'_coloring
-    let C := S ∪ W'.support.tail.toSet
+    let C := S ∪ W'.support.tail.toFinset
 
     have u_not_in_W' : u ∉ W'.support := ((Walk.cons_isPath_iff adj W').mp W_is_path).right
     have u_not_in_W'_tail : u ∉ W'.support.tail := by
@@ -117,22 +153,8 @@ theorem color_path
       simp [N, C]
       exact ⟨G.adj_symm adj, P_outside_S.left, u_not_in_W'_tail⟩
 
-    have card_fact : (C ↓∩ N).toFinset.card = (C ∩ N).toFinset.card :=
-      -- TODO the below gives a timeout error
-      -- preimage_val_card
-      sorry
-
-    have unused_color : ∃ c : Fin k, c ∉ P'_coloring '' (C ↓∩ N) := by
-      suffices (P'_coloring '' (C ↓∩ N)).toFinset.card < (Set.univ : Set (Fin k)).toFinset.card from by
-        have ⟨c, hc⟩ := Finset.exists_mem_not_mem_of_card_lt_card this
-        simp only [Set.mem_toFinset] at hc
-        exact ⟨c, hc.right⟩
-      simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin]
-      suffices (C ↓∩ N).toFinset.card < k from calc
-        (Finset.image (⇑P'_coloring) (C ↓∩ N).toFinset).card ≤ (C ↓∩ N).toFinset.card := Finset.card_image_le
-        _ < k := this
-      have ineq1 : (C ↓∩ N).toFinset.card + (N \ C).toFinset.card ≤ k := calc
-        (C ↓∩ N).toFinset.card + (N \ C).toFinset.card = (N ∩ C).toFinset.card + (N \ C).toFinset.card := by simp only [card_fact, Set.inter_comm]
+    have h : (N ∩ C).toFinset.card < k := by
+      have ineq1 : (N ∩ C).toFinset.card + (N \ C).toFinset.card ≤ k := calc
         _ = N.toFinset.card := by simp only [Set.toFinset_inter, Set.toFinset_diff, Finset.card_inter_add_card_sdiff]
         _ ≤ G.maxDegree := G.degree_le_maxDegree w
         _ ≤ k := maxDeg_le_k
@@ -141,30 +163,65 @@ theorem color_path
         exact ⟨u, hu⟩
       linarith
 
-    let ⟨c, hc⟩ := unused_color
-    have extended_coloring := extend_coloring G (S ∪ W'.support.tail.toSet) P'_coloring w c hc
+    have extended_coloring := by
+      apply extend_coloring' G C P'_colorable w
+      -- TODO without "convert" this gives a timeout error
+      convert h
 
-    have fact : (W'.support.tail.toSet ∪ {w} : Set V) = W'.support.toSet := by
-      simp [List.toSet, Set.union_def, Or.comm, Walk.mem_support_iff]
+    have fact : (W'.support.tail.toFinset ∪ {w} : Set V) = W'.support.toFinset := by
+      simp only [coe_toFinset, Set.union_def, Set.mem_setOf_eq, Set.mem_singleton_iff, Or.comm, mem_support_iff]
 
     rw [Set.union_assoc, fact] at extended_coloring
-    exact Nonempty.intro extended_coloring
-
--- lemma trivial_graph_colorable {k : ℕ} (h : Fintype.card V = 0) : Colorable G k := by
---   simp [Fintype.card_eq_zero_iff, IsEmpty] at h
---   apply Nonempty.intro
---   apply Coloring.mk
---   case color => exact isEmptyElim
---   case valid =>
---     intro v
---     exact isEmptyElim v
-
-namespace SimpleGraph
-  theorem maxDegree_mono (G' : Subgraph G) : G'.maxDegree ≤ G.maxDegree := by
-    apply maxDegree_le_of_forall_degree_le
-    intro v
-    calc
-      G'.degree v
+    exact extended_coloring
+
+lemma induce_maxDegree_mono (S : Set V) : (G.induce S).maxDegree ≤ G.maxDegree := by
+  simp only [G.induce_eq_coe_induce_top S]
+  apply maxDegree_le_of_forall_degree_le
+  intro v
+  rw [Subgraph.coe_degree]
+  calc
+    ((⊤ : G.Subgraph).induce S).degree v ≤ G.degree v := Subgraph.degree_le ((⊤ : G.Subgraph).induce S) v
+    _ ≤ G.maxDegree := G.degree_le_maxDegree v
+
+noncomputable def extend_path_maximally {u v : V} (P : G.Path u v)
+  : ∃ w : V, ∃ Q : G.Walk w u, IsPath (Walk.append Q P.1) ∧ G.neighborFinset w ⊆ (Walk.append Q P.1).support.toFinset := by
+  replace ⟨P, hP⟩ := P
+  induction hn : Fintype.card V - P.support.length generalizing u P
+
+  case zero =>
+    have fact : P.support.toFinset = Finset.univ := by
+      apply Finset.eq_univ_of_card
+      rw [isPath_def] at hP
+      rw [←(List.toFinset_card_of_nodup hP)] at hn
+      apply Nat.le_antisymm
+      · exact Finset.card_le_univ P.support.toFinset
+      · omega
+    use u, Walk.nil
+    simp only [Walk.nil_append, fact, Finset.coe_univ, Finset.subset_univ, and_true]
+    assumption
+
+  case succ n ih =>
+    by_cases hu : G.neighborFinset u ⊆ P.support.toFinset
+    case pos =>
+      use u, Walk.nil
+      simp only [Walk.nil_append]
+      exact ⟨hP, hu⟩
+    case neg =>
+      simp [Finset.subset_iff] at hu
+      have ⟨x, e, hx⟩ := hu
+      replace e : G.Adj x u := G.adj_symm e
+      let P' := Walk.cons e P
+      have hP' : IsPath P' := IsPath.cons hP hx
+      have hn' : Fintype.card V - P'.support.length = n := by
+        simp only [P', Walk.support_cons, List.length_cons]
+        omega
+      have ⟨w, Q', hQ'⟩ := ih P' hP' hn'
+      let Q := Walk.concat Q' e
+      use w, Q
+      simp only [Q, Walk.concat_append]
+      simp only [P'] at hQ'
+      assumption
+
 
 theorem brooks'
   (k : ℕ) (k_ge_3 : k ≥ 3)
@@ -172,16 +229,78 @@ theorem brooks'
   (no_max_clique : CliqueFree G (k + 1))
   : Colorable G k := by
   induction hn : Fintype.card V using Nat.strong_induction_on generalizing V G
-  case h n ih _ =>
+  case h n ih _ _ =>
     by_cases h : n ≤ k
     · have n_colorable := G.colorable_of_fintype
       rw [hn] at n_colorable
       exact Colorable.mono h n_colorable
     · by_cases k_reg : G.IsRegularOfDegree k
+      -- Assume G is not k-regular.
       case neg =>
         simp [IsRegularOfDegree] at k_reg
         have ⟨x, hx⟩ := k_reg
         let S : Set V := Set.univ \ {x}
         let G' := G.induce S
-        have S_maxDeg_le_k : G'.maxDegree ≤ k := G.
-      case pos => sorry
+
+        -- Apply induction
+        have S_maxDeg_le_k : G'.maxDegree ≤ k := sorry -- induce_maxDegree_mono G S
+        have S_no_max_clique : G'.CliqueFree (k + 1) := CliqueFree.comap (Embedding.induce S) no_max_clique
+        have S_card : Fintype.card (↑S) = n - 1 := by
+          simp only [S, ←Set.toFinset_card, Set.toFinset_diff, Set.toFinset_univ, Set.toFinset_singleton]
+          have fact := Finset.card_inter_add_card_sdiff Finset.univ {x}
+          simp [hn] at fact
+          omega
+        have fact : n - 1 < n := by omega
+        have S_colorable : (G.induce S).Colorable k := ih (n - 1) fact (G.induce S) S_maxDeg_le_k S_no_max_clique S_card
+
+        replace hx : G.degree x < k := by
+          have hx' : G.degree x ≤ k := Nat.le_trans (G.degree_le_maxDegree x) maxDeg_le_k
+          omega
+
+        have G_colorable := extend_coloring'' G S S_colorable x hx
+        have fact : S ∪ {x} = Set.univ := by simp only [Set.union_singleton,
+          Set.insert_diff_singleton, Set.mem_univ, Set.insert_eq_of_mem, S]
+        rw [fact] at G_colorable
+        exact Colorable.of_embedding (G.induceUnivIso.symm.toEmbedding) G_colorable
+
+      -- Assume G is k-regular.
+      case pos =>
+        -- Pick any vertex v.
+        have V_nonempty : Nonempty V := by
+          apply Fintype.card_pos_iff.mp
+          omega
+        let v := V_nonempty.some
+
+        -- Since G does not contain a clique on k+1 vertices, there exist
+        -- two neighbours x, y of v that are not adjacent in G.
+        have claim : ∃ x y : V, x ≠ y ∧ G.Adj v x ∧ G.Adj v y ∧ ¬G.Adj x y := by
+          by_contra wrong
+          apply no_max_clique
+          case t => exact (G.neighborSet v ∪ {v}).toFinset
+          case a =>
+            apply IsNClique.mk
+            case card_eq =>
+              simp only [Set.union_singleton, Set.toFinset_insert, Set.mem_toFinset,
+                mem_neighborSet, SimpleGraph.irrefl, not_false_eq_true,
+                Finset.card_insert_of_not_mem, Set.toFinset_card, Fintype.card_ofFinset,
+                Nat.add_left_inj]
+              have fact : ({x | G.Adj v x} : Finset V) = G.neighborFinset v := by
+                ext a
+                simp only [Finset.mem_filter, Finset.mem_univ, true_and, mem_neighborFinset]
+              simp only [fact, card_neighborFinset_eq_degree]
+              exact k_reg v
+            case isClique =>
+              intro x hx y hy x_ne_y
+              simp at hx hy
+              cases' hx with x_eq_v hx <;> cases' hy with y_eq_v hy
+              · rw [x_eq_v, y_eq_v] at x_ne_y
+                contradiction
+              · rw [←x_eq_v] at hy
+                assumption
+              · rw [←y_eq_v] at hx
+                exact G.adj_symm hx
+              · simp at wrong
+                exact wrong x y x_ne_y hx hy
+
+        have ⟨x, y, x_ne_y, hx, hy, x_nadj_y⟩ := claim
+        sorry