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

Author: ctchou

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
@@ -110,6 +109,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]

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
@@ -228,6 +227,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,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