refactor: provide a properly encapsulated implementation of OmegaLanguage (#485)

This PR provides a properly encapsulated implementation of
OmegaLanguage, using a one-field `structure`. It is influenced and will
be affected by mathlib#36934, but it is not dependent on it.

Author: ctchou

Cslib/Computability/Automata/DA/Buchi.lean

@@ -21,14 +21,13 @@ open scoped FinAcc Buchi
 
 variable {State Symbol : Type*}
 
-open Acceptor ωAcceptor in
+open Acceptor ωAcceptor ωLanguage in
 /-- The ω-language accepted by a deterministic Buchi automaton is the ω-limit
-of the language accepted by the same automaton.
--/
+of the language accepted by the same automaton. -/
 @[scoped grind =]
 theorem buchi_eq_finAcc_omegaLim {da : DA State Symbol} {acc : Set State} :
     language (Buchi.mk da acc) = (language (FinAcc.mk da acc))↗ω := by
-  ext xs
-  simp +instances
+  apply mem_ext
+  grind [ωAcceptor.Accepts, Acceptor.Accepts]
 
 end Cslib.Automata.DA

Cslib/Computability/Automata/NA/BuchiEquiv.lean

@@ -12,14 +12,12 @@ public import Cslib.Computability.Automata.NA.Basic
 
 /-! # 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
+open Set Function Filter ωSequence ωLanguage ωAcceptor
+open scoped LTS
 
 variable {Symbol : Type u} {State : Type v} {State' : Type w}
 
@@ -57,7 +55,8 @@ theorem reindex_run_iff' {f : State ≃ State'} {nba : Buchi State Symbol}
 @[simp, scoped grind =]
 theorem reindex_language_eq {f : State ≃ State'} {nba : Buchi State Symbol} :
     language (nba.reindex f) = language nba := by
-  ext xs
+  apply mem_ext
+  intro xs
   constructor
   · rintro ⟨ss', h_run', h_acc'⟩
     #adaptation_note

Cslib/Computability/Automata/NA/BuchiInter.lean

@@ -26,7 +26,7 @@ simply because toggling can be easily modeled by the boolean operation `not`.
 
 namespace Cslib.Automata.NA.Buchi
 
-open Set Prod Filter ωSequence ωAcceptor
+open Set Prod Filter ωSequence ωLanguage ωAcceptor
 open scoped LTS
 
 variable {Symbol : Type*} {State : Bool → Type*}
@@ -93,16 +93,15 @@ lemma inter_freq_comp_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((
   apply leadsTo_cases_or (q := {⟨_, b⟩ | b = false}) <;>
   grind [until_frequently_leadsTo_and, univ_inter]
 
--- TODO: fix proof to work with backward.isDefEq.respectTransparency
-set_option backward.isDefEq.respectTransparency false in
 /-- The language accepted by the intersection automaton is the intersection of
 the languages accepted by the two component automata. -/
 @[simp, scoped grind =]
 theorem inter_language_eq :
     language (Buchi.mk (interNA na acc) (interAccept acc)) =
-    ⋂ i, language (Buchi.mk (na i) (acc i)) := by
-  ext xs
-  rw [mem_iInter]
+    ⨅ i, language (Buchi.mk (na i) (acc i)) := by
+  apply mem_ext
+  intro xs
+  simp only [ωLanguage.mem_iInf]
   constructor
   · intro ⟨ss, h_run, h_inf⟩ i
     use ss.map (fun s ↦ s.fst i)

Cslib/Computability/Automata/NA/Pair.lean

@@ -104,7 +104,8 @@ of the form `L * M^ω`, where all `L`s and `M`s are regular languages. -/
 theorem language_eq_fin_iSup_hmul_omegaPow
     [Inhabited Symbol] [Finite State] (na : Buchi State Symbol) :
     language na = ⨆ s ∈ na.start, ⨆ t ∈ na.accept, (na.pairLang s t) * (na.pairLang t t)^ω := by
-  ext xs
+  apply mem_ext
+  intro xs
   simp only [ωAcceptor.mem_language, ωLanguage.mem_iSup, ωLanguage.mem_hmul, LTS.mem_pairLang]
   constructor
   · rintro ⟨ss, h_run, h_inf⟩

Cslib/Computability/Automata/NA/Sum.lean

@@ -12,11 +12,11 @@ public import Cslib.Computability.Automata.NA.Basic
 
 /-! # Sum of nondeterministic automata. -/
 
-open Set Function Filter Cslib.ωSequence
-open scoped Cslib.LTS
-
 namespace Cslib.Automata.NA
 
+open Set Function ωSequence ωLanguage
+open scoped Cslib.LTS
+
 variable {Symbol I : Type*} {State : I → Type*}
 
 /-- The sum of an indexed family of nondeterministic automata. -/
@@ -58,16 +58,15 @@ namespace Buchi
 
 open ωAcceptor
 
--- TODO: fix proof to work with backward.isDefEq.respectTransparency
-set_option backward.isDefEq.respectTransparency false in
 /-- The ω-language accepted by the Buchi sum automata is the union of the ω-languages accepted
 by its component automata. -/
 @[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]
+    ⨆ i, language (Buchi.mk (na i) (acc i)) := by
+  apply mem_ext
+  intro xs
+  simp only [mem_language, mem_iSup]
   constructor
   · rintro ⟨ss, h_run, h_acc⟩
     simp only [mem_iUnion] at h_acc

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -115,7 +115,8 @@ This theorem uses the Ramsey theorem for infinite graphs and does not depend on
 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
+  apply mem_ext
+  intro xs
   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 ⟦ [] ⟧
@@ -175,7 +176,8 @@ private lemma frequently_via_accept [Inhabited Symbol]
   · grind only [!List.take_append_drop]
 
 /-- `na.buchiFamily` saturates the ω-language accepted by `na`. -/
-theorem buchiFamily_saturation [Inhabited Symbol] : Saturates na.buchiFamily (language na) := by
+theorem buchiFamily_saturation [Inhabited Symbol] :
+    Saturates (fun i ↦ (na.buchiFamily i).toSet) (language na).toSet := by
   rintro ⟨a, b⟩ ⟨xs, h_xs, h_lang⟩ ys h_ys
   obtain ⟨xl, xls, h_xl_c, h_xls_c, rfl⟩ := mem_buchiFamily.mp h_xs
   obtain ⟨yl, yls, h_yl_c, h_yls_c, rfl⟩ := mem_buchiFamily.mp h_ys