feat: prove that omega-regularity is closed under union and is universe-polymorphic

Cslib.lean

@@ -5,9 +5,11 @@ import Cslib.Computability.Automata.DAToNA
 import Cslib.Computability.Automata.EpsilonNA
 import Cslib.Computability.Automata.EpsilonNAToNA
 import Cslib.Computability.Automata.NA
+import Cslib.Computability.Automata.NABuchiEquiv
 import Cslib.Computability.Automata.NAToDA
 import Cslib.Computability.Automata.OmegaAcceptor
 import Cslib.Computability.Automata.Prod
+import Cslib.Computability.Automata.Sum
 import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage

Cslib/Computability/Automata/DAToNA.lean

@@ -26,14 +26,14 @@ def toNA (a : DA State Symbol) : NA State Symbol :=
 instance : Coe (DA State Symbol) (NA State Symbol) where
   coe := toNA
 
-open scoped FLTS NA in
+open scoped FLTS NA NA.Run in
 @[simp, scoped grind =]
 theorem toNA_run {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} :
     a.toNA.Run xs ss ↔ a.run xs = ss := by
   constructor
   · rintro _
     ext n
-    induction n <;> grind
+    induction n <;> grind [NA.Run]
   · grind
 
 namespace FinAcc

Cslib/Computability/Automata/NA.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi, Ching-Tsun Chou
+Authors: Fabrizio Montesi, Ching-Tsun Chou, Chris Henson.
 -/
 
 import Cslib.Computability.Automata.Acceptor
@@ -40,10 +40,28 @@ namespace NA
 variable {State : Type _} {Symbol : Type _}
 
 /-- Infinite run. -/
-@[scoped grind =]
 def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) :=
   ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))
 
+-- The following lemmas help `grind` deal with the definition of `NA.Run` better.
+section NARunGrind
+
+variable {na : NA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State}
+
+@[scoped grind <=]
+lemma Run.mk (h₁ : ss 0 ∈ na.start) (h₂ : ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))) : Run na xs ss
+  := ⟨h₁, h₂⟩
+
+@[scoped grind →]
+lemma Run.start (run : Run na xs ss) : ss 0 ∈ na.start :=
+  run.left
+
+@[scoped grind =>]
+lemma Run.trans (run : Run na xs ss) : ∀ n, na.Tr (ss n) (xs n) (ss (n + 1)) :=
+  run.right
+
+end NARunGrind
+
 /-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends NA State Symbol where
   /-- The accept states. -/

Cslib/Computability/Automata/NABuchiEquiv.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
+Relexsed under Apache 2.0 license xs described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-! # Equivalence of nondeterministic Buchi automata (NBAs). -/
+
+open Set Function Filter Cslib.ωSequence
+open scoped Cslib.LTS
+
+universe u v w
+
+namespace Cslib.Automata.NA.Buchi
+
+open ωAcceptor
+
+variable {Symbol : Type u} {State : Type v} {State' : Type w}
+
+/-- Lifts an equivalence on states to an equivalence on NBAs. -/
+@[scoped grind =]
+def reindex (f : State ≃ State') : Buchi State Symbol ≃ Buchi State' Symbol where
+  toFun nba := {
+    Tr s x t := nba.Tr (f.symm s) x (f.symm t)
+    start := f '' nba.start
+    accept := f.symm ⁻¹' nba.accept
+  }
+  invFun nba' := {
+    Tr s x t := nba'.Tr (f s) x (f t)
+    start := f.symm '' nba'.start
+    accept := f ⁻¹' nba'.accept
+  }
+  left_inv nba := by simp
+  right_inv nba' := by simp
+
+theorem reindex_run_iff {f : State ≃ State'} {nba : Buchi State Symbol}
+    {xs : ωSequence Symbol} {ss' : ωSequence State'} :
+    (nba.reindex f).Run xs ss' ↔ nba.Run xs (ss'.map f.symm) := by
+  constructor <;>
+  { rintro ⟨h_init, h_next⟩
+    constructor
+    · grind
+    · exact fun n ↦ h_next n }
+
+@[simp]
+theorem reindex_run_iff' {f : State ≃ State'} {nba : Buchi State Symbol}
+    {xs : ωSequence Symbol} {ss : ωSequence State} :
+    (nba.reindex f).Run xs (ss.map f) ↔ nba.Run xs ss := by
+  simp [reindex_run_iff]
+
+@[simp, scoped grind =]
+theorem reindex_language_eq {f : State ≃ State'} {nba : Buchi State Symbol} :
+    language (nba.reindex f) = language nba := by
+  ext xs
+  constructor
+  · rintro ⟨ss', h_run', h_acc'⟩
+    grind [reindex_run_iff]
+  · rintro ⟨ss, h_run, h_acc⟩
+    use ss.map f
+    constructor <;> grind [reindex_run_iff']
+
+end Cslib.Automata.NA.Buchi

Cslib/Computability/Automata/Sum.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
+Relexsed under Apache 2.0 license xs described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-! # Sum of automata. -/
+
+open Set Function Filter Cslib.ωSequence
+open scoped Cslib.LTS
+
+namespace Cslib.Automata.NA
+open scoped Run
+
+variable {Symbol I : Type*} {State : I → Type*}
+
+@[scoped grind =]
+def iSum (na : (i : I) → NA (State i) Symbol) : NA (Σ i, State i) Symbol where
+  start := ⋃ i, Sigma.mk i '' (na i).start
+  Tr s x t := ∃ i s_i t_i, (na i).Tr s_i x t_i ∧ ⟨i, s_i⟩ = s ∧ ⟨i, t_i⟩ = t
+
+@[simp, scoped grind =]
+theorem iSum_run_iff {na : (i : I) → NA (State i) Symbol}
+    {xs : ωSequence Symbol} {ss : ωSequence (Σ i, State i)} :
+    (iSum na).Run xs ss ↔ ∃ i ss_i, (na i).Run xs ss_i ∧ ss_i.map (Sigma.mk i) = ss := by
+  constructor
+  · rintro ⟨h_init, h_next⟩
+    obtain ⟨i, s0, h_s0, h_ss0⟩ := mem_iUnion.mp h_init
+    have h_exists n : ∃ s_i, ⟨i, s_i⟩ = ss n := by
+      induction n
+      case zero => use s0
+      case succ n h_ind =>
+        obtain ⟨j, s_j, t_j, _⟩ := h_next n
+        grind
+    choose ss_i h_ss_i using h_exists
+    use i, ss_i
+    refine ⟨⟨?_, ?_⟩, ?_⟩
+    · grind
+    · intro n
+      obtain ⟨j, _⟩ := h_next n
+      grind
+    · ext <;> grind
+  · rintro ⟨i, ss, h_run, rfl⟩
+    constructor
+    · simp only [iSum, get_map, mem_iUnion, mem_image, Sigma.mk.injEq]
+      grind
+    · intro n
+      use i
+      grind [Run]
+
+namespace Buchi
+
+open ωAcceptor
+
+@[simp]
+theorem iSum_language_eq {na : (i : I) → NA (State i) Symbol} {acc : (i : I) → Set (State i)} :
+    language (Buchi.mk (iSum na) (⋃ i, Sigma.mk i '' (acc i))) =
+    ⋃ i, language (Buchi.mk (na i) (acc i)) := by
+  ext xs
+  rw [mem_iUnion]
+  constructor
+  · rintro ⟨ss, h_run, h_acc⟩
+    simp only [mem_iUnion] at h_acc
+    grind
+  · rintro ⟨i, ss_i, _⟩
+    use ss_i.map (Sigma.mk i)
+    simp only [mem_iUnion]
+    grind
+
+end Buchi
+
+end Cslib.Automata.NA

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -5,8 +5,11 @@ Authors: Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.DABuchi
+import Cslib.Computability.Automata.NABuchiEquiv
+import Cslib.Computability.Automata.Sum
 import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.RegularLanguage
+import Mathlib.Data.Finite.Sigma
 
 /-!
 # ω-Regular languages
@@ -17,14 +20,31 @@ This file defines ω-regular languages and proves some properties of them.
 open Set Function Filter Cslib.ωSequence Cslib.Automata ωAcceptor
 open scoped Computability
 
+universe u v
+
 namespace Cslib.ωLanguage
 
-variable {Symbol : Type*}
+variable {Symbol : Type u}
 
 /-- An ω-language is ω-regular iff it is accepted by a
 finite-state nondeterministic Buchi automaton. -/
 def IsRegular (p : ωLanguage Symbol) :=
-  ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, language na = p
+  ∃ (State : Type) (_ : Finite State) (na : NA.Buchi State Symbol), language na = p
+
+/-- Helper lemma for `isRegular_iff` below. -/
+private lemma isRegular_iff.helper.{v'} {Symbol : Type u} {p : ωLanguage Symbol}
+    (h : ∃ (σ : Type v) (_ : Finite σ) (na : NA.Buchi σ Symbol), language na = p) :
+    ∃ (σ' : Type v') (_ : Finite σ') (na : NA.Buchi σ' Symbol), language na = p := by
+  have ⟨σ, _, na, h_na⟩ := h
+  have ⟨σ', ⟨f⟩⟩ := Small.equiv_small.{v', v} (α := σ)
+  use σ', Finite.of_equiv σ f, na.reindex f
+  rwa [NA.Buchi.reindex_language_eq]
+
+/-- The state space of the accepting finite-state nondeterministic Buchi automaton
+can in fact be universe-polymorphic. -/
+theorem isRegular_iff {p : ωLanguage Symbol} :
+    p.IsRegular ↔ ∃ (σ : Type v) (_ : Finite σ) (na : NA.Buchi σ Symbol), language na = p :=
+  ⟨isRegular_iff.helper, isRegular_iff.helper⟩
 
 /-- The ω-language accepted by a finite-state deterministic Buchi automaton is ω-regular. -/
 theorem IsRegular.of_da_buchi {State : Type} [Finite State] (da : DA.Buchi State Symbol) :
@@ -34,8 +54,8 @@ theorem IsRegular.of_da_buchi {State : Type} [Finite State] (da : DA.Buchi State
 /-- There is an ω-regular language that is not accepted by any deterministic Buchi automaton,
 where the automaton is not even required to be finite-state. -/
 theorem IsRegular.not_da_buchi :
-  ∃ Symbol : Type, ∃ p : ωLanguage Symbol, p.IsRegular ∧
-    ¬ ∃ State : Type, ∃ da : DA.Buchi State Symbol, language da = p := by
+  ∃ (Symbol : Type) (p : ωLanguage Symbol), p.IsRegular ∧
+    ¬ ∃ (State : Type) (da : DA.Buchi State Symbol), language da = p := by
   refine ⟨Fin 2, Example.eventually_zero, ?_, ?_⟩
   · use Fin 2, inferInstance, Example.eventually_zero_na,
       Example.eventually_zero_accepted_by_na_buchi
@@ -44,14 +64,59 @@ theorem IsRegular.not_da_buchi :
     grind [DA.buchi_eq_finAcc_omegaLim]
 
 /-- The ω-limit of a regular language is ω-regular. -/
+@[simp]
 theorem IsRegular.regular_omegaLim {l : Language Symbol}
     (h : l.IsRegular) : (l↗ω).IsRegular := by
   obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := Language.IsRegular.iff_cslib_dfa.mp h
   grind [IsRegular.of_da_buchi, =_ DA.buchi_eq_finAcc_omegaLim]
 
+/-- The empty language is ω-regular. -/
+@[simp]
+theorem IsRegular.bot : (⊥ : ωLanguage Symbol).IsRegular := by
+  let na : NA.Buchi Unit Symbol := {
+    Tr _ _ _ := False
+    start := ∅
+    accept := ∅ }
+  use Unit, inferInstance, na
+  ext xs
+  simp [na]
+
+/-- The union of two ω-regular languages is ω-regular. -/
+@[simp]
+theorem IsRegular.sup {p1 p2 : ωLanguage Symbol}
+    (h1 : p1.IsRegular) (h2 : p2.IsRegular) : (p1 ⊔ p2).IsRegular := by
+  obtain ⟨State1, h_fin1, ⟨na1, acc1⟩, rfl⟩ := h1
+  obtain ⟨State2, h_fin1, ⟨na2, acc2⟩, rfl⟩ := h2
+  let State : Fin 2 → Type
+    | 0 => State1 | 1 => State2
+  let na : (i : Fin 2) → NA (State i) Symbol
+    | 0 => na1 | 1 => na2
+  let acc : (i : Fin 2) → Set (State i)
+    | 0 => acc1 | 1 => acc2
+  have : ∀ i, Finite (State i) := by grind
+  use (Σ i : Fin 2, State i), inferInstance, ⟨(NA.iSum na), (⋃ i, Sigma.mk i '' (acc i))⟩
+  ext xs
+  simp only [NA.Buchi.iSum_language_eq, mem_sup, mem_language]
+  rw [mem_iUnion, Fin.exists_fin_two]
+  grind
+
+/-- The union of any finite number of ω-regular languages is ω-regular. -/
+@[simp]
+theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {p : I → ωLanguage Symbol}
+    (h : ∀ i ∈ s, (p i).IsRegular) : (⨆ i ∈ s, p i).IsRegular := by
+  generalize h_n : s.ncard = n
+  induction n generalizing s
+  case zero =>
+    have := ncard_eq_zero (s := s)
+    grind [IsRegular.bot, iSup_bot]
+  case succ n h_ind =>
+    obtain ⟨i, t, h_i, rfl, rfl⟩ := (ncard_eq_succ (s := s)).mp h_n
+    rw [iSup_insert]
+    grind [IsRegular.sup]
+
 /-- McNaughton's Theorem. -/
 proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔
-    ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, language da = p
+    ∃ (State : Type) (_ : Finite State) (da : DA.Muller State Symbol), language da = p
 
 end Cslib.ωLanguage