From 84a294e5691c4337b608ee190719cb4ca8bd485d Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Wed, 14 Jan 2026 21:16:56 -0800
Subject: [PATCH 1/2] feat: prepare for proving the closure of omega-regular
 languages under complementation

---
 Cslib.lean                                    |  1 +
 .../Languages/OmegaRegularLanguage.lean       | 18 +++++++
 Cslib/Foundations/Data/Set/Saturation.lean    | 48 +++++++++++++++++++
 3 files changed, 67 insertions(+)
 create mode 100644 Cslib/Foundations/Data/Set/Saturation.lean

diff --git a/Cslib.lean b/Cslib.lean
index 8c6984eb..f10f2800 100644
--- a/Cslib.lean
+++ b/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
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 35072807..21267955 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/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,23 @@ 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
+  have hq : q = ⨆ i ∈ {i | (p i ⊓ q).Nonempty}, p i := saturates_eq_biUnion hs hc
+  rw [hq]
+  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 := by
+  exact IsRegular.fin_cover_saturates (saturates_compl hs) hc hr
+
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔
diff --git a/Cslib/Foundations/Data/Set/Saturation.lean b/Cslib/Foundations/Data/Set/Saturation.lean
new file mode 100644
index 00000000..4edcaf9c
--- /dev/null
+++ b/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 h_y : (f i ∩ s).Nonempty := by use y; grind
+  grind [hs i h_y]
+
+/-- 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

From f60543223b4ee4db7367b75dcce620bbcfb3b0e8 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Sat, 17 Jan 2026 16:15:53 -0800
Subject: [PATCH 2/2] incorporate Chris Henson's comments

---
 Cslib/Computability/Languages/OmegaRegularLanguage.lean | 7 +++----
 Cslib/Foundations/Data/Set/Saturation.lean              | 4 ++--
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 21267955..5f948404 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -191,8 +191,7 @@ 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
-  have hq : q = ⨆ i ∈ {i | (p i ⊓ q).Nonempty}, p i := saturates_eq_biUnion hs hc
-  rw [hq]
+  rw [saturates_eq_biUnion hs hc]
   apply IsRegular.iSup
   grind
 
@@ -200,8 +199,8 @@ theorem IsRegular.fin_cover_saturates {I : Type*} [Finite I]
 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 := by
-  exact IsRegular.fin_cover_saturates (saturates_compl hs) hc hr
+    (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} :
diff --git a/Cslib/Foundations/Data/Set/Saturation.lean b/Cslib/Foundations/Data/Set/Saturation.lean
index 4edcaf9c..45cde752 100644
--- a/Cslib/Foundations/Data/Set/Saturation.lean
+++ b/Cslib/Foundations/Data/Set/Saturation.lean
@@ -30,8 +30,8 @@ variable {f : ι → Set α} {s : Set α}
 @[simp, scoped grind .]
 theorem saturates_compl (hs : Saturates f s) : Saturates f sᶜ := by
   rintro i ⟨_, _⟩ y _ _
-  have h_y : (f i ∩ s).Nonempty := by use y; grind
-  grind [hs i h_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) :