From 8561629f9d6f83ce61b567aa67db2259411c8f0a Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 29 Sep 2025 10:09:18 +0200 Subject: [PATCH 01/29] feat: introduce NA for discussion --- Cslib/Computability/Automata/NA.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 Cslib/Computability/Automata/NA.lean diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean new file mode 100644 index 00000000..5fa821b8 --- /dev/null +++ b/Cslib/Computability/Automata/NA.lean @@ -0,0 +1,14 @@ +/- +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 a labelled transition system with a set of initial states. +-/ +structure NA State Symbol extends LTS State Symbol where + start : Set State From cae4e0d14c9ee2480c00352b883589b0e8847b6d Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 29 Sep 2025 10:09:28 +0200 Subject: [PATCH 02/29] chore: rename Dfa to DFA and Lts to LTS --- Cslib.lean | 6 +- .../{Dfa => Automata/DFA}/Basic.lean | 50 +-- .../Semantics/{Lts => LTS}/Basic.lean | 316 +++++++++--------- .../Semantics/{Lts => LTS}/Bisimulation.lean | 184 +++++----- .../Semantics/{Lts => LTS}/Simulation.lean | 24 +- .../Semantics/{Lts => LTS}/TraceEq.lean | 42 +-- Cslib/Languages/CCS/BehaviouralTheory.lean | 16 +- Cslib/Languages/CCS/Semantics.lean | 4 +- CslibTests/Bisimulation.lean | 8 +- CslibTests/{Dfa.lean => DFA.lean} | 4 +- CslibTests/{Lts.lean => LTS.lean} | 22 +- 11 files changed, 338 insertions(+), 338 deletions(-) rename Cslib/Computability/{Dfa => Automata/DFA}/Basic.lean (65%) rename Cslib/Foundations/Semantics/{Lts => LTS}/Basic.lean (65%) rename Cslib/Foundations/Semantics/{Lts => LTS}/Bisimulation.lean (87%) rename Cslib/Foundations/Semantics/{Lts => LTS}/Simulation.lean (86%) rename Cslib/Foundations/Semantics/{Lts => LTS}/TraceEq.lean (71%) rename CslibTests/{Dfa.lean => DFA.lean} (91%) rename CslibTests/{Lts.lean => LTS.lean} (84%) diff --git a/Cslib.lean b/Cslib.lean index c50fa2ec..f696325f 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Computability/Dfa/Basic.lean b/Cslib/Computability/Automata/DFA/Basic.lean similarity index 65% rename from Cslib/Computability/Dfa/Basic.lean rename to Cslib/Computability/Automata/DFA/Basic.lean index 052ff92a..d2d737f6 100644 --- a/Cslib/Computability/Dfa/Basic.lean +++ b/Cslib/Computability/Automata/DFA/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic +import Cslib.Foundations.Semantics.LTS.Basic set_option linter.style.longLine false in /-! # Deterministic Finite-State Automata @@ -20,7 +20,7 @@ a finite string. /-- A Deterministic Finite-State 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 _) where +structure DFA (State : Type _) (Symbol : Type _) where /-- The transition function of the automaton. -/ tr : State → Symbol → State /-- Start state. -/ @@ -32,7 +32,7 @@ structure Dfa (State : Type _) (Symbol : Type _) where /-- The type of symbols (also called 'alphabet') is finite. -/ finite_symbol : Finite Symbol -namespace Dfa +namespace DFA /-- Extended transition function. @@ -40,50 +40,50 @@ Implementation note: compared to [Hopcroft2006], the definition consumes the inp from the left (instead of the right), in order to follow the way lists are constructed. -/ @[grind] -def mtr (dfa : Dfa State Symbol) (s : State) (xs : List Symbol) := +def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := match xs with | [] => s | x :: xs => dfa.mtr (dfa.tr s x) xs @[grind] -theorem mtr_nil_eq {dfa : Dfa State Symbol} : dfa.mtr s [] = s := by rfl +theorem mtr_nil_eq {dfa : DFA State Symbol} : dfa.mtr s [] = s := by rfl /-- A DFA accepts a trace if there is a multi-step accepting derivative with that trace from the start state. -/ @[grind] -def Accepts (dfa : Dfa State Symbol) (μs : List Symbol) := +def Accepts (dfa : DFA State Symbol) (μs : List Symbol) := (dfa.mtr dfa.start μs) ∈ dfa.accept /-- The language of a DFA is the set of traces that it accepts. -/ @[grind] -def language (dfa : Dfa State Symbol) : Set (List Symbol) := +def language (dfa : DFA State Symbol) : Set (List Symbol) := { μs | dfa.Accepts μs } /-- A trace is accepted by a DFA iff it is in the language of the DFA. -/ @[grind] -theorem accepts_mem_language (dfa : Dfa State Symbol) (μs : List Symbol) : +theorem accepts_mem_language (dfa : DFA State Symbol) (μs : List Symbol) : dfa.Accepts μs ↔ μs ∈ dfa.language := by rfl -section Lts +section LTS -/-- `Dfa` is a special case of `Lts`. -/ +/-- `DFA` is a special case of `LTS`. -/ @[grind] -def toLts (dfa : Dfa State Symbol) : Lts State Symbol := - Lts.mk (fun s1 μ s2 => dfa.tr s1 μ = s2) +def toLTS (dfa : DFA State Symbol) : LTS State Symbol := + LTS.mk (fun s1 μ s2 => dfa.tr s1 μ = s2) -instance : Coe (Dfa State Symbol) (Lts State Symbol) where - coe := toLts +instance : Coe (DFA State Symbol) (LTS State Symbol) where + coe := toLTS -/-- `Dfa.toLts` correctly characterises transitions. -/ +/-- `DFA.toLTS` correctly characterises transitions. -/ @[grind] -theorem toLts_tr {dfa : Dfa State Symbol} : - dfa.toLts.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by +theorem toLTS_tr {dfa : DFA State Symbol} : + dfa.toLTS.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by rfl -/-- `Dfa.toLts` correctly characterises multistep transitions. -/ +/-- `DFA.toLTS` correctly characterises multistep transitions. -/ @[grind] -theorem toLts_mtr {dfa : Dfa State Symbol} : - dfa.toLts.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by +theorem toLTS_mtr {dfa : DFA State Symbol} : + dfa.toLTS.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by constructor <;> intro h case mp => induction h <;> grind @@ -91,18 +91,18 @@ theorem toLts_mtr {dfa : Dfa State Symbol} : induction xs generalizing s1 case nil => grind case cons x xs ih => - apply Lts.MTr.stepL (s2 := dfa.tr s1 x) <;> grind + apply LTS.MTr.stepL (s2 := dfa.tr s1 x) <;> grind /-- The LTS induced by a DFA is deterministic. -/ @[grind] -theorem toLts_deterministic (dfa : Dfa State Symbol) : dfa.toLts.Deterministic := by +theorem toLTS_deterministic (dfa : DFA State Symbol) : dfa.toLTS.Deterministic := by grind /-- The LTS induced by a DFA is finite-state. -/ @[grind] -theorem toLts_finiteState (dfa : Dfa State Symbol) : dfa.toLts.FiniteState := +theorem toLTS_finiteState (dfa : DFA State Symbol) : dfa.toLTS.FiniteState := dfa.finite_state -end Lts +end LTS -end Dfa +end DFA diff --git a/Cslib/Foundations/Semantics/Lts/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean similarity index 65% rename from Cslib/Foundations/Semantics/Lts/Basic.lean rename to Cslib/Foundations/Semantics/LTS/Basic.lean index b6eaa4d1..fba2cd5e 100644 --- a/Cslib/Foundations/Semantics/Lts/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -15,31 +15,31 @@ import Mathlib.Util.Notation3 /-! # Labelled Transition System (LTS) -A Labelled Transition System (`Lts`) models the observable behaviour of the possible states of a +A Labelled Transition System (`LTS`) models the observable behaviour of the possible states of a system. They are particularly popular in the fields of concurrency theory, logic, and programming languages. ## Main definitions -- `Lts` is a structure for labelled transition systems, consisting of a labelled transition +- `LTS` is a structure for labelled transition systems, consisting of a labelled transition relation `Tr` between states. We follow the style and conventions in [Sangiorgi2011]. -- `Lts.MTr` extends the transition relation of any Lts to a multi-step transition relation, +- `LTS.MTr` extends the transition relation of any LTS to a multi-step transition relation, formalising the inference system and admissible rules for such relations in [Montesi2023]. -- Definitions for all the common classes of Ltss: image-finite, finitely branching, finite-state, +- Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state, finite, and deterministic. ## Main statements -- A series of results on `Lts.MTr` that allow for obtaining and composing multi-step transitions in +- A series of results on `LTS.MTr` that allow for obtaining and composing multi-step transitions in different ways. -- `Lts.deterministic_imageFinite`: every deterministic Lts is also image-finite. +- `LTS.deterministic_imageFinite`: every deterministic LTS is also image-finite. -- `Lts.finiteState_imageFinite`: every finite-state Lts is also image-finite. +- `LTS.finiteState_imageFinite`: every finite-state LTS is also image-finite. -- `Lts.finiteState_finitelyBranching`: every finite-state Lts is also finitely-branching, if the +- `LTS.finiteState_finitelyBranching`: every finite-state LTS is also finitely-branching, if the type of labels is finite. ## References @@ -51,10 +51,10 @@ type of labels is finite. universe u v /-- -A Labelled Transition System (Lts) consists of a type of states (`State`), a type of transition +A Labelled Transition System (LTS) consists of a type of states (`State`), a type of transition labels (`Label`), and a labelled transition relation (`Tr`). -/ -structure Lts (State : Type u) (Label : Type v) where +structure LTS (State : Type u) (Label : Type v) where /-- The transition relation. -/ Tr : State → Label → State → Prop @@ -62,7 +62,7 @@ section MultiStep /-! ## Multi-step transitions -/ -variable {State : Type u} {Label : Type v} (lts : Lts State Label) +variable {State : Type u} {Label : Type v} (lts : LTS State Label) /-- Definition of a multi-step transition. @@ -72,7 +72,7 @@ rule. This makes working with lists of labels more convenient, because we follow construction. It is also similar to what is done in the `SimpleGraph` library in mathlib.) -/ @[grind] -inductive Lts.MTr (lts : Lts State Label) : State → List Label → State → Prop where +inductive LTS.MTr (lts : LTS State Label) : State → List Label → State → Prop where | refl {s : State} : lts.MTr s [] s | stepL {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} : lts.Tr s1 μ s2 → lts.MTr s2 μs s3 → @@ -80,41 +80,41 @@ inductive Lts.MTr (lts : Lts State Label) : State → List Label → State → P /-- Any transition is also a multi-step transition. -/ @[grind] -theorem Lts.MTr.single {s1 : State} {μ : Label} {s2 : State} : +theorem LTS.MTr.single {s1 : State} {μ : Label} {s2 : State} : lts.Tr s1 μ s2 → lts.MTr s1 [μ] s2 := by intro h - apply Lts.MTr.stepL + apply LTS.MTr.stepL · exact h - · apply Lts.MTr.refl + · apply LTS.MTr.refl /-- Any multi-step transition can be extended by adding a transition. -/ @[grind] -theorem Lts.MTr.stepR {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} : +theorem LTS.MTr.stepR {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} : lts.MTr s1 μs s2 → lts.Tr s2 μ s3 → lts.MTr s1 (μs ++ [μ]) s3 := by intro h1 h2 induction h1 - case refl s1' => exact Lts.MTr.single lts h2 + case refl s1' => exact LTS.MTr.single lts h2 case stepL s1' μ' s2' μs' s3' h1' h3 ih => - apply Lts.MTr.stepL + apply LTS.MTr.stepL · exact h1' · apply ih h2 /-- Multi-step transitions can be composed. -/ @[grind] -theorem Lts.MTr.comp {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List Label} {s3 : State} : +theorem LTS.MTr.comp {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List Label} {s3 : State} : lts.MTr s1 μs1 s2 → lts.MTr s2 μs2 s3 → lts.MTr s1 (μs1 ++ μs2) s3 := by intro h1 h2 induction h1 case refl => assumption case stepL s1 μ s' μs1' s'' h1' h3 ih => - apply Lts.MTr.stepL + apply LTS.MTr.stepL · exact h1' · apply ih h2 /-- Any 1-sized multi-step transition implies a transition with the same states and label. -/ @[grind] -theorem Lts.MTr.single_invert (s1 : State) (μ : Label) (s2 : State) : +theorem LTS.MTr.single_invert (s1 : State) (μ : Label) (s2 : State) : lts.MTr s1 [μ] s2 → lts.Tr s1 μ s2 := by intro h cases h @@ -124,22 +124,22 @@ theorem Lts.MTr.single_invert (s1 : State) (μ : Label) (s2 : State) : /-- In any zero-steps multi-step transition, the origin and the derivative are the same. -/ @[grind] -theorem Lts.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by +theorem LTS.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by cases h rfl /-- A state `s1` can reach a state `s2` if there exists a multi-step transition from `s1` to `s2`. -/ -def Lts.CanReach (s1 s2 : State) : Prop := +def LTS.CanReach (s1 s2 : State) : Prop := ∃ μs, lts.MTr s1 μs s2 /-- Any state can reach itself. -/ -theorem Lts.CanReach.refl (s : State) : lts.CanReach s s := by +theorem LTS.CanReach.refl (s : State) : lts.CanReach s s := by exists [] - apply Lts.MTr.refl + apply LTS.MTr.refl -/-- The Lts generated by a state `s` is the Lts given by all the states reachable from `s`. -/ -def Lts.generatedBy (s : State) : Lts {s' : State // lts.CanReach s s'} Label where +/-- The LTS generated by a state `s` is the LTS given by all the states reachable from `s`. -/ +def LTS.generatedBy (s : State) : LTS {s' : State // lts.CanReach s s'} Label where Tr := fun s1 μ s2 => lts.CanReach s s1 ∧ lts.CanReach s s2 ∧ lts.Tr s1 μ s2 end MultiStep @@ -147,34 +147,34 @@ end MultiStep section Termination /-! ## Definitions about termination -/ -variable {State} {Label} (lts : Lts State Label) {Terminated : State → Prop} +variable {State} {Label} (lts : LTS State Label) {Terminated : State → Prop} /-- A state 'may terminate' if it can reach a terminated state. The definition of `Terminated` is a parameter. -/ -def Lts.MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s' +def LTS.MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s' /-- A state 'is stuck' if it is not terminated and cannot go forward. The definition of `Terminated` is a parameter. -/ -def Lts.Stuck (s : State) : Prop := +def LTS.Stuck (s : State) : Prop := ¬Terminated s ∧ ¬∃ μ s', lts.Tr s μ s' end Termination section Union -/-! ## Definitions for the unions of Ltss +/-! ## Definitions for the unions of LTSs Note: there is a nontrivial balance between ergonomics and generality here. These definitions might change in the future. -/ variable {State : Type u} {Label : Type v} -/-- The union of two Ltss that have common supertypes for states and labels. -/ -def Lts.unionSubtype +/-- The union of two LTSs that have common supertypes for states and labels. -/ +def LTS.unionSubtype {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop} [DecidablePred S1] [DecidablePred L1] [DecidablePred S2] [DecidablePred L2] -(lts1 : Lts (@Subtype State S1) (@Subtype Label L1)) -(lts2 : Lts (@Subtype State S2) (@Subtype Label L2)) : - Lts State Label where +(lts1 : LTS (@Subtype State S1) (@Subtype Label L1)) +(lts2 : LTS (@Subtype State S2) (@Subtype Label L2)) : + LTS State Label where Tr := fun s μ s' => if h : S1 s ∧ L1 μ ∧ S1 s' then lts1.Tr ⟨s, h.1⟩ ⟨μ, h.2.1⟩ ⟨s', h.2.2⟩ @@ -189,9 +189,9 @@ def Sum.isLeftP {α} {β} (x : α ⊕ β) : Prop := Sum.isLeft x = true /-- TODO: move this to `Sum`? -/ def Sum.isRightP {α} {β} (x : α ⊕ β) : Prop := Sum.isRight x = true -/-- Lifting of an `Lts State Label` to `Lts (State ⊕ State') Label`. -/ -def Lts.inl {State'} (lts : Lts State Label) : - Lts (@Subtype (State ⊕ State') Sum.isLeftP) (@Subtype Label (Function.const Label True)) where +/-- Lifting of an `LTS State Label` to `LTS (State ⊕ State') Label`. -/ +def LTS.inl {State'} (lts : LTS State Label) : + LTS (@Subtype (State ⊕ State') Sum.isLeftP) (@Subtype Label (Function.const Label True)) where Tr := fun s μ s' => let ⟨s, _⟩ := s let ⟨s', _⟩ := s' @@ -199,9 +199,9 @@ def Lts.inl {State'} (lts : Lts State Label) : | Sum.inl s1, μ, Sum.inl s2 => lts.Tr s1 μ s2 | _, _, _ => False -/-- Lifting of an `Lts State Label` to `Lts (State' ⊕ State) Label`. -/ -def Lts.inr {State'} (lts : Lts State Label) : - Lts (@Subtype (State' ⊕ State) Sum.isRightP) (@Subtype Label (Function.const Label True)) where +/-- Lifting of an `LTS State Label` to `LTS (State' ⊕ State) Label`. -/ +def LTS.inr {State'} (lts : LTS State Label) : + LTS (@Subtype (State' ⊕ State) Sum.isRightP) (@Subtype Label (Function.const Label True)) where Tr := fun s μ s' => let ⟨s, _⟩ := s let ⟨s', _⟩ := s' @@ -209,11 +209,11 @@ def Lts.inr {State'} (lts : Lts State Label) : | Sum.inr s1, μ, Sum.inr s2 => lts.Tr s1 μ s2 | _, _, _ => False -/-- Union of two Ltss with the same `Label` type. The result combines the original respective state +/-- Union of two LTSs with the same `Label` type. The result combines the original respective state types `State1` and `State2` into `(State1 ⊕ State2)`. -/ -def Lts.unionSum {State1} {State2} (lts1 : Lts State1 Label) (lts2 : Lts State2 Label) : - Lts (State1 ⊕ State2) Label := - @Lts.unionSubtype +def LTS.unionSum {State1} {State2} (lts1 : LTS State1 Label) (lts2 : LTS State2 Label) : + LTS (State1 ⊕ State2) Label := + @LTS.unionSubtype (State1 ⊕ State2) Label Sum.isLeftP (Function.const Label True) @@ -250,30 +250,30 @@ end Union section Classes /-! -### Classes of Ltss +### Classes of LTSs -/ -variable {State : Type u} {Label : Type v} (lts : Lts State Label) +variable {State : Type u} {Label : Type v} (lts : LTS State Label) /-- An lts is deterministic if a state cannot reach different states with the same transition label. -/ @[grind] -def Lts.Deterministic : Prop := +def LTS.Deterministic : Prop := ∀ (s1 : State) (μ : Label) (s2 s3 : State), lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3 /-- The `μ`-image of a state `s` is the set of all `μ`-derivatives of `s`. -/ @[grind] -def Lts.Image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' } +def LTS.Image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' } /-- An lts is image-finite if all images of its states are finite. -/ @[grind] -def Lts.ImageFinite : Prop := +def LTS.ImageFinite : Prop := ∀ s μ, Finite (lts.Image s μ) -/-- In a deterministic Lts, if a state has a `μ`-derivative, then it can have no other +/-- In a deterministic LTS, if a state has a `μ`-derivative, then it can have no other `μ`-derivative. -/ -theorem Lts.deterministic_not_lto (hDet : lts.Deterministic) : +theorem LTS.deterministic_not_lto (hDet : lts.Deterministic) : ∀ s μ s' s'', s' ≠ s'' → lts.Tr s μ s' → ¬lts.Tr s μ s'' := by intro s μ s' s'' hneq hltos' by_contra hltos'' @@ -281,18 +281,18 @@ theorem Lts.deterministic_not_lto (hDet : lts.Deterministic) : simp only [← hDet'] at hneq contradiction -/-- In a deterministic Lts, any image is either a singleton or the empty set. -/ -theorem Lts.deterministic_image_char (hDet : lts.Deterministic) : +/-- In a deterministic LTS, any image is either a singleton or the empty set. -/ +theorem LTS.deterministic_image_char (hDet : lts.Deterministic) : ∀ s μ, (∃ s', lts.Image s μ = { s' }) ∨ (lts.Image s μ = ∅) := by intro s μ by_cases hs' : ∃ s', lts.Tr s μ s' <;> aesop (add simp [Image]) -/-- Every deterministic Lts is also image-finite. -/ -theorem Lts.deterministic_imageFinite : +/-- Every deterministic LTS is also image-finite. -/ +theorem LTS.deterministic_imageFinite : lts.Deterministic → lts.ImageFinite := by simp only [ImageFinite] intro h s μ - have hDet := Lts.deterministic_image_char lts h s μ + have hDet := LTS.deterministic_image_char lts h s μ cases hDet case inl hDet => obtain ⟨s', hDet'⟩ := hDet @@ -303,44 +303,44 @@ theorem Lts.deterministic_imageFinite : apply Set.finite_empty /-- A state has an outgoing label `μ` if it has a `μ`-derivative. -/ -def Lts.HasOutLabel (s : State) (μ : Label) : Prop := +def LTS.HasOutLabel (s : State) (μ : Label) : Prop := ∃ s', lts.Tr s μ s' /-- The set of outgoing labels of a state. -/ -def Lts.OutgoingLabels (s : State) := { μ | lts.HasOutLabel s μ } +def LTS.OutgoingLabels (s : State) := { μ | lts.HasOutLabel s μ } -/-- An Lts is finitely branching if it is image-finite and all states have finite sets of +/-- An LTS is finitely branching if it is image-finite and all states have finite sets of outgoing labels. -/ -def Lts.FinitelyBranching : Prop := +def LTS.FinitelyBranching : Prop := lts.ImageFinite ∧ ∀ s, Finite (lts.OutgoingLabels s) -/-- An Lts is finite-state if it has a finite `State` type. -/ +/-- An LTS is finite-state if it has a finite `State` type. -/ @[nolint unusedArguments] -def Lts.FiniteState (_ : Lts State Label) : Prop := Finite State +def LTS.FiniteState (_ : LTS State Label) : Prop := Finite State -/-- Every finite-state Lts is also image-finite. -/ -theorem Lts.finiteState_imageFinite (hFinite : lts.FiniteState) : +/-- Every finite-state LTS is also image-finite. -/ +theorem LTS.finiteState_imageFinite (hFinite : lts.FiniteState) : lts.ImageFinite := by intro s μ apply @Subtype.finite State hFinite -/-- Every Lts with finite types for states and labels is also finitely branching. -/ -theorem Lts.finiteState_finitelyBranching +/-- Every LTS with finite types for states and labels is also finitely branching. -/ +theorem LTS.finiteState_finitelyBranching (hFiniteLabel : Finite Label) (hFiniteState : lts.FiniteState) : lts.FinitelyBranching := by constructor case left => - apply Lts.finiteState_imageFinite lts hFiniteState + apply LTS.finiteState_imageFinite lts hFiniteState case right => intro s apply @Subtype.finite Label hFiniteLabel -/-- An Lts is acyclic if there are no infinite multi-step transitions. -/ -def Lts.Acyclic : Prop := +/-- An LTS is acyclic if there are no infinite multi-step transitions. -/ +def LTS.Acyclic : Prop := ∃ n, ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n -/-- An Lts is finite if it is finite-state and acyclic. -/ -def Lts.Finite : Prop := +/-- An LTS is finite if it is finite-state and acyclic. -/ +def LTS.Finite : Prop := lts.FiniteState ∧ lts.Acyclic end Classes @@ -354,22 +354,22 @@ class HasTau (Label : Type v) where τ : Label /-- Saturated transition relation. -/ -inductive Lts.STr [HasTau Label] (lts : Lts State Label) : State → Label → State → Prop where +inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where | refl : lts.STr s HasTau.τ s | tr : lts.STr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STr s3 HasTau.τ s4 → lts.STr s1 μ s4 -/-- The `Lts` obtained by saturating the transition relation in `lts`. -/ -def Lts.saturate [HasTau Label] (lts : Lts State Label) : Lts State Label where - Tr := Lts.STr lts +/-- The `LTS` obtained by saturating the transition relation in `lts`. -/ +def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where + Tr := LTS.STr lts /-- Any transition is also a saturated transition. -/ -theorem Lts.STr.single [HasTau Label] (lts : Lts State Label) : lts.Tr s μ s' → lts.STr s μ s' := by +theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) : lts.Tr s μ s' → lts.STr s μ s' := by intro h - apply Lts.STr.tr Lts.STr.refl h Lts.STr.refl + apply LTS.STr.tr LTS.STr.refl h LTS.STr.refl -/-- As `Lts.str`, but counts the number of `τ`-transitions. This is convenient as induction +/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction metric. -/ -inductive Lts.strN [HasTau Label] (lts : Lts State Label) : +inductive LTS.strN [HasTau Label] (lts : LTS State Label) : ℕ → State → Label → State → Prop where | refl : lts.strN 0 s HasTau.τ s | tr : @@ -378,92 +378,92 @@ inductive Lts.strN [HasTau Label] (lts : Lts State Label) : lts.strN m s3 HasTau.τ s4 → lts.strN (n + m + 1) s1 μ s4 -/-- `Lts.str` and `Lts.strN` are equivalent. -/ -theorem Lts.str_strN [HasTau Label] (lts : Lts State Label) : +/-- `LTS.str` and `LTS.strN` are equivalent. -/ +theorem LTS.str_strN [HasTau Label] (lts : LTS State Label) : lts.STr s1 μ s2 ↔ ∃ n, lts.strN n s1 μ s2 := by apply Iff.intro <;> intro h case mp => induction h case refl => exists 0 - exact Lts.strN.refl + exact LTS.strN.refl case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 => obtain ⟨n1, ih1⟩ := ih1 obtain ⟨n2, ih2⟩ := ih2 exists (n1 + n2 + 1) - apply Lts.strN.tr ih1 htr ih2 + apply LTS.strN.tr ih1 htr ih2 case mpr => obtain ⟨n, h⟩ := h induction h case refl => constructor case tr n s1 sb μ sb' m s2 hstr1 htr hstr2 ih1 ih2 => - apply Lts.STr.tr ih1 htr ih2 + apply LTS.STr.tr ih1 htr ih2 /-- Saturated transitions labelled by τ can be composed (weighted version). -/ -theorem Lts.strN.trans_τ - [HasTau Label] (lts : Lts State Label) +theorem LTS.strN.trans_τ + [HasTau Label] (lts : LTS State Label) (h1 : lts.strN n s1 HasTau.τ s2) (h2 : lts.strN m s2 HasTau.τ s3) : lts.strN (n + m) s1 HasTau.τ s3 := by cases h1 case refl => grind case tr n1 sb sb' n2 hstr1 htr hstr2 => - have ih := Lts.strN.trans_τ lts hstr2 h2 - have conc := Lts.strN.tr hstr1 htr ih + have ih := LTS.strN.trans_τ lts hstr2 h2 + have conc := LTS.strN.tr hstr1 htr ih grind /-- Saturated transitions labelled by τ can be composed. -/ -theorem Lts.STr.trans_τ - [HasTau Label] (lts : Lts State Label) +theorem LTS.STr.trans_τ + [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : lts.STr s1 HasTau.τ s3 := by - obtain ⟨n, h1N⟩ := (Lts.str_strN lts).1 h1 - obtain ⟨m, h2N⟩ := (Lts.str_strN lts).1 h2 - have concN := Lts.strN.trans_τ lts h1N h2N - apply (Lts.str_strN lts).2 ⟨n + m, concN⟩ + obtain ⟨n, h1N⟩ := (LTS.str_strN lts).1 h1 + obtain ⟨m, h2N⟩ := (LTS.str_strN lts).1 h2 + have concN := LTS.strN.trans_τ lts h1N h2N + apply (LTS.str_strN lts).2 ⟨n + m, concN⟩ /-- Saturated transitions can be appended with τ-transitions (weighted version). -/ -theorem Lts.strN.append - [HasTau Label] (lts : Lts State Label) +theorem LTS.strN.append + [HasTau Label] (lts : LTS State Label) (h1 : lts.strN n1 s1 μ s2) (h2 : lts.strN n2 s2 HasTau.τ s3) : lts.strN (n1 + n2) s1 μ s3 := by cases h1 case refl => grind case tr n11 sb sb' n12 hstr1 htr hstr2 => - have hsuffix := Lts.strN.trans_τ lts hstr2 h2 + have hsuffix := LTS.strN.trans_τ lts hstr2 h2 have n_eq : n11 + (n12 + n2) + 1 = (n11 + n12 + 1 + n2) := by omega rw [← n_eq] - apply Lts.strN.tr hstr1 htr hsuffix + apply LTS.strN.tr hstr1 htr hsuffix /-- Saturated transitions can be composed (weighted version). -/ -theorem Lts.strN.comp - [HasTau Label] (lts : Lts State Label) +theorem LTS.strN.comp + [HasTau Label] (lts : LTS State Label) (h1 : lts.strN n1 s1 HasTau.τ s2) (h2 : lts.strN n2 s2 μ s3) (h3 : lts.strN n3 s3 HasTau.τ s4) : lts.strN (n1 + n2 + n3) s1 μ s4 := by cases h2 case refl => - apply Lts.strN.trans_τ lts h1 h3 + apply LTS.strN.trans_τ lts h1 h3 case tr n21 sb sb' n22 hstr1 htr hstr2 => - have hprefix_τ := Lts.strN.trans_τ lts h1 hstr1 - have hprefix := Lts.strN.tr hprefix_τ htr hstr2 - have conc := Lts.strN.append lts hprefix h3 + have hprefix_τ := LTS.strN.trans_τ lts h1 hstr1 + have hprefix := LTS.strN.tr hprefix_τ htr hstr2 + have conc := LTS.strN.append lts hprefix h3 grind /-- Saturated transitions can be composed. -/ -theorem Lts.STr.comp - [HasTau Label] (lts : Lts State Label) +theorem LTS.STr.comp + [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 μ s3) (h3 : lts.STr s3 HasTau.τ s4) : lts.STr s1 μ s4 := by - obtain ⟨n1, h1N⟩ := (Lts.str_strN lts).1 h1 - obtain ⟨n2, h2N⟩ := (Lts.str_strN lts).1 h2 - obtain ⟨n3, h3N⟩ := (Lts.str_strN lts).1 h3 - have concN := Lts.strN.comp lts h1N h2N h3N - apply (Lts.str_strN lts).2 ⟨n1 + n2 + n3, concN⟩ + obtain ⟨n1, h1N⟩ := (LTS.str_strN lts).1 h1 + obtain ⟨n2, h2N⟩ := (LTS.str_strN lts).1 h2 + obtain ⟨n3, h3N⟩ := (LTS.str_strN lts).1 h3 + have concN := LTS.strN.comp lts h1N h2N h3N + apply (LTS.str_strN lts).2 ⟨n1 + n2 + n3, concN⟩ end Weak @@ -473,27 +473,27 @@ section Divergence /-- A divergent execution is a stream of states where each state is the anti-τ-derivative of the next. -/ -def Lts.DivergentExecution [HasTau Label] (lts : Lts State Label) +def LTS.DivergentExecution [HasTau Label] (lts : LTS State Label) (stream : Stream' State) : Prop := ∀ n, lts.Tr (stream n) HasTau.τ (stream n.succ) /-- A state is divergent if there is a divergent execution from it. -/ -def Lts.Divergent [HasTau Label] (lts : Lts State Label) (s : State) : Prop := +def LTS.Divergent [HasTau Label] (lts : LTS State Label) (s : State) : Prop := ∃ stream : Stream' State, stream 0 = s ∧ lts.DivergentExecution stream /-- If a stream is a divergent execution, then any 'suffix' is also a divergent execution. -/ -theorem Lts.divergent_drop - [HasTau Label] (lts : Lts State Label) (stream : Stream' State) +theorem LTS.divergent_drop + [HasTau Label] (lts : LTS State Label) (stream : Stream' State) (h : lts.DivergentExecution stream) (n : ℕ) : lts.DivergentExecution (stream.drop n) := by - simp only [Lts.DivergentExecution] + simp only [LTS.DivergentExecution] intro m simp only [Stream'.drop, Stream'.get] - simp [Lts.DivergentExecution] at h + simp [LTS.DivergentExecution] at h grind -/-- An Lts is divergence-free if it has no divergent state. -/ -def Lts.DivergenceFree [HasTau Label] (lts : Lts State Label) : Prop := +/-- An LTS is divergence-free if it has no divergent state. -/ +def LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) : Prop := ¬∃ s, lts.Divergent s end Divergence @@ -501,17 +501,17 @@ end Divergence section Relation /-- Returns the relation that relates all states `s1` and `s2` via a fixed transition label `μ`. -/ -def Lts.Tr.toRelation (lts : Lts State Label) (μ : Label) : State → State → Prop := +def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop := fun s1 s2 => lts.Tr s1 μ s2 /-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition labels `μs`. -/ -def Lts.MTr.toRelation (lts : Lts State Label) (μs : List Label) : State → State → Prop := +def LTS.MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop := fun s1 s2 => lts.MTr s1 μs s2 -/-- Any homogeneous relation can be seen as an Lts where all transitions have the same label. -/ -def Relation.toLts [DecidableEq Label] (r : State → State → Prop) (μ : Label) : - Lts State Label where +/-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/ +def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) : + LTS State Label where Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False end Relation @@ -521,54 +521,54 @@ section Trans /-! ## Support for the calc tactic -/ /-- Transitions can be chained. -/ -instance (lts : Lts State Label) : +instance (lts : LTS State Label) : Trans - (Lts.Tr.toRelation lts μ1) - (Lts.Tr.toRelation lts μ2) - (Lts.MTr.toRelation lts [μ1, μ2]) where + (LTS.Tr.toRelation lts μ1) + (LTS.Tr.toRelation lts μ2) + (LTS.MTr.toRelation lts [μ1, μ2]) where trans := by intro s1 s2 s3 htr1 htr2 - apply Lts.MTr.single at htr1 - apply Lts.MTr.single at htr2 - apply Lts.MTr.comp lts htr1 htr2 + apply LTS.MTr.single at htr1 + apply LTS.MTr.single at htr2 + apply LTS.MTr.comp lts htr1 htr2 /-- Transitions can be chained with multi-step transitions. -/ -instance (lts : Lts State Label) : +instance (lts : LTS State Label) : Trans - (Lts.Tr.toRelation lts μ) - (Lts.MTr.toRelation lts μs) - (Lts.MTr.toRelation lts (μ :: μs)) where + (LTS.Tr.toRelation lts μ) + (LTS.MTr.toRelation lts μs) + (LTS.MTr.toRelation lts (μ :: μs)) where trans := by intro s1 s2 s3 htr1 hmtr2 - apply Lts.MTr.single at htr1 - apply Lts.MTr.comp lts htr1 hmtr2 + apply LTS.MTr.single at htr1 + apply LTS.MTr.comp lts htr1 hmtr2 /-- Multi-step transitions can be chained with transitions. -/ -instance (lts : Lts State Label) : +instance (lts : LTS State Label) : Trans - (Lts.MTr.toRelation lts μs) - (Lts.Tr.toRelation lts μ) - (Lts.MTr.toRelation lts (μs ++ [μ])) where + (LTS.MTr.toRelation lts μs) + (LTS.Tr.toRelation lts μ) + (LTS.MTr.toRelation lts (μs ++ [μ])) where trans := by intro s1 s2 s3 hmtr1 htr2 - apply Lts.MTr.single at htr2 - apply Lts.MTr.comp lts hmtr1 htr2 + apply LTS.MTr.single at htr2 + apply LTS.MTr.comp lts hmtr1 htr2 /-- Multi-step transitions can be chained. -/ -instance (lts : Lts State Label) : +instance (lts : LTS State Label) : Trans - (Lts.MTr.toRelation lts μs1) - (Lts.MTr.toRelation lts μs2) - (Lts.MTr.toRelation lts (μs1 ++ μs2)) where + (LTS.MTr.toRelation lts μs1) + (LTS.MTr.toRelation lts μs2) + (LTS.MTr.toRelation lts (μs1 ++ μs2)) where trans := by intro s1 s2 s3 hmtr1 hmtr2 - apply Lts.MTr.comp lts hmtr1 hmtr2 + apply LTS.MTr.comp lts hmtr1 hmtr2 end Trans open Lean Elab Meta Command Term -/-- A command to create an `Lts` from a labelled transition `α → β → α → Prop`, robust to use of +/-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of `variable `-/ elab "create_lts" lt:ident name:ident : command => do liftTermElabM do @@ -584,7 +584,7 @@ elab "create_lts" lt:ident name:ident : command => do throwError m!"expecting Prop, not{indentExpr ty}" let params := ci.levelParams.map .param let lt := mkAppN (.const lt params) args[0:args.size-3] - let bundle ← mkAppM ``Lts.mk #[lt] + let bundle ← mkAppM ``LTS.mk #[lt] let value ← mkLambdaFVars args[0:args.size-3] bundle let type ← inferType value addAndCompile <| .defnDecl { @@ -599,7 +599,7 @@ elab "create_lts" lt:ident name:ident : command => do addDeclarationRangesFromSyntax name.getId name /-- - This command adds transition notations for an `Lts`. This should not usually be called directly, + This command adds transition notations for an `LTS`. This should not usually be called directly, but from the `lts` attribute. As an example `lts_transition_notation foo "β"` will add the notations "[⬝]⭢β" and "[⬝]↠β" @@ -612,13 +612,13 @@ syntax "lts_transition_notation" ident (str)? : command macro_rules | `(lts_transition_notation $lts $sym) => `( - notation3 t:39 "["μ"]⭢" $sym:str t':39 => (Lts.Tr.toRelation $lts μ) t t' - notation3 t:39 "["μs"]↠" $sym:str t':39 => (Lts.MTr.toRelation $lts μs) t t' + notation3 t:39 "["μ"]⭢" $sym:str t':39 => (LTS.Tr.toRelation $lts μ) t t' + notation3 t:39 "["μs"]↠" $sym:str t':39 => (LTS.MTr.toRelation $lts μs) t t' ) | `(lts_transition_notation $lts) => `( - notation3 t:39 "["μ"]⭢" t':39 => (Lts.Tr.toRelation $lts μ) t t' - notation3 t:39 "["μs"]↠" t':39 => (Lts.MTr.toRelation $lts μs) t t' + notation3 t:39 "["μ"]⭢" t':39 => (LTS.Tr.toRelation $lts μ) t t' + notation3 t:39 "["μs"]↠" t':39 => (LTS.MTr.toRelation $lts μs) t t' ) /-- This attribute calls the `lts_transition_notation` command for the annotated declaration. -/ @@ -626,7 +626,7 @@ syntax (name := lts_attr) "lts" ident (ppSpace str)? : attr initialize Lean.registerBuiltinAttribute { name := `lts_attr - descr := "Register notation for an Lts" + descr := "Register notation for an LTS" add := fun decl stx _ => MetaM.run' do match stx with | `(attr | lts $lts $sym) => diff --git a/Cslib/Foundations/Semantics/Lts/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean similarity index 87% rename from Cslib/Foundations/Semantics/Lts/Bisimulation.lean rename to Cslib/Foundations/Semantics/LTS/Bisimulation.lean index fd805642..92b32900 100644 --- a/Cslib/Foundations/Semantics/Lts/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -4,21 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic -import Cslib.Foundations.Semantics.Lts.TraceEq +import Cslib.Foundations.Semantics.LTS.Basic +import Cslib.Foundations.Semantics.LTS.TraceEq import Cslib.Foundations.Data.Relation -import Cslib.Foundations.Semantics.Lts.Simulation +import Cslib.Foundations.Semantics.LTS.Simulation import Mathlib.Order.CompleteLattice.Defs /-! # Bisimulation and Bisimilarity -A bisimulation is a binary relation on the states of an `Lts`, which establishes a tight semantic +A bisimulation is a binary relation on the states of an `LTS`, which establishes a tight semantic correspondence. More specifically, if two states `s1` and `s2` are related by a bisimulation, then `s1` can mimic all transitions of `s2` and vice versa. Furthermore, the derivatives reaches through these transitions remain related by the bisimulation. -Bisimilarity is the largest bisimulation: given an `Lts`, it relates any two states that are related -by a bisimulation for that Lts. +Bisimilarity is the largest bisimulation: given an `LTS`, it relates any two states that are related +by a bisimulation for that LTS. Weak bisimulation (resp. bisimilarity) is the relaxed version of bisimulation (resp. bisimilarity) whereby internal actions performed by processes can be ignored. @@ -33,7 +33,7 @@ related by some bisimulation on `lts`. - `lts.IsBisimulationUpTo r`: the relation `r` is a bisimulation up to bisimilarity (this is known as one of the 'up to' techniques for bisimulation). -- `lts.IsWeakBisimulation r`: the relation `r` on the states of the Lts `lts` is a weak +- `lts.IsWeakBisimulation r`: the relation `r` on the states of the LTS `lts` is a weak bisimulation. - `WeakBisimilarity lts` is the binary relation on the states of `lts` that relates any two states related by some weak bisimulation on `lts`. @@ -44,24 +44,24 @@ related by some sw-bisimulation on `lts`. ## Notations -- `s1 ~[lts] s2`: the states `s1` and `s2` are bisimilar in the Lts `lts`. -- `s1 ≈[lts] s2`: the states `s1` and `s2` are weakly bisimilar in the Lts `lts`. -- `s1 ≈sw[lts] s2`: the states `s1` and `s2` are sw bisimilar in the Lts `lts`. +- `s1 ~[lts] s2`: the states `s1` and `s2` are bisimilar in the LTS `lts`. +- `s1 ≈[lts] s2`: the states `s1` and `s2` are weakly bisimilar in the LTS `lts`. +- `s1 ≈sw[lts] s2`: the states `s1` and `s2` are sw bisimilar in the LTS `lts`. ## Main statements -- `Lts.IsBisimulation.inv`: the inverse of a bisimulation is a bisimulation. +- `LTS.IsBisimulation.inv`: the inverse of a bisimulation is a bisimulation. - `Bisimilarity.eqv`: bisimilarity is an equivalence relation (see `Equivalence`). - `Bisimilarity.isBisimulation`: bisimilarity is itself a bisimulation. - `Bisimilarity.largest_bisimulation`: bisimilarity is the largest bisimulation. - `Bisimilarity.gfp`: the union of bisimilarity and any bisimulation is equal to bisimilarity. -- `Lts.IsBisimulationUpTo.isBisimulation`: any bisimulation up to bisimilarity is a bisimulation. -- `Lts.IsBisimulation.traceEq`: any bisimulation that relates two states implies that they are +- `LTS.IsBisimulationUpTo.isBisimulation`: any bisimulation up to bisimilarity is a bisimulation. +- `LTS.IsBisimulation.traceEq`: any bisimulation that relates two states implies that they are trace equivalent (see `TraceEq`). -- `Bisimilarity.deterministic_bisim_eq_traceEq`: in a deterministic Lts, bisimilarity and trace +- `Bisimilarity.deterministic_bisim_eq_traceEq`: in a deterministic LTS, bisimilarity and trace equivalence coincide. - `WeakBisimilarity.weakBisim_eq_swBisim`: weak bisimilarity and sw-bisimilarity coincide in all -Ltss. +LTSs. - `WeakBisimilarity.eqv`: weak bisimilarity is an equivalence relation. - `SWBisimilarity.eqv`: sw-bisimilarity is an equivalence relation. @@ -71,22 +71,22 @@ universe u v section Bisimulation -variable {State : Type u} {Label : Type v} {lts : Lts State Label} +variable {State : Type u} {Label : Type v} {lts : LTS State Label} /-- A relation is a bisimulation if, whenever it relates two states in an lts, the transitions originating from these states mimic each other and the reached derivatives are themselves related. -/ @[grind] -def Lts.IsBisimulation (lts : Lts State Label) (r : State → State → Prop) : Prop := +def LTS.IsBisimulation (lts : LTS State Label) (r : State → State → Prop) : Prop := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2') ∧ (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2') ) -/- Semi-bundled version of `Lts.IsBisimulation`. -/ +/- Semi-bundled version of `LTS.IsBisimulation`. -/ -- @[grind ext] --- structure Bisimulation (lts : Lts State Label) where +-- structure Bisimulation (lts : LTS State Label) where -- /-- The relation on the states of the lts. -/ -- rel : State → State → Prop -- /-- Proof that the relation is a bisimulation. -/ @@ -97,20 +97,20 @@ def Lts.IsBisimulation (lts : Lts State Label) (r : State → State → Prop) : -- coe := fun bisim => bisim.rel /-- Helper for following a transition by the first state in a pair of a `Bisimulation`. -/ -theorem Lts.IsBisimulation.follow_fst +theorem LTS.IsBisimulation.follow_fst (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') : ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' := (hb hr μ).1 _ htr /-- Helper for following a transition by the second state in a pair of a `Bisimulation`. -/ -theorem Lts.IsBisimulation.follow_snd +theorem LTS.IsBisimulation.follow_snd (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') : ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2' := (hb hr μ).2 _ htr /-- Two states are bisimilar if they are related by some bisimulation. -/ @[grind] -def Bisimilarity (lts : Lts State Label) : State → State → Prop := +def Bisimilarity (lts : LTS State Label) : State → State → Prop := fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsBisimulation r /-- @@ -129,7 +129,7 @@ theorem Bisimilarity.refl (s : State) : s ~[lts] s := by /-- The inverse of a bisimulation is a bisimulation. -/ @[grind] -theorem Lts.IsBisimulation.inv (h : lts.IsBisimulation r) : +theorem LTS.IsBisimulation.inv (h : lts.IsBisimulation r) : lts.IsBisimulation (flip r) := by grind [flip] /-- Bisimilarity is symmetric. -/ @@ -141,7 +141,7 @@ theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := b /-- The composition of two bisimulations is a bisimulation. -/ @[grind] -theorem Lts.IsBisimulation.comp +theorem LTS.IsBisimulation.comp (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) : lts.IsBisimulation (Relation.Comp r1 r2) := by grind [Relation.Comp] @@ -295,7 +295,7 @@ end Order states in an lts, the transitions originating from these states mimic each other and the reached derivatives are themselves related by `r` up to bisimilarity. -/ @[grind] -def Lts.IsBisimulationUpTo (lts : Lts State Label) (r : State → State → Prop) : Prop := +def LTS.IsBisimulationUpTo (lts : LTS State Label) (r : State → State → Prop) : Prop := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ Relation.UpTo r (Bisimilarity lts) s1' s2') ∧ @@ -304,7 +304,7 @@ def Lts.IsBisimulationUpTo (lts : Lts State Label) (r : State → State → Prop /-- Any bisimulation up to bisimilarity is a bisimulation. -/ @[grind] -theorem Lts.IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) : +theorem LTS.IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) : lts.IsBisimulation (Relation.UpTo r (Bisimilarity lts)) := by intro s1 s2 hr μ rcases hr with ⟨s1b, hr1b, s2b, hrb, hr2b⟩ @@ -389,7 +389,7 @@ theorem Bisimulation.bisim_trace /-- Any bisimulation implies trace equivalence. -/ @[grind] -theorem Lts.IsBisimulation.traceEq +theorem LTS.IsBisimulation.traceEq (hb : lts.IsBisimulation r) (hr : r s1 s2) : s1 ~tr[lts] s2 := by funext μs @@ -431,10 +431,10 @@ private inductive BisimMotTr : ℕ → Char → ℕ → Prop where /-- In general, trace equivalence is not a bisimulation (extra conditions are needed, see for example `Bisimulation.deterministic_trace_eq_is_bisim`). -/ theorem Bisimulation.traceEq_not_bisim : - ∃ (State : Type) (Label : Type) (lts : Lts State Label), ¬(lts.IsBisimulation (TraceEq lts)) := by + ∃ (State : Type) (Label : Type) (lts : LTS State Label), ¬(lts.IsBisimulation (TraceEq lts)) := by exists ℕ exists Char - let lts := Lts.mk BisimMotTr + let lts := LTS.mk BisimMotTr exists lts intro h -- specialize h 1 5 @@ -472,18 +472,18 @@ theorem Bisimulation.traceEq_not_bisim : case inl h1 => simp only [h1] exists 2 - apply Lts.MTr.single; constructor + apply LTS.MTr.single; constructor case inr h1 => cases h1 case inl h1 => simp only [h1] exists 3 - constructor; apply BisimMotTr.one2two; apply Lts.MTr.single; + constructor; apply BisimMotTr.one2two; apply LTS.MTr.single; apply BisimMotTr.two2three case inr h1 => cases h1 exists 4 - constructor; apply BisimMotTr.one2two; apply Lts.MTr.single; + constructor; apply BisimMotTr.one2two; apply LTS.MTr.single; apply BisimMotTr.two2four have htraces2 : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by apply Set.ext_iff.2 @@ -529,18 +529,18 @@ theorem Bisimulation.traceEq_not_bisim : case inl h1 => simp only [h1] exists 6 - apply Lts.MTr.single; constructor + apply LTS.MTr.single; constructor case inr h1 => cases h1 case inl h1 => simp only [h1] exists 7 - constructor; apply BisimMotTr.five2six; apply Lts.MTr.single; + constructor; apply BisimMotTr.five2six; apply LTS.MTr.single; apply BisimMotTr.six2seven case inr h1 => cases h1 exists 9 - constructor; apply BisimMotTr.five2eight; apply Lts.MTr.single; + constructor; apply BisimMotTr.five2eight; apply LTS.MTr.single; apply BisimMotTr.eight2nine simp [htraces1, htraces2] specialize h htreq @@ -690,7 +690,7 @@ theorem Bisimulation.traceEq_not_bisim : /-- In general, bisimilarity and trace equivalence are distinct. -/ theorem Bisimilarity.bisimilarity_neq_traceEq : - ∃ (State : Type) (Label : Type) (lts : Lts State Label), Bisimilarity lts ≠ TraceEq lts := by + ∃ (State : Type) (Label : Type) (lts : LTS State Label), Bisimilarity lts ≠ TraceEq lts := by obtain ⟨State, Label, lts, h⟩ := Bisimulation.traceEq_not_bisim exists State; exists Label; exists lts intro heq @@ -698,11 +698,11 @@ theorem Bisimilarity.bisimilarity_neq_traceEq : rw [heq] at hb contradiction -/-- In any deterministic Lts, trace equivalence is a bisimulation. -/ +/-- In any deterministic LTS, trace equivalence is a bisimulation. -/ theorem Bisimulation.deterministic_traceEq_is_bisim (hdet : lts.Deterministic) : (lts.IsBisimulation (TraceEq lts)) := by - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 hteq μ constructor case left => @@ -719,7 +719,7 @@ theorem Bisimulation.deterministic_traceEq_is_bisim case right => apply h.2.symm -/-- In any deterministic Lts, trace equivalence implies bisimilarity. -/ +/-- In any deterministic LTS, trace equivalence implies bisimilarity. -/ theorem Bisimilarity.deterministic_traceEq_bisim (hdet : lts.Deterministic) (h : s1 ~tr[lts] s2) : (s1 ~[lts] s2) := by @@ -730,9 +730,9 @@ theorem Bisimilarity.deterministic_traceEq_bisim case right => apply Bisimulation.deterministic_traceEq_is_bisim hdet -/-- In any deterministic Lts, bisimilarity and trace equivalence coincide. -/ +/-- In any deterministic LTS, bisimilarity and trace equivalence coincide. -/ theorem Bisimilarity.deterministic_bisim_eq_traceEq - (lts : Lts State Label) (hdet : lts.Deterministic) : + (lts : LTS State Label) (hdet : lts.Deterministic) : Bisimilarity lts = TraceEq lts := by funext s1 s2 simp only [eq_iff_iff] @@ -745,16 +745,16 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq /-! ## Relation to simulation -/ /-- Any bisimulation is also a simulation. -/ -theorem Bisimulation.is_simulation (lts : Lts State Label) (r : State → State → Prop) : +theorem Bisimulation.is_simulation (lts : LTS State Label) (r : State → State → Prop) : lts.IsBisimulation r → Simulation lts r := by grind [Simulation] /-- A relation is a bisimulation iff both it and its inverse are simulations. -/ -theorem Bisimulation.simulation_iff (lts : Lts State Label) (r : State → State → Prop) : +theorem Bisimulation.simulation_iff (lts : LTS State Label) (r : State → State → Prop) : lts.IsBisimulation r ↔ (Simulation lts r ∧ Simulation lts (flip r)) := by constructor case mp => grind [Simulation, flip] - case mpr => aesop (add simp [Lts.IsBisimulation]) + case mpr => aesop (add simp [LTS.IsBisimulation]) end Bisimulation @@ -763,12 +763,12 @@ section WeakBisimulation /-! ## Weak bisimulation and weak bisimilarity -/ /-- A weak bisimulation is similar to a `Bisimulation`, but allows for the related processes to do -internal work. Technically, this is defined as a `Bisimulation` on the saturation of the Lts. -/ -def Lts.IsWeakBisimulation [HasTau Label] (lts : Lts State Label) (r : State → State → Prop) := +internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTS. -/ +def LTS.IsWeakBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) := lts.saturate.IsBisimulation r /-- Two states are weakly bisimilar if they are related by some weak bisimulation. -/ -def WeakBisimilarity [HasTau Label] (lts : Lts State Label) : State → State → Prop := +def WeakBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop := fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsWeakBisimulation r @@ -778,7 +778,7 @@ notation s:max " ≈[" lts "] " s':max => WeakBisimilarity lts s s' /-- An `SWBisimulation` is a more convenient definition of weak bisimulation, because the challenge is a single transition. We prove later that this technique is sound, following a strategy inspired by [Sangiorgi2011]. -/ -def Lts.IsSWBisimulation [HasTau Label] (lts : Lts State Label) (r : State → State → Prop) : Prop := +def LTS.IsSWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) : Prop := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.STr s2 μ s2' ∧ r s1' s2') ∧ @@ -786,7 +786,7 @@ def Lts.IsSWBisimulation [HasTau Label] (lts : Lts State Label) (r : State → S ) /-- Two states are sw-bisimilar if they are related by some sw-bisimulation. -/ -def SWBisimilarity [HasTau Label] (lts : Lts State Label) : State → State → Prop := +def SWBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop := fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsSWBisimulation r @@ -796,7 +796,7 @@ notation s:max " ≈sw[" lts "] " s':max => SWBisimilarity lts s s' /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (first component, weighted version). -/ theorem SWBisimulation.follow_internal_fst_n - [HasTau Label] {lts : Lts State Label} + [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.strN n s1 HasTau.τ s1') : ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by cases n @@ -817,13 +817,13 @@ theorem SWBisimulation.follow_internal_fst_n obtain ⟨s2', hstrs2', hrs2⟩ := ih2 exists s2' constructor - · apply Lts.STr.trans_τ lts (Lts.STr.trans_τ lts hstrs2 hstrsb2) hstrs2' + · apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs2 hstrsb2) hstrs2' · exact hrs2 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (second component, weighted version). -/ theorem SWBisimulation.follow_internal_snd_n - [HasTau Label] {lts : Lts State Label} + [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.strN n s2 HasTau.τ s2') : ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by cases n @@ -844,31 +844,31 @@ theorem SWBisimulation.follow_internal_snd_n obtain ⟨s2', hstrs2', hrs2⟩ := ih2 exists s2' constructor - · apply Lts.STr.trans_τ lts (Lts.STr.trans_τ lts hstrs1 hstrsb2) hstrs2' + · apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs1 hstrsb2) hstrs2' · exact hrs2 /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (first component). -/ theorem SWBisimulation.follow_internal_fst - [HasTau Label] {lts : Lts State Label} + [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') : ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by - obtain ⟨n, hstrN⟩ := (Lts.str_strN lts).1 hstr + obtain ⟨n, hstrN⟩ := (LTS.str_strN lts).1 hstr apply SWBisimulation.follow_internal_fst_n hswb hr hstrN /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (second component). -/ theorem SWBisimulation.follow_internal_snd - [HasTau Label] {lts : Lts State Label} + [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') : ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by - obtain ⟨n, hstrN⟩ := (Lts.str_strN lts).1 hstr + obtain ⟨n, hstrN⟩ := (LTS.str_strN lts).1 hstr apply SWBisimulation.follow_internal_snd_n hswb hr hstrN /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`. This formalises lemma 4.2.10 in [Sangiorgi2011]. -/ -theorem Lts.isWeakBisimulation_iff_isSWBisimulation - [HasTau Label] {lts : Lts State Label} : +theorem LTS.isWeakBisimulation_iff_isSWBisimulation + [HasTau Label] {lts : LTS State Label} : lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r := by apply Iff.intro case mp => @@ -877,13 +877,13 @@ theorem Lts.isWeakBisimulation_iff_isSWBisimulation case left => intro s1' htr specialize h hr μ - have h' := h.1 s1' (Lts.STr.single lts htr) + have h' := h.1 s1' (LTS.STr.single lts htr) obtain ⟨s2', htr2, hr2⟩ := h' exists s2' case right => intro s2' htr specialize h hr μ - have h' := h.2 s2' (Lts.STr.single lts htr) + have h' := h.2 s2' (LTS.STr.single lts htr) obtain ⟨s1', htr1, hr1⟩ := h' exists s1' case mpr => @@ -902,7 +902,7 @@ theorem Lts.isWeakBisimulation_iff_isSWBisimulation obtain ⟨s2', hstr2', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2 exists s2' constructor - · exact Lts.STr.comp lts hstr2b hstr2b' hstr2' + · exact LTS.STr.comp lts hstr2b hstr2b' hstr2' · exact hrb2 case right => intro s2' hstr @@ -917,29 +917,29 @@ theorem Lts.isWeakBisimulation_iff_isSWBisimulation obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2 exists s1' constructor - · exact Lts.STr.comp lts hstr1b hstr1b' hstr1' + · exact LTS.STr.comp lts hstr1b hstr1b' hstr1' · exact hrb2 theorem WeakBisimulation.toSwBisimulation - [HasTau Label] {lts : Lts State Label} {r : State → State → Prop} (h : lts.IsWeakBisimulation r) : - lts.IsSWBisimulation r := Lts.isWeakBisimulation_iff_isSWBisimulation.1 h + [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsWeakBisimulation r) : + lts.IsSWBisimulation r := LTS.isWeakBisimulation_iff_isSWBisimulation.1 h theorem SWBisimulation.toWeakBisimulation - [HasTau Label] {lts : Lts State Label} {r : State → State → Prop} (h : lts.IsSWBisimulation r) : - lts.IsWeakBisimulation r := Lts.isWeakBisimulation_iff_isSWBisimulation.2 h + [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsSWBisimulation r) : + lts.IsWeakBisimulation r := LTS.isWeakBisimulation_iff_isSWBisimulation.2 h /-- If two states are related by an `SWBisimulation`, then they are weakly bisimilar. -/ theorem WeakBisimilarity.by_swBisimulation [HasTau Label] - (lts : Lts State Label) (r : State → State → Prop) + (lts : LTS State Label) (r : State → State → Prop) (hb : lts.IsSWBisimulation r) (hr : r s1 s2) : s1 ≈[lts] s2 := by exists r constructor · exact hr - apply Lts.isWeakBisimulation_iff_isSWBisimulation.2 hb + apply LTS.isWeakBisimulation_iff_isSWBisimulation.2 hb -/-- Weak bisimilarity and sw-bisimilarity coincide for all Ltss. -/ +/-- Weak bisimilarity and sw-bisimilarity coincide for all LTSs. -/ @[grind _=_] -theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : Lts State Label) : +theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : LTS State Label) : WeakBisimilarity lts = SWBisimilarity lts := by funext s1 s2 simp only [eq_iff_iff] @@ -950,21 +950,21 @@ theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : Lts State La exists r constructor · exact hr - apply Lts.isWeakBisimulation_iff_isSWBisimulation.1 hrh + apply LTS.isWeakBisimulation_iff_isSWBisimulation.1 hrh case mpr => intro h obtain ⟨r, hr, hrh⟩ := h exists r constructor · exact hr - apply Lts.isWeakBisimulation_iff_isSWBisimulation.2 hrh + apply LTS.isWeakBisimulation_iff_isSWBisimulation.2 hrh /-- sw-bisimilarity is reflexive. -/ -theorem SWBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) : s ≈sw[lts] s := by +theorem SWBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : s ≈sw[lts] s := by exists Eq constructor · rfl - simp only [Lts.IsSWBisimulation] + simp only [LTS.IsSWBisimulation] intro s1 s2 hr μ cases hr constructor @@ -972,26 +972,26 @@ theorem SWBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) : intro s1' htr exists s1' constructor - · apply Lts.STr.single _ htr + · apply LTS.STr.single _ htr · constructor case right => intro s2' htr exists s2' constructor - · apply Lts.STr.single _ htr + · apply LTS.STr.single _ htr · constructor /-- Weak bisimilarity is reflexive. -/ -theorem WeakBisimilarity.refl [HasTau Label] (lts : Lts State Label) (s : State) : s ≈[lts] s := by +theorem WeakBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : s ≈[lts] s := by rw [WeakBisimilarity.weakBisim_eq_swBisim lts] apply SWBisimilarity.refl /-- The inverse of an sw-bisimulation is an sw-bisimulation. -/ -theorem SWBisimulation.inv [HasTau Label] (lts : Lts State Label) +theorem SWBisimulation.inv [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) (h : lts.IsSWBisimulation r) : lts.IsSWBisimulation (flip r) := by - simp only [Lts.IsSWBisimulation] at h - simp only [Lts.IsSWBisimulation] + simp only [LTS.IsSWBisimulation] at h + simp only [LTS.IsSWBisimulation] intro s1 s2 hrinv μ constructor case left => @@ -1008,7 +1008,7 @@ theorem SWBisimulation.inv [HasTau Label] (lts : Lts State Label) exists s1' /-- The inverse of a weak bisimulation is a weak bisimulation. -/ -theorem WeakBisimulation.inv [HasTau Label] (lts : Lts State Label) +theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) (h : lts.IsWeakBisimulation r) : lts.IsWeakBisimulation (flip r) := by apply WeakBisimulation.toSwBisimulation at h @@ -1017,7 +1017,7 @@ theorem WeakBisimulation.inv [HasTau Label] (lts : Lts State Label) exact h' /-- sw-bisimilarity is symmetric. -/ -theorem SWBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈sw[lts] s2) : +theorem SWBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈sw[lts] s2) : s2 ≈sw[lts] s1 := by obtain ⟨r, hr, hrh⟩ := h exists (flip r) @@ -1029,7 +1029,7 @@ theorem SWBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈sw apply SWBisimulation.inv lts r hrh /-- Weak bisimilarity is symmetric. -/ -theorem WeakBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈[lts] s2) : +theorem WeakBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈[lts] s2) : s2 ≈[lts] s1 := by rw [WeakBisimilarity.weakBisim_eq_swBisim] rw [WeakBisimilarity.weakBisim_eq_swBisim] at h @@ -1038,26 +1038,26 @@ theorem WeakBisimilarity.symm [HasTau Label] (lts : Lts State Label) (h : s1 ≈ /-- The composition of two weak bisimulations is a weak bisimulation. -/ theorem WeakBisimulation.comp [HasTau Label] - (lts : Lts State Label) + (lts : LTS State Label) (r1 r2 : State → State → Prop) (h1 : lts.IsWeakBisimulation r1) (h2 : lts.IsWeakBisimulation r2) : lts.IsWeakBisimulation (Relation.Comp r1 r2) := by - simp_all only [Lts.IsWeakBisimulation] + simp_all only [LTS.IsWeakBisimulation] exact h1.comp h2 /-- The composition of two sw-bisimulations is an sw-bisimulation. -/ theorem SWBisimulation.comp [HasTau Label] - (lts : Lts State Label) + (lts : LTS State Label) (r1 r2 : State → State → Prop) (h1 : lts.IsSWBisimulation r1) (h2 : lts.IsSWBisimulation r2) : lts.IsSWBisimulation (Relation.Comp r1 r2) := by apply SWBisimulation.toWeakBisimulation at h1 apply SWBisimulation.toWeakBisimulation at h2 - apply Lts.isWeakBisimulation_iff_isSWBisimulation.1 + apply LTS.isWeakBisimulation_iff_isSWBisimulation.1 apply WeakBisimulation.comp lts r1 r2 h1 h2 /-- Weak bisimilarity is transitive. -/ theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State} - (lts : Lts State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3 := by + (lts : LTS State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3 := by obtain ⟨r1, hr1, hr1b⟩ := h1 obtain ⟨r2, hr2, hr2b⟩ := h2 exists Relation.Comp r1 r2 @@ -1069,12 +1069,12 @@ theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State} /-- sw-bisimilarity is transitive. -/ theorem SWBisimilarity.trans [HasTau Label] {s1 s2 s3 : State} - (lts : Lts State Label) (h1 : s1 ≈sw[lts] s2) (h2 : s2 ≈sw[lts] s3) : s1 ≈sw[lts] s3 := by + (lts : LTS State Label) (h1 : s1 ≈sw[lts] s2) (h2 : s2 ≈sw[lts] s3) : s1 ≈sw[lts] s3 := by rw [← (WeakBisimilarity.weakBisim_eq_swBisim lts)] at * apply WeakBisimilarity.trans lts h1 h2 /-- Weak bisimilarity is an equivalence relation. -/ -theorem WeakBisimilarity.eqv [HasTau Label] {lts : Lts State Label} : +theorem WeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : Equivalence (WeakBisimilarity lts) := { refl := WeakBisimilarity.refl lts symm := WeakBisimilarity.symm lts @@ -1082,7 +1082,7 @@ theorem WeakBisimilarity.eqv [HasTau Label] {lts : Lts State Label} : } /-- SW-bisimilarity is an equivalence relation. -/ -theorem SWBisimilarity.eqv [HasTau Label] {lts : Lts State Label} : +theorem SWBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : Equivalence (SWBisimilarity lts) := { refl := SWBisimilarity.refl lts symm := SWBisimilarity.symm lts diff --git a/Cslib/Foundations/Semantics/Lts/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean similarity index 86% rename from Cslib/Foundations/Semantics/Lts/Simulation.lean rename to Cslib/Foundations/Semantics/LTS/Simulation.lean index 9e69c92a..7b6066d4 100644 --- a/Cslib/Foundations/Semantics/Lts/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -4,23 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic +import Cslib.Foundations.Semantics.LTS.Basic import Cslib.Foundations.Data.Relation /-! # Simulation and Similarity -A simulation is a binary relation on the states of an `Lts`: if two states `s1` and `s2` are +A simulation is a binary relation on the states of an `LTS`: if two states `s1` and `s2` are related by a simulation, then `s2` can mimic all transitions of `s1`. Furthermore, the derivatives reaches through these transitions remain related by the simulation. -Similarity is the largest simulation: given an `Lts`, it relates any two states that are related -by a simulation for that Lts. +Similarity is the largest simulation: given an `LTS`, it relates any two states that are related +by a simulation for that LTS. For an introduction to theory of simulation, we refer to [Sangiorgi2011]. ## Main definitions -- `Simulation lts r`: the relation `r` on the states of the Lts `lts` is a simulation. +- `Simulation lts r`: the relation `r` on the states of the LTS `lts` is a simulation. - `Similarity lts` is the binary relation on the states of `lts` that relates any two states related by some simulation on `lts`. - `SimulationEquiv lts` is the binary relation on the states of `lts` that relates any two states @@ -28,8 +28,8 @@ similar to each other. ## Notations -- `s1 ≤[lts] s2`: the states `s1` and `s2` are similar in the Lts `lts`. -- `s1 ≤≥[lts] s2`: the states `s1` and `s2` are simulation equivalent in the Lts `lts`. +- `s1 ≤[lts] s2`: the states `s1` and `s2` are similar in the LTS `lts`. +- `s1 ≤≥[lts] s2`: the states `s1` and `s2` are simulation equivalent in the LTS `lts`. ## Main statements @@ -41,16 +41,16 @@ universe u v section Simulation -variable {State : Type u} {Label : Type v} (lts : Lts State Label) +variable {State : Type u} {Label : Type v} (lts : LTS State Label) /-- A relation is a simulation if, whenever it relates two states in an lts, any transition originating from the first state is mimicked by a transition from the second state and the reached derivatives are themselves related. -/ -def Simulation (lts : Lts State Label) (r : State → State → Prop) : Prop := +def Simulation (lts : LTS State Label) (r : State → State → Prop) : Prop := ∀ s1 s2, r s1 s2 → ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' /-- Two states are similar if they are related by some simulation. -/ -def Similarity (lts : Lts State Label) : State → State → Prop := +def Similarity (lts : LTS State Label) : State → State → Prop := fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ Simulation lts r @@ -98,7 +98,7 @@ theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lt /-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts] s2` and `s2 ≤[lts] s1`. -/ -def SimulationEquiv (lts : Lts State Label) : State → State → Prop := +def SimulationEquiv (lts : LTS State Label) : State → State → Prop := fun s1 s2 => s1 ≤[lts] s2 ∧ s2 ≤[lts] s1 @@ -121,7 +121,7 @@ theorem SimulationEquiv.trans {s1 s2 s3 : State} (h1 : s1 ≤≥[lts] s2) (h2 : grind [SimulationEquiv, Similarity.trans] /-- Simulation equivalence is an equivalence relation. -/ -theorem SimulationEquiv.eqv (lts : Lts State Label) : +theorem SimulationEquiv.eqv (lts : LTS State Label) : Equivalence (SimulationEquiv lts) := { refl := SimulationEquiv.refl lts symm := SimulationEquiv.symm lts diff --git a/Cslib/Foundations/Semantics/Lts/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean similarity index 71% rename from Cslib/Foundations/Semantics/Lts/TraceEq.lean rename to Cslib/Foundations/Semantics/LTS/TraceEq.lean index 0ecd49e0..adc8806e 100644 --- a/Cslib/Foundations/Semantics/Lts/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -4,17 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic +import Cslib.Foundations.Semantics.LTS.Basic import Mathlib.Data.Set.Finite.Basic /-! # Trace Equivalence -Definitions and results on trace equivalence for `Lts`s. +Definitions and results on trace equivalence for `LTS`s. ## Main definitions -- `Lts.traces`: the set of traces of a state. +- `LTS.traces`: the set of traces of a state. - `TraceEq s1 s2`: `s1` and `s2` are trace equivalent, i.e., they have the same sets of traces. ## Notations @@ -24,21 +24,21 @@ Definitions and results on trace equivalence for `Lts`s. ## Main statements - `TraceEq.eqv`: trace equivalence is an equivalence relation (see `Equivalence`). -- `TraceEq.deterministic_sim`: in any deterministic `Lts`, trace equivalence is a simulation. +- `TraceEq.deterministic_sim`: in any deterministic `LTS`, trace equivalence is a simulation. -/ universe u v -variable {State : Type u} {Label : Type v} (lts : Lts State Label) +variable {State : Type u} {Label : Type v} (lts : LTS State Label) /-- The traces of a state `s` is the set of all lists of labels `μs` such that there is a multi-step transition labelled by `μs` originating from `s`. -/ -def Lts.traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } +def LTS.traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } /-- If there is a multi-step transition from `s` labelled by `μs`, then `μs` is in the traces of `s`. -/ -theorem Lts.traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') : +theorem LTS.traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') : μs ∈ lts.traces s := by exists s' @@ -58,7 +58,7 @@ theorem TraceEq.refl (s : State) : s ~tr[lts] s := by simp only [TraceEq] /-- Trace equivalence is symmetric. -/ -theorem TraceEq.symm (lts : Lts State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) : +theorem TraceEq.symm (lts : LTS State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) : s2 ~tr[lts] s1 := by simp only [TraceEq] at h simp only [TraceEq] @@ -71,7 +71,7 @@ theorem TraceEq.trans {s1 s2 s3 : State} (h1 : s1 ~tr[lts] s2) (h2 : s2 ~tr[lts] rw [h1, h2] /-- Trace equivalence is an equivalence relation. -/ -theorem TraceEq.eqv (lts : Lts State Label) : Equivalence (TraceEq lts) := { +theorem TraceEq.eqv (lts : LTS State Label) : Equivalence (TraceEq lts) := { refl := TraceEq.refl lts symm := TraceEq.symm lts trans := TraceEq.trans lts @@ -81,19 +81,19 @@ theorem TraceEq.eqv (lts : Lts State Label) : Equivalence (TraceEq lts) := { instance : Trans (TraceEq lts) (TraceEq lts) (TraceEq lts) where trans := TraceEq.trans lts -/-- In a deterministic Lts, trace equivalence is a simulation. -/ +/-- In a deterministic LTS, trace equivalence is a simulation. -/ theorem TraceEq.deterministic_sim - (lts : Lts State Label) (hdet : lts.Deterministic) (s1 s2 : State) (h : s1 ~tr[lts] s2) : + (lts : LTS State Label) (hdet : lts.Deterministic) (s1 s2 : State) (h : s1 ~tr[lts] s2) : ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ s1' ~tr[lts] s2' := by intro μ s1' htr1 - have hmtr1 := Lts.MTr.single lts htr1 - have hin := Lts.traces_in lts s1 [μ] s1' hmtr1 + have hmtr1 := LTS.MTr.single lts htr1 + have hin := LTS.traces_in lts s1 [μ] s1' hmtr1 rw [h] at hin obtain ⟨s2', hmtr2⟩ := hin exists s2' constructor - · apply Lts.MTr.single_invert lts _ _ _ hmtr2 - · simp only [TraceEq, Lts.traces] + · apply LTS.MTr.single_invert lts _ _ _ hmtr2 + · simp only [TraceEq, LTS.traces] funext μs' simp only [eq_iff_iff] simp only [setOf] @@ -101,28 +101,28 @@ theorem TraceEq.deterministic_sim case mp => intro hmtr1' obtain ⟨s1'', hmtr1'⟩ := hmtr1' - have hmtr1comp := Lts.MTr.comp lts hmtr1 hmtr1' - have hin := Lts.traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp + have hmtr1comp := LTS.MTr.comp lts hmtr1 hmtr1' + have hin := LTS.traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp rw [h] at hin obtain ⟨s', hmtr2'⟩ := hin cases hmtr2' case stepL s2'' htr2 hmtr2' => exists s' - have htr2' := Lts.MTr.single_invert lts _ _ _ hmtr2 + have htr2' := LTS.MTr.single_invert lts _ _ _ hmtr2 have hdets2 := hdet s2 μ s2' s2'' htr2' htr2 rw [hdets2] exact hmtr2' case mpr => intro hmtr2' obtain ⟨s2'', hmtr2'⟩ := hmtr2' - have hmtr2comp := Lts.MTr.comp lts hmtr2 hmtr2' - have hin := Lts.traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp + have hmtr2comp := LTS.MTr.comp lts hmtr2 hmtr2' + have hin := LTS.traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp rw [← h] at hin obtain ⟨s', hmtr1'⟩ := hin cases hmtr1' case stepL s1'' htr1 hmtr1' => exists s' - have htr1' := Lts.MTr.single_invert lts _ _ _ hmtr1 + have htr1' := LTS.MTr.single_invert lts _ _ _ hmtr1 have hdets1 := hdet s1 μ s1' s1'' htr1' htr1 rw [hdets1] exact hmtr1' diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 4c627441..838aa0e8 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic -import Cslib.Foundations.Semantics.Lts.Bisimulation +import Cslib.Foundations.Semantics.LTS.Basic +import Cslib.Foundations.Semantics.LTS.Bisimulation import Cslib.Languages.CCS.Basic import Cslib.Languages.CCS.Semantics @@ -61,7 +61,7 @@ theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by case left => constructor case right => - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 hr μ cases hr case parComm p q => @@ -237,7 +237,7 @@ private inductive ChoiceComm : (Process Name Constant) → (Process Name Constan theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q p) := by exists @ChoiceComm Name Constant defs repeat constructor - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 hr μ cases hr case choiceComm => @@ -302,7 +302,7 @@ theorem bisimilarity_congr_pre : exists @PreBisim _ _ defs constructor · constructor; assumption - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 hr μ' cases hr case pre => @@ -355,7 +355,7 @@ theorem bisimilarity_congr_res : exists @ResBisim _ _ defs constructor · constructor; assumption - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 hr μ' cases hr rename_i p q a h @@ -390,7 +390,7 @@ theorem bisimilarity_congr_choice : exists @ChoiceBisim _ _ defs constructor · constructor; assumption - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 r μ constructor case left => @@ -458,7 +458,7 @@ theorem bisimilarity_congr_par : exists @ParBisim _ _ defs constructor · constructor; assumption - simp only [Lts.IsBisimulation] + simp only [LTS.IsBisimulation] intro s1 s2 r μ constructor case left => diff --git a/Cslib/Languages/CCS/Semantics.lean b/Cslib/Languages/CCS/Semantics.lean index 212b1473..65f183f5 100644 --- a/Cslib/Languages/CCS/Semantics.lean +++ b/Cslib/Languages/CCS/Semantics.lean @@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic +import Cslib.Foundations.Semantics.LTS.Basic import Cslib.Languages.CCS.Basic /-! # Semantics of CCS ## Main definitions - `CCS.Tr`: transition relation for CCS. -- `CCS.lts`: the `Lts` of CCS. +- `CCS.lts`: the `LTS` of CCS. -/ diff --git a/CslibTests/Bisimulation.lean b/CslibTests/Bisimulation.lean index 5b2f3818..ed2cb44e 100644 --- a/CslibTests/Bisimulation.lean +++ b/CslibTests/Bisimulation.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Bisimulation +import Cslib.Foundations.Semantics.LTS.Bisimulation /- An LTS with two bisimilar states. -/ private inductive tr1 : ℕ → Char → ℕ → Prop where @@ -17,7 +17,7 @@ private inductive tr1 : ℕ → Char → ℕ → Prop where | six2seven : tr1 6 'b' 7 | six2eight : tr1 6 'c' 8 -def lts1 := Lts.mk tr1 +def lts1 := LTS.mk tr1 private inductive Bisim15 : ℕ → ℕ → Prop where | oneFive : Bisim15 1 5 @@ -50,8 +50,8 @@ example : 1 ~[lts1] 5 := by -- (add simp Bisimulation) -- (add safe constructors Bisim15) -- (add safe cases Bisim15) - -- (add safe cases [Lts.mtr]) - -- (add simp Lts.tr) + -- (add safe cases [LTS.mtr]) + -- (add simp LTS.tr) -- (add safe constructors tr1) -- (add unsafe apply Bisimulation.follow_fst) -- (add unsafe apply Bisimulation.follow_snd) diff --git a/CslibTests/Dfa.lean b/CslibTests/DFA.lean similarity index 91% rename from CslibTests/Dfa.lean rename to CslibTests/DFA.lean index fd6a3463..1a436fe1 100644 --- a/CslibTests/Dfa.lean +++ b/CslibTests/DFA.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Dfa.Basic +import Cslib.Computability.Automata.DFA.Basic /-! A simple elevator. -/ @@ -39,7 +39,7 @@ def tr (floor : Floor) (dir : Direction) : Floor := | .two, .up => .two | .two, .down => .one -def elevator : Dfa Floor Direction := { +def elevator : DFA Floor Direction := { tr := tr start := .one accept := { Floor.one } diff --git a/CslibTests/Lts.lean b/CslibTests/LTS.lean similarity index 84% rename from CslibTests/Lts.lean rename to CslibTests/LTS.lean index 4f292dc2..7f24d5d8 100644 --- a/CslibTests/Lts.lean +++ b/CslibTests/LTS.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.Lts.Basic -import Cslib.Foundations.Semantics.Lts.Bisimulation +import Cslib.Foundations.Semantics.LTS.Basic +import Cslib.Foundations.Semantics.LTS.Bisimulation import Mathlib.Algebra.Group.Even import Mathlib.Algebra.Ring.Parity @@ -21,7 +21,7 @@ theorem NatTr.dom : NatTr n μ m → (n = 1 ∨ n = 2) ∧ (m = 1 ∨ m = 2) := intro h cases h <;> simp -def natLts : Lts ℕ ℕ := ⟨NatTr⟩ +def natLTS : LTS ℕ ℕ := ⟨NatTr⟩ inductive NatBisim : ℕ → ℕ → Prop where | one_one : NatBisim 1 1 @@ -29,7 +29,7 @@ inductive NatBisim : ℕ → ℕ → Prop where | two_one : NatBisim 2 1 | two_two : NatBisim 2 2 -example : 1 ~[natLts] 2 := by +example : 1 ~[natLTS] 2 := by exists NatBisim constructor · constructor @@ -50,32 +50,32 @@ instance : HasTau TLabel := { inductive NatDivergentTr : ℕ → TLabel → ℕ → Prop where | step : NatDivergentTr n τ n.succ -def natDivLts : Lts ℕ TLabel := ⟨NatDivergentTr⟩ +def natDivLTS : LTS ℕ TLabel := ⟨NatDivergentTr⟩ def natInfiniteExecution : Stream' ℕ := fun n => n theorem natInfiniteExecution.infiniteExecution : - natDivLts.DivergentExecution natInfiniteExecution := by + natDivLTS.DivergentExecution natInfiniteExecution := by intro n constructor -example : natDivLts.Divergent 0 := by +example : natDivLTS.Divergent 0 := by exists natInfiniteExecution constructor; constructor exact natInfiniteExecution.infiniteExecution -example : natDivLts.Divergent 3 := by +example : natDivLTS.Divergent 3 := by exists natInfiniteExecution.drop 3 constructor · constructor · intro; constructor -example : natDivLts.Divergent n := by +example : natDivLTS.Divergent n := by exists natInfiniteExecution.drop n simp only [Stream'.drop, zero_add] constructor · constructor - · apply Lts.divergent_drop + · apply LTS.divergent_drop exact natInfiniteExecution.infiniteExecution -- check that notation works @@ -104,7 +104,7 @@ end foo #guard_msgs in #check foo.bar -/-- info: foo.namespaced_lts : Lts ℕ ℕ -/ +/-- info: foo.namespaced_lts : LTS ℕ ℕ -/ #guard_msgs in #check foo.namespaced_lts From 69b0c1e8d31555207313e9180e0562fdf2ae41eb Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 29 Sep 2025 10:27:43 +0200 Subject: [PATCH 03/29] feat: introduce DA, plus some documentation for automata --- Cslib/Computability/Automata/DA.lean | 16 ++++++++++++++++ Cslib/Computability/Automata/DFA/Basic.lean | 7 ++----- Cslib/Computability/Automata/NA.lean | 3 ++- 3 files changed, 20 insertions(+), 6 deletions(-) create mode 100644 Cslib/Computability/Automata/DA.lean diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean new file mode 100644 index 00000000..c404d5ea --- /dev/null +++ b/Cslib/Computability/Automata/DA.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2025 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +/-! # Deterministic Automaton + +A Deterministic Automaton (DA) is a deterministic labelled transition system with an initial state. +For convenience, it is expressed by giving 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 diff --git a/Cslib/Computability/Automata/DFA/Basic.lean b/Cslib/Computability/Automata/DFA/Basic.lean index d2d737f6..7a03e233 100644 --- a/Cslib/Computability/Automata/DFA/Basic.lean +++ b/Cslib/Computability/Automata/DFA/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ +import Cslib.Computability.Automata.DA import Cslib.Foundations.Semantics.LTS.Basic set_option linter.style.longLine false in @@ -20,11 +21,7 @@ a finite string. /-- A Deterministic Finite-State 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 _) where - /-- The transition function of the automaton. -/ - tr : State → Symbol → State - /-- Start state. -/ - start : State +structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where /-- Accept states. -/ accept : Finset State /-- The automaton is finite-state. -/ diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index 5fa821b8..a94f489e 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -10,5 +10,6 @@ import Cslib.Foundations.Semantics.LTS.Basic A Nondeterministic Automaton (NA) is a labelled transition system with a set of initial states. -/ -structure NA State Symbol 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 From b1e50147167df5d4e084f692d3031d4c2a5f7d6f Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 29 Sep 2025 10:32:40 +0200 Subject: [PATCH 04/29] feat: move general defs and theorems from DFA to DA --- Cslib/Computability/Automata/DA.lean | 56 +++++++++++++++++++++ Cslib/Computability/Automata/DFA/Basic.lean | 52 ++----------------- 2 files changed, 59 insertions(+), 49 deletions(-) diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean index c404d5ea..62c4fd7b 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ +import Cslib.Foundations.Semantics.LTS.Basic + /-! # Deterministic Automaton A Deterministic Automaton (DA) is a deterministic labelled transition system with an initial state. @@ -14,3 +16,57 @@ structure DA (State : Type _) (Symbol : Type _) where start : State /-- The transition function of the automaton. -/ tr : State → Symbol → State + +namespace DA + +/-- 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 follow the way lists are constructed. +-/ +@[grind] +def mtr (da : DA State Symbol) (s : State) (xs : List Symbol) := + match xs with + | [] => s + | x :: xs => da.mtr (da.tr s x) xs + +@[grind] +theorem mtr_nil_eq {da : DA State Symbol} : da.mtr s [] = s := by rfl + +section LTS + +/-- `DA` is a special case of `LTS`. -/ +@[grind] +def toLTS (da : DA State Symbol) : LTS State Symbol := + LTS.mk (fun s1 μ s2 => da.tr s1 μ = s2) + +instance : Coe (DA State Symbol) (LTS State Symbol) where + coe := toLTS + +/-- `DA.toLTS` correctly characterises transitions. -/ +@[grind] +theorem toLTS_tr {da : DA State Symbol} : + da.toLTS.Tr s1 μ s2 ↔ da.tr s1 μ = s2 := by + rfl + +/-- `DA.toLTS` correctly characterises multistep transitions. -/ +@[grind] +theorem toLTS_mtr {da : DA State Symbol} : + da.toLTS.MTr s1 xs s2 ↔ da.mtr s1 xs = s2 := by + constructor <;> intro h + case mp => + induction h <;> grind + case mpr => + induction xs generalizing s1 + case nil => grind + case cons x xs ih => + apply LTS.MTr.stepL (s2 := da.tr s1 x) <;> grind + +/-- The LTS induced by a DA is deterministic. -/ +@[grind] +theorem toLTS_deterministic (da : DA State Symbol) : da.toLTS.Deterministic := by + grind + +end LTS + +end DA diff --git a/Cslib/Computability/Automata/DFA/Basic.lean b/Cslib/Computability/Automata/DFA/Basic.lean index 7a03e233..73a05c84 100644 --- a/Cslib/Computability/Automata/DFA/Basic.lean +++ b/Cslib/Computability/Automata/DFA/Basic.lean @@ -31,70 +31,24 @@ structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where 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 follow the way lists are constructed. --/ -@[grind] -def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := - match xs with - | [] => s - | x :: xs => dfa.mtr (dfa.tr s x) xs - -@[grind] -theorem mtr_nil_eq {dfa : DFA State Symbol} : dfa.mtr s [] = s := by rfl - -/-- A DFA accepts a trace if there is a multi-step accepting derivative with that trace from +/-- A DA accepts a trace if there is a multi-step accepting derivative with that trace from the start state. -/ @[grind] def Accepts (dfa : DFA State Symbol) (μs : List Symbol) := (dfa.mtr dfa.start μs) ∈ dfa.accept -/-- The language of a DFA is the set of traces that it accepts. -/ +/-- The language of a DA is the set of traces that it accepts. -/ @[grind] def language (dfa : DFA State Symbol) : Set (List Symbol) := { μs | dfa.Accepts μs } -/-- A trace is accepted by a DFA iff it is in the language of the DFA. -/ +/-- A trace is accepted by a DA iff it is in the language of the DA. -/ @[grind] theorem accepts_mem_language (dfa : DFA State Symbol) (μs : List Symbol) : dfa.Accepts μs ↔ μs ∈ dfa.language := by rfl section LTS -/-- `DFA` is a special case of `LTS`. -/ -@[grind] -def toLTS (dfa : DFA State Symbol) : LTS State Symbol := - LTS.mk (fun s1 μ s2 => dfa.tr s1 μ = s2) - -instance : Coe (DFA State Symbol) (LTS State Symbol) where - coe := toLTS - -/-- `DFA.toLTS` correctly characterises transitions. -/ -@[grind] -theorem toLTS_tr {dfa : DFA State Symbol} : - dfa.toLTS.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by - rfl - -/-- `DFA.toLTS` correctly characterises multistep transitions. -/ -@[grind] -theorem toLTS_mtr {dfa : DFA State Symbol} : - dfa.toLTS.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by - constructor <;> intro h - case mp => - induction h <;> grind - case mpr => - induction xs generalizing s1 - case nil => grind - case cons x xs ih => - apply LTS.MTr.stepL (s2 := dfa.tr s1 x) <;> grind - -/-- The LTS induced by a DFA is deterministic. -/ -@[grind] -theorem toLTS_deterministic (dfa : DFA State Symbol) : dfa.toLTS.Deterministic := by - grind - /-- The LTS induced by a DFA is finite-state. -/ @[grind] theorem toLTS_finiteState (dfa : DFA State Symbol) : dfa.toLTS.FiniteState := From 362ec6a6fb77968e08b1dc90daceb9637c9db76c Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 30 Sep 2025 12:44:32 +0200 Subject: [PATCH 05/29] feat: add LTS.setImage, the image of a set of states --- Cslib/Foundations/Semantics/LTS/Basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index fba2cd5e..ef34270f 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -11,6 +11,7 @@ import Mathlib.Logic.Function.Defs import Mathlib.Data.Set.Finite.Basic import Mathlib.Data.Stream.Defs import Mathlib.Util.Notation3 +import Mathlib.Order.SetNotation /-! # Labelled Transition System (LTS) @@ -271,6 +272,11 @@ def LTS.Image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ def LTS.ImageFinite : Prop := ∀ s μ, Finite (lts.Image s μ) +/-- The `μ`-image of a set of states `S` is the union of all `μ`-images of the states in `S`. -/ +@[grind] +def LTS.setImage (S : Set State) (μ : Label) : Set State := + ⋃ s ∈ S, lts.Image s μ + /-- In a deterministic LTS, if a state has a `μ`-derivative, then it can have no other `μ`-derivative. -/ theorem LTS.deterministic_not_lto (hDet : lts.Deterministic) : From 40585d4d2dea4ab5936874ac73075bef50c3c0eb Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 30 Sep 2025 12:48:01 +0200 Subject: [PATCH 06/29] chore: rename LTS.Image and LTS.OutgoingLabels with lowercase initials --- Cslib/Foundations/Semantics/LTS/Basic.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index ef34270f..1ef02e76 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -265,17 +265,17 @@ def LTS.Deterministic : Prop := /-- The `μ`-image of a state `s` is the set of all `μ`-derivatives of `s`. -/ @[grind] -def LTS.Image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' } +def LTS.image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' } /-- An lts is image-finite if all images of its states are finite. -/ @[grind] def LTS.ImageFinite : Prop := - ∀ s μ, Finite (lts.Image s μ) + ∀ s μ, Finite (lts.image s μ) /-- The `μ`-image of a set of states `S` is the union of all `μ`-images of the states in `S`. -/ @[grind] def LTS.setImage (S : Set State) (μ : Label) : Set State := - ⋃ s ∈ S, lts.Image s μ + ⋃ s ∈ S, lts.image s μ /-- In a deterministic LTS, if a state has a `μ`-derivative, then it can have no other `μ`-derivative. -/ @@ -289,9 +289,9 @@ theorem LTS.deterministic_not_lto (hDet : lts.Deterministic) : /-- In a deterministic LTS, any image is either a singleton or the empty set. -/ theorem LTS.deterministic_image_char (hDet : lts.Deterministic) : - ∀ s μ, (∃ s', lts.Image s μ = { s' }) ∨ (lts.Image s μ = ∅) := by + ∀ s μ, (∃ s', lts.image s μ = { s' }) ∨ (lts.image s μ = ∅) := by intro s μ - by_cases hs' : ∃ s', lts.Tr s μ s' <;> aesop (add simp [Image]) + by_cases hs' : ∃ s', lts.Tr s μ s' <;> aesop (add simp [image]) /-- Every deterministic LTS is also image-finite. -/ theorem LTS.deterministic_imageFinite : @@ -313,12 +313,12 @@ def LTS.HasOutLabel (s : State) (μ : Label) : Prop := ∃ s', lts.Tr s μ s' /-- The set of outgoing labels of a state. -/ -def LTS.OutgoingLabels (s : State) := { μ | lts.HasOutLabel s μ } +def LTS.outgoingLabels (s : State) := { μ | lts.HasOutLabel s μ } /-- An LTS is finitely branching if it is image-finite and all states have finite sets of outgoing labels. -/ def LTS.FinitelyBranching : Prop := - lts.ImageFinite ∧ ∀ s, Finite (lts.OutgoingLabels s) + lts.ImageFinite ∧ ∀ s, Finite (lts.outgoingLabels s) /-- An LTS is finite-state if it has a finite `State` type. -/ @[nolint unusedArguments] From 33f033161372e2dc1ceea541344ee369e5567758 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 1 Oct 2025 12:22:32 +0200 Subject: [PATCH 07/29] chore: fix casing of Sum.isLeft/RightP --- Cslib/Foundations/Semantics/LTS/Basic.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 1ef02e76..3c23c00f 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -185,14 +185,14 @@ def LTS.unionSubtype False /-- TODO: move this to `Sum`? -/ -def Sum.isLeftP {α} {β} (x : α ⊕ β) : Prop := Sum.isLeft x = true +def Sum.IsLeftP {α} {β} (x : α ⊕ β) : Prop := Sum.isLeft x = true /-- TODO: move this to `Sum`? -/ -def Sum.isRightP {α} {β} (x : α ⊕ β) : Prop := Sum.isRight x = true +def Sum.IsRightP {α} {β} (x : α ⊕ β) : Prop := Sum.isRight x = true /-- Lifting of an `LTS State Label` to `LTS (State ⊕ State') Label`. -/ def LTS.inl {State'} (lts : LTS State Label) : - LTS (@Subtype (State ⊕ State') Sum.isLeftP) (@Subtype Label (Function.const Label True)) where + LTS (@Subtype (State ⊕ State') Sum.IsLeftP) (@Subtype Label (Function.const Label True)) where Tr := fun s μ s' => let ⟨s, _⟩ := s let ⟨s', _⟩ := s' @@ -202,7 +202,7 @@ def LTS.inl {State'} (lts : LTS State Label) : /-- Lifting of an `LTS State Label` to `LTS (State' ⊕ State) Label`. -/ def LTS.inr {State'} (lts : LTS State Label) : - LTS (@Subtype (State' ⊕ State) Sum.isRightP) (@Subtype Label (Function.const Label True)) where + LTS (@Subtype (State' ⊕ State) Sum.IsRightP) (@Subtype Label (Function.const Label True)) where Tr := fun s μ s' => let ⟨s, _⟩ := s let ⟨s', _⟩ := s' @@ -216,16 +216,16 @@ def LTS.unionSum {State1} {State2} (lts1 : LTS State1 Label) (lts2 : LTS State2 LTS (State1 ⊕ State2) Label := @LTS.unionSubtype (State1 ⊕ State2) Label - Sum.isLeftP + Sum.IsLeftP (Function.const Label True) - Sum.isRightP + Sum.IsRightP (Function.const Label True) (by intro s cases h : s · apply Decidable.isTrue trivial - · simp only [Sum.isLeftP, Sum.isLeft_inr, Bool.false_eq_true] + · simp only [Sum.IsLeftP, Sum.isLeft_inr, Bool.false_eq_true] apply Decidable.isFalse trivial) (by @@ -235,7 +235,7 @@ def LTS.unionSum {State1} {State2} (lts1 : LTS State1 Label) (lts2 : LTS State2 (by intro s cases h : s - · simp only [Sum.isRightP, Sum.isRight_inl, Bool.false_eq_true] + · simp only [Sum.IsRightP, Sum.isRight_inl, Bool.false_eq_true] apply Decidable.isFalse trivial · apply Decidable.isTrue From f113731e058c947028b9aa41de837695c0124a2d Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 1 Oct 2025 13:39:01 +0200 Subject: [PATCH 08/29] feat (LTS): union of two LTSs with the same state and label types --- Cslib/Foundations/Semantics/LTS/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 3c23c00f..473f0e46 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -169,6 +169,10 @@ change in the future. -/ variable {State : Type u} {Label : Type v} +/-- The union of two LTSs defined on the same types. -/ +def LTS.union (lts1 lts2 : LTS State Label) : LTS State Label where + Tr := lts1.Tr ⊔ lts2.Tr + /-- The union of two LTSs that have common supertypes for states and labels. -/ def LTS.unionSubtype {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop} From bd0b5681d5212afb56cee80f5a9d3ec3b4a908d9 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 3 Oct 2025 10:04:51 +0200 Subject: [PATCH 09/29] feat: extension of LTS theory to deal with image transitions, and application to automata theory to prove the subset construction correct --- Cslib/Computability/Automata/DA.lean | 139 +++++++++++++++--- .../Automata/{DFA/Basic.lean => DFA.lean} | 31 ---- Cslib/Computability/Automata/NA.lean | 24 ++- Cslib/Foundations/Semantics/LTS/Basic.lean | 59 +++++++- CslibTests/DFA.lean | 2 +- 5 files changed, 195 insertions(+), 60 deletions(-) rename Cslib/Computability/Automata/{DFA/Basic.lean => DFA.lean} (55%) diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean index 62c4fd7b..cf6ad2b8 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA.lean @@ -4,16 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Basic +import Cslib.Computability.Automata.NA /-! # Deterministic Automaton -A Deterministic Automaton (DA) is a deterministic labelled transition system with an initial state. -For convenience, it is expressed by giving a transition function. +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 set of accepting states of the automaton. -/ + accept : Set State /-- The transition function of the automaton. -/ tr : State → Symbol → State @@ -22,37 +23,61 @@ namespace DA /-- 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 follow the way lists are constructed. +from the left (instead of the right), in order to match the way lists are constructed. -/ @[grind] -def mtr (da : DA State Symbol) (s : State) (xs : List Symbol) := - match xs with - | [] => s - | x :: xs => da.mtr (da.tr s x) xs +def mtr (da : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl da.tr s + -- match xs with + -- | [] => s + -- | x :: xs => da.mtr (da.tr s x) xs @[grind] theorem mtr_nil_eq {da : DA State Symbol} : da.mtr s [] = s := by rfl -section LTS +/-- A DA accepts a string if there is a multi-step accepting derivative with that trace from +the start state. -/ +@[grind] +def Accepts (da : DA State Symbol) (xs : List Symbol) := + (da.mtr da.start xs) ∈ da.accept + +/-- The language of a DA is the set of strings that it accepts. -/ +@[grind] +def language (da : DA State Symbol) : Set (List Symbol) := + { xs | da.Accepts xs } + +/-- A string is accepted by a DA iff it is in the language of the DA. -/ +@[grind] +theorem accepts_mem_language (da : DA State Symbol) (xs : List Symbol) : + da.Accepts xs ↔ xs ∈ da.language := by rfl + +/-! # From DA to NA -/ + +section NA + +/-- `DA` is a special case of `NA`. -/ +@[grind] +def toNA (da : DA State Symbol) : NA State Symbol := { + start := {da.start} + accept := da.accept + Tr := fun s1 μ s2 => da.tr s1 μ = s2 +} -/-- `DA` is a special case of `LTS`. -/ @[grind] -def toLTS (da : DA State Symbol) : LTS State Symbol := - LTS.mk (fun s1 μ s2 => da.tr s1 μ = s2) +lemma toNA_start {da : DA State Symbol} : da.toNA.start = {da.start} := rfl -instance : Coe (DA State Symbol) (LTS State Symbol) where - coe := toLTS +instance : Coe (DA State Symbol) (NA State Symbol) where + coe := toNA -/-- `DA.toLTS` correctly characterises transitions. -/ +/-- `DA.toNA` correctly characterises transitions. -/ @[grind] -theorem toLTS_tr {da : DA State Symbol} : - da.toLTS.Tr s1 μ s2 ↔ da.tr s1 μ = s2 := by +theorem toNA_tr {da : DA State Symbol} : + da.toNA.Tr s1 μ s2 ↔ da.tr s1 μ = s2 := by rfl -/-- `DA.toLTS` correctly characterises multistep transitions. -/ +/-- Characterisation of multistep transitions. -/ @[grind] -theorem toLTS_mtr {da : DA State Symbol} : - da.toLTS.MTr s1 xs s2 ↔ da.mtr s1 xs = s2 := by +theorem toNA_mtr {da : DA State Symbol} : + da.toNA.MTr s1 xs s2 ↔ da.mtr s1 xs = s2 := by constructor <;> intro h case mp => induction h <;> grind @@ -62,11 +87,77 @@ theorem toLTS_mtr {da : DA State Symbol} : case cons x xs ih => apply LTS.MTr.stepL (s2 := da.tr s1 x) <;> grind -/-- The LTS induced by a DA is deterministic. -/ +/-- The transition system of a DA is deterministic. -/ @[grind] -theorem toLTS_deterministic (da : DA State Symbol) : da.toLTS.Deterministic := by - grind +theorem toNA_deterministic (da : DA State Symbol) : da.toNA.Deterministic := by grind + +/-- The transition system of a DA is image-finite. -/ +@[grind] +theorem toNA_imageFinite (da : DA State Symbol) : da.toNA.ImageFinite := + da.toNA.deterministic_imageFinite da.toNA_deterministic + +/-- The `NA` constructed from a `DA` has the same language. -/ +@[grind] +theorem toNA_language_eq {da : DA State Symbol} : + da.toNA.language = da.language := by + ext xs + rw [← DA.accepts_mem_language, ← NA.accepts_mem_language] + simp only [NA.Accepts, DA.Accepts] + apply Iff.intro <;> intro h + case mp => + grind + case mpr => + exists da.start + grind -end LTS +end NA end DA + +/-! # Subset construction (conversion from NA to DA) -/ +section SubsetConstruction + +/-- Converts an `NA` into a `DA` using the subset construction. -/ +@[grind] +def NA.toDA (na : NA State Symbol) : DA (Set State) Symbol := { + start := na.start + accept := { S | ∃ s ∈ S, s ∈ na.accept } + tr := na.setImage +} + +/-- Characterisation of transitions in `NA.toDA` wrt transitions in the original NA. -/ +@[grind] +theorem NA.toDA_mem_tr {na : NA State Symbol} : + s' ∈ na.toDA.tr S x ↔ ∃ s ∈ S, na.Tr s x s' := by + simp only [NA.toDA, LTS.setImage, Set.mem_iUnion, exists_prop] + grind + +/-- Characterisation of multistep transitions in `NA.toDA` wrt multistep transitions in the +original NA. -/ +@[grind] +theorem NA.toDA_mem_mtr {na : NA State Symbol} : + s' ∈ na.toDA.mtr S xs ↔ ∃ s ∈ S, na.MTr s xs s' := by + simp only [NA.toDA, 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 `NA.toDA_language_eq`. + + labels: grind, lts, automata + -/ + rw [← LTS.setImageMultistep_foldl_setImage] + grind + +/-- Characterisation of multistep transitions in `NA.toDA` as image transitions in `LTS`. -/ +@[grind] +theorem NA.toDA_mtr_setImageMultistep {na : NA State Symbol} : + na.toDA.mtr = na.setImageMultistep := by grind + +/-- The `DA` constructed from an `NA` has the same language. -/ +@[grind] +theorem NA.toDA_language_eq {na : NA State Symbol} : + na.toDA.language = na.language := by + ext xs + rw [← DA.accepts_mem_language, ← NA.accepts_mem_language] + grind + +end SubsetConstruction diff --git a/Cslib/Computability/Automata/DFA/Basic.lean b/Cslib/Computability/Automata/DFA.lean similarity index 55% rename from Cslib/Computability/Automata/DFA/Basic.lean rename to Cslib/Computability/Automata/DFA.lean index 73a05c84..381e2026 100644 --- a/Cslib/Computability/Automata/DFA/Basic.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -22,38 +22,7 @@ a finite string. `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 - /-- Accept states. -/ - accept : Finset 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 - -/-- A DA accepts a trace if there is a multi-step accepting derivative with that trace from -the start state. -/ -@[grind] -def Accepts (dfa : DFA State Symbol) (μs : List Symbol) := - (dfa.mtr dfa.start μs) ∈ dfa.accept - -/-- The language of a DA is the set of traces that it accepts. -/ -@[grind] -def language (dfa : DFA State Symbol) : Set (List Symbol) := - { μs | dfa.Accepts μs } - -/-- A trace is accepted by a DA iff it is in the language of the DA. -/ -@[grind] -theorem accepts_mem_language (dfa : DFA State Symbol) (μs : List Symbol) : - dfa.Accepts μs ↔ μs ∈ dfa.language := by rfl - -section LTS - -/-- The LTS induced by a DFA is finite-state. -/ -@[grind] -theorem toLTS_finiteState (dfa : DFA State Symbol) : dfa.toLTS.FiniteState := - dfa.finite_state - -end LTS - -end DFA diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index a94f489e..58d48f20 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -8,8 +8,30 @@ import Cslib.Foundations.Semantics.LTS.Basic /-! # Nondeterministic Automaton -A Nondeterministic Automaton (NA) is a labelled transition system with a set of initial states. +A Nondeterministic Automaton (NA) is an automaton with a set of initial states. -/ structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where /-- The set of initial states of the automaton. -/ start : Set State + /-- The set of accepting states of the automaton. -/ + accept : Set State + +namespace NA + +/-- An NA accepts a string if there is a multi-step accepting derivative with that trace from +the start state. -/ +@[grind] +def Accepts (na : NA State Symbol) (xs : List Symbol) := + ∃ s ∈ na.start, ∃ s' ∈ na.accept, na.MTr s xs s' + +/-- The language of a DA is the set of strings that it accepts. -/ +@[grind] +def language (na : NA State Symbol) : Set (List Symbol) := + { xs | na.Accepts xs } + +/-- A string is accepted by an NA iff it is in the language of the NA. -/ +@[grind] +theorem accepts_mem_language (na : NA State Symbol) (xs : List Symbol) : + na.Accepts xs ↔ xs ∈ na.language := by rfl + +end NA diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 473f0e46..1941d1f5 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -271,16 +271,64 @@ def LTS.Deterministic : Prop := @[grind] def LTS.image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' } -/-- An lts is image-finite if all images of its states are finite. -/ +/-- The `μs`-image of a state `s`, where `μs` is a list of labels, is the set of all +`μs`-derivatives of `s`. -/ @[grind] -def LTS.ImageFinite : Prop := - ∀ s μ, Finite (lts.image s μ) +def LTS.imageMultistep (s : State) (μs : List Label) : Set State := { s' : State | lts.MTr s μs s' } /-- The `μ`-image of a set of states `S` is the union of all `μ`-images of the states in `S`. -/ @[grind] def LTS.setImage (S : Set State) (μ : Label) : Set State := ⋃ s ∈ S, lts.image s μ +/-- The `μs`-image of a set of states `S`, where `μs` is a list of labels, is the union of all +`μs`-images of the states in `S`. -/ +@[grind] +def LTS.setImageMultistep (S : Set State) (μs : List Label) : Set State := + ⋃ s ∈ S, lts.imageMultistep s μs + +/-- Characterisation of `setImage` wrt `Tr`. -/ +@[grind] +theorem LTS.mem_setImage (lts : LTS State Label) : + s' ∈ lts.setImage S μ ↔ ∃ s ∈ S, lts.Tr s μ s' := by + simp only [setImage, Set.mem_iUnion, exists_prop] + grind + +@[grind] +theorem LTS.tr_setImage (lts : LTS State Label) (hs : s ∈ S) (htr : lts.Tr s μ s') : + s' ∈ lts.setImage S μ := by grind + +/-- Characterisation of `setImageMultistep` with `MTr`. -/ +@[grind] +theorem LTS.mem_setImageMultistep (lts : LTS State Label) : + s' ∈ lts.setImageMultistep S μs ↔ ∃ s ∈ S, lts.MTr s μs s' := by + simp only [setImageMultistep, Set.mem_iUnion, exists_prop] + grind + +@[grind] +theorem LTS.mtr_setImage (lts : LTS State Label) (hs : s ∈ S) (htr : lts.MTr s μs s') : + s' ∈ lts.setImageMultistep S μs := by grind + +/-- The image of the empty set is always the empty set. -/ +@[grind] +theorem LTS.setImage_empty (lts : LTS State Label) : lts.setImage ∅ μ = ∅ := by grind + +@[grind] +lemma LTS.setImageMultistep_setImage_head (lts : LTS State Label) : + lts.setImageMultistep S (μ :: μs) = lts.setImageMultistep (lts.setImage S μ ) μs := by grind + +/-- Characterisation of `LTS.setImageMultistep` as `List.foldl` on `LTS.setImage`. -/ +@[grind _=_] +theorem LTS.setImageMultistep_foldl_setImage (lts : LTS State Label) : + lts.setImageMultistep = List.foldl lts.setImage := by + ext S μs s' + induction μs generalizing S <;> grind + +/-- An lts is image-finite if all images of its states are finite. -/ +@[grind] +def LTS.ImageFinite : Prop := + ∀ s μ, Finite (lts.image s μ) + /-- In a deterministic LTS, if a state has a `μ`-derivative, then it can have no other `μ`-derivative. -/ theorem LTS.deterministic_not_lto (hDet : lts.Deterministic) : @@ -353,6 +401,11 @@ def LTS.Acyclic : Prop := def LTS.Finite : Prop := lts.FiniteState ∧ lts.Acyclic +/- +/-- An LTS has a complete transition relation if every state has a `μ`-derivative for every `μ`. -/ +def LTS.CompleteTr (lts : LTS State Label) : Prop := ∀ s μ, ∃ s', lts.Tr s μ s' +-/ + end Classes /-! ## Weak transitions (single- and multi-step) -/ diff --git a/CslibTests/DFA.lean b/CslibTests/DFA.lean index 1a436fe1..705f7441 100644 --- a/CslibTests/DFA.lean +++ b/CslibTests/DFA.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.DFA.Basic +import Cslib.Computability.Automata.DFA /-! A simple elevator. -/ From 898d941058f2cf49088122d612c60707c6ab622e Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 3 Oct 2025 10:13:30 +0200 Subject: [PATCH 10/29] docs: alternative shapes for transitions in NA --- Cslib/Computability/Automata/NA.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index 58d48f20..a8906af0 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -9,6 +9,10 @@ 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. -/ From fee5bad889f84697b81d96ce8aa9da933857f745 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 3 Oct 2025 20:59:55 +0200 Subject: [PATCH 11/29] feat: add NFA and EpsilonNA --- Cslib/Computability/Automata/DFA.lean | 1 - Cslib/Computability/Automata/EpsilonNA.lean | 31 +++++++++++++++++++++ Cslib/Computability/Automata/NFA.lean | 15 ++++++++++ 3 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 Cslib/Computability/Automata/EpsilonNA.lean create mode 100644 Cslib/Computability/Automata/NFA.lean diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean index 381e2026..37dc8d6d 100644 --- a/Cslib/Computability/Automata/DFA.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -5,7 +5,6 @@ Authors: Fabrizio Montesi -/ import Cslib.Computability.Automata.DA -import Cslib.Foundations.Semantics.LTS.Basic set_option linter.style.longLine false in /-! # Deterministic Finite-State Automata diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA.lean new file mode 100644 index 00000000..a4cc5d86 --- /dev/null +++ b/Cslib/Computability/Automata/EpsilonNA.lean @@ -0,0 +1,31 @@ +/- +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 + +structure εNA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) + +private instance : HasTau (Option α) := ⟨.none⟩ + +namespace εNA + +/-- An εNA accepts a string if there is a saturated multistep accepting derivative with that trace +from the start state. -/ +@[grind] +def Accepts (ena : εNA State Symbol) (xs : List Symbol) := + ∃ s ∈ ena.start, ∃ s' ∈ ena.accept, ena.saturate.MTr s xs s' + +/-- The language of an εDA is the set of strings that it accepts. -/ +@[grind] +def language (ena : εNA State Symbol) : Set (List Symbol) := + { xs | ena.Accepts xs } + +/-- A string is accepted by an εNA iff it is in the language of the NA. -/ +@[grind] +theorem accepts_mem_language (ena : εNA State Symbol) (xs : List Symbol) : + ena.Accepts xs ↔ xs ∈ ena.language := by rfl + +end εNA diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean new file mode 100644 index 00000000..00537cca --- /dev/null +++ b/Cslib/Computability/Automata/NFA.lean @@ -0,0 +1,15 @@ +/- +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-State 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 automaton is finite-state. -/ + finite_state : Finite State + /-- The type of symbols (also called 'alphabet') is finite. -/ + finite_symbol : Finite Symbol From d00c2fb367790acff343a2cb5c829ca7a43ce5cd Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 3 Oct 2025 21:10:58 +0200 Subject: [PATCH 12/29] feat: EpsilonNA.toNAWithoutEpsilon --- Cslib/Computability/Automata/EpsilonNA.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA.lean index a4cc5d86..cc698685 100644 --- a/Cslib/Computability/Automata/EpsilonNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA.lean @@ -28,4 +28,19 @@ def language (ena : εNA State Symbol) : Set (List Symbol) := theorem accepts_mem_language (ena : εNA State Symbol) (xs : List Symbol) : ena.Accepts xs ↔ xs ∈ ena.language := by rfl +section NA + +@[grind] +def toNAWithoutEpsilon (ena : εNA State Symbol) : NA State Symbol := { + start := ena.setImage ena.start HasTau.τ + accept := ena.accept + Tr := fun s x s' => ena.saturate.Tr s (some x) s' +} + +-- theorem toNAWithoutEpsilon_language_eq {ena : εNA State Symbol} : +-- ena.toNAWithoutEpsilon.language = ena.language := by +-- grind + +end NA + end εNA From a76afcb3f27e5fc5589247952e906196607ee2e3 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 11:24:35 +0200 Subject: [PATCH 13/29] feat (EpsilonNA): conversion of EpsilonNA into NA, with proof of correctness --- Cslib/Computability/Automata/EpsilonNA.lean | 85 +++++++++++- Cslib/Foundations/Semantics/LTS/Basic.lean | 126 ++++++++++++------ .../Semantics/LTS/Bisimulation.lean | 4 +- 3 files changed, 167 insertions(+), 48 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA.lean index cc698685..8a5cec87 100644 --- a/Cslib/Computability/Automata/EpsilonNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA.lean @@ -6,17 +6,40 @@ Authors: Fabrizio Montesi import Cslib.Computability.Automata.NA +/-! # Nondeterministic automata with ε-transitions. -/ + +/-- A nondeterministic automaton with ε-transitions (`εNA`) 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 εNA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) +@[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 εNA.εClosure (ena : εNA State Symbol) (S : Set State) := ena.τClosure S + +/-- 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 := { + Tr := fun s μ s' => lts.Tr s (some μ) s' +} + namespace εNA /-- An εNA accepts a string if there is a saturated multistep accepting derivative with that trace from the start state. -/ @[grind] def Accepts (ena : εNA State Symbol) (xs : List Symbol) := - ∃ s ∈ ena.start, ∃ s' ∈ ena.accept, ena.saturate.MTr s xs s' + ∃ s ∈ ena.εClosure ena.start, ∃ s' ∈ ena.accept, + ena.saturate.MTr s (xs.map (some ·)) s' /-- The language of an εDA is the set of strings that it accepts. -/ @[grind] @@ -30,16 +53,66 @@ theorem accepts_mem_language (ena : εNA State Symbol) (xs : List Symbol) : section NA +/-- Any εNA can be converted into an NA that does not use ε-transitions. -/ @[grind] def toNAWithoutEpsilon (ena : εNA State Symbol) : NA State Symbol := { - start := ena.setImage ena.start HasTau.τ + start := ena.εClosure ena.start accept := ena.accept - Tr := fun s x s' => ena.saturate.Tr s (some x) s' + Tr := ena.saturate.noε.Tr } --- theorem toNAWithoutEpsilon_language_eq {ena : εNA State Symbol} : --- ena.toNAWithoutEpsilon.language = ena.language := by --- grind +@[grind] +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 + +@[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 + case nil => grind + case cons μ μs ih => + apply Iff.intro <;> intro h + case mp => + simp only [LTS.noε] + cases h + rename_i sb htr hmtr + apply LTS.MTr.stepL (s1 := s) (s2 := sb) (s3 := s') <;> grind + case mpr => + simp only [LTS.noε] at h + grind + + +/-- Correctness of `toNAWithoutEpsilon`. -/ +@[grind] +theorem toNAWithoutEpsilon_language_eq {ena : εNA State Symbol} : + ena.toNAWithoutEpsilon.language = ena.language := by + ext xs + apply Iff.intro + case mp => + rw [← εNA.accepts_mem_language, ← NA.accepts_mem_language] + simp only [NA.Accepts, toNAWithoutEpsilon, Accepts, forall_exists_index, and_imp] + intro s hs s' hs' hmtr + exists s + apply And.intro hs + exists s' + apply And.intro hs' + rw [LTS.noε_saturate_mTr] + assumption + case mpr => + rw [← εNA.accepts_mem_language, ← NA.accepts_mem_language] + simp only [NA.Accepts, toNAWithoutEpsilon, Accepts, forall_exists_index, and_imp] + intro s hs s' hs' hmtr + exists s + apply And.intro hs + exists s' + apply And.intro hs' + rw [← LTS.noε_saturate_mTr] + assumption end NA diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 1941d1f5..2176a77d 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -306,7 +306,7 @@ theorem LTS.mem_setImageMultistep (lts : LTS State Label) : grind @[grind] -theorem LTS.mtr_setImage (lts : LTS State Label) (hs : s ∈ S) (htr : lts.MTr s μs s') : +theorem LTS.mTr_setImage (lts : LTS State Label) (hs : s ∈ S) (htr : lts.MTr s μs s') : s' ∈ lts.setImageMultistep S μs := by grind /-- The image of the empty set is always the empty set. -/ @@ -422,39 +422,43 @@ inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → S | tr : lts.STr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STr s3 HasTau.τ s4 → lts.STr s1 μ s4 /-- The `LTS` obtained by saturating the transition relation in `lts`. -/ +@[grind =] def LTS.saturate [HasTau Label] (lts : LTS State Label) : LTS State Label where - Tr := LTS.STr lts + Tr := lts.STr /-- Any transition is also a saturated transition. -/ +@[grind] theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) : lts.Tr s μ s' → lts.STr s μ s' := by intro h apply LTS.STr.tr LTS.STr.refl h LTS.STr.refl /-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction metric. -/ -inductive LTS.strN [HasTau Label] (lts : LTS State Label) : +@[grind] +inductive LTS.STrN [HasTau Label] (lts : LTS State Label) : ℕ → State → Label → State → Prop where - | refl : lts.strN 0 s HasTau.τ s + | refl : lts.STrN 0 s HasTau.τ s | tr : - lts.strN n s1 HasTau.τ s2 → + lts.STrN n s1 HasTau.τ s2 → lts.Tr s2 μ s3 → - lts.strN m s3 HasTau.τ s4 → - lts.strN (n + m + 1) s1 μ s4 + lts.STrN m s3 HasTau.τ s4 → + lts.STrN (n + m + 1) s1 μ s4 /-- `LTS.str` and `LTS.strN` are equivalent. -/ -theorem LTS.str_strN [HasTau Label] (lts : LTS State Label) : - lts.STr s1 μ s2 ↔ ∃ n, lts.strN n s1 μ s2 := by +@[grind] +theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) : + lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by apply Iff.intro <;> intro h case mp => induction h case refl => exists 0 - exact LTS.strN.refl + exact LTS.STrN.refl case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 => obtain ⟨n1, ih1⟩ := ih1 obtain ⟨n2, ih2⟩ := ih2 exists (n1 + n2 + 1) - apply LTS.strN.tr ih1 htr ih2 + apply LTS.STrN.tr ih1 htr ih2 case mpr => obtain ⟨n, h⟩ := h induction h @@ -464,69 +468,111 @@ theorem LTS.str_strN [HasTau Label] (lts : LTS State Label) : apply LTS.STr.tr ih1 htr ih2 /-- Saturated transitions labelled by τ can be composed (weighted version). -/ -theorem LTS.strN.trans_τ +@[grind] +theorem LTS.STrN.trans_τ [HasTau Label] (lts : LTS State Label) - (h1 : lts.strN n s1 HasTau.τ s2) (h2 : lts.strN m s2 HasTau.τ s3) : - lts.strN (n + m) s1 HasTau.τ s3 := by + (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) : + lts.STrN (n + m) s1 HasTau.τ s3 := by cases h1 case refl => grind case tr n1 sb sb' n2 hstr1 htr hstr2 => - have ih := LTS.strN.trans_τ lts hstr2 h2 - have conc := LTS.strN.tr hstr1 htr ih + have ih := LTS.STrN.trans_τ lts hstr2 h2 + have conc := LTS.STrN.tr hstr1 htr ih grind /-- Saturated transitions labelled by τ can be composed. -/ +@[grind] theorem LTS.STr.trans_τ [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : lts.STr s1 HasTau.τ s3 := by - obtain ⟨n, h1N⟩ := (LTS.str_strN lts).1 h1 - obtain ⟨m, h2N⟩ := (LTS.str_strN lts).1 h2 - have concN := LTS.strN.trans_τ lts h1N h2N - apply (LTS.str_strN lts).2 ⟨n + m, concN⟩ + obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1 + obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2 + have concN := LTS.STrN.trans_τ lts h1N h2N + apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩ /-- Saturated transitions can be appended with τ-transitions (weighted version). -/ -theorem LTS.strN.append +@[grind] +theorem LTS.STrN.append [HasTau Label] (lts : LTS State Label) - (h1 : lts.strN n1 s1 μ s2) - (h2 : lts.strN n2 s2 HasTau.τ s3) : - lts.strN (n1 + n2) s1 μ s3 := by + (h1 : lts.STrN n1 s1 μ s2) + (h2 : lts.STrN n2 s2 HasTau.τ s3) : + lts.STrN (n1 + n2) s1 μ s3 := by cases h1 case refl => grind case tr n11 sb sb' n12 hstr1 htr hstr2 => - have hsuffix := LTS.strN.trans_τ lts hstr2 h2 + have hsuffix := LTS.STrN.trans_τ lts hstr2 h2 have n_eq : n11 + (n12 + n2) + 1 = (n11 + n12 + 1 + n2) := by omega rw [← n_eq] - apply LTS.strN.tr hstr1 htr hsuffix + apply LTS.STrN.tr hstr1 htr hsuffix /-- Saturated transitions can be composed (weighted version). -/ -theorem LTS.strN.comp +@[grind] +theorem LTS.STrN.comp [HasTau Label] (lts : LTS State Label) - (h1 : lts.strN n1 s1 HasTau.τ s2) - (h2 : lts.strN n2 s2 μ s3) - (h3 : lts.strN n3 s3 HasTau.τ s4) : - lts.strN (n1 + n2 + n3) s1 μ s4 := by + (h1 : lts.STrN n1 s1 HasTau.τ s2) + (h2 : lts.STrN n2 s2 μ s3) + (h3 : lts.STrN n3 s3 HasTau.τ s4) : + lts.STrN (n1 + n2 + n3) s1 μ s4 := by cases h2 case refl => - apply LTS.strN.trans_τ lts h1 h3 + apply LTS.STrN.trans_τ lts h1 h3 case tr n21 sb sb' n22 hstr1 htr hstr2 => - have hprefix_τ := LTS.strN.trans_τ lts h1 hstr1 - have hprefix := LTS.strN.tr hprefix_τ htr hstr2 - have conc := LTS.strN.append lts hprefix h3 + have hprefix_τ := LTS.STrN.trans_τ lts h1 hstr1 + have hprefix := LTS.STrN.tr hprefix_τ htr hstr2 + have conc := LTS.STrN.append lts hprefix h3 grind /-- Saturated transitions can be composed. -/ +@[grind] theorem LTS.STr.comp [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 μ s3) (h3 : lts.STr s3 HasTau.τ s4) : lts.STr s1 μ s4 := by - obtain ⟨n1, h1N⟩ := (LTS.str_strN lts).1 h1 - obtain ⟨n2, h2N⟩ := (LTS.str_strN lts).1 h2 - obtain ⟨n3, h3N⟩ := (LTS.str_strN lts).1 h3 - have concN := LTS.strN.comp lts h1N h2N h3N - apply (LTS.str_strN lts).2 ⟨n1 + n2 + n3, concN⟩ + obtain ⟨n1, h1N⟩ := (LTS.sTr_sTrN lts).1 h1 + obtain ⟨n2, h2N⟩ := (LTS.sTr_sTrN lts).1 h2 + obtain ⟨n3, h3N⟩ := (LTS.sTr_sTrN lts).1 h3 + have concN := LTS.STrN.comp lts h1N h2N h3N + apply (LTS.sTr_sTrN lts).2 ⟨n1 + n2 + n3, concN⟩ + +@[grind _=_] +lemma LTS.saturate_tr_sTr [HasTau Label] (lts : LTS State Label) : + lts.saturate.Tr s HasTau.τ = lts.STr s HasTau.τ := by simp [LTS.saturate] + +/-- In a saturated LTS, the transition and saturated transition relations are the same. -/ +@[grind _=_] +theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label) + (hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by + ext s' + apply Iff.intro <;> intro h + case mp => + induction h + case refl => constructor + case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 => + rw [hμ] at htr + apply LTS.STr.single at htr + rw [← LTS.saturate_tr_sTr] at htr + grind [LTS.STr.tr] + case mpr => + induction h + case refl => constructor + case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 => + simp only [LTS.saturate] at ih1 htr ih2 + simp only [LTS.saturate] + grind + +/-- In a saturated LTS, every state is in its τ-image. -/ +@[grind] +theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) : + s ∈ lts.saturate.image s HasTau.τ := LTS.STr.refl + +/-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S` +by performing only `τ`-transitions. -/ +@[grind =] +def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State := + lts.saturate.setImage S HasTau.τ end Weak diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 92b32900..fae99337 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -797,7 +797,7 @@ notation s:max " ≈sw[" lts "] " s':max => SWBisimilarity lts s s' (first component, weighted version). -/ theorem SWBisimulation.follow_internal_fst_n [HasTau Label] {lts : LTS State Label} - (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.strN n s1 HasTau.τ s1') : + (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s1 HasTau.τ s1') : ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by cases n case zero => @@ -824,7 +824,7 @@ theorem SWBisimulation.follow_internal_fst_n (second component, weighted version). -/ theorem SWBisimulation.follow_internal_snd_n [HasTau Label] {lts : LTS State Label} - (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.strN n s2 HasTau.τ s2') : + (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s2 HasTau.τ s2') : ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by cases n case zero => From bdf5285eae7ae71f18a288d372e111bede9ae78c Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 12:39:43 +0200 Subject: [PATCH 14/29] chore: Split automata theory translations into multiple files --- Cslib/Computability/Automata/DA.lean | 144 ------------------ Cslib/Computability/Automata/DFA.lean | 34 ++++- Cslib/Computability/Automata/DFAToNFA.lean | 75 +++++++++ Cslib/Computability/Automata/EpsilonNA.lean | 119 --------------- Cslib/Computability/Automata/EpsilonNFA.lean | 50 ++++++ .../Automata/EpsilonNFAToNFA.lean | 89 +++++++++++ Cslib/Computability/Automata/NA.lean | 20 --- Cslib/Computability/Automata/NFA.lean | 22 ++- Cslib/Computability/Automata/NFAToDFA.lean | 64 ++++++++ .../Semantics/LTS/Bisimulation.lean | 4 +- 10 files changed, 334 insertions(+), 287 deletions(-) create mode 100644 Cslib/Computability/Automata/DFAToNFA.lean delete mode 100644 Cslib/Computability/Automata/EpsilonNA.lean create mode 100644 Cslib/Computability/Automata/EpsilonNFA.lean create mode 100644 Cslib/Computability/Automata/EpsilonNFAToNFA.lean create mode 100644 Cslib/Computability/Automata/NFAToDFA.lean diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean index cf6ad2b8..3e9322a5 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA.lean @@ -17,147 +17,3 @@ structure DA (State : Type _) (Symbol : Type _) where accept : Set State /-- The transition function of the automaton. -/ tr : State → Symbol → State - -namespace DA - -/-- 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. --/ -@[grind] -def mtr (da : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl da.tr s - -- match xs with - -- | [] => s - -- | x :: xs => da.mtr (da.tr s x) xs - -@[grind] -theorem mtr_nil_eq {da : DA State Symbol} : da.mtr s [] = s := by rfl - -/-- A DA accepts a string if there is a multi-step accepting derivative with that trace from -the start state. -/ -@[grind] -def Accepts (da : DA State Symbol) (xs : List Symbol) := - (da.mtr da.start xs) ∈ da.accept - -/-- The language of a DA is the set of strings that it accepts. -/ -@[grind] -def language (da : DA State Symbol) : Set (List Symbol) := - { xs | da.Accepts xs } - -/-- A string is accepted by a DA iff it is in the language of the DA. -/ -@[grind] -theorem accepts_mem_language (da : DA State Symbol) (xs : List Symbol) : - da.Accepts xs ↔ xs ∈ da.language := by rfl - -/-! # From DA to NA -/ - -section NA - -/-- `DA` is a special case of `NA`. -/ -@[grind] -def toNA (da : DA State Symbol) : NA State Symbol := { - start := {da.start} - accept := da.accept - Tr := fun s1 μ s2 => da.tr s1 μ = s2 -} - -@[grind] -lemma toNA_start {da : DA State Symbol} : da.toNA.start = {da.start} := rfl - -instance : Coe (DA State Symbol) (NA State Symbol) where - coe := toNA - -/-- `DA.toNA` correctly characterises transitions. -/ -@[grind] -theorem toNA_tr {da : DA State Symbol} : - da.toNA.Tr s1 μ s2 ↔ da.tr s1 μ = s2 := by - rfl - -/-- Characterisation of multistep transitions. -/ -@[grind] -theorem toNA_mtr {da : DA State Symbol} : - da.toNA.MTr s1 xs s2 ↔ da.mtr s1 xs = s2 := by - constructor <;> intro h - case mp => - induction h <;> grind - case mpr => - induction xs generalizing s1 - case nil => grind - case cons x xs ih => - apply LTS.MTr.stepL (s2 := da.tr s1 x) <;> grind - -/-- The transition system of a DA is deterministic. -/ -@[grind] -theorem toNA_deterministic (da : DA State Symbol) : da.toNA.Deterministic := by grind - -/-- The transition system of a DA is image-finite. -/ -@[grind] -theorem toNA_imageFinite (da : DA State Symbol) : da.toNA.ImageFinite := - da.toNA.deterministic_imageFinite da.toNA_deterministic - -/-- The `NA` constructed from a `DA` has the same language. -/ -@[grind] -theorem toNA_language_eq {da : DA State Symbol} : - da.toNA.language = da.language := by - ext xs - rw [← DA.accepts_mem_language, ← NA.accepts_mem_language] - simp only [NA.Accepts, DA.Accepts] - apply Iff.intro <;> intro h - case mp => - grind - case mpr => - exists da.start - grind - -end NA - -end DA - -/-! # Subset construction (conversion from NA to DA) -/ -section SubsetConstruction - -/-- Converts an `NA` into a `DA` using the subset construction. -/ -@[grind] -def NA.toDA (na : NA State Symbol) : DA (Set State) Symbol := { - start := na.start - accept := { S | ∃ s ∈ S, s ∈ na.accept } - tr := na.setImage -} - -/-- Characterisation of transitions in `NA.toDA` wrt transitions in the original NA. -/ -@[grind] -theorem NA.toDA_mem_tr {na : NA State Symbol} : - s' ∈ na.toDA.tr S x ↔ ∃ s ∈ S, na.Tr s x s' := by - simp only [NA.toDA, LTS.setImage, Set.mem_iUnion, exists_prop] - grind - -/-- Characterisation of multistep transitions in `NA.toDA` wrt multistep transitions in the -original NA. -/ -@[grind] -theorem NA.toDA_mem_mtr {na : NA State Symbol} : - s' ∈ na.toDA.mtr S xs ↔ ∃ s ∈ S, na.MTr s xs s' := by - simp only [NA.toDA, 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 `NA.toDA_language_eq`. - - labels: grind, lts, automata - -/ - rw [← LTS.setImageMultistep_foldl_setImage] - grind - -/-- Characterisation of multistep transitions in `NA.toDA` as image transitions in `LTS`. -/ -@[grind] -theorem NA.toDA_mtr_setImageMultistep {na : NA State Symbol} : - na.toDA.mtr = na.setImageMultistep := by grind - -/-- The `DA` constructed from an `NA` has the same language. -/ -@[grind] -theorem NA.toDA_language_eq {na : NA State Symbol} : - na.toDA.language = na.language := by - ext xs - rw [← DA.accepts_mem_language, ← NA.accepts_mem_language] - grind - -end SubsetConstruction diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean index 37dc8d6d..1bf475a4 100644 --- a/Cslib/Computability/Automata/DFA.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -17,7 +17,7 @@ a finite string. * [J. E. Hopcroft, R. Motwani, J. D. Ullman, *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006] -/ -/-- A Deterministic Finite-State Automaton (DFA) consists of a labelled transition function +/-- 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 @@ -25,3 +25,35 @@ structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where 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. +-/ +@[grind] +def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s + +@[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. -/ +@[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. -/ +@[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. -/ +@[grind] +theorem accepts_mem_language (dfa : DFA State Symbol) (xs : List Symbol) : + dfa.Accepts xs ↔ xs ∈ dfa.language := by rfl + +end DFA diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean new file mode 100644 index 00000000..7bd44d6b --- /dev/null +++ b/Cslib/Computability/Automata/DFAToNFA.lean @@ -0,0 +1,75 @@ +/- +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`. -/ +@[grind =] +def toNFA (dfa : DFA State Symbol) : NFA State Symbol := { + start := {dfa.start} + accept := dfa.accept + Tr := fun s1 μ s2 => dfa.tr s1 μ = s2 + finite_state := dfa.finite_state + finite_symbol := dfa.finite_symbol +} + +@[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. -/ +@[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. -/ +@[grind] +theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by + grind + +/-- The transition system of a DA is image-finite. -/ +@[grind] +theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite := + dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic + +/-- Characterisation of multistep transitions. -/ +@[grind] +theorem toNFA_mtr {dfa : DFA State Symbol} : + dfa.toNFA.MTr s1 xs s2 ↔ dfa.mtr s1 xs = s2 := by + constructor <;> intro h + case mp => + induction h <;> grind + case mpr => + induction xs generalizing s1 + case nil => grind + case cons x xs ih => + apply LTS.MTr.stepL (s2 := dfa.tr s1 x) <;> grind + +/-- The `NFA` constructed from a `DFA` has the same language. -/ +@[grind] +theorem toNFA_language_eq {dfa : DFA State Symbol} : + dfa.toNFA.language = dfa.language := by + ext xs + rw [← DFA.accepts_mem_language, ← NFA.accepts_mem_language] + simp only [NFA.Accepts, DFA.Accepts] + apply Iff.intro <;> intro h + case mp => + grind + case mpr => + exists dfa.start + grind + +end NFA +end DFA diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA.lean deleted file mode 100644 index 8a5cec87..00000000 --- a/Cslib/Computability/Automata/EpsilonNA.lean +++ /dev/null @@ -1,119 +0,0 @@ -/- -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 automaton with ε-transitions (`εNA`) 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 εNA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) - -@[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 εNA.εClosure (ena : εNA State Symbol) (S : Set State) := ena.τClosure S - -/-- 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 := { - Tr := fun s μ s' => lts.Tr s (some μ) s' -} - -namespace εNA - -/-- An εNA accepts a string if there is a saturated multistep accepting derivative with that trace -from the start state. -/ -@[grind] -def Accepts (ena : εNA State Symbol) (xs : List Symbol) := - ∃ s ∈ ena.εClosure ena.start, ∃ s' ∈ ena.accept, - ena.saturate.MTr s (xs.map (some ·)) s' - -/-- The language of an εDA is the set of strings that it accepts. -/ -@[grind] -def language (ena : εNA State Symbol) : Set (List Symbol) := - { xs | ena.Accepts xs } - -/-- A string is accepted by an εNA iff it is in the language of the NA. -/ -@[grind] -theorem accepts_mem_language (ena : εNA State Symbol) (xs : List Symbol) : - ena.Accepts xs ↔ xs ∈ ena.language := by rfl - -section NA - -/-- Any εNA can be converted into an NA that does not use ε-transitions. -/ -@[grind] -def toNAWithoutEpsilon (ena : εNA State Symbol) : NA State Symbol := { - start := ena.εClosure ena.start - accept := ena.accept - Tr := ena.saturate.noε.Tr -} - -@[grind] -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 - -@[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 - case nil => grind - case cons μ μs ih => - apply Iff.intro <;> intro h - case mp => - simp only [LTS.noε] - cases h - rename_i sb htr hmtr - apply LTS.MTr.stepL (s1 := s) (s2 := sb) (s3 := s') <;> grind - case mpr => - simp only [LTS.noε] at h - grind - - -/-- Correctness of `toNAWithoutEpsilon`. -/ -@[grind] -theorem toNAWithoutEpsilon_language_eq {ena : εNA State Symbol} : - ena.toNAWithoutEpsilon.language = ena.language := by - ext xs - apply Iff.intro - case mp => - rw [← εNA.accepts_mem_language, ← NA.accepts_mem_language] - simp only [NA.Accepts, toNAWithoutEpsilon, Accepts, forall_exists_index, and_imp] - intro s hs s' hs' hmtr - exists s - apply And.intro hs - exists s' - apply And.intro hs' - rw [LTS.noε_saturate_mTr] - assumption - case mpr => - rw [← εNA.accepts_mem_language, ← NA.accepts_mem_language] - simp only [NA.Accepts, toNAWithoutEpsilon, Accepts, forall_exists_index, and_imp] - intro s hs s' hs' hmtr - exists s - apply And.intro hs - exists s' - apply And.intro hs' - rw [← LTS.noε_saturate_mTr] - assumption - -end NA - -end εNA diff --git a/Cslib/Computability/Automata/EpsilonNFA.lean b/Cslib/Computability/Automata/EpsilonNFA.lean new file mode 100644 index 00000000..79276c48 --- /dev/null +++ b/Cslib/Computability/Automata/EpsilonNFA.lean @@ -0,0 +1,50 @@ +/- +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 automaton is finite-state. -/ + finite_state : Finite State + /-- The type of symbols (also called 'alphabet') is finite. -/ + finite_symbol : Finite Symbol + +@[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. -/ +@[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. -/ +@[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. -/ +@[grind] +theorem accepts_mem_language (enfa : εNFA State Symbol) (xs : List Symbol) : + enfa.Accepts xs ↔ xs ∈ enfa.language := by rfl + +end εNFA diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean new file mode 100644 index 00000000..db132d22 --- /dev/null +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -0,0 +1,89 @@ +/- +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 := { + Tr := fun s μ s' => lts.Tr s (some μ) s' +} + +@[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. -/ +@[grind] +def toNFA (enfa : εNFA State Symbol) : NFA State Symbol := { + start := enfa.εClosure enfa.start + accept := enfa.accept + Tr := enfa.saturate.noε.Tr + finite_state := enfa.finite_state + finite_symbol := enfa.finite_symbol +} + +@[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 + case nil => grind + case cons μ μs ih => + apply Iff.intro <;> intro h + case mp => + simp only [LTS.noε] + cases h + rename_i sb htr hmtr + apply LTS.MTr.stepL (s1 := s) (s2 := sb) (s3 := s') <;> grind + case mpr => + simp only [LTS.noε] at h + grind + + +/-- Correctness of `toNAWithoutEpsilon`. -/ +@[grind] +theorem toNAWithoutEpsilon_language_eq {enfa : εNFA State Symbol} : + enfa.toNFA.language = enfa.language := by + ext xs + apply Iff.intro + case mp => + rw [← εNFA.accepts_mem_language, ← NFA.accepts_mem_language] + simp only [NFA.Accepts, toNFA, Accepts, forall_exists_index, and_imp] + intro s hs s' hs' hmtr + exists s + apply And.intro hs + exists s' + apply And.intro hs' + rw [LTS.noε_saturate_mTr] + assumption + case mpr => + rw [← εNFA.accepts_mem_language, ← NFA.accepts_mem_language] + simp only [NFA.Accepts, toNFA, Accepts, forall_exists_index, and_imp] + intro s hs s' hs' hmtr + exists s + apply And.intro hs + exists s' + apply And.intro hs' + rw [← LTS.noε_saturate_mTr] + assumption + +end NFA + +end εNFA diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index a8906af0..99841a81 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -19,23 +19,3 @@ structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where start : Set State /-- The set of accepting states of the automaton. -/ accept : Set State - -namespace NA - -/-- An NA accepts a string if there is a multi-step accepting derivative with that trace from -the start state. -/ -@[grind] -def Accepts (na : NA State Symbol) (xs : List Symbol) := - ∃ s ∈ na.start, ∃ s' ∈ na.accept, na.MTr s xs s' - -/-- The language of a DA is the set of strings that it accepts. -/ -@[grind] -def language (na : NA State Symbol) : Set (List Symbol) := - { xs | na.Accepts xs } - -/-- A string is accepted by an NA iff it is in the language of the NA. -/ -@[grind] -theorem accepts_mem_language (na : NA State Symbol) (xs : List Symbol) : - na.Accepts xs ↔ xs ∈ na.language := by rfl - -end NA diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean index 00537cca..109b8402 100644 --- a/Cslib/Computability/Automata/NFA.lean +++ b/Cslib/Computability/Automata/NFA.lean @@ -6,10 +6,30 @@ Authors: Fabrizio Montesi import Cslib.Computability.Automata.NA -/-- A Nondeterministic Finite-State Automaton (NFA) is a nondeterministic automaton (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 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. -/ +@[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. -/ +@[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. -/ +@[grind] +theorem accepts_mem_language (nfa : NFA State Symbol) (xs : List Symbol) : + nfa.Accepts xs ↔ xs ∈ nfa.language := by rfl + +end NFA diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean new file mode 100644 index 00000000..136e5ec4 --- /dev/null +++ b/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 `NA` into a `DA` using the subset construction. -/ +@[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 + apply Set.instFinite + finite_symbol := nfa.finite_symbol +} + +/-- Characterisation of transitions in `NFA.toDFA` wrt transitions in the original NA. -/ +@[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. -/ +@[grind] +theorem toDA_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`. -/ +@[grind] +theorem toDA_mtr_setImageMultistep {nfa : NFA State Symbol} : + nfa.toDFA.mtr = nfa.setImageMultistep := by grind + +/-- The `DA` constructed from an `NA` has the same language. -/ +@[grind] +theorem toDA_language_eq {nfa : NFA State Symbol} : + nfa.toDFA.language = nfa.language := by + ext xs + rw [← DFA.accepts_mem_language, ← NFA.accepts_mem_language] + grind + +end SubsetConstruction +end NFA diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index fae99337..bcf40bae 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -853,7 +853,7 @@ theorem SWBisimulation.follow_internal_fst [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') : ∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by - obtain ⟨n, hstrN⟩ := (LTS.str_strN lts).1 hstr + obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr apply SWBisimulation.follow_internal_fst_n hswb hr hstrN /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` @@ -862,7 +862,7 @@ theorem SWBisimulation.follow_internal_snd [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') : ∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by - obtain ⟨n, hstrN⟩ := (LTS.str_strN lts).1 hstr + obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr apply SWBisimulation.follow_internal_snd_n hswb hr hstrN /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`. From 75f0bf0f657f2be1ff0d0e2fc8a868d5d4b5dc1b Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 12:42:11 +0200 Subject: [PATCH 15/29] chore: renaming to toNFA` --- Cslib/Computability/Automata/EpsilonNFAToNFA.lean | 6 ++---- Cslib/Computability/Automata/NFAToDFA.lean | 4 ++-- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean index db132d22..16b8b5c0 100644 --- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -25,7 +25,6 @@ private lemma LTS.noε_saturate_tr grind namespace εNFA - section NFA /-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/ @@ -57,9 +56,9 @@ lemma LTS.noε_saturate_mTr grind -/-- Correctness of `toNAWithoutEpsilon`. -/ +/-- Correctness of `toNFA`. -/ @[grind] -theorem toNAWithoutEpsilon_language_eq {enfa : εNFA State Symbol} : +theorem toNFA_language_eq {enfa : εNFA State Symbol} : enfa.toNFA.language = enfa.language := by ext xs apply Iff.intro @@ -85,5 +84,4 @@ theorem toNAWithoutEpsilon_language_eq {enfa : εNFA State Symbol} : assumption end NFA - end εNFA diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean index 136e5ec4..61d0860d 100644 --- a/Cslib/Computability/Automata/NFAToDFA.lean +++ b/Cslib/Computability/Automata/NFAToDFA.lean @@ -13,7 +13,7 @@ import Mathlib.Data.Fintype.Powerset namespace NFA section SubsetConstruction -/-- Converts an `NA` into a `DA` using the subset construction. -/ +/-- Converts an `NFA` into a `DFA` using the subset construction. -/ @[grind] def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := { start := nfa.start @@ -52,7 +52,7 @@ theorem toDA_mem_mtr {nfa : NFA State Symbol} : theorem toDA_mtr_setImageMultistep {nfa : NFA State Symbol} : nfa.toDFA.mtr = nfa.setImageMultistep := by grind -/-- The `DA` constructed from an `NA` has the same language. -/ +/-- The `DFA` constructed from an `NFA` has the same language. -/ @[grind] theorem toDA_language_eq {nfa : NFA State Symbol} : nfa.toDFA.language = nfa.language := by From a4eb319357993b9b3981e80fe94e58d2099ed78b Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 12:43:12 +0200 Subject: [PATCH 16/29] chore: spacing --- Cslib/Computability/Automata/NFAToDFA.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean index 61d0860d..5bd99f87 100644 --- a/Cslib/Computability/Automata/NFAToDFA.lean +++ b/Cslib/Computability/Automata/NFAToDFA.lean @@ -8,7 +8,7 @@ import Cslib.Computability.Automata.DFA import Cslib.Computability.Automata.NFA import Mathlib.Data.Fintype.Powerset -/-! # Translation of NFA into DFA (subset construction)-/ +/-! # Translation of NFA into DFA (subset construction) -/ namespace NFA section SubsetConstruction From 87336de84b02850eda44cbdfc5b482066b19aaba Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:26:25 +0200 Subject: [PATCH 17/29] Update Cslib/Computability/Automata/DFA.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/DFA.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean index 1bf475a4..06f792c6 100644 --- a/Cslib/Computability/Automata/DFA.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -44,7 +44,7 @@ theorem mtr_nil_eq {dfa : DFA State Symbol} : dfa.mtr s [] = s := by rfl the start state. -/ @[grind] def Accepts (dfa : DFA State Symbol) (xs : List Symbol) := - (dfa.mtr dfa.start xs) ∈ dfa.accept + dfa.mtr dfa.start xs ∈ dfa.accept /-- The language of a DFA is the set of strings that it accepts. -/ @[grind] From c71741a736f8a156b82376e9d07a6da2ef2aa1fe Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:27:21 +0200 Subject: [PATCH 18/29] Update Cslib/Computability/Automata/DFAToNFA.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/DFAToNFA.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean index 7bd44d6b..57867a4f 100644 --- a/Cslib/Computability/Automata/DFAToNFA.lean +++ b/Cslib/Computability/Automata/DFAToNFA.lean @@ -14,13 +14,12 @@ section NFA /-- `DFA` is a special case of `NFA`. -/ @[grind =] -def toNFA (dfa : DFA State Symbol) : NFA State Symbol := { +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 -} @[grind =] lemma toNFA_start {dfa : DFA State Symbol} : dfa.toNFA.start = {dfa.start} := rfl From 740c26ca2479ef3e2d45f6cafa17c46d6ae2dd56 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:27:41 +0200 Subject: [PATCH 19/29] Update Cslib/Computability/Automata/EpsilonNFAToNFA.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/EpsilonNFAToNFA.lean | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean index 16b8b5c0..87b38b99 100644 --- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -42,18 +42,7 @@ 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 - case nil => grind - case cons μ μs ih => - apply Iff.intro <;> intro h - case mp => - simp only [LTS.noε] - cases h - rename_i sb htr hmtr - apply LTS.MTr.stepL (s1 := s) (s2 := sb) (s3 := s') <;> grind - case mpr => - simp only [LTS.noε] at h - grind + induction μs generalizing s <;> grind [<= LTS.MTr.stepL] /-- Correctness of `toNFA`. -/ From f915549b49b9ffc50fce2bb77b271f80f70abf78 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:29:08 +0200 Subject: [PATCH 20/29] Update Cslib/Computability/Automata/EpsilonNFAToNFA.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- .../Automata/EpsilonNFAToNFA.lean | 24 +++---------------- 1 file changed, 3 insertions(+), 21 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean index 87b38b99..1569a3e3 100644 --- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -50,27 +50,9 @@ lemma LTS.noε_saturate_mTr theorem toNFA_language_eq {enfa : εNFA State Symbol} : enfa.toNFA.language = enfa.language := by ext xs - apply Iff.intro - case mp => - rw [← εNFA.accepts_mem_language, ← NFA.accepts_mem_language] - simp only [NFA.Accepts, toNFA, Accepts, forall_exists_index, and_imp] - intro s hs s' hs' hmtr - exists s - apply And.intro hs - exists s' - apply And.intro hs' - rw [LTS.noε_saturate_mTr] - assumption - case mpr => - rw [← εNFA.accepts_mem_language, ← NFA.accepts_mem_language] - simp only [NFA.Accepts, toNFA, Accepts, forall_exists_index, and_imp] - intro s hs s' hs' hmtr - exists s - apply And.intro hs - exists s' - apply And.intro hs' - rw [← LTS.noε_saturate_mTr] - assumption + have : ∀ s s', enfa.saturate.MTr s (xs.map (some ·)) s' = enfa.saturate.noε.MTr s xs s' := by + simp [LTS.noε_saturate_mTr] + grind end NFA end εNFA From b1f9cb23765b27e141b33fd3f3a6547dc8fd13d3 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:29:23 +0200 Subject: [PATCH 21/29] Update Cslib/Computability/Automata/DFAToNFA.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/DFAToNFA.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean index 57867a4f..ef14acde 100644 --- a/Cslib/Computability/Automata/DFAToNFA.lean +++ b/Cslib/Computability/Automata/DFAToNFA.lean @@ -29,8 +29,7 @@ instance : Coe (DFA State Symbol) (NFA State Symbol) where /-- `DA.toNA` correctly characterises transitions. -/ @[grind] -theorem toNA_tr {dfa : DFA State Symbol} : - dfa.toNFA.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by +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. -/ From 81cb3a19c1a9d553f8e23c6ff578d191f691bf07 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:30:28 +0200 Subject: [PATCH 22/29] Update Cslib/Computability/Automata/DFAToNFA.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/DFAToNFA.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean index ef14acde..88be6c60 100644 --- a/Cslib/Computability/Automata/DFAToNFA.lean +++ b/Cslib/Computability/Automata/DFAToNFA.lean @@ -60,14 +60,7 @@ theorem toNFA_mtr {dfa : DFA State Symbol} : theorem toNFA_language_eq {dfa : DFA State Symbol} : dfa.toNFA.language = dfa.language := by ext xs - rw [← DFA.accepts_mem_language, ← NFA.accepts_mem_language] - simp only [NFA.Accepts, DFA.Accepts] - apply Iff.intro <;> intro h - case mp => - grind - case mpr => - exists dfa.start - grind + refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> grind end NFA end DFA From 2b5ac8f183fd1ec1419ee769e18ae76378fea0bd Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:49:53 +0200 Subject: [PATCH 23/29] Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/NFAToDFA.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean index 5bd99f87..aa732c25 100644 --- a/Cslib/Computability/Automata/NFAToDFA.lean +++ b/Cslib/Computability/Automata/NFAToDFA.lean @@ -21,7 +21,7 @@ def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := { tr := nfa.setImage finite_state := by haveI := nfa.finite_state - apply Set.instFinite + infer_instance finite_symbol := nfa.finite_symbol } From 066a62b8433c3fea955005ee29b47778df8abac3 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:50:28 +0200 Subject: [PATCH 24/29] Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/EpsilonNFAToNFA.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean index 1569a3e3..7a969400 100644 --- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -12,10 +12,8 @@ import Cslib.Computability.Automata.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 := { +private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where Tr := fun s μ s' => lts.Tr s (some μ) s' -} @[grind] private lemma LTS.noε_saturate_tr From 0ff5f1aa3264d44c02c8859bf7fc4b811776eecc Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:50:51 +0200 Subject: [PATCH 25/29] Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/EpsilonNFAToNFA.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean index 7a969400..206bb2b0 100644 --- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -27,13 +27,12 @@ section NFA /-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/ @[grind] -def toNFA (enfa : εNFA State Symbol) : NFA State Symbol := { +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 -} @[grind] lemma LTS.noε_saturate_mTr From a48173f6549ea2fa56f228bc5db0435c6eca6d26 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:52:19 +0200 Subject: [PATCH 26/29] Apply suggestion from @chenson2018 Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> --- Cslib/Computability/Automata/NFAToDFA.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean index aa732c25..c9f14e2f 100644 --- a/Cslib/Computability/Automata/NFAToDFA.lean +++ b/Cslib/Computability/Automata/NFAToDFA.lean @@ -57,7 +57,7 @@ theorem toDA_mtr_setImageMultistep {nfa : NFA State Symbol} : theorem toDA_language_eq {nfa : NFA State Symbol} : nfa.toDFA.language = nfa.language := by ext xs - rw [← DFA.accepts_mem_language, ← NFA.accepts_mem_language] + rw [← DFA.accepts_mem_language] grind end SubsetConstruction From 4b17e096fe8ae90f661419c61db0bbb339535c42 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:50:36 +0200 Subject: [PATCH 27/29] grind annotations --- Cslib/Computability/Automata/DFA.lean | 10 +++++----- Cslib/Computability/Automata/DFAToNFA.lean | 23 ++++++++++------------ 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean index 06f792c6..5550da40 100644 --- a/Cslib/Computability/Automata/DFA.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -34,25 +34,25 @@ namespace DFA 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. -/ -@[grind] +@[grind =] def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s -@[grind] +@[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. -/ -@[grind] +@[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. -/ -@[grind] +@[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. -/ -@[grind] +@[grind _=_] theorem accepts_mem_language (dfa : DFA State Symbol) (xs : List Symbol) : dfa.Accepts xs ↔ xs ∈ dfa.language := by rfl diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean index 88be6c60..fd739435 100644 --- a/Cslib/Computability/Automata/DFAToNFA.lean +++ b/Cslib/Computability/Automata/DFAToNFA.lean @@ -28,35 +28,32 @@ instance : Coe (DFA State Symbol) (NFA State Symbol) where coe := toNFA /-- `DA.toNA` correctly characterises transitions. -/ -@[grind] -theorem toNA_tr {dfa : DFA State Symbol} : dfa.toNFA.Tr s1 μ s2 ↔ dfa.tr s1 μ = s2 := by +@[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. -/ -@[grind] +@[grind ⇒] theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by grind /-- The transition system of a DA is image-finite. -/ -@[grind] +@[grind ⇒] theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite := dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic /-- Characterisation of multistep transitions. -/ -@[grind] +@[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 - case nil => grind - case cons x xs ih => - apply LTS.MTr.stepL (s2 := dfa.tr s1 x) <;> grind + case mp => induction h <;> grind + case mpr => induction xs generalizing s1 <;> grind /-- The `NFA` constructed from a `DFA` has the same language. -/ -@[grind] +@[grind =] theorem toNFA_language_eq {dfa : DFA State Symbol} : dfa.toNFA.language = dfa.language := by ext xs From ec94a2031f9d14b2ae08d1ea7e72753e110ff2ec Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 20:59:01 +0200 Subject: [PATCH 28/29] scope all the grinds --- Cslib/Computability/Automata/DFA.lean | 10 +++++----- Cslib/Computability/Automata/DFAToNFA.lean | 16 ++++++++-------- Cslib/Computability/Automata/EpsilonNFA.lean | 8 ++++---- .../Automata/EpsilonNFAToNFA.lean | 10 +++++----- Cslib/Computability/Automata/NFA.lean | 6 +++--- Cslib/Computability/Automata/NFAToDFA.lean | 18 +++++++++--------- 6 files changed, 34 insertions(+), 34 deletions(-) diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean index 5550da40..b64ce190 100644 --- a/Cslib/Computability/Automata/DFA.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -34,25 +34,25 @@ namespace DFA 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. -/ -@[grind =] +@[scoped grind =] def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s -@[grind =] +@[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. -/ -@[grind →] +@[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. -/ -@[grind =] +@[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. -/ -@[grind _=_] +@[scoped grind _=_] theorem accepts_mem_language (dfa : DFA State Symbol) (xs : List Symbol) : dfa.Accepts xs ↔ xs ∈ dfa.language := by rfl diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean index fd739435..ee85b12b 100644 --- a/Cslib/Computability/Automata/DFAToNFA.lean +++ b/Cslib/Computability/Automata/DFAToNFA.lean @@ -13,7 +13,7 @@ namespace DFA section NFA /-- `DFA` is a special case of `NFA`. -/ -@[grind =] +@[scoped grind =] def toNFA (dfa : DFA State Symbol) : NFA State Symbol where start := {dfa.start} accept := dfa.accept @@ -21,30 +21,30 @@ def toNFA (dfa : DFA State Symbol) : NFA State Symbol where finite_state := dfa.finite_state finite_symbol := dfa.finite_symbol -@[grind =] +@[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. -/ -@[grind =] +@[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. -/ -@[grind ⇒] +@[scoped grind ⇒] theorem toNFA_deterministic (dfa : DFA State Symbol) : dfa.toNFA.Deterministic := by grind /-- The transition system of a DA is image-finite. -/ -@[grind ⇒] +@[scoped grind ⇒] theorem toNFA_imageFinite (dfa : DFA State Symbol) : dfa.toNFA.ImageFinite := dfa.toNFA.deterministic_imageFinite dfa.toNFA_deterministic /-- Characterisation of multistep transitions. -/ -@[grind =] +@[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 @@ -53,11 +53,11 @@ theorem toNFA_mtr {dfa : DFA State Symbol} : case mpr => induction xs generalizing s1 <;> grind /-- The `NFA` constructed from a `DFA` has the same language. -/ -@[grind =] +@[scoped grind =] theorem toNFA_language_eq {dfa : DFA State Symbol} : dfa.toNFA.language = dfa.language := by ext xs - refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> grind + refine ⟨?_, fun _ => ⟨dfa.start, ?_⟩⟩ <;> open NFA in grind end NFA end DFA diff --git a/Cslib/Computability/Automata/EpsilonNFA.lean b/Cslib/Computability/Automata/EpsilonNFA.lean index 79276c48..07b8056a 100644 --- a/Cslib/Computability/Automata/EpsilonNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFA.lean @@ -20,7 +20,7 @@ structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symb /-- The type of symbols (also called 'alphabet') is finite. -/ finite_symbol : Finite Symbol -@[grind] +@[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` @@ -32,18 +32,18 @@ namespace εNFA /-- An εNFA accepts a string if there is a saturated multistep accepting derivative with that trace from the start state. -/ -@[grind] +@[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. -/ -@[grind] +@[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. -/ -@[grind] +@[scoped grind =] theorem accepts_mem_language (enfa : εNFA State Symbol) (xs : List Symbol) : enfa.Accepts xs ↔ xs ∈ enfa.language := by rfl diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean index 206bb2b0..e705fe58 100644 --- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean @@ -15,7 +15,7 @@ import Cslib.Computability.Automata.NFA private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where Tr := fun s μ s' => lts.Tr s (some μ) s' -@[grind] +@[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 @@ -26,7 +26,7 @@ namespace εNFA section NFA /-- Any εNFA can be converted into an NFA that does not use ε-transitions. -/ -@[grind] +@[scoped grind] def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where start := enfa.εClosure enfa.start accept := enfa.accept @@ -34,7 +34,7 @@ def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where finite_state := enfa.finite_state finite_symbol := enfa.finite_symbol -@[grind] +@[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 @@ -43,13 +43,13 @@ lemma LTS.noε_saturate_mTr /-- Correctness of `toNFA`. -/ -@[grind] +@[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] - grind + open NFA in grind end NFA end εNFA diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean index 109b8402..b19c0bf2 100644 --- a/Cslib/Computability/Automata/NFA.lean +++ b/Cslib/Computability/Automata/NFA.lean @@ -18,17 +18,17 @@ namespace NFA /-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from the start state. -/ -@[grind] +@[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. -/ -@[grind] +@[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. -/ -@[grind] +@[scoped grind] theorem accepts_mem_language (nfa : NFA State Symbol) (xs : List Symbol) : nfa.Accepts xs ↔ xs ∈ nfa.language := by rfl diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean index c9f14e2f..6a852474 100644 --- a/Cslib/Computability/Automata/NFAToDFA.lean +++ b/Cslib/Computability/Automata/NFAToDFA.lean @@ -14,7 +14,7 @@ namespace NFA section SubsetConstruction /-- Converts an `NFA` into a `DFA` using the subset construction. -/ -@[grind] +@[scoped grind =] def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := { start := nfa.start accept := { S | ∃ s ∈ S, s ∈ nfa.accept } @@ -26,7 +26,7 @@ def toDFA (nfa : NFA State Symbol) : DFA (Set State) Symbol := { } /-- Characterisation of transitions in `NFA.toDFA` wrt transitions in the original NA. -/ -@[grind] +@[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] @@ -34,8 +34,8 @@ theorem toDFA_mem_tr {nfa : NFA State Symbol} : /-- Characterisation of multistep transitions in `NFA.toDFA` wrt multistep transitions in the original NA. -/ -@[grind] -theorem toDA_mem_mtr {nfa : NFA State Symbol} : +@[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 @@ -48,17 +48,17 @@ theorem toDA_mem_mtr {nfa : NFA State Symbol} : grind /-- Characterisation of multistep transitions in `NFA.toDFA` as image transitions in `LTS`. -/ -@[grind] -theorem toDA_mtr_setImageMultistep {nfa : NFA State Symbol} : +@[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. -/ -@[grind] -theorem toDA_language_eq {nfa : NFA State Symbol} : +@[scoped grind =] +theorem toDFA_language_eq {nfa : NFA State Symbol} : nfa.toDFA.language = nfa.language := by ext xs rw [← DFA.accepts_mem_language] - grind + open DFA in grind end SubsetConstruction end NFA From 9a01e8442e7c76af3b9f87bb047bdb7b0d226692 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 6 Oct 2025 21:18:42 +0200 Subject: [PATCH 29/29] Move accept conditions around for better extensibility to omega automata in the future --- Cslib/Computability/Automata/DA.lean | 2 -- Cslib/Computability/Automata/DFA.lean | 2 ++ Cslib/Computability/Automata/EpsilonNFA.lean | 2 ++ Cslib/Computability/Automata/NA.lean | 2 -- Cslib/Computability/Automata/NFA.lean | 2 ++ 5 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean index 3e9322a5..a9f5a85f 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA.lean @@ -13,7 +13,5 @@ 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 set of accepting states of the automaton. -/ - accept : Set State /-- The transition function of the automaton. -/ tr : State → Symbol → State diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean index b64ce190..c6a42f33 100644 --- a/Cslib/Computability/Automata/DFA.lean +++ b/Cslib/Computability/Automata/DFA.lean @@ -21,6 +21,8 @@ a finite string. `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. -/ diff --git a/Cslib/Computability/Automata/EpsilonNFA.lean b/Cslib/Computability/Automata/EpsilonNFA.lean index 07b8056a..0b62a42c 100644 --- a/Cslib/Computability/Automata/EpsilonNFA.lean +++ b/Cslib/Computability/Automata/EpsilonNFA.lean @@ -15,6 +15,8 @@ Internally, ε (`Option.none`) is treated as the `τ` label of the underlying tr 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. -/ diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index 99841a81..71d5592d 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -17,5 +17,3 @@ type `State → Symbol → Set State`; it gets automatically expanded to the for structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where /-- The set of initial states of the automaton. -/ start : Set State - /-- The set of accepting states of the automaton. -/ - accept : Set State diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean index b19c0bf2..1d3df5ba 100644 --- a/Cslib/Computability/Automata/NFA.lean +++ b/Cslib/Computability/Automata/NFA.lean @@ -9,6 +9,8 @@ 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. -/