feat: prove the existence of an omega-regular language not accepted by any deterministic Buchi automaton

Cslib.lean

@@ -1,12 +1,14 @@
 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
 import Cslib.Computability.Automata.NA
 import Cslib.Computability.Automata.NAToDA
 import Cslib.Computability.Automata.OmegaAcceptor
 import Cslib.Computability.Automata.Prod
+import Cslib.Computability.Languages.ExampleEventuallyZero
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
 import Cslib.Computability.Languages.OmegaRegularLanguage
@@ -19,6 +21,7 @@ import Cslib.Foundations.Data.HasFresh
 import Cslib.Foundations.Data.Nat.Segment
 import Cslib.Foundations.Data.OmegaSequence.Defs
 import Cslib.Foundations.Data.OmegaSequence.Flatten
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
 import Cslib.Foundations.Data.OmegaSequence.Init
 import Cslib.Foundations.Data.Relation
 import Cslib.Foundations.Lint.Basic

Cslib/Computability/Automata/DA.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Foundations.Semantics.LTS.FLTS
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.OmegaAcceptor
-import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
+import Cslib.Foundations.Semantics.LTS.FLTS
 
 /-! # Deterministic Automata
 
@@ -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)
+theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} :
+    xs ∈ language a ↔ a.mtr a.start xs ∈ a.accept :=
+  Iff.rfl
 
-/-- Infinite run. -/
-@[scoped grind =]
-def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
-
-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,30 @@
+/-
+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
+
+/-! # 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
+  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

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
-import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Foundations.Data.OmegaSequence.InfOcc
 import Cslib.Foundations.Semantics.LTS.Basic
-import Cslib.Foundations.Semantics.LTS.FLTS
 import Cslib.Computability.Automata.Acceptor
 import Cslib.Computability.Automata.OmegaAcceptor
 
@@ -40,6 +39,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 +60,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 +77,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 +98,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