feat: define BuchiCongruence and prove that it is a right congruence of finite index

Cslib.lean

@@ -6,6 +6,7 @@ public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic
 public import Cslib.Computability.Automata.DA.Buchi
+public import Cslib.Computability.Automata.DA.Congr
 public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.EpsilonNA.Basic
@@ -21,6 +22,8 @@ public import Cslib.Computability.Automata.NA.Prod
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Languages.Congruences.BuchiCongruence
+public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage

Cslib/Computability/Automata/DA/Congr.lean

@@ -0,0 +1,67 @@
+/-
+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.Computability.Automata.DA.Basic
+public import Cslib.Computability.Languages.Congruences.RightCongruence
+
+@[expose] public section
+
+/-! # Deterministic automaton corresponding to a right congruence. -/
+
+namespace Cslib
+
+open scoped FLTS RightCongruence
+
+variable {Symbol : Type*}
+
+/-- Every right congruence gives rise to a DA whose states are the equivalence classes of
+the right congruence, whose start state is the empty word, and whose transition functiuon
+is concatenation on the right of the input symbol. Note that the transition function is
+well-defined only because `c` is a right congruence. -/
+@[scoped grind =]
+def RightCongruence.toDA [c : RightCongruence Symbol] : Automata.DA (Quotient c.eq) Symbol where
+  tr s x := Quotient.lift (fun u ↦ ⟦ u ++ [x] ⟧) (by
+    intro u v h_eq
+    apply Quotient.sound
+    exact right_cov.elim [x] h_eq
+  ) s
+  start := ⟦ [] ⟧
+
+namespace Automata.DA
+
+variable [c : RightCongruence Symbol]
+
+/-- After consuming a finite word `xs`, `c.toDA` reaches the state `⟦ xs ⟧` which is
+the equivalence class of `xs`. -/
+@[simp, scoped grind =]
+theorem congr_mtr_eq {xs : List Symbol} :
+    c.toDA.mtr c.toDA.start xs = ⟦ xs ⟧ := by
+  generalize h_rev : xs.reverse = ys
+  induction ys generalizing xs
+  case nil => grind [List.reverse_eq_nil_iff]
+  case cons y ys h_ind =>
+    obtain ⟨rfl⟩ := List.reverse_eq_cons_iff.mp h_rev
+    specialize h_ind (xs := ys.reverse) (by grind)
+    grind [Quotient.lift_mk]
+
+namespace FinAcc
+
+open Acceptor RightCongruence
+
+/-- The language of `c.toDA` with a single accepting state `s` is exactly
+the equivalence class corresponding to `s`. -/
+@[simp]
+theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a}) = eqvCls a := by
+  ext
+  grind
+
+end FinAcc
+
+end Automata.DA
+
+end Cslib

Cslib/Computability/Automata/NA/Pair.lean

@@ -37,6 +37,67 @@ theorem LTS.pairLang_regular [Finite State] {lts : LTS State Symbol} {s t : Stat
   ext
   simp
 
+/-- `LTS.pairViaLang via s t` is the language of finite words that can take the LTS
+from state `s` to state `t` via a state in `via`. -/
+def LTS.pairViaLang (lts : LTS State Symbol) (via : Set State) (s t : State) : Language Symbol :=
+  ⨆ r ∈ via, lts.pairLang s r * lts.pairLang r t
+
+@[simp, scoped grind =]
+theorem LTS.mem_pairViaLang {lts : LTS State Symbol} {via : Set State}
+    {s t : State} {xs : List Symbol} : xs ∈ lts.pairViaLang via s t ↔
+      ∃ r ∈ via, ∃ xs1 xs2, lts.MTr s xs1 r ∧ lts.MTr r xs2 t ∧ xs1 ++ xs2 = xs := by
+  simp [LTS.pairViaLang, Language.mem_mul]
+
+/-- `LTS.pairViaLang via s t` is a regular language if there are only finitely many states. -/
+@[simp]
+theorem LTS.pairViaLang_regular [Inhabited Symbol] [Finite State] {lts : LTS State Symbol}
+    {via : Set State} {s t : State} : (lts.pairViaLang via s t).IsRegular := by
+  apply IsRegular.iSup
+  grind [Language.IsRegular.mul, LTS.pairLang_regular]
+
+theorem LTS.pairLang_append {lts : LTS State Symbol} {s0 s1 s2 : State} {xs1 xs2 : List Symbol}
+    (h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) :
+    xs1 ++ xs2 ∈ lts.pairLang s0 s2 := by
+  grind [<= LTS.MTr.comp]
+
+theorem LTS.pairLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol}
+    (h : xs1 ++ xs2 ∈ lts.pairLang s0 s2) :
+    ∃ s1, xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2 := by
+  obtain ⟨r, _, _⟩ := LTS.MTr.split <| LTS.mem_pairLang.mp h
+  use r
+  grind
+
+theorem LTS.pairViaLang_append_pairLang {lts : LTS State Symbol}
+    {s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State}
+    (h1 : xs1 ∈ lts.pairViaLang via s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) :
+    xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2 := by
+  obtain ⟨r, _, _, _, _, _, rfl⟩ := LTS.mem_pairViaLang.mp h1
+  apply LTS.mem_pairViaLang.mpr
+  use r
+  grind [<= LTS.MTr.comp]
+
+theorem LTS.pairLang_append_pairViaLang {lts : LTS State Symbol}
+    {s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State}
+    (h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairViaLang via s1 s2) :
+    xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2 := by
+  obtain ⟨r, _, _, _, _, _, rfl⟩ := LTS.mem_pairViaLang.mp h2
+  apply LTS.mem_pairViaLang.mpr
+  use r
+  grind [<= LTS.MTr.comp]
+
+theorem LTS.pairViaLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol}
+    {via : Set State} (h : xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2) :
+    ∃ s1, xs1 ∈ lts.pairViaLang via s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2 ∨
+          xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairViaLang via s1 s2 := by
+  obtain ⟨r, h_r, ys1, ys2, h_ys1, h_ys2, h_eq⟩ := LTS.mem_pairViaLang.mp h
+  obtain ⟨zs1, rfl, rfl⟩ | ⟨zs2, rfl, rfl⟩ := List.append_eq_append_iff.mp h_eq
+  · obtain ⟨s1, _, _⟩ := LTS.MTr.split h_ys2
+    use s1
+    grind
+  · obtain ⟨s1, _, _⟩ := LTS.MTr.split h_ys1
+    use s1
+    grind
+
 namespace Automata.NA.Buchi
 
 open Set Filter ωSequence ωLanguage ωAcceptor

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -0,0 +1,75 @@
+/-
+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.Computability.Automata.NA.Pair
+public import Cslib.Computability.Languages.Congruences.RightCongruence
+
+@[expose] public section
+
+/-!
+# Buchi Congruence
+
+A special type of right congruences used by J.R. Büchi to prove the closure
+of ω-regular languages under complementation.
+-/
+
+namespace Cslib.Automata.NA.Buchi
+
+open Function
+
+variable {Symbol : Type*} {State : Type}
+
+/-- Given a Buchi automaton `na`, two finite words `u` and `v` are Buchi-congruent
+according to `na` iff for every pair of states `s` and `t` of `na`, both of the
+following two conditions hold:
+(1) `u` can move `na` from `s` to `t` iff `v` can move `na` from `s` to `t`;
+(2) `u` can move `na` from `s` to `t` via an acceptingg states iff `v` can move `na`
+from `s` to `t` via an acceptingg states. -/
+def BuchiCongruence (na : Buchi State Symbol) : RightCongruence Symbol where
+  eq.r u v :=
+    ∀ {s t}, (u ∈ na.pairLang s t ↔ v ∈ na.pairLang s t) ∧
+      (u ∈ na.pairViaLang na.accept s t ↔ v ∈ na.pairViaLang na.accept s t)
+  eq.iseqv.refl := by grind
+  eq.iseqv.symm := by grind
+  eq.iseqv.trans := by grind
+  right_cov.elim := by
+    grind [Covariant, → LTS.pairLang_split, <= LTS.pairLang_append, → LTS.pairViaLang_split,
+      <= LTS.pairViaLang_append_pairLang, <= LTS.pairLang_append_pairViaLang]
+
+open scoped Classical in
+/-- `BuchiCongrParam` is a parameterization of the equivalence classes of `na.BuchiCongruence`
+using the type `State → State → Prop × Prop`, which is finite if `State` is. -/
+noncomputable def BuchiCongrParam (na : Buchi State Symbol)
+    (f : State → State → Prop × Prop) : Quotient na.BuchiCongruence.eq :=
+  if h : ∃ u, ∀ s t, ((f s t).1 ↔ u ∈ na.pairLang s t) ∧
+      ((f s t).2 ↔ u ∈ na.pairViaLang na.accept s t)
+  then ⟦ Classical.choose h ⟧
+  else ⟦ [] ⟧
+
+variable {na : Buchi State Symbol}
+
+/-- `BuchiCongrParam` is surjective. -/
+lemma buchiCongrParam_surjective : Surjective na.BuchiCongrParam := by
+  intro q
+  let f s t := (q.out ∈ na.pairLang s t, q.out ∈ na.pairViaLang na.accept s t)
+  have h : ∃ u, ∀ s t, ((f s t).1 ↔ u ∈ na.pairLang s t) ∧
+        ((f s t).2 ↔ u ∈ na.pairViaLang na.accept s t) := by
+    use q.out
+    grind
+  use f
+  simp only [BuchiCongrParam, h, ↓reduceDIte]
+  rw [← Quotient.out_eq q]
+  apply Quotient.sound
+  intro s t
+  grind
+
+/-- `na.BuchiCongruence` is of finite index if `na` has only finitely many states. -/
+theorem buchiCongruence_fin_index [Finite State] : Finite (Quotient na.BuchiCongruence.eq) :=
+  Finite.of_surjective na.BuchiCongrParam buchiCongrParam_surjective
+
+end Cslib.Automata.NA.Buchi

Cslib/Computability/Languages/Congruences/RightCongruence.lean

@@ -0,0 +1,41 @@
+/-
+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.Computability.Language
+
+@[expose] public section
+
+/-!
+# Right Congruence
+
+This file contains basic definitions about right congruences on finite sequences.
+
+NOTE: Left congruences and two-sided congruences can be similarly defined.
+But they are left to future work because they are not needed for now.
+-/
+
+namespace Cslib
+
+/-- A right congruence is an equivalence relation on finite sequences (represented by lists)
+that is preserved by concatenation on the right.  The equivalence relation is represented
+by a setoid to to enable ready access to the quotient construction. -/
+class RightCongruence (α : Type*) extends eq : Setoid (List α) where
+  right_cov : CovariantClass _ _ (fun x y => y ++ x) eq
+
+namespace RightCongruence
+
+variable {α : Type*}
+
+/-- The equivalence class (as a language) corresponding to an element of the quotient type. -/
+abbrev eqvCls [c : RightCongruence α] (a : Quotient c.eq) : Language α :=
+  (Quotient.mk c.eq) ⁻¹' {a}
+
+end RightCongruence
+
+end Cslib

Cslib/Computability/Languages/RegularLanguage.lean

@@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou
 
 module
 
+public import Cslib.Computability.Automata.DA.Congr
 public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.NA.Concat
@@ -24,7 +25,7 @@ public import Mathlib.Tactic.Common
 
 namespace Cslib.Language
 
-open Set List Prod Automata Acceptor
+open Set List Prod Automata Acceptor RightCongruence
 open scoped Computability FLTS DA NA DA.FinAcc NA.FinAcc
 
 variable {Symbol : Type*}
@@ -159,4 +160,13 @@ theorem IsRegular.kstar [Inhabited Symbol] {l : Language Symbol}
     obtain ⟨State, h_fin, nfa, rfl⟩ := h
     use Unit ⊕ (State ⊕ Unit), inferInstance, ⟨finLoop nfa, {inl ()}⟩, loop_language_eq h_l
 
+/-- If a right congruence is of finite index, then each of its equivalence classes is regular. -/
+@[simp]
+theorem IsRegular.congr_fin_index {Symbol : Type}
+    [c : RightCongruence Symbol] [Finite (Quotient c.eq)]
+    (a : Quotient c.eq) : (eqvCls a).IsRegular := by
+  rw [IsRegular.iff_dfa]
+  use Quotient c.eq, inferInstance, ⟨c.toDA, {a}⟩
+  exact DA.FinAcc.congr_language_eq
+
 end Cslib.Language

Cslib/Foundations/Semantics/FLTS/Basic.lean

@@ -45,9 +45,14 @@ from the left (instead of the right), in order to match the way lists are constr
 @[scoped grind =]
 def mtr (flts : FLTS State Label) (s : State) (μs : List Label) := μs.foldl flts.tr s
 
-@[scoped grind =]
+@[simp, scoped grind =]
 theorem mtr_nil_eq {flts : FLTS State Label} {s : State} : flts.mtr s [] = s := rfl
 
+@[simp, scoped grind =]
+theorem mtr_concat_eq {flts : FLTS State Label} {s : State} {μs : List Label} {μ : Label} :
+    flts.mtr s (μs ++ [μ]) = flts.tr (flts.mtr s μs) μ := by
+  grind
+
 end FLTS
 
 end Cslib