Skip to content

Commit e9cfac9

Browse files
fmontesichenson2018
fmontesi
and
chenson2018
authored
feat (Computability/Automata): Automata theory based on LTS, including DFA, NFA, EpsilonNFA, and translations between them, plus supporting theorems generalised to LTS (#83)
* feat: introduce NA for discussion * chore: rename Dfa to DFA and Lts to LTS * feat: introduce DA, plus some documentation for automata * feat: move general defs and theorems from DFA to DA * feat: add LTS.setImage, the image of a set of states * chore: rename LTS.Image and LTS.OutgoingLabels with lowercase initials * chore: fix casing of Sum.isLeft/RightP * feat (LTS): union of two LTSs with the same state and label types * feat: extension of LTS theory to deal with image transitions, and application to automata theory to prove the subset construction correct * docs: alternative shapes for transitions in NA * feat: add NFA and EpsilonNA * feat: EpsilonNA.toNAWithoutEpsilon * feat (EpsilonNA): conversion of EpsilonNA into NA, with proof of correctness * chore: Split automata theory translations into multiple files * chore: renaming to toNFA` * chore: spacing * Update Cslib/Computability/Automata/DFA.lean Co-authored-by: Chris Henson <[email protected]> * Update Cslib/Computability/Automata/DFAToNFA.lean Co-authored-by: Chris Henson <[email protected]> * Update Cslib/Computability/Automata/EpsilonNFAToNFA.lean Co-authored-by: Chris Henson <[email protected]> * Update Cslib/Computability/Automata/EpsilonNFAToNFA.lean Co-authored-by: Chris Henson <[email protected]> * Update Cslib/Computability/Automata/DFAToNFA.lean Co-authored-by: Chris Henson <[email protected]> * Update Cslib/Computability/Automata/DFAToNFA.lean Co-authored-by: Chris Henson <[email protected]> * Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <[email protected]> * Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <[email protected]> * Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <[email protected]> * Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <[email protected]> * grind annotations * scope all the grinds * Move accept conditions around for better extensibility to omega automata in the future --------- Co-authored-by: Chris Henson <[email protected]>
1 parent f5be8a8 commit e9cfac9

File tree

19 files changed

+816
-447
lines changed

19 files changed

+816
-447
lines changed

‎Cslib.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
import Cslib.Foundations.Semantics.Lts.Basic
2-
import Cslib.Foundations.Semantics.Lts.Bisimulation
3-
import Cslib.Foundations.Semantics.Lts.TraceEq
1+
import Cslib.Foundations.Semantics.LTS.Basic
2+
import Cslib.Foundations.Semantics.LTS.Bisimulation
3+
import Cslib.Foundations.Semantics.LTS.TraceEq
44
import Cslib.Foundations.Data.Relation
55
import Cslib.Languages.CombinatoryLogic.Defs
66
import Cslib.Languages.CombinatoryLogic.Basic

‎Cslib/Computability/Automata/DA.lean‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.NA
8+
9+
/-! # Deterministic Automaton
10+
11+
A Deterministic Automaton (DA) is an automaton defined by a transition function.
12+
-/
13+
structure DA (State : Type _) (Symbol : Type _) where
14+
/-- The initial state of the automaton. -/
15+
start : State
16+
/-- The transition function of the automaton. -/
17+
tr : State → Symbol → State

‎Cslib/Computability/Automata/DFA.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.DA
8+
9+
set_option linter.style.longLine false in
10+
/-! # Deterministic Finite-State Automata
11+
12+
A Deterministic Finite Automaton (DFA) is a finite-state machine that accepts or rejects
13+
a finite string.
14+
15+
## References
16+
17+
* [J. E. Hopcroft, R. Motwani, J. D. Ullman, *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
18+
-/
19+
20+
/-- A Deterministic Finite Automaton (DFA) consists of a labelled transition function
21+
`tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
22+
set of accepting states `accept`. -/
23+
structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
24+
/-- The set of accepting states of the automaton. -/
25+
accept : Set State
26+
/-- The automaton is finite-state. -/
27+
finite_state : Finite State
28+
/-- The type of symbols (also called 'alphabet') is finite. -/
29+
finite_symbol : Finite Symbol
30+
31+
32+
namespace DFA
33+
34+
/-- Extended transition function.
35+
36+
Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
37+
from the left (instead of the right), in order to match the way lists are constructed.
38+
-/
39+
@[scoped grind =]
40+
def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s
41+
42+
@[scoped grind =]
43+
theorem mtr_nil_eq {dfa : DFA State Symbol} : dfa.mtr s [] = s := by rfl
44+
45+
/-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
46+
the start state. -/
47+
@[scoped grind →]
48+
def Accepts (dfa : DFA State Symbol) (xs : List Symbol) :=
49+
dfa.mtr dfa.start xs ∈ dfa.accept
50+
51+
/-- The language of a DFA is the set of strings that it accepts. -/
52+
@[scoped grind =]
53+
def language (dfa : DFA State Symbol) : Set (List Symbol) :=
54+
{ xs | dfa.Accepts xs }
55+
56+
/-- A string is accepted by a DFA iff it is in the language of the DFA. -/
57+
@[scoped grind _=_]
58+
theorem accepts_mem_language (dfa : DFA State Symbol) (xs : List Symbol) :
59+
dfa.Accepts xs ↔ xs ∈ dfa.language := by rfl
60+
61+
end DFA

‎Cslib/Computability/Automata/DFAToNFA.lean‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.DFA
8+
import Cslib.Computability.Automata.NFA
9+
10+
/-! # Translation of DFA into NFA -/
11+
12+
namespace DFA
13+
section NFA
14+
15+
/-- `DFA` is a special case of `NFA`. -/
16+
@[scoped grind =]
17+
def toNFA (dfa : DFA State Symbol) : NFA State Symbol where
18+
start := {dfa.start}
19+
accept := dfa.accept
20+
Tr := fun s1 μ s2 => dfa.tr s1 μ = s2
21+
finite_state := dfa.finite_state
22+
finite_symbol := dfa.finite_symbol
23+
24+
@[scoped grind =]
25+
lemma toNFA_start {dfa : DFA State Symbol} : dfa.toNFA.start = {dfa.start} := rfl
26+
27+
instance : Coe (DFA State Symbol) (NFA State Symbol) where
28+
coe := toNFA
29+
30+
/-- `DA.toNA` correctly characterises transitions. -/
31+
@[scoped grind =]
32+
theorem toNA_tr {dfa : DFA State Symbol} :
33+
dfa.toNFA.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by
34+
rfl
35+
36+
/-- The transition system of a DA is deterministic. -/
37+
@[scoped grind ⇒]
38+
theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by
39+
grind
40+
41+
/-- The transition system of a DA is image-finite. -/
42+
@[scoped grind ⇒]
43+
theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite :=
44+
dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic
45+
46+
/-- Characterisation of multistep transitions. -/
47+
@[scoped grind =]
48+
theorem toNFA_mtr {dfa : DFA State Symbol} :
49+
dfa.toNFA.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by
50+
have : ∀ x, dfa.toNFA.Tr s1 x (dfa.tr s1 x) := by grind
51+
constructor <;> intro h
52+
case mp => induction h <;> grind
53+
case mpr => induction xs generalizing s1 <;> grind
54+
55+
/-- The `NFA` constructed from a `DFA` has the same language. -/
56+
@[scoped grind =]
57+
theorem toNFA_language_eq {dfa : DFA State Symbol} :
58+
dfa.toNFA.language = dfa.language := by
59+
ext xs
60+
refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> open NFA in grind
61+
62+
end NFA
63+
end DFA

‎Cslib/Computability/Automata/EpsilonNFA.lean‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.NA
8+
9+
/-! # Nondeterministic automata with ε-transitions. -/
10+
11+
/-- A nondeterministic finite automaton with ε-transitions (`εNFA`) is an `NA` with an `Option`
12+
symbol type. The special symbol ε is represented by the `Option.none` case.
13+
14+
Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
15+
allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
16+
ε-closure. -/
17+
structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) where
18+
/-- The set of accepting states of the automaton. -/
19+
accept : Set State
20+
/-- The automaton is finite-state. -/
21+
finite_state : Finite State
22+
/-- The type of symbols (also called 'alphabet') is finite. -/
23+
finite_symbol : Finite Symbol
24+
25+
@[local grind =]
26+
private instance : HasTau (Option α) := ⟨.none⟩
27+
28+
/-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S`
29+
by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance
30+
of `HasTau.τ`. -/
31+
abbrev εNFA.εClosure (enfa : εNFA State Symbol) (S : Set State) := enfa.τClosure S
32+
33+
namespace εNFA
34+
35+
/-- An εNFA accepts a string if there is a saturated multistep accepting derivative with that trace
36+
from the start state. -/
37+
@[scoped grind]
38+
def Accepts (enfa : εNFA State Symbol) (xs : List Symbol) :=
39+
∃ s ∈ enfa.εClosure enfa.start, ∃ s' ∈ enfa.accept,
40+
enfa.saturate.MTr s (xs.map (some ·)) s'
41+
42+
/-- The language of an εDA is the set of strings that it accepts. -/
43+
@[scoped grind =]
44+
def language (enfa : εNFA State Symbol) : Set (List Symbol) :=
45+
{ xs | enfa.Accepts xs }
46+
47+
/-- A string is accepted by an εNFA iff it is in the language of the NA. -/
48+
@[scoped grind =]
49+
theorem accepts_mem_language (enfa : εNFA State Symbol) (xs : List Symbol) :
50+
enfa.Accepts xs ↔ xs ∈ enfa.language := by rfl
51+
52+
end εNFA

‎Cslib/Computability/Automata/EpsilonNFAToNFA.lean‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.EpsilonNFA
8+
import Cslib.Computability.Automata.NFA
9+
10+
/-! # Translation of εNFA into NFA -/
11+
12+
/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
13+
ε-transitions. -/
14+
@[grind]
15+
private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
16+
Tr := fun s μ s' => lts.Tr s (some μ) s'
17+
18+
@[local grind]
19+
private lemma LTS.noε_saturate_tr
20+
{lts : LTS State (Option Label)} {h : μ = some μ'} :
21+
lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
22+
simp only [LTS.noε]
23+
grind
24+
25+
namespace εNFA
26+
section NFA
27+
28+
/-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/
29+
@[scoped grind]
30+
def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
31+
start := enfa.εClosure enfa.start
32+
accept := enfa.accept
33+
Tr := enfa.saturate.noε.Tr
34+
finite_state := enfa.finite_state
35+
finite_symbol := enfa.finite_symbol
36+
37+
@[scoped grind]
38+
lemma LTS.noε_saturate_mTr
39+
{lts : LTS State (Option Label)} :
40+
lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
41+
ext s'
42+
induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
43+
44+
45+
/-- Correctness of `toNFA`. -/
46+
@[scoped grind]
47+
theorem toNFA_language_eq {enfa : εNFA State Symbol} :
48+
enfa.toNFA.language = enfa.language := by
49+
ext xs
50+
have : ∀ s s', enfa.saturate.MTr s (xs.map (some ·)) s' = enfa.saturate.noε.MTr s xs s' := by
51+
simp [LTS.noε_saturate_mTr]
52+
open NFA in grind
53+
54+
end NFA
55+
end εNFA

‎Cslib/Computability/Automata/NA.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Foundations.Semantics.LTS.Basic
8+
9+
/-! # Nondeterministic Automaton
10+
11+
A Nondeterministic Automaton (NA) is an automaton with a set of initial states.
12+
13+
This definition extends `LTS` and thus stores the transition system as a relation `Tr` of the form
14+
`State → Symbol → State → Prop`. Note that you can also instantiate `Tr` by passing an argument of
15+
type `State → Symbol → Set State`; it gets automatically expanded to the former shape.
16+
-/
17+
structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
18+
/-- The set of initial states of the automaton. -/
19+
start : Set State

‎Cslib/Computability/Automata/NFA.lean‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.NA
8+
9+
/-- A Nondeterministic Finite Automaton (NFA) is a nondeterministic automaton (NA)
10+
over finite sets of states and symbols. -/
11+
structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
12+
/-- The set of accepting states of the automaton. -/
13+
accept : Set State
14+
/-- The automaton is finite-state. -/
15+
finite_state : Finite State
16+
/-- The type of symbols (also called 'alphabet') is finite. -/
17+
finite_symbol : Finite Symbol
18+
19+
namespace NFA
20+
21+
/-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
22+
the start state. -/
23+
@[scoped grind]
24+
def Accepts (nfa : NFA State Symbol) (xs : List Symbol) :=
25+
∃ s ∈ nfa.start, ∃ s' ∈ nfa.accept, nfa.MTr s xs s'
26+
27+
/-- The language of an NFA is the set of strings that it accepts. -/
28+
@[scoped grind]
29+
def language (nfa : NFA State Symbol) : Set (List Symbol) :=
30+
{ xs | nfa.Accepts xs }
31+
32+
/-- A string is accepted by an NFA iff it is in the language of the NFA. -/
33+
@[scoped grind]
34+
theorem accepts_mem_language (nfa : NFA State Symbol) (xs : List Symbol) :
35+
nfa.Accepts xs ↔ xs ∈ nfa.language := by rfl
36+
37+
end NFA

‎Cslib/Computability/Automata/NFAToDFA.lean‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
/-
2+
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fabrizio Montesi
5+
-/
6+
7+
import Cslib.Computability.Automata.DFA
8+
import Cslib.Computability.Automata.NFA
9+
import Mathlib.Data.Fintype.Powerset
10+
11+
/-! # Translation of NFA into DFA (subset construction) -/
12+
13+
namespace NFA
14+
section SubsetConstruction
15+
16+
/-- Converts an `NFA` into a `DFA` using the subset construction. -/
17+
@[scoped grind =]
18+
def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := {
19+
start := nfa.start
20+
accept := { S | ∃ s ∈ S, s ∈ nfa.accept }
21+
tr := nfa.setImage
22+
finite_state := by
23+
haveI := nfa.finite_state
24+
infer_instance
25+
finite_symbol := nfa.finite_symbol
26+
}
27+
28+
/-- Characterisation of transitions in `NFA.toDFA` wrt transitions in the original NA. -/
29+
@[scoped grind =]
30+
theorem toDFA_mem_tr {nfa : NFA State Symbol} :
31+
s' ∈ nfa.toDFA.tr S x ↔ ∃ s ∈ S, nfa.Tr s x s' := by
32+
simp only [NFA.toDFA, LTS.setImage, Set.mem_iUnion, exists_prop]
33+
grind
34+
35+
/-- Characterisation of multistep transitions in `NFA.toDFA` wrt multistep transitions in the
36+
original NA. -/
37+
@[scoped grind =]
38+
theorem toDFA_mem_mtr {nfa : NFA State Symbol} :
39+
s' ∈ nfa.toDFA.mtr S xs ↔ ∃ s ∈ S, nfa.MTr s xs s' := by
40+
simp only [NFA.toDFA, DFA.mtr]
41+
/- TODO: Grind does not catch a useful rewrite in the subset construction for automata
42+
43+
A very similar issue seems to occur in the proof of `NFA.toDFA_language_eq`.
44+
45+
labels: grind, lts, automata
46+
-/
47+
rw [← LTS.setImageMultistep_foldl_setImage]
48+
grind
49+
50+
/-- Characterisation of multistep transitions in `NFA.toDFA` as image transitions in `LTS`. -/
51+
@[scoped grind =]
52+
theorem toDFA_mtr_setImageMultistep {nfa : NFA State Symbol} :
53+
nfa.toDFA.mtr = nfa.setImageMultistep := by grind
54+
55+
/-- The `DFA` constructed from an `NFA` has the same language. -/
56+
@[scoped grind =]
57+
theorem toDFA_language_eq {nfa : NFA State Symbol} :
58+
nfa.toDFA.language = nfa.language := by
59+
ext xs
60+
rw [← DFA.accepts_mem_language]
61+
open DFA in grind
62+
63+
end SubsetConstruction
64+
end NFA

0 commit comments

Comments
 (0)