feat: prepare for proving the closure of omega-regular languages under complementation

Cslib.lean

@@ -37,6 +37,7 @@ public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
 public import Cslib.Foundations.Data.Relation
+public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -14,6 +14,7 @@ public import Cslib.Computability.Automata.NA.Loop
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Foundations.Data.Set.Saturation
 public import Mathlib.Data.Finite.Sigma
 public import Mathlib.Data.Finite.Sum
 
@@ -185,6 +186,22 @@ theorem IsRegular.omegaPow [Inhabited Symbol] {l : Language Symbol}
   use Unit ⊕ State, inferInstance, ⟨na.loop, {inl ()}⟩
   exact NA.Buchi.loop_language_eq
 
+/-- If an ω-language has a finite saturating cover made of ω-regular languages,
+then it is an ω-regular language. -/
+theorem IsRegular.fin_cover_saturates {I : Type*} [Finite I]
+    {p : I → ωLanguage Symbol} {q : ωLanguage Symbol}
+    (hs : Saturates p q) (hc : ⨆ i, p i = ⊤) (hr : ∀ i, (p i).IsRegular) : q.IsRegular := by
+  rw [saturates_eq_biUnion hs hc]
+  apply IsRegular.iSup
+  grind
+
+/-- If an ω-language has a finite saturating cover made of ω-regular languages,
+then its complement is an ω-regular language. -/
+theorem IsRegular.fin_cover_saturates_compl {I : Type*} [Finite I]
+    {p : I → ωLanguage Symbol} {q : ωLanguage Symbol}
+    (hs : Saturates p q) (hc : ⨆ i, p i = ⊤) (hr : ∀ i, (p i).IsRegular) : (qᶜ).IsRegular :=
+  IsRegular.fin_cover_saturates (saturates_compl hs) hc hr
+
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔

Cslib/Foundations/Data/Set/Saturation.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Set.Lattice
+
+@[expose] public section
+
+/-!
+# Saturation
+-/
+
+namespace Set
+
+variable {ι α : Type*}
+
+/-- `f : ι → Set α` saturates `s : Set α` iff `f i` is a subset of `s`
+whenever `f i` and `s` has any intersection at all. -/
+def Saturates (f : ι → Set α) (s : Set α) : Prop :=
+  ∀ i : ι, (f i ∩ s).Nonempty → f i ⊆ s
+
+variable {f : ι → Set α} {s : Set α}
+
+/-- If `f` saturates `s`, then `f` saturates its complement `sᶜ` as well. -/
+@[simp, scoped grind .]
+theorem saturates_compl (hs : Saturates f s) : Saturates f sᶜ := by
+  rintro i ⟨_, _⟩ y _ _
+  have : (f i ∩ s).Nonempty := ⟨y, by grind⟩
+  grind [Saturates]
+
+/-- If `f` is a cover and saturates `s`, then `s` is the union of all `f i` that intersects `s`. -/
+theorem saturates_eq_biUnion (hs : Saturates f s) (hc : ⋃ i, f i = univ) :
+    s = ⋃ i ∈ {i | (f i ∩ s).Nonempty}, f i := by
+  ext x
+  simp only [mem_setOf_eq, mem_iUnion, exists_prop]
+  constructor
+  · intro h_x
+    obtain ⟨i, _⟩ := mem_iUnion.mp <| univ_subset_iff.mpr hc <| mem_univ x
+    use i, ⟨x, by grind⟩, by grind
+  · rintro ⟨i, h_i, _⟩
+    grind [hs i h_i]
+
+end Set