feat: prove that omega-regular languages are closed under complementation

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -7,8 +7,7 @@ Authors: Ching-Tsun Chou
 module
 
 public import Cslib.Computability.Automata.NA.Pair
-public import Cslib.Computability.Languages.Congruences.RightCongruence
-public import Cslib.Computability.Languages.OmegaLanguage
+public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Data.Set.Saturation
 
 @[expose] public section
@@ -106,6 +105,32 @@ theorem mem_buchiFamily [Inhabited Symbol]
       xl ++ω xls.flatten = xs := by
   grind [buchiFamily]
 
+open Finset in
+/-- `na.buchiFamily` is a cover if `na` has only finitely many states.
+This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details
+of `na.BuchiCongruence` other than that it is of finite index. -/
+theorem buchiFamily_cover [Inhabited Symbol] [Finite State] :
+    ⨆ i, na.buchiFamily i = ⊤ := by
+  ext xs
+  have : Finite (Quotient na.BuchiCongruence.eq) := buchiCongruence_fin_index
+  let color (t : Finset ℕ) : Quotient na.BuchiCongruence.eq :=
+    if h : t.Nonempty then ⟦ xs.extract (t.min' h) (t.max' h) ⟧ else ⟦ [] ⟧
+  obtain ⟨b, ns, h_ns, h_color⟩ := infinite_graph_ramsey color
+  obtain ⟨f, h_mono, rfl⟩ := strictMono_of_infinite h_ns
+  simp only [ωLanguage.mem_iSup, Prod.exists, ωLanguage.mem_top, iff_true]
+  use ⟦ xs.take (f 0) ⟧, b
+  apply mem_buchiFamily.mpr
+  use xs.take (f 0), xs.drop (f 0) |>.toSegs (f · - f 0)
+  split_ands
+  · grind
+  · intro k
+    specialize h_color {f k, f (k + 1)}
+    have := @h_mono 0 k
+    have := @h_mono k (k + 1)
+    grind [extract_drop, Finset.insert_nonempty, Finset.singleton_nonempty, min'_insert,
+      min'_singleton, max'_insert, max'_singleton, toSegs_def, Language.mem_sub_one]
+  · grind [Nat.base_zero_strictMono h_mono]
+
 -- This intermediate result is split out of the proof of `buchiCongruence_saturation` below
 -- because that proof was too big and kept exceeding the default `maxHeartbeats`.
 private lemma frequently_via_accept [Inhabited Symbol]

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -9,10 +9,9 @@ module
 public import Cslib.Computability.Automata.DA.Buchi
 public import Cslib.Computability.Automata.NA.BuchiEquiv
 public import Cslib.Computability.Automata.NA.BuchiInter
-public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Sum
+public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
-public import Cslib.Foundations.Data.Set.Saturation
 public import Mathlib.Data.Finite.Card
 public import Mathlib.Data.Finite.Sigma
 public import Mathlib.Logic.Equiv.Fin.Basic
@@ -234,6 +233,19 @@ theorem IsRegular.fin_cover_saturates_compl {I : Type*} [Finite I]
     (hs : Saturates p q) (hc : ⨆ i, p i = ⊤) (hr : ∀ i, (p i).IsRegular) : (qᶜ).IsRegular :=
   IsRegular.fin_cover_saturates (saturates_compl hs) hc hr
 
+open NA.Buchi in
+/-- The complementation of an ω-regular language is ω-regular. -/
+@[simp]
+theorem IsRegular.compl {Symbol : Type} [Inhabited Symbol] {p : ωLanguage Symbol}
+    (h : p.IsRegular) : (pᶜ).IsRegular := by
+  obtain ⟨State, h_fin, na, rfl⟩ := h
+  have : Finite (Quotient na.BuchiCongruence.eq) := buchiCongruence_fin_index
+  have h_sat := buchiFamily_saturation (na := na)
+  have h_cov := buchiFamily_cover (na := na)
+  apply IsRegular.fin_cover_saturates_compl h_sat h_cov
+  have := Language.IsRegular.congr_fin_index (c := na.BuchiCongruence)
+  grind [buchiFamily, IsRegular.hmul, IsRegular.omegaPow]
+
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔

Cslib/Foundations/Data/OmegaSequence/InfOcc.lean

@@ -77,6 +77,12 @@ theorem frequently_in_strictMono {p : ℕ → Prop} {f : ℕ → ℕ}
   · use k - f (segment f k)
     grind [segment_lower_bound' hm h0, segment_upper_bound' hm h0]
 
+open Nat in
+/-- Every infinite subset of ℕ is the range of a strictly monotonic function from ℕ to ℕ. -/
+theorem strictMono_of_infinite {ns : Set ℕ} (h : ns.Infinite) :
+    ∃ φ : ℕ → ℕ, StrictMono φ ∧ range φ = ns :=
+  ⟨nth (· ∈ ns), nth_strictMono h, range_nth_of_infinite h⟩
+
 end ωSequence
 
 end Cslib