From 7f07a18b1861b8b8adc9c1962c896dd2dcd5535f Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Mon, 9 Feb 2026 13:58:13 -0800
Subject: [PATCH 1/2] feat: prove that omega-regular languages are closed under
 complementation

---
 .../Congruences/BuchiCongruence.lean          | 35 +++++++++++++++++--
 .../Languages/OmegaRegularLanguage.lean       | 16 +++++++--
 .../Data/OmegaSequence/InfOcc.lean            |  9 +++++
 3 files changed, 56 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean
index c9b0be95c..2125ca809 100644
--- a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean
+++ b/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,38 @@ theorem mem_buchiFamily [Inhabited Symbol]
       xl ++ω xls.flatten = xs := by
   grind [buchiFamily]
 
+/-- `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
+  simp only [ωLanguage.mem_iSup, Prod.exists, ωLanguage.mem_top, iff_true]
+  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
+  let a : Quotient na.BuchiCongruence.eq := ⟦ xs.take (f 0) ⟧
+  use a, b
+  apply mem_buchiFamily.mpr
+  let ys := xs.drop (f 0)
+  let g := (f · - f 0)
+  have h_mono' : StrictMono g := Nat.base_zero_strictMono h_mono
+  use xs.take (f 0), ys.toSegs g, by grind, ?_, by grind
+  intro k
+  simp only [toSegs_def, Language.mem_sub_one]
+  split_ands
+  · have := h_mono.monotone (show 0 ≤ k by grind)
+    have := h_mono.monotone (show 0 ≤ k + 1 by grind)
+    simp [ys, g, extract_drop, show f 0 + (f k - f 0) = f k by grind,
+      show f 0 + (f (k + 1) - f 0) = f (k + 1) by grind]
+    have := h_mono (show k < k + 1 by grind)
+    specialize h_color ({f k, f (k + 1)} : Finset ℕ) (by grind) (by grind)
+    simp [color] at h_color
+    grind
+  · grind [h_mono' (show k < k + 1 by grind)]
+
 -- 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]
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 94f25f205..526cd5e2a 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/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 ↔
diff --git a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
index 67ce614bd..b39c0fadc 100644
--- a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
@@ -77,6 +77,15 @@ 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 := by
+  use (nth (· ∈ ns))
+  split_ands
+  · exact nth_strictMono h
+  · exact range_nth_of_infinite h
+
 end ωSequence
 
 end Cslib

From d3208d1a1aa79385413541f05fda25432530c0ff Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Fri, 20 Mar 2026 15:49:54 -0700
Subject: [PATCH 2/2] incorporate Chris Henson's comments

---
 .../Congruences/BuchiCongruence.lean          | 30 ++++++++-----------
 .../Data/OmegaSequence/InfOcc.lean            |  7 ++---
 2 files changed, 14 insertions(+), 23 deletions(-)

diff --git a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean
index 2125ca809..ec1af6a0f 100644
--- a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean
+++ b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean
@@ -105,37 +105,31 @@ 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
-  simp only [ωLanguage.mem_iSup, Prod.exists, ωLanguage.mem_top, iff_true]
   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
-  let a : Quotient na.BuchiCongruence.eq := ⟦ xs.take (f 0) ⟧
-  use a, b
+  simp only [ωLanguage.mem_iSup, Prod.exists, ωLanguage.mem_top, iff_true]
+  use ⟦ xs.take (f 0) ⟧, b
   apply mem_buchiFamily.mpr
-  let ys := xs.drop (f 0)
-  let g := (f · - f 0)
-  have h_mono' : StrictMono g := Nat.base_zero_strictMono h_mono
-  use xs.take (f 0), ys.toSegs g, by grind, ?_, by grind
-  intro k
-  simp only [toSegs_def, Language.mem_sub_one]
+  use xs.take (f 0), xs.drop (f 0) |>.toSegs (f · - f 0)
   split_ands
-  · have := h_mono.monotone (show 0 ≤ k by grind)
-    have := h_mono.monotone (show 0 ≤ k + 1 by grind)
-    simp [ys, g, extract_drop, show f 0 + (f k - f 0) = f k by grind,
-      show f 0 + (f (k + 1) - f 0) = f (k + 1) by grind]
-    have := h_mono (show k < k + 1 by grind)
-    specialize h_color ({f k, f (k + 1)} : Finset ℕ) (by grind) (by grind)
-    simp [color] at h_color
-    grind
-  · grind [h_mono' (show k < k + 1 by grind)]
+  · 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`.
diff --git a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
index b39c0fadc..03313f428 100644
--- a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
@@ -80,11 +80,8 @@ theorem frequently_in_strictMono {p : ℕ → Prop} {f : ℕ → ℕ}
 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 := by
-  use (nth (· ∈ ns))
-  split_ands
-  · exact nth_strictMono h
-  · exact range_nth_of_infinite h
+    ∃ φ : ℕ → ℕ, StrictMono φ ∧ range φ = ns :=
+  ⟨nth (· ∈ ns), nth_strictMono h, range_nth_of_infinite h⟩
 
 end ωSequence