/- This file was mostly generated by Aristotle (https://aristotle.harmonic.fun), based on the note "Interval graphs admit optimal greedy colouring in order of finish time", W. Cames van Batenburg, S. Kelk, 2026. Currently available at https://woutercvb.github.io/greedy_by_finish_time_draft22april2026.pdf The code below formalizes Theorem 1.2 from the note. Warnings, check for axioms, etc. have been addressed manually. To typecheck it online, you can copy and paste the formalised proof to https://live.lean-lang.org/ Lean version: leanprover/lean4:v4.24.0 Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 This project request had uuid: 6fa2d60a-a056-4996-96cd-5bcd501d2f49 -/ Formalization of the non-deterministic greedy coloring algorithm for interval graphs. Main result: `nondeterministic_greedy_achieves_clique_number` proves that the algorithm can achieve a coloring with exactly `cliqueNumber` colors. Key components: - `GreedyState`: Represents the state of the greedy algorithm. - `Invariant`: A predicate on the state that ensures correctness and optimality. - `exists_reachable_invariant_state_at_k`: Shows that a state satisfying the invariant is reachable. - `exists_proper_coloring_le_cliqueNumber`: Proves the existence of a proper coloring with at most `cliqueNumber` colors (using First-Fit on start-time sorted intervals). - `invariant_implies_bound`: Shows that the invariant implies the number of colors is bounded by `cliqueNumber`. -/ import Mathlib set_option linter.mathlibStandardSet false open scoped BigOperators open scoped Real open scoped Nat open scoped Classical open scoped Pointwise set_option maxHeartbeats 0 set_option maxRecDepth 4000 set_option synthInstance.maxHeartbeats 20000 set_option synthInstance.maxSize 128 set_option relaxedAutoImplicit false set_option autoImplicit false noncomputable section /-- An interval is a pair (start, finish) with start < finish. We use natural numbers for endpoints; this suffices since we only care about the combinatorial (order) structure. -/ structure GreedyInterval where start : ℕ finish : ℕ h : start < finish deriving DecidableEq, Repr def overlap (a b : GreedyInterval) : Prop := a.start < b.finish ∧ b.start < a.finish /-- Overlap is symmetric. -/ theorem overlap_symm (a b : GreedyInterval) : overlap a b ↔ overlap b a := by constructor <;> intro ⟨h1, h2⟩ <;> exact ⟨h2, h1⟩ /-- A coloring of a list of intervals assigns a color (natural number) to each index. -/ def Coloring (n : ℕ) := Fin n → ℕ /-- A coloring is proper if overlapping intervals get distinct colors. -/ def Coloring.proper {n : ℕ} (intervals : Fin n → GreedyInterval) (c : Coloring n) : Prop := ∀ i j : Fin n, i ≠ j → overlap (intervals i) (intervals j) → c i ≠ c j /-- The number of colors used by a coloring. -/ noncomputable def Coloring.numColors {n : ℕ} (c : Coloring n) : ℕ := (Finset.univ.image c).card /-- A set of indices forms a clique if all pairs of distinct intervals overlap. -/ def IsClique {n : ℕ} (intervals : Fin n → GreedyInterval) (S : Finset (Fin n)) : Prop := ∀ i ∈ S, ∀ j ∈ S, i ≠ j → overlap (intervals i) (intervals j) /-- The clique number ω is the maximum size of a clique. -/ noncomputable def cliqueNumber {n : ℕ} (intervals : Fin n → GreedyInterval) : ℕ := Finset.sup (Finset.univ.filter (IsClique intervals)) Finset.card /-- The intervals are sorted by (non-strictly) increasing finish time. -/ def SortedByFinishTime {n : ℕ} (intervals : Fin n → GreedyInterval) : Prop := ∀ i j : Fin n, i ≤ j → (intervals i).finish ≤ (intervals j).finish /-- The state of the greedy algorithm after processing k intervals. - `color`: the coloring γ assigned to intervals 0, ..., k-1 - `introduced`: the set S of introduced colors - `sigma`: the injection σ from S into {0, ..., ω-1} The state records the greedy coloring built so far. -/ structure GreedyState (n : ℕ) (k : ℕ) where /-- The coloring γ assigned so far (defined on indices < k). -/ color : Fin k → ℕ /-- The set S of introduced colors. -/ introduced : Finset ℕ /-- The mapping σ : S → ℕ. -/ sigma : ℕ → ℕ /-- Color c is available for interval I at step k: c is introduced, and no interval among those already colored with γ-value c overlaps I. -/ def available {n : ℕ} {k : ℕ} (intervals : Fin n → GreedyInterval) (state : GreedyState n k) (c : ℕ) (idx : Fin n) : Prop := c ∈ state.introduced ∧ ∀ j : Fin k, state.color j = c → if h : j.val < n then ¬ overlap (intervals ⟨j.val, h⟩) (intervals idx) else True -- Should not happen if k <= n def ValidGreedyStep {n k : ℕ} (intervals : Fin n → GreedyInterval) (old : GreedyState n k) (new : GreedyState n (k + 1)) : Prop := if h : k < n then let idx : Fin n := ⟨k, h⟩ let c := new.color (Fin.last k) (∀ i : Fin k, new.color (Fin.castSucc i) = old.color i) ∧ if ∃ c', available intervals old c' idx then available intervals old c idx ∧ new.introduced = old.introduced else c ∉ old.introduced ∧ new.introduced = insert c old.introduced else False inductive Reachable {n : ℕ} (intervals : Fin n → GreedyInterval) : {k : ℕ} → GreedyState n k → Prop | base (state : GreedyState n 0) : state.introduced = ∅ → Reachable intervals state | step {k : ℕ} {old : GreedyState n k} {new : GreedyState n (k+1)} : Reachable intervals old → ValidGreedyStep intervals old new → Reachable intervals new def Invariant {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (state : GreedyState n k) : Prop := ∃ (h_le : k ≤ n), (∀ i j : Fin k, i ≠ j → overlap (intervals ⟨i, i.2.trans_le h_le⟩) (intervals ⟨j, j.2.trans_le h_le⟩) → state.color i ≠ state.color j) ∧ (∀ c1 ∈ state.introduced, ∀ c2 ∈ state.introduced, state.sigma c1 = state.sigma c2 → c1 = c2) ∧ (∀ c ∈ state.introduced, ∃ j : Fin k, state.color j = c ∧ (∀ j' : Fin k, state.color j' = c → j' ≤ j) ∧ phi ⟨j, j.2.trans_le h_le⟩ = state.sigma c) /- Suppose $\gamma$ has been defined on $I_1,\dots,I_k$, is proper, and $c\in S$. Let $J$ be the last of $I_1,\dots,I_k$ with $\gamma(J)=c$. If a future interval~$I$ does not overlap~$J$, then $I$ overlaps no interval among $I_1,\dots,I_k$ with $\gamma$-value~$c$. -/ lemma lemma_last {n k : ℕ} (intervals : Fin n → GreedyInterval) (state : GreedyState n k) (h_le : k ≤ n) (h_sorted : SortedByFinishTime intervals) (_h_proper : ∀ i j : Fin k, i ≠ j → overlap (intervals ⟨i, i.2.trans_le h_le⟩) (intervals ⟨j, j.2.trans_le h_le⟩) → state.color i ≠ state.color j) (c : ℕ) (_hc : c ∈ state.introduced) (J : Fin k) (_hJ_color : state.color J = c) (hJ_last : ∀ j : Fin k, state.color j = c → j ≤ J) (I : Fin n) (hI : k ≤ I) -- Future interval (index >= k) (h_no_overlap : ¬ overlap (intervals ⟨J, J.2.trans_le h_le⟩) (intervals I)) : ∀ j : Fin k, state.color j = c → ¬ overlap (intervals ⟨j, j.2.trans_le h_le⟩) (intervals I) := by intro j hj_color hj_overlap; simp_all +decide [ overlap ]; contrapose! h_no_overlap; constructor <;> try linarith! [ h_sorted ⟨ j, by linarith [ Fin.is_lt j ] ⟩ ⟨ J, by linarith [ Fin.is_lt J ] ⟩ ( hJ_last j hj_color ) ] ; refine' lt_of_lt_of_le _ ( h_sorted _ _ _ ); exact ( intervals ⟨ J, by linarith [ Fin.is_lt J ] ⟩ ).h; exact Nat.le_trans ( Nat.le_of_lt J.2 ) hI def nextState {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (old : GreedyState n k) (h_k : k < n) : GreedyState n (k + 1) := let idx := ⟨k, h_k⟩ let j := phi idx let S := old.introduced let sigma := old.sigma let Avail := S.filter (fun c => available intervals old c idx) if h_exists : ∃ c ∈ S, sigma c = j then let c := Classical.choose h_exists { color := Fin.snoc old.color c introduced := old.introduced sigma := old.sigma } else if h_avail : Avail.Nonempty then let c := Classical.choose h_avail { color := Fin.snoc old.color c introduced := old.introduced sigma := Function.update old.sigma c j } else let c_new := (S.image id).sup id + 1 { color := Fin.snoc old.color c_new introduced := insert c_new S sigma := Function.update old.sigma c_new j } /- The `nextState` construction yields a valid greedy step, assuming the invariant holds for the previous state. -/ lemma nextState_valid {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (old : GreedyState n k) (h_k : k < n) (h_sorted : SortedByFinishTime intervals) (h_phi_proper : Coloring.proper intervals phi) (h_inv : Invariant intervals phi old) : ValidGreedyStep intervals old (nextState intervals phi old h_k) := by obtain ⟨ h_le, h_proper, h_sigma_inj, h_sigma_last ⟩ := h_inv; unfold nextState; simp +decide ; split_ifs with h_exists h_avail; · -- Since $c$ is in the introduced set and $\sigma(c) = \phi(k)$, we need to show that $c$ is available for the new interval. have h_available : available intervals old (Classical.choose h_exists) ⟨k, h_k⟩ := by obtain ⟨ j, hj₁, hj₂, hj₃ ⟩ := h_sigma_last _ ( Classical.choose_spec h_exists |>.1 ); have h_no_overlap : ¬ overlap (intervals ⟨j, by exact lt_of_lt_of_le j.2 h_le⟩) (intervals ⟨k, h_k⟩) := by intro h_overlap generalize_proofs at *; have := h_phi_proper ⟨ j, by linarith ⟩ ⟨ k, h_k ⟩ ; simp_all +decide [ overlap ] ; exact this ( ne_of_lt j.2 ) ( by linarith [ Classical.choose_spec h_exists |>.2 ] ) generalize_proofs at *; have h_no_overlap : ∀ j' : Fin k, old.color j' = Classical.choose h_exists → ¬ overlap (intervals ⟨j', by exact lt_of_lt_of_le j'.2 h_le⟩) (intervals ⟨k, h_k⟩) := by intros j' hj'_color apply lemma_last intervals old (by linarith) h_sorted (by exact h_proper) (Classical.choose h_exists) (by exact Classical.choose_spec h_exists |>.1) j hj₁ (by exact hj₂) ⟨k, h_k⟩ (by norm_num) h_no_overlap generalize_proofs at *; exact hj'_color generalize_proofs at *; exact ⟨ Classical.choose_spec h_exists |>.1, fun j' hj' => by specialize h_no_overlap j' hj'; aesop ⟩; unfold ValidGreedyStep; simp +decide [ h_k, h_available ] ; exact fun h => False.elim <| h _ h_available; · have := Classical.choose_spec h_avail; unfold ValidGreedyStep; aesop; · unfold ValidGreedyStep; simp +decide [ h_k ] ; split_ifs <;> simp_all +decide [ Finset.Nonempty ]; · rename_i h; obtain ⟨ c', hc' ⟩ := h; specialize h_exists c'; specialize h_avail c'; simp_all +decide [ available ] ; · exact fun h => not_lt_of_ge ( Finset.le_sup ( f := id ) h ) ( Nat.lt_succ_self _ ) /- A valid greedy step preserves the proper coloring property. -/ lemma ValidGreedyStep_implies_proper {n k : ℕ} (intervals : Fin n → GreedyInterval) (old : GreedyState n k) (new : GreedyState n (k + 1)) (h_k : k < n) (h_step : ValidGreedyStep intervals old new) (h_old_proper : ∀ i j : Fin k, i ≠ j → overlap (intervals ⟨i, i.2.trans_le (Nat.le_of_lt h_k)⟩) (intervals ⟨j, j.2.trans_le (Nat.le_of_lt h_k)⟩) → old.color i ≠ old.color j) (h_old_colors_introduced : ∀ i : Fin k, old.color i ∈ old.introduced) : ∀ i j : Fin (k + 1), i ≠ j → overlap (intervals ⟨i, i.2.trans_le (Nat.succ_le_of_lt h_k)⟩) (intervals ⟨j, j.2.trans_le (Nat.succ_le_of_lt h_k)⟩) → new.color i ≠ new.color j := by unfold ValidGreedyStep at h_step; simp_all +decide; intro i j hij h; cases i using Fin.lastCases <;> cases j using Fin.lastCases <;> simp_all +decide ; · split_ifs at h_step <;> simp_all +decide [ overlap_symm ]; · contrapose! h_step; intro h₁ h₂; unfold available at h₂; aesop; · exact fun h => h_step.2.1 <| h ▸ h_old_colors_introduced _; · split_ifs at h_step <;> simp_all +decide [ available ] ; aesop; exact fun h' => h_step.2.1 <| h'.symm ▸ h_old_colors_introduced _ /- The `nextState` construction preserves the property that all used colors are in the set of introduced colors. -/ def StateHasColorsInIntroduced {n k : ℕ} (state : GreedyState n k) : Prop := ∀ i : Fin k, state.color i ∈ state.introduced lemma nextState_preserves_colors_introduced {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (old : GreedyState n k) (h_k : k < n) (h_inv : StateHasColorsInIntroduced old) : StateHasColorsInIntroduced (nextState intervals phi old h_k) := by intro i; rcases i with ⟨ _ | i, hi ⟩; · unfold nextState at *; simp_all +decide ; split_ifs <;> simp_all +decide [ Fin.snoc ]; · split_ifs <;> [ exact h_inv _ ; exact Classical.choose_spec ‹∃ c ∈ old.introduced, old.sigma c = phi ⟨ k, h_k ⟩ › |>.1 ]; · split_ifs <;> [ exact h_inv _ ; exact Classical.choose_spec ‹_› |> fun h => Finset.mem_filter.mp h |>.1 ]; · cases k <;> aesop; · simp_all +decide [ nextState ]; split_ifs <;> simp_all +decide [ Fin.snoc ]; · split_ifs <;> [ exact h_inv _ ; exact Classical.choose_spec ‹∃ c ∈ old.introduced, old.sigma c = phi ⟨ k, h_k ⟩ › |>.1 ]; · split_ifs <;> [ exact h_inv _ ; exact Classical.choose_spec ‹_› |> fun x => Finset.mem_filter.mp x |>.1 ]; · split_ifs <;> simp_all +decide ; exact Or.inr ( h_inv _ ) /- The color assigned to the new interval by `nextState` does not conflict with any existing overlapping intervals. -/ lemma nextState_new_color_proper {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (old : GreedyState n k) (h_k : k < n) (h_sorted : SortedByFinishTime intervals) (h_phi_proper : Coloring.proper intervals phi) (h_inv : Invariant intervals phi old) (h_intro : StateHasColorsInIntroduced old) : let new := nextState intervals phi old h_k ∀ i : Fin k, overlap (intervals ⟨i, i.2.trans h_k⟩) (intervals ⟨k, h_k⟩) → new.color (Fin.castSucc i) ≠ new.color (Fin.last k) := by intro new i hi; have := nextState_valid intervals phi old h_k h_sorted h_phi_proper h_inv; unfold ValidGreedyStep at this; split_ifs at this ; simp_all +decide; split_ifs at this <;> simp_all +decide [ available ]; · grind +ring; · exact fun h => this.2.1 <| h.symm ▸ this.1 i ▸ h_intro i /- The `nextState` construction preserves the injectivity of $\sigma$. -/ lemma nextState_sigma_injective {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (old : GreedyState n k) (h_k : k < n) (h_inv : Invariant intervals phi old) : let new := nextState intervals phi old h_k ∀ c1 ∈ new.introduced, ∀ c2 ∈ new.introduced, new.sigma c1 = new.sigma c2 → c1 = c2 := by obtain ⟨ h_le, h_proper, h_sigma_inj, h_sigma_last ⟩ := h_inv; field_simp; unfold nextState; intro c1 hc1 c2 hc2 h_eq; by_cases h_exists : ∃ c ∈ old.introduced, old.sigma c = phi ⟨ k, h_k ⟩ <;> simp +decide [ h_exists ] at hc1 hc2 h_eq ⊢; · exact h_sigma_inj c1 hc1 c2 hc2 h_eq; · split_ifs at hc1 hc2 h_eq <;> simp +decide [ *, Function.update ] at hc1 hc2 h_eq ⊢; · split_ifs at h_eq <;> simp_all +decide; · exact False.elim (h_exists c2 hc2 rfl); · exact h_sigma_inj _ hc1 _ hc2 h_eq; · split_ifs at h_eq <;> simp_all +decide [ Finset.Nonempty ]; · exact False.elim (h_exists c2 hc2 rfl); · exact h_sigma_inj _ hc1 _ hc2 h_eq /- The `nextState` construction preserves the last interval property (H4). -/ lemma nextState_last_interval_property {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (old : GreedyState n k) (h_k : k < n) (_h_sorted : SortedByFinishTime intervals) (_h_phi_proper : Coloring.proper intervals phi) (h_inv : Invariant intervals phi old) : let new := nextState intervals phi old h_k ∀ c ∈ new.introduced, ∃ j : Fin (k + 1), new.color j = c ∧ (∀ j' : Fin (k + 1), new.color j' = c → j' ≤ j) ∧ phi ⟨j, j.2.trans_le (Nat.succ_le_of_lt h_k)⟩ = new.sigma c := by intro new c hc generalize_proofs at *; -- Let's consider the two cases: whether `c` is the color of the new interval `I_{k+1}` (index `k`) or not. by_cases hc_new : c = new.color (Fin.last k); · refine' ⟨ Fin.last k, _, _, _ ⟩ <;> simp +decide [ hc_new ]; · exact fun j' hj' => Fin.le_last _; · simp +zetaDelta at *; unfold nextState at *; field_simp; split_ifs <;> simp_all +decide [ Fin.snoc ]; · exact Eq.symm ( Classical.choose_spec ‹∃ c ∈ old.introduced, old.sigma c = phi ⟨ k, h_k ⟩ › |>.2 ); · simp +decide [ Function.update ]; · simp +decide [ Function.update_apply ]; · have := h_inv.2.2.2 c (by simp +zetaDelta at *; unfold nextState at hc; unfold nextState at hc_new; aesop;) generalize_proofs at *; obtain ⟨ j, hj₁, hj₂, hj₃ ⟩ := this generalize_proofs at *; use Fin.castSucc j generalize_proofs at *; refine' ⟨ _, _, _ ⟩ all_goals generalize_proofs at *; · simp +zetaDelta at *; unfold nextState; aesop; · intro j' hj'; cases j' using Fin.lastCases <;> simp_all +decide; simp +zetaDelta at *; convert hj₂ _ _ using 1 generalize_proofs at *; ( unfold nextState at hj'; aesop;); · simp +zetaDelta at *; unfold nextState at *; aesop; /- The `nextState` construction preserves the invariant and the introduced colors property. -/ lemma invariant_step_v2 {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (h_sorted : SortedByFinishTime intervals) (h_phi_proper : Coloring.proper intervals phi) (old : GreedyState n k) (h_inv : Invariant intervals phi old) (h_intro : StateHasColorsInIntroduced old) (h_k : k < n) : ∃ new : GreedyState n (k + 1), ValidGreedyStep intervals old new ∧ Invariant intervals phi new ∧ StateHasColorsInIntroduced new := by refine' ⟨ nextState intervals phi old h_k, _, _, _ ⟩; · exact nextState_valid intervals phi old h_k h_sorted h_phi_proper h_inv; · refine' ⟨ _, _, _ ⟩; exact Nat.succ_le_of_lt h_k; · apply ValidGreedyStep_implies_proper; apply nextState_valid; all_goals try assumption; exact h_inv.2.1; · exact ⟨ nextState_sigma_injective intervals phi old h_k h_inv, nextState_last_interval_property intervals phi old h_k h_sorted h_phi_proper h_inv ⟩; · exact nextState_preserves_colors_introduced intervals phi old h_k h_intro /- The base state satisfies the invariant. -/ def baseState (n : ℕ) : GreedyState n 0 := { color := Fin.elim0 introduced := ∅ sigma := fun _ => 0 } lemma baseState_invariant {n : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) : Invariant intervals phi (baseState n) ∧ StateHasColorsInIntroduced (baseState n) := by unfold Invariant StateHasColorsInIntroduced baseState; aesop; /- Any state satisfying the invariant uses at most $\omega$ colors. -/ lemma invariant_implies_bound {n k : ℕ} (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (state : GreedyState n k) (h_inv : Invariant intervals phi state) (h_intro : StateHasColorsInIntroduced state) (h_phi_colors : Coloring.numColors phi = cliqueNumber intervals) : Coloring.numColors state.color ≤ cliqueNumber intervals := by obtain ⟨ h_le, h_proper, h_sigma_inj, h_last_interval ⟩ := h_inv; -- Since `sigma` is an injection from `introduced` to `image(phi)`, we have `|introduced| ≤ |image(phi)|`. have h_card_introduced : (state.introduced).card ≤ (Finset.image phi Finset.univ).card := by have h_introduced_subset_image : state.introduced.image state.sigma ⊆ Finset.image phi Finset.univ := by exact Finset.image_subset_iff.mpr fun c hc => by obtain ⟨ j, hj₁, hj₂, hj₃ ⟩ := h_last_interval c hc; exact Finset.mem_image.mpr ⟨ _, Finset.mem_univ _, hj₃ ⟩ ; exact le_trans ( by rw [ Finset.card_image_of_injOn fun x hx y hy hxy => h_sigma_inj x hx y hy hxy ] ) ( Finset.card_mono h_introduced_subset_image ); refine le_trans ?_ ( h_card_introduced.trans ?_ ); · exact Finset.card_le_card fun x hx => by aesop; · exact h_phi_colors ▸ le_refl _ /- There exists a reachable state at step $n$ satisfying the invariant. -/ lemma exists_reachable_invariant_state (n : ℕ) (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (h_sorted : SortedByFinishTime intervals) (h_phi_proper : Coloring.proper intervals phi) : ∃ state : GreedyState n n, Reachable intervals state ∧ Invariant intervals phi state ∧ StateHasColorsInIntroduced state := by let P (k : ℕ) := ∃ state : GreedyState n k, Reachable intervals state ∧ Invariant intervals phi state ∧ StateHasColorsInIntroduced state have h_base : P 0 := by use baseState n refine ⟨Reachable.base _ rfl, baseState_invariant intervals phi⟩ have h_step : ∀ k, k < n → P k → P (k + 1) := by intro k h_k h_Pk obtain ⟨old, h_reach_old, h_inv_old, h_intro_old⟩ := h_Pk obtain ⟨new, h_valid, h_inv_new, h_intro_new⟩ := invariant_step_v2 intervals phi h_sorted h_phi_proper old h_inv_old h_intro_old h_k use new refine ⟨Reachable.step h_reach_old h_valid, h_inv_new, h_intro_new⟩ let rec reach (k : ℕ) (h : k ≤ n) : P k := match k with | 0 => h_base | k'+1 => have h_lt : k' < n := Nat.lt_of_lt_of_le (Nat.lt_succ_self k') h h_step k' h_lt (reach k' (Nat.le_of_lt h_lt)) exact reach n (Nat.le_refl n) /- For any k <= n, there exists a reachable state at step k satisfying the invariant. -/ lemma exists_reachable_invariant_state_at_k (n : ℕ) (intervals : Fin n → GreedyInterval) (phi : Fin n → ℕ) (h_sorted : SortedByFinishTime intervals) (h_phi_proper : Coloring.proper intervals phi) (k : ℕ) (hk : k ≤ n) : ∃ state : GreedyState n k, Reachable intervals state ∧ Invariant intervals phi state ∧ StateHasColorsInIntroduced state := by induction k with | zero => use baseState n constructor · apply Reachable.base; rfl · exact baseState_invariant intervals phi | succ k ih => have hk_lt_n : k < n := Nat.lt_of_lt_of_le (Nat.lt_succ_self k) hk have hk_le_n : k ≤ n := Nat.le_of_lt hk_lt_n obtain ⟨old, h_reach, h_inv, h_intro⟩ := ih hk_le_n obtain ⟨new, h_step, h_inv_new, h_intro_new⟩ := invariant_step_v2 intervals phi h_sorted h_phi_proper old h_inv h_intro hk_lt_n use new constructor · exact Reachable.step h_reach h_step · exact ⟨h_inv_new, h_intro_new⟩ /- Any proper coloring uses at least as many colors as the clique number. -/ lemma proper_coloring_ge_cliqueNumber {n : ℕ} (intervals : Fin n → GreedyInterval) (c : Coloring n) (h_proper : Coloring.proper intervals c) : cliqueNumber intervals ≤ Coloring.numColors c := by -- Since $S$ is a clique, for any distinct $i, j \in S$, $intervals i$ and $intervals j$ overlap. have h_clique_overlaps : ∀ S : Finset (Fin n), IsClique intervals S → (Finset.card S ≤ Finset.card (Finset.univ.image c)) := by intros S hS_clique have h_clique_overlaps : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → c i ≠ c j := by exact fun i hi j hj hij => h_proper i j hij ( hS_clique i hi j hj hij ); exact Finset.card_le_card ( show S.image c ⊆ Finset.image c Finset.univ from Finset.image_subset_image <| Finset.subset_univ _ ) |> le_trans ( by rw [ Finset.card_image_of_injOn fun i hi j hj hij => by contrapose hij; exact h_clique_overlaps i hi j hj hij ] ); exact Finset.sup_le fun S hS => by aesop; /- If intervals are sorted by start time, then for any interval $i$, the set of preceding intervals that overlap $i$, together with $i$, forms a clique. -/ def SortedByStartTime {n : ℕ} (intervals : Fin n → GreedyInterval) : Prop := ∀ i j : Fin n, i ≤ j → (intervals i).start ≤ (intervals j).start lemma clique_at_start_time {n : ℕ} (intervals : Fin n → GreedyInterval) (h_sorted : SortedByStartTime intervals) (i : Fin n) : let previous_overlaps := (Finset.univ.filter (fun j => j < i ∧ overlap (intervals j) (intervals i))) IsClique intervals (insert i previous_overlaps) := by -- Let's unfold the definition of `IsClique`. unfold IsClique; simp +zetaDelta at *; refine' ⟨ fun a ha₁ ha₂ ha₃ => _, fun a ha₁ ha₂ => ⟨ fun _ => ha₂, fun b hb₁ hb₂ hab => _ ⟩ ⟩; · exact (overlap_symm (intervals a) (intervals i)).mp ha₂; · unfold overlap at *; -- Since $a < b$, we have $(intervals a).start \leq (intervals b).start$. have h_start_le : (intervals a).start ≤ (intervals b).start ∨ (intervals b).start ≤ (intervals a).start := by exact le_total _ _; cases h_start_le <;> constructor <;> linarith [ h_sorted _ _ ha₁.le, h_sorted _ _ hb₁.le ] /- The minimum excluded value (mex) of a finite set of natural numbers. -/ def mex (s : Finset ℕ) : ℕ := Nat.find (by have h : ∃ n, n ∉ s := by exact s.exists_notMem exact h) /- The minimum excluded value (mex) of a finite set is not in the set. -/ lemma mex_not_mem (s : Finset ℕ) : mex s ∉ s := by exact Nat.find_spec (by have h : ∃ n, n ∉ s := by exact s.exists_notMem exact h) /- The First-Fit coloring (greedy by start time). -/ def firstFitColoring {n : ℕ} (intervals : Fin n → GreedyInterval) (sorted : SortedByStartTime intervals) (i : Fin n) : ℕ := let previous_overlaps := Finset.univ.filter (fun j => j < i ∧ overlap (intervals j) (intervals i)) let used_colors := previous_overlaps.attach.image (fun ⟨j, _⟩ => firstFitColoring intervals sorted j) mex used_colors termination_by i decreasing_by grind /- The First-Fit coloring is a proper coloring. -/ lemma firstFitColoring_proper {n : ℕ} (intervals : Fin n → GreedyInterval) (sorted : SortedByStartTime intervals) : Coloring.proper intervals (firstFitColoring intervals sorted) := by intro i j hij h overlap_j_i by_contra h_contra; -- Without loss of generality, assume $j < i$. suffices h_wlog : ∀ {i j : Fin n}, i < j → overlap (intervals j) (intervals i) → firstFitColoring intervals sorted j ≠ firstFitColoring intervals sorted i by cases lt_trichotomy i j <;> simp_all +decide [ overlap_symm ]; exact h_wlog ‹_› h ( overlap_j_i.symm ); intros i j hij h_overlap have h_color_j : firstFitColoring intervals sorted j = mex (Finset.image (fun k => firstFitColoring intervals sorted k) (Finset.filter (fun k => k < j ∧ overlap (intervals k) (intervals j)) Finset.univ)) := by rw [firstFitColoring]; exact congr_arg _ ( by ext; aesop ); -- Since $j < i$, the color of $i$ is in the image of the previous overlaps of $j$. have h_color_i_in_image : firstFitColoring intervals sorted i ∈ Finset.image (fun k => firstFitColoring intervals sorted k) (Finset.filter (fun k => k < j ∧ overlap (intervals k) (intervals j)) Finset.univ) := by exact Finset.mem_image.mpr ⟨ i, Finset.mem_filter.mpr ⟨ Finset.mem_univ _, hij, by simpa only [ overlap_symm ] using h_overlap ⟩, rfl ⟩; exact h_color_j.symm ▸ fun h => mex_not_mem _ ( h.symm ▸ h_color_i_in_image ) /- If `k` is less than `mex s`, then `k` is in `s`. -/ lemma mex_subset_of_lt (s : Finset ℕ) (k : ℕ) (hk : k < mex s) : k ∈ s := by by_contra h_not_in have h_le : mex s ≤ k := Nat.find_min' _ h_not_in linarith /- The First-Fit coloring uses colors strictly less than the clique number. -/ lemma firstFitColoring_bound {n : ℕ} (intervals : Fin n → GreedyInterval) (sorted : SortedByStartTime intervals) (i : Fin n) : firstFitColoring intervals sorted i < cliqueNumber intervals := by -- Let $k = \text{firstFitColoring}(i)$. set k := firstFitColoring intervals sorted i let P := Finset.univ.filter (fun j => j < i ∧ overlap (intervals j) (intervals i)); -- By definition of `mex`, for every $c < k$, there is some $j \in P$ with $\text{color}(j) = c$. have h_mex_def : ∀ c < k, ∃ j ∈ P, firstFitColoring intervals sorted j = c := by intro c hc have h_mex : c ∈ P.attach.image (fun ⟨j, _⟩ => firstFitColoring intervals sorted j) := by apply mex_subset_of_lt; convert hc using 1; exact Eq.symm (firstFitColoring.eq_def intervals sorted i) aesop; -- Since the coloring is proper, all intervals in $P$ with distinct colors must be distinct. have h_distinct_colors : (P.image (fun j => firstFitColoring intervals sorted j)).card ≥ k := by have h_distinct_colors : Finset.image (fun j => firstFitColoring intervals sorted j) P ⊇ Finset.range k := by intro c hc; specialize h_mex_def c ( Finset.mem_range.mp hc ) ; aesop; exact le_trans ( by simp ) ( Finset.card_mono h_distinct_colors ); -- Since $P \cup \{i\}$ is a clique, we have $|P| + 1 \leq \omega$. have h_clique_size : (P.card + 1 : ℕ) ≤ cliqueNumber intervals := by have h_clique_size : IsClique intervals (insert i P) := by exact clique_at_start_time intervals sorted i; refine' le_trans _ ( Finset.le_sup <| Finset.mem_filter.mpr ⟨ Finset.mem_univ _, h_clique_size ⟩ ); rw [ Finset.card_insert_of_notMem ] ; aesop; exact lt_of_le_of_lt h_distinct_colors ( lt_of_le_of_lt ( Finset.card_image_le ) ( Nat.lt_of_succ_le h_clique_size ) ) /- There exists a permutation that sorts the intervals by start time. -/ lemma exists_permutation_sorted_by_start_time {n : ℕ} (intervals : Fin n → GreedyInterval) : ∃ p : Fin n ≃ Fin n, SortedByStartTime (intervals ∘ p) := by by_contra! h_contra; -- By definition of sorted list, we can construct a permutation `p` that sorts the intervals by their start times. have h_sorted : ∃ p : Fin n ≃ Fin n, ∀ i j, i < j → (intervals (p i)).start ≤ (intervals (p j)).start := by -- We can prove this using induction on $n$. have h_ind : ∀ (n : ℕ) (f : Fin n → ℕ), ∃ p : Fin n ≃ Fin n, ∀ i j, i < j → f (p i) ≤ f (p j) := by intro n f; induction' n with n ih <;> simp_all +decide [ Fin.forall_fin_succ ] ; -- Let $m$ be the index of the minimum element in $f$. obtain ⟨m, hm⟩ : ∃ m : Fin (n + 1), ∀ i : Fin (n + 1), f i ≥ f m := by simpa using Finset.exists_min_image Finset.univ ( fun i => f i ) ( Finset.univ_nonempty ); obtain ⟨ p, hp ⟩ := ih ( fun i => f ( Fin.succAbove m i ) ) ; use Equiv.ofBijective ( Fin.cons m ( fun i => Fin.succAbove m ( p i ) ) ) ⟨ by intro i j; induction i using Fin.inductionOn <;> induction j using Fin.inductionOn <;> aesop;, by intro i; by_cases hi : i = m <;> simp_all +decide [ Fin.exists_fin_succ ] ; exact Or.inr <| by rcases Fin.exists_succAbove_eq hi with ⟨ j, hj ⟩ ; exact ⟨ p.symm j, by simpa [ Fin.succAbove_ne ] using hj ⟩ ; ⟩ ; aesop; exact h_ind n fun i => ( intervals i ).start; exact h_contra h_sorted.choose fun i j hij => by obtain hij' | rfl := lt_or_eq_of_le hij <;> [ exact h_sorted.choose_spec _ _ hij'; rfl ] ; /- The number of colors used by a coloring is invariant under permutation of the indices. -/ lemma numColors_comp_perm {n : ℕ} (c : Coloring n) (p : Fin n ≃ Fin n) : Coloring.numColors (c ∘ p) = Coloring.numColors c := by -- The image of the coloring function is the same under permutation. have h_image : Finset.image (c ∘ p) Finset.univ = Finset.image c Finset.univ := by simp +decide [ Finset.ext_iff ]; exact fun a => ⟨ fun ⟨ i, hi ⟩ => ⟨ p i, hi ⟩, fun ⟨ i, hi ⟩ => ⟨ p.symm i, by simpa using hi ⟩ ⟩; exact congr_arg Finset.card h_image /- The clique number is invariant under permutation of the intervals. -/ lemma cliqueNumber_perm {n : ℕ} (intervals : Fin n → GreedyInterval) (p : Fin n ≃ Fin n) : cliqueNumber (intervals ∘ p) = cliqueNumber intervals := by refine' le_antisymm _ _; · refine' Finset.sup_le fun S hS => _; -- Since $S$ is a clique in the permuted intervals, $p(S)$ is a clique in the original intervals. have h_pS_clique : IsClique intervals (Finset.image p S) := by intro i hi j hj hij; aesop; exact Finset.le_sup ( f := Finset.card ) ( Finset.mem_filter.mpr ⟨ Finset.mem_univ _, h_pS_clique ⟩ ) |> le_trans ( by rw [ Finset.card_image_of_injective _ p.injective ] ); · refine' Finset.sup_le fun S hS => _; refine' le_trans _ ( Finset.le_sup <| Finset.mem_filter.mpr ⟨ Finset.mem_univ _, _ ⟩ ); rotate_left; exact Finset.image p.symm S; · intro i hi j hj hij; aesop; · rw [ Finset.card_image_of_injective _ p.symm.injective ] /- There exists a proper coloring using at most `cliqueNumber` colors. -/ lemma exists_proper_coloring_le_cliqueNumber {n : ℕ} (intervals : Fin n → GreedyInterval) : ∃ c : Coloring n, Coloring.proper intervals c ∧ Coloring.numColors c ≤ cliqueNumber intervals := by obtain ⟨ p, hp ⟩ := exists_permutation_sorted_by_start_time intervals; -- Apply `firstFitColoring` to the sorted intervals to get `c_sorted`. set c_sorted : Coloring n := firstFitColoring (intervals ∘ p) hp; refine' ⟨ c_sorted ∘ p.symm, _, _ ⟩; · intro i j hij h overlap; have := firstFitColoring_proper ( intervals ∘ p ) hp; aesop; · convert firstFitColoring_bound ( intervals ∘ p ) hp using 1; constructor <;> intro h <;> simp_all +decide [ Coloring.numColors ]; · exact fun i => firstFitColoring_bound (intervals ∘ ⇑p) hp i; · exact le_trans ( Finset.card_le_card ( Finset.image_subset_iff.mpr fun i _ => Finset.mem_Iio.mpr ( h ( p.symm i ) ) ) ) ( by simp +decide [ cliqueNumber_perm intervals p ] ) /- The non-deterministic greedy algorithm can achieve a coloring with `cliqueNumber` colors. -/ theorem nondeterministic_greedy_achieves_clique_number {n : ℕ} (intervals : Fin n → GreedyInterval) (h_sorted : SortedByFinishTime intervals) : ∃ state : GreedyState n n, Reachable intervals state ∧ Coloring.numColors state.color = cliqueNumber intervals := by -- Existence of an optimal proper coloring obtain ⟨phi, h_phi_proper, h_phi_le⟩ := exists_proper_coloring_le_cliqueNumber intervals have h_phi_ge := proper_coloring_ge_cliqueNumber intervals phi h_phi_proper have h_phi_eq : Coloring.numColors phi = cliqueNumber intervals := le_antisymm h_phi_le h_phi_ge -- Existence of a reachable state consistent with phi obtain ⟨state, h_reach, h_inv, h_intro⟩ := exists_reachable_invariant_state_at_k n intervals phi h_sorted h_phi_proper n (Nat.le_refl n) use state constructor · exact h_reach · apply le_antisymm · -- Upper bound: numColors state <= cliqueNumber apply invariant_implies_bound intervals phi state h_inv h_intro h_phi_eq · -- Lower bound: cliqueNumber <= numColors state apply proper_coloring_ge_cliqueNumber obtain ⟨_, h_proper_state, _, _⟩ := h_inv exact h_proper_state #check nondeterministic_greedy_achieves_clique_number #print axioms nondeterministic_greedy_achieves_clique_number