diff options
| -rw-r--r-- | Brooks.lean | 504 |
1 files changed, 422 insertions, 82 deletions
diff --git a/Brooks.lean b/Brooks.lean index 669ecc7..1619387 100644 --- a/Brooks.lean +++ b/Brooks.lean @@ -20,41 +20,120 @@ open Classical variable {α : Type} {V : Type} [Fintype V] - (G : SimpleGraph V) [DecidableRel G.Adj] + {G : SimpleGraph V} + +-- API for partial colorings + +namespace SimpleGraph.Coloring + + structure Extension {S : Set V} (C : (G.induce S).Coloring α) (T : Set V) where + subset : S ⊆ T + coloring : (G.induce T).Coloring α + compatible : @Set.restrict₂ V (fun _ => α) S T subset coloring = C + + def trivial_extension {S : Set V} (C : (G.induce S).Coloring α) : Extension C S := by + apply Extension.mk + case subset => exact subset_refl S + case coloring => exact C + case compatible => + ext x + simp only [Set.restrict₂, Subtype.coe_eta] + + def extension_trans + {S T U : Set V} + (C : (G.induce S).Coloring α) + (E : Extension C T) + (F : Extension E.coloring U) + : Extension C U := by + apply Extension.mk + case subset => exact subset_trans E.subset F.subset + case coloring => exact F.coloring + case compatible => simp only [←(Set.restrict₂_comp_restrict₂ E.subset F.subset), Function.comp_apply, F.compatible, E.compatible] + +end SimpleGraph.Coloring + +namespace SimpleGraph.Path + + def split [dec_eq : DecidableEq V] {u v : V} (p : G.Path u v) (z : V) (hz : z ∈ p.val.support) + : Σ p₁ : G.Path u z, Σ' p₂ : G.Path z v, p.val = p₁.val.append p₂.val := by + replace ⟨p, hp⟩ := p + cases dec_eq z u with + | isTrue h => + rw [h] + use Path.nil, ⟨p, hp⟩ + simp only [nil_coe, Walk.nil_append] + | isFalse h => + cases p with + | nil => + simp only [support_nil, mem_cons, not_mem_nil, or_false] at hz + contradiction + | @cons u w v adj tl => + simp only [support_cons, mem_cons, h, false_or] at hz + obtain ⟨⟨tl₁, htl₁⟩, ⟨tl₂, htl₂⟩, happ⟩ := split ⟨tl, IsPath.of_cons hp⟩ z hz + simp only at happ + simp only [happ, cons_isPath_iff, mem_support_append_iff, not_or] at hp + let p₁ := Walk.cons adj tl₁ + have hp₁ : IsPath p₁ := IsPath.cons htl₁ hp.right.left + use ⟨p₁, hp₁⟩, ⟨tl₂, htl₂⟩ + simp only [Walk.cons_append, p₁, happ] + +end SimpleGraph.Path noncomputable def extend_coloring - (S : Set V) (S_coloring : Coloring (G.induce S) α) + (S : Set V) (C : Coloring (G.induce S) α) (v : V) (c : α) - (h : c ∉ S_coloring '' (S ↓∩ G.neighborSet v)) - : Coloring (G.induce (S ∪ {v})) α + (h : c ∉ C '' (S ↓∩ G.neighborSet v)) + : Coloring.Extension C (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] + apply Coloring.Extension.mk + case subset => exact Set.subset_union_left + case coloring => + apply Coloring.mk + case color => + intro ⟨x, _⟩ + by_cases hx : x ∈ S + · exact C ⟨x, hx⟩ + · exact c + case valid => + simp only [Set.mem_image, Set.mem_preimage, mem_neighborSet, Subtype.exists, + exists_and_left, not_exists, not_and] at h + rintro ⟨x, hx⟩ ⟨y, hy⟩ adj + by_cases hxS : x ∈ S <;> by_cases hyS : y ∈ S + · simp only [hxS, hyS] + exact C.valid adj + · simp only [hxS, hyS] + replace hyS : y = v := hy.resolve_left hyS + simp only [hyS, comap_adj, Function.Embedding.subtype_apply] at adj + exact h x (G.adj_symm adj) hxS + · simp only [hxS, hyS] + replace hxS : x = v := hx.resolve_left hxS + simp only [hxS] at adj + intro wrong + exact h y adj hyS (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] + + case compatible => + ext ⟨x, hx⟩ + simp only [Coloring.mk, Set.restrict₂_def, RelHom.instFunLike] + simp only [hx, ↓reduceDIte, RelHom.coe_fn_toFun] + +noncomputable def extend_coloring_of_image_card + {k : ℕ} + (S : Set V) (C : Coloring (G.induce S) (Fin k)) + (v : V) (h : (C '' (S ↓∩ G.neighborSet v)).toFinset.card < k) + : Coloring.Extension C (S ∪ {v}) := by + let N := G.neighborSet v + + have unused_color : ∃ c : Fin k, c ∉ C '' (S ↓∩ N) := by + suffices (C '' (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_univ, Finset.card_univ, Fintype.card_fin] + exact h + exact extend_coloring S C v (Exists.choose unused_color) (Exists.choose_spec unused_color) lemma preimage_val_card (A B : Set V) : (A ↓∩ B).toFinset.card = (A ∩ B).toFinset.card := by apply Finset.card_bij' @@ -78,12 +157,11 @@ 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' +noncomputable def extend_coloring_of_lt_colored_neighbors {k : ℕ} - (S : Set V) (S_colorable : Colorable (G.induce S) k) + (S : Set V) (C : Coloring (G.induce S) (Fin k)) (v : V) (h : (G.neighborSet v ∩ S).toFinset.card < k) - : Colorable (G.induce (S ∪ {v})) k := by - have S_coloring := S_colorable.some + : Coloring.Extension C (S ∪ {v}) := by let N := G.neighborSet v have card_fact : (S ↓∩ N).toFinset.card = (S ∩ N).toFinset.card := by @@ -91,28 +169,23 @@ lemma extend_coloring' 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⟩ + replace h : (C '' (S ↓∩ G.neighborSet v)).toFinset.card < k := by 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 + (Finset.image C (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'' + exact extend_coloring_of_image_card S C v h + +noncomputable def extend_coloring_of_degree_lt {k : ℕ} - (S : Set V) (S_colorable : Colorable (G.induce S) k) + (S : Set V) (C : Coloring (G.induce S) (Fin k)) (v : V) (h : G.degree v < k) - : Colorable (G.induce (S ∪ {v})) k := by - apply extend_coloring' - · assumption - · calc + : Coloring.Extension C (S ∪ {v}) := by + apply extend_coloring_of_lt_colored_neighbors + calc (G.neighborSet v ∩ S).toFinset.card ≤ (G.neighborSet v).toFinset.card := by simp only [Set.toFinset_inter] apply Finset.card_le_card @@ -120,28 +193,63 @@ lemma extend_coloring'' _ = G.degree v := by simp only [Set.toFinset_card, G.card_neighborSet_eq_degree] _ < k := h -theorem color_path +noncomputable def extend_coloring_of_two_neighbors_eq_color + {k : ℕ} + (S : Set V) (C : Coloring (G.induce S) (Fin k)) + (v : V) (hv : G.degree v ≤ k) + (x y : S) (hx : G.Adj v x) (hy : G.Adj v y) (x_ne_y : x ≠ y) + (hC : C x = C y) + : Coloring.Extension C (S ∪ {v}) := by + let N := G.neighborSet v + apply extend_coloring_of_image_card + simp only [Set.toFinset_image, Set.toFinset_univ, Finset.card_univ, Fintype.card_fin] + + 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 S_inter_N_card_le_k : (S ↓∩ N).toFinset.card ≤ k := calc + (S ↓∩ N).toFinset.card = (S ∩ N).toFinset.card := card_fact + _ ≤ N.toFinset.card := Finset.card_le_card (Set.toFinset_subset_toFinset.mpr Set.inter_subset_right) + _ ≤ k := hv + + apply Ne.lt_of_le + · intro hk + have k_le_S_inter_N_card : k ≤ (S ↓∩ N).toFinset.card := calc + k = (Finset.image C (S ↓∩ N).toFinset).card := hk.symm + _ ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le + have k_eq_S_inter_N_card := Nat.le_antisymm k_le_S_inter_N_card S_inter_N_card_le_k + simp only [k_eq_S_inter_N_card] at hk + have C_inj_on_S_inter_N := Finset.card_image_iff.mp hk + simp only [Set.coe_toFinset] at C_inj_on_S_inter_N + have x_eq_y := C_inj_on_S_inter_N hx hy hC + contradiction + · calc + (Finset.image C (S ↓∩ N).toFinset).card ≤ (S ↓∩ N).toFinset.card := Finset.card_image_le + _ ≤ k := S_inter_N_card_le_k + +noncomputable def 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.toFinset)) k := by - classical + (S_coloring : Coloring (G.induce S) (Fin k)) + : Coloring.Extension S_coloring (S ∪ P.val.support.tail.toFinset) := by let ⟨W, W_is_path⟩ := P cases W with | nil => - simp - rw [Finset.coe_empty, Set.union_empty] - exact S_colorable + simp only [support_nil, List.tail_cons, toFinset_nil, Finset.coe_empty, Set.union_empty] + exact Coloring.trivial_extension S_coloring | @cons u w v adj W' => - simp at * + simp only [support_cons, mem_cons, forall_eq_or_imp] at P_outside_S + 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 + have T_ext := color_path k maxDeg_le_k P' S (P_outside_S.right) S_coloring let N := G.neighborSet w -- set of vertices already colored by P'_coloring - let C := S ∪ W'.support.tail.toFinset + let T := 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 @@ -149,22 +257,22 @@ theorem color_path 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] + have hu : u ∈ (N \ T) := by + simp [N, T] exact ⟨G.adj_symm adj, P_outside_S.left, u_not_in_W'_tail⟩ - have h : (N ∩ C).toFinset.card < k := by - have ineq1 : (N ∩ C).toFinset.card + (N \ C).toFinset.card ≤ k := calc + have h : (N ∩ T).toFinset.card < k := by + have ineq1 : (N ∩ T).toFinset.card + (N \ T).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 - have ineq2 : 1 ≤ (N \ C).toFinset.card := by + have ineq2 : 1 ≤ (N \ T).toFinset.card := by simp only [Finset.one_le_card, Set.toFinset_nonempty] exact ⟨u, hu⟩ linarith have extended_coloring := by - apply extend_coloring' G C P'_colorable w + apply extend_coloring_of_lt_colored_neighbors T T_ext.coloring w -- TODO without "convert" this gives a timeout error convert h @@ -172,7 +280,7 @@ theorem color_path 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 extended_coloring + exact Coloring.extension_trans S_coloring T_ext 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] @@ -184,7 +292,7 @@ lemma induce_maxDegree_mono (S : Set V) : (G.induce S).maxDegree ≤ G.maxDegree _ ≤ 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 + : ∃ w : V, ∃ Q : G.Walk w u, IsPath (Q.append P.1) ∧ G.neighborFinset w ⊆ (Q.append P.1).support.toFinset := by replace ⟨P, hP⟩ := P induction hn : Fintype.card V - P.support.length generalizing u P @@ -222,46 +330,44 @@ noncomputable def extend_path_maximally {u v : V} (P : G.Path u v) simp only [P'] at hQ' assumption - 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 + case h n ih _ => + by_cases hnk : n ≤ k · have n_colorable := G.colorable_of_fintype rw [hn] at n_colorable - exact Colorable.mono h n_colorable + exact Colorable.mono hnk n_colorable · by_cases k_reg : G.IsRegularOfDegree k -- Assume G is not k-regular. case neg => simp [IsRegularOfDegree] at k_reg + -- x is a vertex of degree strictly less than k have ⟨x, hx⟩ := k_reg let S : Set V := Set.univ \ {x} let G' := G.induce S - -- Apply induction - have S_maxDeg_le_k : G'.maxDegree ≤ k := sorry -- induce_maxDegree_mono G S + -- Color every vertex except x by induction + have S_maxDeg_le_k : G'.maxDegree ≤ k := sorry -- Nat.le_trans (induce_maxDegree_mono S) maxDeg_le_k 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 + have S_colorable : (G.induce S).Colorable k := ih (n - 1) (by omega) 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 + replace hx : G.degree x < k := Ne.lt_of_le hx (Nat.le_trans (G.degree_le_maxDegree x) maxDeg_le_k) - have G_colorable := extend_coloring'' G S S_colorable x hx + -- We can also color x since it has degree < k + have ⟨_, G_colorable, _⟩ := extend_coloring_of_degree_lt S S_colorable.some 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 + exact Colorable.of_embedding (G.induceUnivIso.symm.toEmbedding) (Nonempty.intro G_colorable) -- Assume G is k-regular. case pos => @@ -276,6 +382,7 @@ theorem brooks' 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 + -- If not, v and its neighbors would form a clique on k+1 vertices. case t => exact (G.neighborSet v ∪ {v}).toFinset case a => apply IsNClique.mk @@ -301,6 +408,239 @@ theorem brooks' exact G.adj_symm hx · simp at wrong exact wrong x y x_ne_y hx hy + have ⟨x, y, x_ne_y, v_adj_x, v_adj_y, x_nadj_y⟩ := claim + + -- P is the path x → v → y + let P : G.Walk x y := Walk.cons (G.adj_symm v_adj_x) (Walk.cons v_adj_y nil) + have hP : IsPath P := by + apply IsPath.cons + · simp only [cons_isPath_iff, isPath_iff_eq_nil, support_nil, mem_cons, not_mem_nil, + or_false, true_and] + by_contra v_eq_y + rw [v_eq_y] at v_adj_y + exact G.irrefl v_adj_y + · simp only [support_cons, support_nil, mem_cons, not_mem_nil, or_false, not_or] + apply And.intro + · by_contra x_eq_v + rw [x_eq_v] at v_adj_x + exact G.irrefl v_adj_x + · assumption + + -- Extend P maximally to the front by a path Q from w to x + have ⟨w, Q, hQP, hw⟩ := extend_path_maximally ⟨P, hP⟩ + have hQ : IsPath Q := IsPath.of_append_left hQP + simp only [isPath_def, Walk.support_append, List.nodup_append] at hQP + replace hQP := hQP.right.right + simp only at hw + + by_cases h : (Q.append P).support.toFinset = Finset.univ + + -- Case 1: Q.append P visits every vertex of G + case pos => + -- Since G is k-regular with k ≥ 3, v has another neighbor z not equal to x or y + have existsThirdNeighbor : (G.neighborFinset v \ {x, y}).Nonempty := by + apply Finset.card_pos.mp + calc + (G.neighborFinset v \ {x, y}).card ≥ (G.neighborFinset v).card - Finset.card {x, y} := Finset.le_card_sdiff {x, y} (G.neighborFinset v) + _ = k - Finset.card {x, y} := by simp only [card_neighborFinset_eq_degree, k_reg v] + _ > 0 := by + have fact : Finset.card {x, y} ≤ 2 := Finset.card_le_two + omega -- recall that k ≥ 3 + have ⟨z, hz⟩ := existsThirdNeighbor + simp only [Finset.mem_sdiff, mem_neighborFinset, Finset.mem_insert, Finset.mem_singleton, + not_or] at hz + have ⟨v_adj_z, z_ne_x, z_ne_y⟩ := hz + + -- By definition z is not on P + have z_not_on_P : z ∉ P.support := by + simp only [P, support_cons, support_nil, mem_cons, z_ne_x, z_ne_y, not_mem_nil, or_self, + or_false, false_or] + by_contra z_eq_v + simp only [z_eq_v, SimpleGraph.irrefl] at v_adj_z + + -- By assumption, z must lie on Q then + have z_on_Q : z ∈ Q.support := by + have obv : z ∈ Finset.univ := Finset.mem_univ z + simp only [←h, mem_toFinset, mem_support_append_iff, z_not_on_P, or_false] at obv + assumption + + -- Split the path Q at z + obtain ⟨⟨Q₁, hQ₁⟩, ⟨Q₂, hQ₂⟩, happ⟩ := Path.split ⟨Q, hQ⟩ z z_on_Q + simp only at happ + + -- Start by giving x and y the same color + let C₁ : Coloring (G.induce {x, y}) (Fin k) := by + apply Coloring.mk + case color => + exact fun _ => Fin.mk 0 (by omega) + case valid => + rintro ⟨a, ha⟩ ⟨b, hb⟩ adj _ + by_cases hab : a = b + · simp only [hab] at adj + exact G.irrefl adj + · simp at ha hb adj + cases ha with + | inl a_eq_x => + rw [a_eq_x, Eq.comm] at hab + have b_eq_y := Or.resolve_left hb hab + rw [a_eq_x, b_eq_y] at adj + contradiction + | inr a_eq_y => + rw [a_eq_y, Eq.comm] at hab + have b_eq_x := Or.resolve_right hb hab + rw [a_eq_y, b_eq_x, G.adj_comm] at adj + contradiction + + -- u is the vertex on Q next to x + let u := Q₂.penultimate + have u_adj_x : G.Adj u x := Walk.adj_penultimate (Walk.not_nil_of_ne z_ne_x) + + -- We will color the paths R₁ and R₂ + let R₁ : G.Walk z u := Q₂.dropLast + let R₂ : G.Walk v w := Walk.cons v_adj_z Q₁.reverse + + have v_not_on_Q : v ∉ Q.support := by + have v_on_P_tail : v ∈ P.support.tail := by simp [P] + exact List.disjoint_symm hQP v_on_P_tail + have v_not_on_Q₁_rev : v ∉ Q₁.reverse.support := by + simp [happ] at v_not_on_Q + simp only [Walk.support_reverse, List.mem_reverse] + exact v_not_on_Q.1 + have v_not_on_Q₂ : v ∉ Q₂.support := by + simp [happ] at v_not_on_Q + exact v_not_on_Q.2 + + have hR₁ : IsPath R₁ := by + have obv : R₁.concat u_adj_x = Q₂ := by simp only [concat_dropLast, R₁] + simp [←obv, Walk.concat_eq_append] at hQ₂ + exact IsPath.of_append_left hQ₂ + have hR₂ : IsPath R₂ := IsPath.cons ((isPath_reverse_iff Q₁).mpr hQ₁) v_not_on_Q₁_rev + + have R₁_support : Q₂.support = R₁.support.concat x := by + rw [←(Walk.support_concat R₁ u_adj_x)] + simp only [concat_dropLast, R₁] + + have x_not_on_R₁ : x ∉ R₁.support := by + simp [isPath_def, R₁_support] at hQ₂ + simpa using List.disjoint_of_nodup_append hQ₂ + + have Q₁_disj_Q₂_tail : Q₁.support.Disjoint Q₂.support.tail := by + simp [isPath_def, happ, Walk.support_append] at hQ + exact List.disjoint_of_nodup_append hQ + + have x_not_on_Q₁ : x ∉ Q₁.support := by + have Q₂_not_nil : ¬Q₂.Nil := Walk.not_nil_of_ne z_ne_x + exact Q₁_disj_Q₂_tail.symm (Walk.end_mem_tail_support Q₂_not_nil) + + have y_not_on_Q : y ∉ Q.support := by + have y_on_P_tail : y ∈ P.support.tail := by simp [P] + exact List.disjoint_symm hQP y_on_P_tail + + simp only [happ, mem_support_append_iff, not_or] at y_not_on_Q + have ⟨y_not_on_Q₁, y_not_on_Q₂⟩ := y_not_on_Q + + have y_not_on_R₁ : y ∉ R₁.support := by + simp only [R₁_support, List.concat_eq_append, mem_append, mem_cons, not_mem_nil, + or_false, not_or] at y_not_on_Q₂ + exact y_not_on_Q₂.left + + have v_not_on_R₁ : v ∉ R₁.support := by + simp only [R₁_support, List.concat_eq_append, mem_append, mem_cons, not_mem_nil, + or_false, not_or] at v_not_on_Q₂ + exact v_not_on_Q₂.left + + have xy_not_on_R₁ : ∀ t ∈ R₁.support, t ∉ ({x, y} : Set V) := by + intro t ht + simp only [Set.mem_insert_iff, Set.mem_singleton_iff, not_or] + apply And.intro + · intro hx + rw [hx] at ht + contradiction + · intro hy + rw [hy] at ht + contradiction + + -- Color the path R₁. + let C₂ := color_path k maxDeg_le_k ⟨R₁, hR₁⟩ {x, y} xy_not_on_R₁ C₁ + simp only at C₂ + + have R₂_not_colored_by_C₂ : ∀ t ∈ R₂.support, t ∉ (({x, y} : Set V) ∪ R₁.support.tail.toFinset) := by + intro t ht + simp only [support_cons, support_reverse, mem_cons, mem_reverse, R₂] at ht + + simp only [coe_toFinset, Set.mem_union, Set.mem_insert_iff, Set.mem_singleton_iff, + Set.mem_setOf_eq, not_or] + + cases ht with + | inl t_eq_v => + rw [t_eq_v] + use ⟨G.ne_of_adj v_adj_x, G.ne_of_adj v_adj_y⟩ + intro hv + exact v_not_on_R₁ (List.mem_of_mem_tail hv) + | inr t_on_Q₁ => + constructor + · constructor + · intro hx + rw [hx] at t_on_Q₁ + contradiction + · intro hy + rw [hy] at t_on_Q₁ + contradiction + · intro ht + have t_not_on_Q₂_tail := Q₁_disj_Q₂_tail t_on_Q₁ + simp only [R₁_support, List.concat_eq_append, ne_eq, support_ne_nil, + not_false_eq_true, tail_append_of_ne_nil, mem_append, mem_cons, not_mem_nil, + or_false, imp_false, not_or] at t_not_on_Q₂_tail + exact t_not_on_Q₂_tail.left ht + + -- Now color the path R₂. + let C₃ := color_path k maxDeg_le_k ⟨R₂, hR₂⟩ ({x, y} ∪ R₁.support.tail.toFinset) R₂_not_colored_by_C₂ C₂.coloring + replace C₃ := Coloring.extension_trans C₁ C₂ C₃ + simp only at C₃ + + -- C₃ colors the set S, which contains every vertex of G except v. + -- We can also color v because v has two neighbors of the same color + -- (namely x and y). + let S : Set V := {x, y} ∪ R₁.support.tail.toFinset ∪ R₂.support.tail.toFinset + have x_in_xy : x ∈ ({x, y} : Set V) := by simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or] + have y_in_xy : y ∈ ({x, y} : Set V) := by simp only [Set.mem_insert_iff, Set.mem_singleton_iff, or_true] + have x_in_S : x ∈ S := by simp only [S, x_in_xy, Set.mem_union, true_or] + have y_in_S : y ∈ S := by simp only [S, y_in_xy, Set.mem_union, true_or] + have x_ne_y : (⟨x, x_in_S⟩ : S) ≠ ⟨y, y_in_S⟩ := by + intro wrong + simp only [Subtype.mk.injEq] at wrong + contradiction + have x_y_same_color : C₃.coloring ⟨x, x_in_S⟩ = C₃.coloring ⟨y, y_in_S⟩ := by + calc + C₃.coloring ⟨x, x_in_S⟩ = C₁ ⟨x, x_in_xy⟩ := by simp only [←C₃.compatible, Set.restrict₂] + _ = C₁ ⟨y, y_in_xy⟩ := rfl + _ = C₃.coloring ⟨y, y_in_S⟩ := by simp only [←C₃.compatible, Set.restrict₂] + + have deg_v_le_k := Nat.le_trans (G.degree_le_maxDegree v) maxDeg_le_k + let C₄ := extend_coloring_of_two_neighbors_eq_color S C₃.coloring v deg_v_le_k ⟨x, x_in_S⟩ ⟨y, y_in_S⟩ v_adj_x v_adj_y x_ne_y x_y_same_color + + -- Now we just need to check that the union of all these paths is indeed all of V. + have C₄_colors_G : S ∪ {v} = Set.univ := by + rw [Set.union_comm] + apply Set.toFinset_inj.mp + simp only [S, Set.toFinset_univ, Set.toFinset_union, Finset.toFinset_coe, Set.toFinset_singleton, Set.toFinset_insert] + simp only [Finset.insert_union, support_cons, support_reverse, List.tail_cons, + toFinset_reverse, Finset.union_assoc, Finset.union_insert, R₂] + simp only [happ, support_append, R₁_support, List.concat_eq_append, ne_eq, + support_ne_nil, not_false_eq_true, tail_append_of_ne_nil, support_cons, support_nil, + List.tail_cons, List.append_assoc, List.cons_append, List.nil_append, toFinset_append, + toFinset_cons, toFinset_nil, insert_emptyc_eq, Finset.union_insert, P] at h + rw [←h] + congr + rw [←Finset.insert_eq] + congr 1 + rw [←Finset.union_assoc, Finset.union_comm] + conv => + lhs + arg 2 + rw [Finset.union_comm] + + rw [C₄_colors_G] at C₄ + exact Colorable.of_embedding G.induceUnivIso.symm.toEmbedding (Nonempty.intro C₄.coloring) - have ⟨x, y, x_ne_y, hx, hy, x_nadj_y⟩ := claim - sorry + case neg => sorry |