1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
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
|