1 files changed, 187 insertions, 0 deletions
diff --git a/Brooks.lean b/Brooks.lean
new file mode 100644
index 0000000..24c6daa
--- /dev/null
+++ b/Brooks.lean
@@ -0,0 +1,187 @@
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Combinatorics.SimpleGraph.Coloring
+import Mathlib.Combinatorics.SimpleGraph.Subgraph
+import Mathlib.Combinatorics.SimpleGraph.Path
+import Mathlib.Combinatorics.SimpleGraph.Walk
+import Mathlib.Combinatorics.SimpleGraph.Maps
+import Mathlib.Order.Disjoint
+import Mathlib.Data.List.Basic
+import Mathlib.Data.List.Lemmas
+import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Fintype.Sets
+import Mathlib.Data.Set.Basic
+import Mathlib.Tactic.Linarith
+
+open SimpleGraph List Walk Set.Notation
+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]
+
+noncomputable def extend_coloring
+  (S : Set V) (S_coloring : Coloring (G.induce S) α)
+  (v : V) (c : α)
+  (h : c ∉ S_coloring '' (S ↓∩ G.neighborSet v))
+  : Coloring (G.induce (S ∪ {v})) α
+  := by
+  simp at h
+  apply Coloring.mk
+  case color =>
+    intro ⟨x, mem⟩
+    by_cases hx : x ∈ S
+    · exact S_coloring ⟨x, hx⟩
+    · exact c
+  case valid =>
+    rintro ⟨x₁, mem_x₁⟩ ⟨x₂, mem_x₂⟩
+    intro adj
+    by_cases hx₁ : x₁ ∈ S <;> by_cases hx₂ : x₂ ∈ S
+    -- 4 cases according to whether x₁ and/or x₂ are in S or not
+    · simp [hx₁, hx₂]
+      exact S_coloring.valid adj
+    · simp [hx₁, hx₂]
+      replace hx₂ : x₂ = v := mem_x₂.resolve_left hx₂
+      simp [hx₂] at adj
+      exact h x₁ (G.adj_symm adj) hx₁
+    · simp [hx₁, hx₂]
+      replace hx₁ : x₁ = v := mem_x₁.resolve_left hx₁
+      simp [hx₁] at adj
+      -- TODO the following 2 lines are kind of cumbersome
+      intro wrong
+      exact (h x₂ adj hx₂) (Eq.symm wrong)
+    · intro a
+      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
+  apply Finset.card_bij'
+  case i => exact fun a _ => ↑a
+  case j =>
+    intro a h
+    simp only [Set.toFinset_inter, Finset.mem_inter, Set.mem_toFinset] at h
+    exact ⟨a, h.left⟩
+  case hi =>
+    intro a ha
+    simp_all only [not_false_eq_true, true_and, Set.mem_toFinset, Set.mem_preimage, Set.toFinset_inter,
+      Finset.mem_inter, Subtype.coe_prop, and_self]
+  case hj =>
+    intro a ha
+    simp_all only [not_false_eq_true, true_and, Set.mem_toFinset, Set.mem_preimage]
+    simp_all only [Set.toFinset_inter, Finset.mem_inter, Set.mem_toFinset]
+  case left_inv =>
+    intro a ha
+    simp_all only [not_false_eq_true, true_and, Subtype.coe_eta]
+  case right_inv =>
+    intro a ha
+    simp_all only [not_false_eq_true, true_and]
+
+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
+  classical
+  let ⟨W, W_is_path⟩ := P
+  cases W with
+  | nil =>
+    simp
+    rw [List.toSet_nil, 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
+
+    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
+      intro wrong
+      have u_in_W' := List.Mem.tail w wrong
+      rw [←(Walk.support_eq_cons W')] at u_in_W'
+      contradiction
+    have hu : u ∈ (N \ C) := by
+      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]
+        _ = 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
+      have ineq2 : 1 ≤ (N \ C).toFinset.card := by
+        simp only [Finset.one_le_card, Set.toFinset_nonempty]
+        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 fact : (W'.support.tail.toSet ∪ {w} : Set V) = W'.support.toSet := by
+      simp [List.toSet, Set.union_def, Or.comm, Walk.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
+
+theorem brooks'
+  (k : ℕ) (k_ge_3 : k ≥ 3)
+  (maxDeg_le_k : G.maxDegree ≤ k)
+  (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 _ =>
+    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
+      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