feat: add Cslib/Computability/Languages/RegularLanguage.lean and associated changes

Cslib.lean

@@ -8,6 +8,7 @@ import Cslib.Computability.Automata.NFA
 import Cslib.Computability.Automata.NFAToDFA
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Foundations.Control.Monad.Free
 import Cslib.Foundations.Control.Monad.Free.Effects
 import Cslib.Foundations.Control.Monad.Free.Fold

Cslib/Computability/Automata/DA.lean

@@ -6,19 +6,48 @@ Authors: Fabrizio Montesi
 
 import Cslib.Computability.Automata.NA
 
-
-
 /-! # Deterministic Automaton
 
 A Deterministic Automaton (DA) is an automaton defined by a transition function.
+
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
 namespace Cslib
 
-structure DA (State : Type _) (Symbol : Type _) where
+open List
+
+structure DA (State : Type*) (Symbol : Type*) where
   /-- The initial state of the automaton. -/
   start : State
   /-- The transition function of the automaton. -/
   tr : State → Symbol → State
 
+namespace DA
+
+variable {State State1 State2 : Type*} {Symbol : Type*}
+
+/-- Extended transition function. -/
+@[scoped grind =]
+def mtr (DA : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl DA.tr s
+
+@[simp, scoped grind =]
+theorem mtr_nil_eq {DA : DA State Symbol} {s : State} : DA.mtr s [] = s := rfl
+
+@[scoped grind =]
+def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
+  start := (da1.start, da2.start)
+  tr := fun (s1, s2) x ↦ (da1.tr s1 x, da2.tr s2 x)
+
+@[simp, scoped grind =]
+theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
+    (s : State1 × State2) (xs : List Symbol) :
+    (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) := by
+  induction xs generalizing s <;> grind
+
+end DA
+
 end Cslib

Cslib/Computability/Automata/DFA.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
+Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.DA
@@ -11,19 +11,17 @@ import Cslib.Computability.Languages.Language
 
 A Deterministic Finite Automaton (DFA) is a finite-state machine that accepts or rejects
 a finite string.
-
-## References
-
-* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
-  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
 namespace Cslib
 
+open List Prod
+open scoped DA Language
+
 /-- A Deterministic Finite Automaton (DFA) consists of a labelled transition function
 `tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
 set of accepting states `accept`. -/
-structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
+structure DFA (State : Type*) (Symbol : Type*) extends DA State Symbol where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -33,18 +31,7 @@ structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
 
 namespace DFA
 
-variable {State : Type _} {Symbol : Type _}
-
-/-- Extended transition function.
-
-Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
-from the left (instead of the right), in order to match the way lists are constructed.
--/
-@[scoped grind =]
-def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s
-
-@[scoped grind =]
-theorem mtr_nil_eq {dfa : DFA State Symbol} {s : State} : dfa.mtr s [] = s := rfl
+variable {State State1 State2 : Type*} {Symbol : Type*}
 
 /-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
 the start state. -/
@@ -62,6 +49,71 @@ def language (dfa : DFA State Symbol) : Language Symbol :=
 theorem mem_language (dfa : DFA State Symbol) (xs : List Symbol) :
   xs ∈ dfa.language ↔ dfa.Accepts xs := Iff.rfl
 
+@[scoped grind =]
+def zero [Finite Symbol] : DFA Unit Symbol where
+  start := ()
+  tr := fun _ _ ↦ ()
+  accept := ∅
+  finite_state := by infer_instance
+  finite_symbol := by infer_instance
+
+@[simp, scoped grind =]
+theorem zero_lang [Finite Symbol] : zero.language = (0 : Language Symbol) := by
+  grind
+
+@[scoped grind =]
+def one [Finite Symbol] : DFA (Fin 2) Symbol where
+  start := 0
+  tr := fun _ _ ↦ 1
+  accept := {0}
+  finite_state := by infer_instance
+  finite_symbol := by infer_instance
+
+@[simp, scoped grind =]
+theorem one_lang [Finite Symbol] : one.language = (1 : Language Symbol) := by
+  ext xs ; constructor
+  · intro h ; by_contra h'
+    have := dropLast_append_getLast h'
+    grind
+  · grind [Language.mem_one]
+
+@[scoped grind =]
+def compl (dfa : DFA State Symbol) : DFA State Symbol :=
+  { dfa with accept := dfa.acceptᶜ }
+
+@[simp, scoped grind =]
+theorem compl_lang (dfa : DFA State Symbol) : dfa.compl.language = (dfa.language)ᶜ := by
+  grind
+
+@[scoped grind =]
+def prod (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) (acc : Set (State1 × State2))
+  : DFA (State1 × State2) Symbol where
+  toDA := DA.prod dfa1.toDA dfa2.toDA
+  accept := acc
+  finite_state := by
+    have := dfa1.finite_state
+    have := dfa2.finite_state
+    infer_instance
+  finite_symbol := dfa1.finite_symbol
+
+@[scoped grind =]
+def inf (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :=
+    dfa1.prod dfa2 (fst ⁻¹' dfa1.accept ∩ snd ⁻¹' dfa2.accept)
+
+@[scoped grind =]
+def add (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :=
+    dfa1.prod dfa2 (fst ⁻¹' dfa1.accept ∪ snd ⁻¹' dfa2.accept)
+
+@[simp, scoped grind =]
+theorem inf_lang (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :
+    (dfa1.inf dfa2).language = dfa1.language ⊓ dfa2.language := by
+  ext xs ; grind
+
+@[simp, scoped grind =]
+theorem add_lang (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :
+    (dfa1.add dfa2).language = dfa1.language + dfa2.language := by
+  ext xs ; grind [Language.mem_add]
+
 end DFA
 
 end Cslib

Cslib/Computability/Automata/DFAToNFA.lean

@@ -11,9 +11,11 @@ import Cslib.Computability.Automata.NFA
 
 namespace Cslib
 
+open scoped DA
+
 namespace DFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section NFA
 

Cslib/Computability/Automata/EpsilonNFA.lean

@@ -17,15 +17,15 @@ symbol type. The special symbol ε is represented by the `Option.none` case.
 Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
 allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
 ε-closure. -/
-structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) where
+structure εNFA (State : Type*) (Symbol : Type*) extends NA State (Option Symbol) where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
   finite_state : Finite State
   /-- The type of symbols (also called 'alphabet') is finite. -/
   finite_symbol : Finite Symbol
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 @[local grind =]
 private instance : HasTau (Option α) := ⟨.none⟩

Cslib/Computability/Automata/EpsilonNFAToNFA.lean

@@ -27,7 +27,7 @@ private lemma LTS.noε_saturate_tr
 
 namespace εNFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section NFA
 
@@ -41,7 +41,7 @@ def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
   finite_symbol := enfa.finite_symbol
 
 @[scoped grind =]
-lemma LTS.noε_saturate_mTr {s : State} {Label : Type _} {μs : List Label}
+lemma LTS.noε_saturate_mTr {s : State} {Label : Type*} {μs : List Label}
   {lts : LTS State (Option Label)} :
   lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
   ext s'

Cslib/Computability/Automata/NA.lean

@@ -17,7 +17,7 @@ type `State → Symbol → Set State`; it gets automatically expanded to the for
 
 namespace Cslib
 
-structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
+structure NA (State : Type*) (Symbol : Type*) extends LTS State Symbol where
   /-- The set of initial states of the automaton. -/
   start : Set State
 

Cslib/Computability/Automata/NFA.lean

@@ -11,7 +11,7 @@ namespace Cslib
 
 /-- A Nondeterministic Finite Automaton (NFA) is a nondeterministic automaton (NA)
 over finite sets of states and symbols. -/
-structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
+structure NFA (State : Type*) (Symbol : Type*) extends NA State Symbol where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -21,7 +21,7 @@ structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
 
 namespace NFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 /-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
 the start state. -/

Cslib/Computability/Automata/NFAToDFA.lean

@@ -13,7 +13,7 @@ namespace Cslib
 
 namespace NFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section SubsetConstruction
 
@@ -41,7 +41,7 @@ original NA. -/
 @[scoped grind =]
 theorem toDFA_mem_mtr {nfa : NFA State Symbol} {S : Set State} {s' : State} {xs : List Symbol} :
   s' ∈ nfa.toDFA.mtr S xs ↔ ∃ s ∈ S, nfa.MTr s xs s' := by
-  simp only [NFA.toDFA, DFA.mtr]
+  simp only [NFA.toDFA, DA.mtr]
   /- TODO: Grind does not catch a useful rewrite in the subset construction for automata
 
     A very similar issue seems to occur in the proof of `NFA.toDFA_language_eq`.

Cslib/Computability/Languages/Language.lean

@@ -20,7 +20,25 @@ namespace Language
 open Set List
 open scoped Computability
 
-variable {α : Type _} {l : Language α}
+variable {α : Type*} {l m : Language α}
+
+@[simp, scoped grind =]
+theorem mem_inf (x : List α) : x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m :=
+  Iff.rfl
+
+@[simp]
+theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
+    (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i :=
+  mem_iInter₂
+
+@[simp]
+theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
+    (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i := by
+  constructor <;> intro h
+  · have := mem_iUnion₂.mp h
+    grind
+  · apply mem_iUnion₂.mpr
+    grind
 
 -- This section will be removed once the following PR gets into mathlib:
 -- https://github.com/leanprover-community/mathlib4/pull/30913

Cslib/Computability/Languages/OmegaLanguage.lean

@@ -59,7 +59,7 @@ open scoped Computability
 
 universe v
 
-variable {α β γ : Type _}
+variable {α β γ : Type*}
 
 /-- An ω-language is a set of strings over an alphabet. -/
 def ωLanguage (α) :=