feat (Computability/Automata): Automata theory based on LTS, including DFA, NFA, EpsilonNFA, and translations between them, plus supporting theorems generalised to LTS

Cslib.lean

@@ -1,6 +1,6 @@
-import Cslib.Foundations.Semantics.Lts.Basic
-import Cslib.Foundations.Semantics.Lts.Bisimulation
-import Cslib.Foundations.Semantics.Lts.TraceEq
+import Cslib.Foundations.Semantics.LTS.Basic
+import Cslib.Foundations.Semantics.LTS.Bisimulation
+import Cslib.Foundations.Semantics.LTS.TraceEq
 import Cslib.Foundations.Data.Relation
 import Cslib.Languages.CombinatoryLogic.Defs
 import Cslib.Languages.CombinatoryLogic.Basic

Cslib/Computability/Automata/DA.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-! # Deterministic Automaton
+
+A Deterministic Automaton (DA) is an automaton defined by a transition function.
+-/
+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

Cslib/Computability/Automata/DFA.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DA
+
+set_option linter.style.longLine false in
+/-! # Deterministic Finite-State Automata
+
+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]
+-/
+
+/-- 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
+  /-- 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
+
+
+namespace DFA
+
+/-- 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} : dfa.mtr s [] = s := by rfl
+
+/-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
+the start state. -/
+@[scoped grind →]
+def Accepts (dfa : DFA State Symbol) (xs : List Symbol) :=
+  dfa.mtr dfa.start xs ∈ dfa.accept
+
+/-- The language of a DFA is the set of strings that it accepts. -/
+@[scoped grind =]
+def language (dfa : DFA State Symbol) : Set (List Symbol) :=
+  { xs | dfa.Accepts xs }
+
+/-- A string is accepted by a DFA iff it is in the language of the DFA. -/
+@[scoped grind _=_]
+theorem accepts_mem_language (dfa : DFA State Symbol) (xs : List Symbol) :
+  dfa.Accepts xs ↔ xs ∈ dfa.language := by rfl
+
+end DFA

Cslib/Computability/Automata/DFAToNFA.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DFA
+import Cslib.Computability.Automata.NFA
+
+/-! # Translation of DFA into NFA -/
+
+namespace DFA
+section NFA
+
+/-- `DFA` is a special case of `NFA`. -/
+@[scoped grind =]
+def toNFA (dfa : DFA State Symbol) : NFA State Symbol where
+  start := {dfa.start}
+  accept := dfa.accept
+  Tr := fun s1 μ s2 => dfa.tr s1 μ = s2
+  finite_state := dfa.finite_state
+  finite_symbol := dfa.finite_symbol
+
+@[scoped grind =]
+lemma toNFA_start {dfa : DFA State Symbol} : dfa.toNFA.start = {dfa.start} := rfl
+
+instance : Coe (DFA State Symbol) (NFA State Symbol) where
+  coe := toNFA
+
+/-- `DA.toNA` correctly characterises transitions. -/
+@[scoped grind =]
+theorem toNA_tr {dfa : DFA State Symbol} :
+  dfa.toNFA.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by
+  rfl
+
+/-- The transition system of a DA is deterministic. -/
+@[scoped grind ⇒]
+theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by
+  grind
+
+/-- The transition system of a DA is image-finite. -/
+@[scoped grind ⇒]
+theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite :=
+  dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic
+
+/-- Characterisation of multistep transitions. -/
+@[scoped grind =]
+theorem toNFA_mtr {dfa : DFA State Symbol} :
+  dfa.toNFA.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by
+  have : ∀ x, dfa.toNFA.Tr s1 x (dfa.tr s1 x) := by grind
+  constructor <;> intro h
+  case mp => induction h <;> grind
+  case mpr => induction xs generalizing s1 <;> grind
+
+/-- The `NFA` constructed from a `DFA` has the same language. -/
+@[scoped grind =]
+theorem toNFA_language_eq {dfa : DFA State Symbol} :
+  dfa.toNFA.language = dfa.language := by
+  ext xs
+  refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> open NFA in grind
+
+end NFA
+end DFA

Cslib/Computability/Automata/EpsilonNFA.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-! # Nondeterministic automata with ε-transitions. -/
+
+/-- A nondeterministic finite automaton with ε-transitions (`εNFA`) is an `NA` with an `Option`
+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
+  /-- 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
+
+@[local grind =]
+private instance : HasTau (Option α) := ⟨.none⟩
+
+/-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S`
+by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance
+of `HasTau.τ`. -/
+abbrev εNFA.εClosure (enfa : εNFA State Symbol) (S : Set State) := enfa.τClosure S
+
+namespace εNFA
+
+/-- An εNFA accepts a string if there is a saturated multistep accepting derivative with that trace
+from the start state. -/
+@[scoped grind]
+def Accepts (enfa : εNFA State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ enfa.εClosure enfa.start, ∃ s' ∈ enfa.accept,
+  enfa.saturate.MTr s (xs.map (some ·)) s'
+
+/-- The language of an εDA is the set of strings that it accepts. -/
+@[scoped grind =]
+def language (enfa : εNFA State Symbol) : Set (List Symbol) :=
+  { xs | enfa.Accepts xs }
+
+/-- A string is accepted by an εNFA iff it is in the language of the NA. -/
+@[scoped grind =]
+theorem accepts_mem_language (enfa : εNFA State Symbol) (xs : List Symbol) :
+  enfa.Accepts xs ↔ xs ∈ enfa.language := by rfl
+
+end εNFA

Cslib/Computability/Automata/EpsilonNFAToNFA.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.EpsilonNFA
+import Cslib.Computability.Automata.NFA
+
+/-! # Translation of εNFA into NFA -/
+
+/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
+ε-transitions. -/
+@[grind]
+private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
+  Tr := fun s μ s' => lts.Tr s (some μ) s'
+
+@[local grind]
+private lemma LTS.noε_saturate_tr
+  {lts : LTS State (Option Label)} {h : μ = some μ'} :
+  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
+  simp only [LTS.noε]
+  grind
+
+namespace εNFA
+section NFA
+
+/-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/
+@[scoped grind]
+def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
+  start := enfa.εClosure enfa.start
+  accept := enfa.accept
+  Tr := enfa.saturate.noε.Tr
+  finite_state := enfa.finite_state
+  finite_symbol := enfa.finite_symbol
+
+@[scoped grind]
+lemma LTS.noε_saturate_mTr
+  {lts : LTS State (Option Label)} :
+  lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
+  ext s'
+  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
+
+
+/-- Correctness of `toNFA`. -/
+@[scoped grind]
+theorem toNFA_language_eq {enfa : εNFA State Symbol} :
+  enfa.toNFA.language = enfa.language := by
+  ext xs
+  have : ∀ s s', enfa.saturate.MTr s (xs.map (some ·)) s' = enfa.saturate.noε.MTr s xs s' := by
+    simp [LTS.noε_saturate_mTr]
+  open NFA in grind
+
+end NFA
+end εNFA

Cslib/Computability/Automata/NA.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Foundations.Semantics.LTS.Basic
+
+/-! # Nondeterministic Automaton
+
+A Nondeterministic Automaton (NA) is an automaton with a set of initial states.
+
+This definition extends `LTS` and thus stores the transition system as a relation `Tr` of the form
+`State → Symbol → State → Prop`. Note that you can also instantiate `Tr` by passing an argument of
+type `State → Symbol → Set State`; it gets automatically expanded to the former shape.
+-/
+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

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.NA
+
+/-- 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
+  /-- 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
+
+namespace NFA
+
+/-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
+the start state. -/
+@[scoped grind]
+def Accepts (nfa : NFA State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ nfa.start, ∃ s' ∈ nfa.accept, nfa.MTr s xs s'
+
+/-- The language of an NFA is the set of strings that it accepts. -/
+@[scoped grind]
+def language (nfa : NFA State Symbol) : Set (List Symbol) :=
+  { xs | nfa.Accepts xs }
+
+/-- A string is accepted by an NFA iff it is in the language of the NFA. -/
+@[scoped grind]
+theorem accepts_mem_language (nfa : NFA State Symbol) (xs : List Symbol) :
+  nfa.Accepts xs ↔ xs ∈ nfa.language := by rfl
+
+end NFA

Cslib/Computability/Automata/NFAToDFA.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Computability.Automata.DFA
+import Cslib.Computability.Automata.NFA
+import Mathlib.Data.Fintype.Powerset
+
+/-! # Translation of NFA into DFA (subset construction) -/
+
+namespace NFA
+section SubsetConstruction
+
+/-- Converts an `NFA` into a `DFA` using the subset construction. -/
+@[scoped grind =]
+def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := {
+  start := nfa.start
+  accept := { S | ∃ s ∈ S, s ∈ nfa.accept }
+  tr := nfa.setImage
+  finite_state := by
+    haveI := nfa.finite_state
+    infer_instance
+  finite_symbol := nfa.finite_symbol
+}
+
+/-- Characterisation of transitions in `NFA.toDFA` wrt transitions in the original NA. -/
+@[scoped grind =]
+theorem toDFA_mem_tr {nfa : NFA State Symbol} :
+  s' ∈ nfa.toDFA.tr S x ↔ ∃ s ∈ S, nfa.Tr s x s' := by
+  simp only [NFA.toDFA, LTS.setImage, Set.mem_iUnion, exists_prop]
+  grind
+
+/-- Characterisation of multistep transitions in `NFA.toDFA` wrt multistep transitions in the
+original NA. -/
+@[scoped grind =]
+theorem toDFA_mem_mtr {nfa : NFA State Symbol} :
+  s' ∈ nfa.toDFA.mtr S xs ↔ ∃ s ∈ S, nfa.MTr s xs s' := by
+  simp only [NFA.toDFA, DFA.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`.
+
+    labels: grind, lts, automata
+  -/
+  rw [← LTS.setImageMultistep_foldl_setImage]
+  grind
+
+/-- Characterisation of multistep transitions in `NFA.toDFA` as image transitions in `LTS`. -/
+@[scoped grind =]
+theorem toDFA_mtr_setImageMultistep {nfa : NFA State Symbol} :
+  nfa.toDFA.mtr = nfa.setImageMultistep := by grind
+
+/-- The `DFA` constructed from an `NFA` has the same language. -/
+@[scoped grind =]
+theorem toDFA_language_eq {nfa : NFA State Symbol} :
+  nfa.toDFA.language = nfa.language := by
+  ext xs
+  rw [← DFA.accepts_mem_language]
+  open DFA in grind
+
+end SubsetConstruction
+end NFA