feat: prove basic properties of deterministic Buchi automata

Cslib.lean

@@ -1,5 +1,6 @@
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.DABuchi
 import Cslib.Computability.Automata.DAToNA
 import Cslib.Computability.Automata.EpsilonNA
 import Cslib.Computability.Automata.EpsilonNAToNA

Cslib/Computability/Automata/DA.lean

@@ -24,6 +24,9 @@ finiteness assumptions), deterministic Buchi automata, and deterministic Muller
   *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
+open List Filter Cslib.ωSequence
+open scoped Cslib.FLTS
+
 namespace Cslib.Automata
 
 structure DA (State Symbol : Type*) extends FLTS State Symbol where
@@ -34,6 +37,33 @@ namespace DA
 
 variable {State : Type _} {Symbol : Type _}
 
+/-- Helper function for defining `run` below. -/
+@[scoped grind =]
+def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
+  | 0 => da.start
+  | n + 1 => da.tr (run' da xs n) (xs n)
+
+/-- Infinite run. -/
+@[scoped grind =]
+def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
+
+@[simp, scoped grind =]
+theorem run_zero {da : DA State Symbol} {xs : ωSequence Symbol} :
+    da.run xs 0 = da.start :=
+  rfl
+
+@[simp, scoped grind =]
+theorem run_succ {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
+    da.run xs (n + 1) = da.tr (da.run xs n) (xs n) := by
+  rfl
+
+@[simp, scoped grind =]
+theorem mtr_extract_eq_run {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
+    da.mtr da.start (xs.extract 0 n) = da.run xs n := by
+  induction n
+  case zero => rfl
+  case succ n h_ind => grind [extract_succ_right]
+
 /-- A deterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends DA State Symbol where
   /-- The accept states. -/
@@ -49,19 +79,13 @@ This is the standard string recognition performed by DFAs in the literature. -/
 instance : Acceptor (DA.FinAcc State Symbol) Symbol where
   Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) := a.mtr a.start xs ∈ a.accept
 
-end FinAcc
-
-/-- Helper function for defining `run` below. -/
+open Acceptor in
 @[simp, scoped grind =]
-def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
-  | 0 => da.start
-  | n + 1 => da.tr (run' da xs n) (xs n)
-
-/-- Infinite run. -/
-@[scoped grind =]
-def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
+theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} :
+    xs ∈ language a ↔ a.mtr a.start xs ∈ a.accept :=
+  Iff.rfl
 
-open List Filter
+end FinAcc
 
 /-- Deterministic Buchi automaton. -/
 structure Buchi (State Symbol : Type*) extends DA State Symbol where
@@ -74,6 +98,12 @@ namespace Buchi
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := ∃ᶠ k in atTop, a.run xs k ∈ a.accept
 
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Buchi State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ ∃ᶠ k in atTop, a.run xs k ∈ a.accept :=
+  Iff.rfl
+
 end Buchi
 
 /-- Deterministic Muller automaton. -/
@@ -87,6 +117,12 @@ namespace Muller
 instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := (a.run xs).infOcc ∈ a.accept
 
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Muller State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ (a.run xs).infOcc ∈ a.accept :=
+  Iff.rfl
+
 end Muller
 
 end DA

Cslib/Computability/Automata/DABuchi.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.DA
+import Cslib.Computability.Automata.NA
+
+/-! # Deterministic Buchi automata.
+-/
+
+open Filter
+
+namespace Cslib.Automata.DA
+
+open scoped FinAcc Buchi
+
+variable {State : Type _} {Symbol : Type _}
+
+open Acceptor ωAcceptor in
+/-- The ω-language accepted by a deterministic Buchi automaton is the ω-limit
+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 ; constructor <;>
+  { intro h ; apply Frequently.mono h ; simp }
+
+end Cslib.Automata.DA

Cslib/Computability/Automata/DAToNA.lean

@@ -26,6 +26,16 @@ 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
+@[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
+  · grind
+
 namespace FinAcc
 
 /-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/
@@ -35,8 +45,8 @@ def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol :=
 
 open Acceptor in
 open scoped FLTS NA.FinAcc in
-/-- The `NA` constructed from a `DA` has the same language. -/
-@[scoped grind _=_]
+/-- The `NA.FinAcc` constructed from a `DA.FinAcc` has the same language. -/
+@[simp, scoped grind _=_]
 theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
     language a.toNAFinAcc = language a := by
   ext xs
@@ -48,6 +58,27 @@ theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
 
 end FinAcc
 
+namespace Buchi
+
+/-- `DA.Buchi` is a special case of `NA.Buchi`. -/
+@[scoped grind =]
+def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol :=
+  { a.toNA with accept := a.accept }
+
+open ωAcceptor in
+open scoped NA.Buchi in
+/-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/
+@[simp, scoped grind _=_]
+theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} :
+    language a.toNABuchi = language a := by
+  ext xs ; constructor
+  · grind
+  · intro _
+    use (a.run xs)
+    grind
+
+end Buchi
+
 end NA
 
 end Cslib.Automata.DA

Cslib/Computability/Automata/NA.lean

@@ -40,6 +40,11 @@ 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))
+
 /-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends NA State Symbol where
   /-- The accept states. -/
@@ -56,12 +61,13 @@ instance : Acceptor (FinAcc State Symbol) Symbol where
   Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
     ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s'
 
-end FinAcc
+open Acceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} :
+    xs ∈ language a ↔ ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s' :=
+  Iff.rfl
 
-/-- 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))
+end FinAcc
 
 /-- Nondeterministic Buchi automaton. -/
 structure Buchi (State Symbol : Type*) extends NA State Symbol where
@@ -72,7 +78,13 @@ namespace Buchi
 @[scoped grind =]
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
-    ∃ ss, ∃ᶠ k in atTop, a.Run xs ss ∧ ss k ∈ a.accept
+    ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept
+
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Buchi State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept :=
+  Iff.rfl
 
 end Buchi
 
@@ -87,6 +99,12 @@ instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
     ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept
 
+open ωAcceptor in
+@[simp, scoped grind =]
+theorem mem_language {a : Muller State Symbol} {xs : ωSequence Symbol} :
+    xs ∈ language a ↔ ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept :=
+  Iff.rfl
+
 end Muller
 
 end NA

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -6,6 +6,9 @@ Authors: Ching-Tsun Chou
 
 import Cslib.Computability.Automata.DA
 import Cslib.Computability.Automata.NA
+import Cslib.Computability.Automata.DAToNA
+import Cslib.Computability.Automata.DABuchi
+import Cslib.Computability.Languages.RegularLanguage
 import Mathlib.Tactic
 
 /-!
@@ -14,26 +17,40 @@ import Mathlib.Tactic
 This file defines ω-regular languages and proves some properties of them.
 -/
 
-open Set Function
+open Set Function Cslib.Automata.ωAcceptor
 open scoped Computability
 open Cslib.Automata
 
 namespace Cslib.ωLanguage
 
 variable {Symbol : Type*}
 
-/-- An ω-regular language is one that is accepted by a finite-state Buchi automaton. -/
+/-- 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, ωAcceptor.language na = p
-
-/-- There is an ω-regular language which is not accepted by any deterministic Buchi automaton. -/
-proof_wanted IsRegular.not_det_buchi :
+  ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, language na = p
+
+/-- 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) :
+    (language da).IsRegular := by
+  use State, inferInstance, da.toNABuchi
+  simp
+
+/-- The ω-limit of a regular language is ω-regular. -/
+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
+  rw [← DA.buchi_eq_finAcc_omegaLim]
+  apply IsRegular.of_da_buchi
+
+/-- There is an ω-regular language that is not accepted by any deterministic Buchi automaton. -/
+proof_wanted IsRegular.not_da_buchi :
   ∃ p : ωLanguage Symbol, p.IsRegular ∧
-    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, ωAcceptor.language da = p
+    ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, language da = p
 
 /-- McNaughton's Theorem. -/
-proof_wanted IsRegular.iff_muller_lang {p : ωLanguage Symbol} :
+proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} :
     p.IsRegular ↔
-    ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, ωAcceptor.language da = p
+    ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, language da = p
 
 end Cslib.ωLanguage