Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/ColoringNumberOrdering/Full.lean
1import Catalog.Sparsity.ColoringNumbers.Full
2import Catalog.Sparsity.Admissibility.Full
3import Mathlib.Tactic
4
5open Catalog.Sparsity.ColoringNumbers
6
7namespace Catalog.Sparsity.ColoringNumberOrdering
8
9variable {V : Type*} [Fintype V] [LinearOrder V]
10
11open Classical
12
13noncomputable section
14
15open Catalog.Sparsity.Admissibility
16
17/-- Every vertex is in its own weak r-reachability set. -/
18private theorem self_mem_wreach (G : SimpleGraph V) (r : ℕ) (v : V) :
19 v ∈ WReach G r v := by
20 simp [WReach]
21
22/-- Every vertex is in its own strong r-reachability set. -/
23private theorem self_mem_sreach (G : SimpleGraph V) (r : ℕ) (v : V) :
24 v ∈ SReach G r v := by
25 simp [SReach]
26
27private def sreachStep (G : SimpleGraph V) (r : ℕ) (v : V) : Finset V :=
28 (SReach G r v \ {v}).toFinset
29
30private def strongLayer (G : SimpleGraph V) (r : ℕ) (v : V) : ℕ → Finset V
31 | 0 => {v}
32 | n + 1 => (strongLayer G r v n).biUnion (sreachStep G r)
33
34private def strongLayersUpTo (G : SimpleGraph V) (r : ℕ) (v : V) : Finset V :=
35 (Finset.range r).biUnion fun n => strongLayer G r v (n + 1)
36
37private theorem sreachStep_card_le_scol_sub_one (G : SimpleGraph V) (r : ℕ) (v : V) :
38 (sreachStep G r v).card ≤ scol G r - 1 := by
39 have hscol : (SReach G r v).ncard ≤ scol G r := by
40 unfold scol
41 exact Finset.le_sup (f := fun w => (SReach G r w).ncard) (by simp)
42 have hself := Set.ncard_diff_singleton_add_one (self_mem_sreach G r v) (Set.toFinite _)
43 have hcard : (sreachStep G r v).card + 1 = (SReach G r v).ncard := by
44 simpa [sreachStep, Set.ncard_eq_toFinset_card' _] using hself
45 omega
46
47private theorem strongLayer_card_le_pow (G : SimpleGraph V) (r : ℕ) (v : V) :
48 ∀ n, (strongLayer G r v n).card ≤ (scol G r - 1) ^ n
49 | 0 => by simp [strongLayer]
50 | n + 1 => by
51 calc
52 (strongLayer G r v (n + 1)).card
53 ≤ (strongLayer G r v n).card * (scol G r - 1) := by
54 simp [strongLayer]
55 exact Finset.card_biUnion_le_card_mul _ _ _ (by
56 intro w hw
57 exact sreachStep_card_le_scol_sub_one G r w)
58 _ ≤ (scol G r - 1) ^ n * (scol G r - 1) :=
59 Nat.mul_le_mul_right (scol G r - 1) (strongLayer_card_le_pow G r v n)
60 _ = (scol G r - 1) ^ (n + 1) := by rw [Nat.pow_succ]
61
62private theorem strongLayersUpTo_card_le_sum (G : SimpleGraph V) (r : ℕ) (v : V) :
63 (strongLayersUpTo G r v).card ≤
64 Finset.sum (Finset.range r) (fun n => (scol G r - 1) ^ (n + 1)) := by
65 unfold strongLayersUpTo
66 refine le_trans Finset.card_biUnion_le ?_
67 exact Finset.sum_le_sum fun n hn => strongLayer_card_le_pow G r v (n + 1)
68
69private theorem sum_pow_succ_le_mul_pow (k r : ℕ) :
70 Finset.sum (Finset.range r) (fun n => k ^ (n + 1)) ≤ r * k ^ r := by
71 by_cases hk : k = 0
72 · subst hk
73 simp
74 · have hk1 : 1 ≤ k := Nat.succ_le_of_lt (Nat.pos_of_ne_zero hk)
75 calc
76 Finset.sum (Finset.range r) (fun n => k ^ (n + 1))
77 ≤ Finset.sum (Finset.range r) (fun _ => k ^ r) := by
78 refine Finset.sum_le_sum ?_
79 intro n hn
80 exact pow_le_pow_right' hk1 (Nat.succ_le_of_lt (Finset.mem_range.mp hn))
81 _ = r * k ^ r := by simp
82
83private theorem exists_strongLayer_of_weak_witness
84 (G : SimpleGraph V) (r : ℕ) {v u : V} (p : G.Walk v u)
85 (hp_path : p.IsPath) (hp_len : p.length ≤ r) (hu_le : u ≤ v)
86 (hp_internal : ∀ i : ℕ, 0 < i → i < p.length → u < p.getVert i) :
87 ∃ t ≤ p.length, u ∈ strongLayer G r v t := by
88 let P : ℕ → Prop := fun n =>
89 ∀ (v u : V) (p : G.Walk v u),
90 p.IsPath →
91 p.length = n →
92 n ≤ r →
93 u ≤ v →
94 (∀ i : ℕ, 0 < i → i < p.length → u < p.getVert i) →
95 ∃ t ≤ n, u ∈ strongLayer G r v t
96 have hP : ∀ n, P n := by
97 intro n
98 refine Nat.strong_induction_on n ?_
99 intro n ih v u p hp_path hlen hn_le_r hu_le hp_internal
100 by_cases huv : u = v
101 · subst u
102 refine ⟨0, Nat.zero_le _, ?_⟩
103 simp [strongLayer]
104 · have hp_not_nil : ¬ p.Nil := by
105 rw [SimpleGraph.Walk.nil_iff_length_eq]
106 intro hp_zero
107 apply huv
108 have hv : v = p.getVert p.length := by
109 simpa [hp_zero] using p.getVert_zero.symm
110 exact (hv.trans p.getVert_length).symm
111 let S : Finset V := p.dropLast.support.toFinset
112 have hv_mem_S : v ∈ S := by
113 have hv : p.dropLast.getVert 0 ∈ p.dropLast.support := p.dropLast.getVert_mem_support 0
114 simpa [S] using hv
115 have hS_nonempty : S.Nonempty := ⟨v, hv_mem_S⟩
116 let w : V := S.min' hS_nonempty
117 have hw_mem_S : w ∈ S := by
118 exact Finset.min'_mem S hS_nonempty
119 have hw_drop_support : w ∈ p.dropLast.support := by
120 simpa [S] using hw_mem_S
121 have hw_le_v : w ≤ v := Finset.min'_le S v hv_mem_S
122 rcases SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hw_drop_support with
123 ⟨i, hget_drop, hi_le_drop⟩
124 have hdrop_len : p.dropLast.length = p.length - 1 := by
125 simp [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_length]
126 have hi_lt : i < p.length := by
127 rw [hdrop_len] at hi_le_drop
128 have hpos : 0 < p.length := Nat.pos_of_ne_zero fun hzero =>
129 hp_not_nil (SimpleGraph.Walk.nil_iff_length_eq.mpr hzero)
130 exact lt_of_le_of_lt hi_le_drop (Nat.sub_lt hpos (by decide))
131 have hi_le : i ≤ p.length := le_of_lt hi_lt
132 have hget : p.getVert i = w := by
133 have hdrop_eq : p.dropLast.getVert i = p.getVert i := by
134 rw [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_getVert]
135 rw [hdrop_len] at hi_le_drop
136 simp [Nat.min_eq_right hi_le_drop]
137 exact hdrop_eq.symm.trans hget_drop
138 let q : G.Walk v w := (p.take i).copy rfl (by simpa [Nat.min_eq_left hi_le, hget])
139 have hq_path : q.IsPath := by
140 simpa [q] using hp_path.take i
141 have hq_len : q.length = i := by
142 simp [q, SimpleGraph.Walk.take_length, Nat.min_eq_left hi_le]
143 have hq_len_le_r : q.length ≤ r := by
144 rw [hq_len]
145 have hi_le_n : i ≤ n := by simpa [hlen] using le_of_lt hi_lt
146 exact le_trans hi_le_n hn_le_r
147 have hq_internal : ∀ j : ℕ, 0 < j → j < q.length → w < q.getVert j := by
148 intro j hj0 hjq
149 have hj_lt_i : j < i := by simpa [hq_len] using hjq
150 have hj_le_p : j ≤ p.length := le_trans (le_of_lt hj_lt_i) hi_le
151 have hj_le_drop : j ≤ p.dropLast.length := by
152 rw [hdrop_len]
153 omega
154 have hj_mem_S : p.getVert j ∈ S := by
155 have hj_mem : p.dropLast.getVert j ∈ p.dropLast.support := p.dropLast.getVert_mem_support j
156 have hj_eq : p.dropLast.getVert j = p.getVert j := by
157 rw [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_getVert]
158 rw [hdrop_len] at hj_le_drop
159 simp [Nat.min_eq_right hj_le_drop]
160 simpa [S, hj_eq] using hj_mem
161 have hw_le : w ≤ p.getVert j := Finset.min'_le S _ hj_mem_S
162 have hw_ne : w ≠ p.getVert j := by
163 intro hw_eq
164 have hij : i = j := hp_path.getVert_injOn hi_le hj_le_p (by rw [hget, hw_eq])
165 omega
166 have hw_lt : w < p.getVert j := lt_of_le_of_ne hw_le hw_ne
167 simpa [q, SimpleGraph.Walk.take_getVert, Nat.min_eq_right (le_of_lt hj_lt_i)] using hw_lt
168 have hw_mem_wreach : w ∈ WReach G r v := by
169 refine ⟨hw_le_v, q, hq_path, hq_len_le_r, hq_internal⟩
170 let s : G.Walk w u := (p.drop i).copy (by simpa [Nat.min_eq_left hi_le, hget]) rfl
171 have hs_path : s.IsPath := by
172 simpa [s] using hp_path.drop i
173 have hs_len : s.length ≤ r := by
174 simp [s, SimpleGraph.Walk.drop_length]
175 omega
176 have hu_lt_w : u < w := by
177 by_cases hi0 : i = 0
178 · have hw_eq : v = w := by simpa [hi0] using hget
179 simpa [hw_eq] using lt_of_le_of_ne hu_le huv
180 · simpa [hget] using hp_internal i (Nat.pos_of_ne_zero hi0) hi_lt
181 have hu_step : u ∈ sreachStep G r w := by
182 have hs_internal : ∀ j : ℕ, 0 < j → j < s.length → w < s.getVert j := by
183 intro j hj0 hjs
184 have hij_le : i + j ≤ p.length := by
185 have hjs' : j ≤ p.length - i := by
186 simp [s, SimpleGraph.Walk.drop_length] at hjs
187 exact le_of_lt hjs
188 simpa [Nat.add_comm] using Nat.add_le_of_le_sub hi_le hjs'
189 have hij_lt : i + j < p.length := by
190 have hjs' : j < p.length - i := by simpa [s, SimpleGraph.Walk.drop_length] using hjs
191 omega
192 have hij_le_drop : i + j ≤ p.dropLast.length := by
193 rw [hdrop_len]
194 omega
195 have hij_mem_S : p.getVert (i + j) ∈ S := by
196 have hij_mem : p.dropLast.getVert (i + j) ∈ p.dropLast.support :=
197 p.dropLast.getVert_mem_support (i + j)
198 have hij_eq : p.dropLast.getVert (i + j) = p.getVert (i + j) := by
199 rw [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_getVert]
200 rw [hdrop_len] at hij_le_drop
201 simp [Nat.min_eq_right hij_le_drop]
202 simpa [S, hij_eq] using hij_mem
203 have hw_le : w ≤ p.getVert (i + j) := Finset.min'_le S _ hij_mem_S
204 have hw_ne : w ≠ p.getVert (i + j) := by
205 intro hw_eq
206 have hij : i = i + j := hp_path.getVert_injOn hi_le (le_of_lt hij_lt) (by rw [hget, hw_eq])
207 omega
208 have hw_lt : w < p.getVert (i + j) := lt_of_le_of_ne hw_le hw_ne
209 simpa [s, SimpleGraph.Walk.drop_getVert, Nat.min_eq_left hij_le] using hw_lt
210 have hu_mem_sreach : u ∈ SReach G r w := by
211 refine ⟨le_of_lt hu_lt_w, s, hs_path, hs_len, hs_internal⟩
212 simp [sreachStep, hu_mem_sreach, hu_lt_w.ne]
213 obtain ⟨t, ht_le, hw_layer⟩ :=
214 let hi_le_r : i ≤ r := by
215 have hi_le_n : i ≤ n := by simpa [hlen] using le_of_lt hi_lt
216 exact le_trans hi_le_n hn_le_r
217 ih i (by
218 rw [← hlen]
219 exact hi_lt) v w q hq_path hq_len hi_le_r hw_le_v hq_internal
220 have ht_succ_le : t + 1 ≤ n := by
221 omega
222 refine ⟨t + 1, ht_succ_le, ?_⟩
223 exact Finset.mem_biUnion.mpr ⟨w, hw_layer, hu_step⟩
224 exact hP p.length v u p hp_path rfl hp_len hu_le hp_internal
225
226private theorem ncard_wreach_sdiff_le_mul_pow (G : SimpleGraph V) (r : ℕ) (v : V) :
227 (WReach G r v \ {v}).ncard ≤ r * (scol G r - 1) ^ r := by
228 have hcover : (WReach G r v \ {v}).toFinset ⊆ strongLayersUpTo G r v := by
229 intro u hu
230 have hu_set : u ∈ WReach G r v \ {v} := by
231 simpa using hu
232 simp only [Set.mem_diff, Set.mem_singleton_iff] at hu_set
233 rcases hu_set with ⟨huW, hu_not_v⟩
234 rcases huW with ⟨hu_le, p, hp_path, hp_len, hp_internal⟩
235 obtain ⟨t, ht_le, hu_layer⟩ :=
236 exists_strongLayer_of_weak_witness G r p hp_path hp_len hu_le hp_internal
237 have ht_ne_zero : t ≠ 0 := by
238 intro ht0
239 have : u = v := by simpa [strongLayer, ht0] using hu_layer
240 exact hu_not_v (by simpa using this)
241 rcases Nat.exists_eq_succ_of_ne_zero ht_ne_zero with ⟨n, rfl⟩
242 have hn_lt_r : n < r := by omega
243 exact Finset.mem_biUnion.mpr ⟨n, Finset.mem_range.mpr hn_lt_r, hu_layer⟩
244 calc
245 (WReach G r v \ {v}).ncard = (WReach G r v \ {v}).toFinset.card := by
246 exact Set.ncard_eq_toFinset_card' (WReach G r v \ {v})
247 _ ≤ (strongLayersUpTo G r v).card := Finset.card_le_card hcover
248 _ ≤ Finset.sum (Finset.range r) (fun n => (scol G r - 1) ^ (n + 1)) :=
249 strongLayersUpTo_card_le_sum G r v
250 _ ≤ r * (scol G r - 1) ^ r :=
251 sum_pow_succ_le_mul_pow (scol G r - 1) r
252
253private theorem exists_sreach_vertex_on_path
254 (G : SimpleGraph V) (r : ℕ) {v u : V} (p : G.Walk v u)
255 (hp_path : p.IsPath) (hp_len : p.length ≤ r) (hu_lt : u < v) :
256 ∃ w, w ∈ SReach G r v \ {v} ∧ w ∈ p.support := by
257 have hp_pos : 0 < p.length := by
258 by_contra h
259 have hzero : p.length = 0 := by omega
260 have huv : u = v := by
261 calc
262 u = p.getVert p.length := by simpa using p.getVert_length.symm
263 _ = v := by simpa [hzero] using p.getVert_zero
264 exact hu_lt.ne huv
265 let P : ℕ → Prop := fun i => 0 < i ∧ p.getVert i ≤ v
266 have hP : ∃ i, P i := ⟨p.length, hp_pos, by simpa using le_of_lt hu_lt⟩
267 let i := Nat.find hP
268 have hi_pos : 0 < i := (Nat.find_spec hP).1
269 have hi_le_v : p.getVert i ≤ v := (Nat.find_spec hP).2
270 have hi_le_len : i ≤ p.length := Nat.find_min' hP ⟨hp_pos, by simpa using le_of_lt hu_lt⟩
271 have hbefore : ∀ j : ℕ, 0 < j → j < i → v < p.getVert j := by
272 intro j hj0 hji
273 have hnot : ¬ p.getVert j ≤ v := by
274 intro hj_le
275 have hfind : i ≤ j := Nat.find_min' hP ⟨hj0, hj_le⟩
276 exact Nat.not_le_of_gt hji hfind
277 exact lt_of_not_ge hnot
278 let q : G.Walk v (p.getVert i) := p.take i
279 have hq_path : q.IsPath := by
280 simpa [q] using hp_path.take i
281 have hq_len_eq : q.length = i := by
282 rw [show q = p.take i by rfl, SimpleGraph.Walk.take_length]
283 simp [Nat.min_eq_left hi_le_len]
284 have hq_len : q.length ≤ r := by
285 rw [hq_len_eq]
286 exact le_trans hi_le_len hp_len
287 have hq_internal : ∀ j : ℕ, 0 < j → j < q.length → v < q.getVert j := by
288 intro j hj0 hjq
289 rw [show q = p.take i by rfl, SimpleGraph.Walk.take_length] at hjq
290 have hji : j < i := by
291 simp [Nat.min_eq_left hi_le_len] at hjq
292 exact hjq
293 rw [show q = p.take i by rfl, SimpleGraph.Walk.take_getVert]
294 simp [Nat.min_eq_right (le_of_lt hji)]
295 exact hbefore j hj0 hji
296 have hq_ne_v : p.getVert i ≠ v := by
297 intro hEq
298 have : i = 0 := (hp_path.getVert_eq_start_iff hi_le_len).mp hEq
299 exact Nat.ne_of_gt hi_pos this
300 refine ⟨p.getVert i, ?_, p.getVert_mem_support i⟩
301 refine ⟨?_, by simpa using hq_ne_v⟩
302 exact ⟨hi_le_v, q, hq_path, hq_len, hq_internal⟩
303
304private theorem adm_family_card_le_sreach_sdiff
305 (G : SimpleGraph V) (r : ℕ) (v : V) {k : ℕ}
306 (paths : Fin k → (u : V) × G.Walk v u) (hpaths : IsAdmFamily G r v paths) :
307 k ≤ (SReach G r v \ {v}).ncard := by
308 classical
309 let pick : Fin k → V := fun i =>
310 Classical.choose <|
311 exists_sreach_vertex_on_path G r (paths i).2 (hpaths.isPath i) (hpaths.length_le i)
312 (hpaths.target_lt i)
313 have hpick_mem : ∀ i, pick i ∈ SReach G r v \ {v} := by
314 intro i
315 exact (Classical.choose_spec <|
316 exists_sreach_vertex_on_path G r (paths i).2 (hpaths.isPath i) (hpaths.length_le i)
317 (hpaths.target_lt i)).1
318 have hpick_support : ∀ i, pick i ∈ (paths i).2.support := by
319 intro i
320 exact (Classical.choose_spec <|
321 exists_sreach_vertex_on_path G r (paths i).2 (hpaths.isPath i) (hpaths.length_le i)
322 (hpaths.target_lt i)).2
323 have hpick_inj : Function.Injective pick := by
324 intro i j hij
325 by_contra hij'
326 have hsupport_j : pick i ∈ (paths j).2.support := by
327 rw [hij]
328 exact hpick_support j
329 have hv :
330 pick i = v := hpaths.disjoint i j hij' (pick i) (hpick_support i) hsupport_j
331 have hnotv : pick i ≠ v := by
332 have hmem := hpick_mem i
333 simpa only [Set.mem_diff, Set.mem_singleton_iff] using hmem.2
334 exact hnotv hv
335 have hcard :
336 (Finset.univ.image pick).card = k := by
337 simpa using Finset.card_image_of_injective (s := Finset.univ) hpick_inj
338 have hsubset :
339 Finset.univ.image pick ⊆ (SReach G r v \ {v}).toFinset := by
340 intro w hw
341 rcases Finset.mem_image.mp hw with ⟨i, -, rfl⟩
342 simpa using hpick_mem i
343 calc
344 k = (Finset.univ.image pick).card := hcard.symm
345 _ ≤ (SReach G r v \ {v}).toFinset.card := Finset.card_le_card hsubset
346 _ = (SReach G r v \ {v}).ncard := (Set.ncard_eq_toFinset_card' _).symm
347
348private theorem admVertex_le_sreach_ncard (G : SimpleGraph V) (r : ℕ) (v : V) :
349 Catalog.Sparsity.Admissibility.admVertex G r v ≤ (SReach G r v).ncard := by
350 unfold Catalog.Sparsity.Admissibility.admVertex
351 have hsup :
352 Finset.sup (Finset.range (Fintype.card V)) (fun k =>
353 if ∃ (paths : Fin k → (u : V) × G.Walk v u), IsAdmFamily G r v paths
354 then k else 0) ≤ (SReach G r v \ {v}).ncard := by
355 apply Finset.sup_le
356 intro k hk
357 by_cases hkfam : ∃ (paths : Fin k → (u : V) × G.Walk v u), IsAdmFamily G r v paths
358 · rcases hkfam with ⟨paths, hpaths⟩
359 have hktrue : ∃ (paths : Fin k → (u : V) × G.Walk v u), IsAdmFamily G r v paths :=
360 ⟨paths, hpaths⟩
361 simpa [if_pos hktrue] using
362 adm_family_card_le_sreach_sdiff G r v paths hpaths
363 · simp [hkfam]
364 have hself := Set.ncard_diff_singleton_add_one (self_mem_sreach G r v) (Set.toFinite _)
365 omega
366
367/-- Proposition 2.4 (first part): adm_r ≤ scol_r. -/
368theorem adm_le_scol (G : SimpleGraph V) (r : ℕ) :
369 adm G r ≤ scol G r := by
370 unfold adm scol
371 apply Finset.sup_le
372 intro v hv
373 exact le_trans (admVertex_le_sreach_ncard G r v)
374 (Finset.le_sup (f := fun w => (SReach G r w).ncard) (by simp [hv]))
375
376/-- Proposition 2.4 (second part): scol_r ≤ wcol_r. -/
377theorem scol_le_wcol (G : SimpleGraph V) (r : ℕ) :
378 scol G r ≤ wcol G r := by
379 unfold scol wcol
380 apply Finset.sup_le
381 intro v _
382 apply le_trans _ (Finset.le_sup (f := fun v =>
383 (Catalog.Sparsity.ColoringNumbers.WReach G r v).ncard) (by simp : v ∈ Finset.univ))
384 apply Set.ncard_le_ncard
385 · intro u hu
386 simp only [Catalog.Sparsity.ColoringNumbers.SReach, Catalog.Sparsity.ColoringNumbers.WReach,
387 Set.mem_setOf_eq] at *
388 obtain ⟨huv, p, hp, hlen, hint⟩ := hu
389 exact ⟨huv, p, hp, hlen, fun i hi1 hi2 => lt_of_le_of_lt huv (hint i hi1 hi2)⟩
390 · exact Set.toFinite _
391
392/-- Lemma 2.6: wcol_r ≤ 1 + r · (scol_r - 1)^r. -/
393theorem wcol_le_of_scol (G : SimpleGraph V) (r : ℕ) :
394 wcol G r ≤ 1 + r * (scol G r - 1) ^ r := by
395 unfold wcol
396 apply Finset.sup_le
397 intro v _
398 have h1 := Set.ncard_diff_singleton_add_one (self_mem_wreach G r v) (Set.toFinite _)
399 have h2 := ncard_wreach_sdiff_le_mul_pow G r v
400 omega
401
402end
403
404end Catalog.Sparsity.ColoringNumberOrdering
405