feat: add notion of finite execution for LTS

Cslib/Computability/Automata/NA/Concat.lean

@@ -96,13 +96,13 @@ theorem concat_run_exists {xs1 : List Symbol} {xs2 : ωSequence Symbol} {ss2 : 
   · obtain ⟨rfl⟩ : xs1 = [] := List.eq_nil_iff_length_eq_zero.mpr h_xs1
     refine ⟨ss2.map inr, by simp only [concat]; grind [Run, LTS.ωTr], by simp⟩
   · obtain ⟨s0, _, _, _, h_mtr⟩ := h1
-    obtain ⟨ss1, _, _, _, _⟩ := LTS.MTr.exists_states h_mtr
+    obtain ⟨ss1, _, _, _, _⟩ := LTS.mTr_isExecution h_mtr
     let ss := (ss1.map inl).take xs1.length ++ω ss2.map inr
     refine ⟨ss, Run.mk ?_ ?_, ?_⟩
     · grind [concat, get_append_left]
     · have (k) (h_k : ¬ k < xs1.length) : k + 1 - xs1.length = k - xs1.length + 1 := by grind
       simp only [concat]
-      grind [Run, LTS.ωTr, get_append_right', get_append_left]
+      grind [Run, LTS.ωTr, get_append_right', get_append_left, LTS.IsExecution]
     · grind [drop_append_of_le_length]
 
 namespace Buchi

Cslib/Computability/Automata/NA/Loop.lean

@@ -95,7 +95,7 @@ theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
     sl[0] = inl () ∧ sl[xl.length] = inl () ∧
     ∀ k, ∀ _ : k < xl.length, na.loop.Tr sl[k] xl[k] sl[k + 1] := by
   obtain ⟨_, _, _, _, h_mtr⟩ := h
-  obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states h_mtr
+  obtain ⟨sl, _, _, _, _⟩ := LTS.mTr_isExecution h_mtr
   by_cases xl.length = 0
   · use [inl ()]
     grind

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -69,7 +69,7 @@ def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Labe
 
 section MultiStep
 
-/-! ## Multistep transitions with finite traces
+/-! ## Multistep transitions and executions with finite traces
 
 This section treats executions with a finite number of steps.
 -/
@@ -140,20 +140,80 @@ theorem LTS.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by
   cases h
   rfl
 
-/-- For every multistep transition, there exists a sequence of intermediate states
-which satisfies the single-step transition at every step. -/
-theorem LTS.MTr.exists_states {lts : LTS State Label} {s1 s2 : State} {μs : List Label}
-    (h : lts.MTr s1 μs s2) : ∃ ss : List State, ∃ _ : ss.length = μs.length + 1,
-    ss[0] = s1 ∧ ss[μs.length] = s2 ∧ ∀ k, ∀ _ : k < μs.length, lts.Tr ss[k] μs[k] ss[k + 1] := by
+/-- A finite execution, or sequence of transitions. -/
+@[scoped grind =]
+def LTS.IsExecution (lts : LTS State Label) (s1 : State) (μs : List Label) (s2 : State)
+    (ss : List State) : Prop :=
+  ∃ _ : ss.length = μs.length + 1, ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧
+  ∀ k, {_ : k < μs.length} → lts.Tr ss[k] μs[k] ss[k + 1]
+
+/-- Every execution has a start state. -/
+@[scoped grind →]
+theorem LTS.isExecution_nonEmpty_states (h : lts.IsExecution s1 μs s2 ss) :
+    ss ≠ [] := by grind
+
+/-- Every state has an execution of zero steps terminating in itself. -/
+@[scoped grind ⇒]
+theorem LTS.IsExecution.refl (lts : LTS State Label) (s : State) : lts.IsExecution s [] s [s] := by
+  grind
+
+/-- Equivalent of `MTr.stepL` for executions. -/
+@[scoped grind →]
+theorem LTS.IsExecution.stepL {lts : LTS State Label} (htr : lts.Tr s1 μ s2)
+    (hexec : lts.IsExecution s2 μs s3 ss) : lts.IsExecution s1 (μ :: μs) s3 (s1 :: ss) := by grind
+
+/-- Deconstruction of executions with `List.cons`. -/
+@[scoped grind →]
+theorem LTS.isExecution_cons_invert (h : lts.IsExecution s1 (μ :: μs) s2 (s1 :: ss)) :
+    lts.IsExecution (ss[0]'(by grind)) μs s2 ss := by
+  obtain ⟨_, _, _, h4⟩ := h
+  exists (by grind)
+  constructorm* _∧_
+  · rfl
+  · grind
+  · intro k valid
+    specialize h4 k <;> grind
+
+open scoped LTS.IsExecution in
+/-- A multistep transition implies the existence of an execution. -/
+@[scoped grind →]
+theorem LTS.mTr_isExecution {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State}
+    (h : lts.MTr s1 μs s2) : ∃ ss : List State, lts.IsExecution s1 μs s2 ss := by
   induction h
   case refl t =>
     use [t]
     grind
-  case stepL t1 μ t2 μs t3 h_tr h_mtr h_ind =>
-    obtain ⟨ss', _, _, _, _⟩ := h_ind
-    use [t1] ++ ss'
+  case stepL t1 μ t2 μs t3 htr hmtr ih =>
+    obtain ⟨ss', _⟩ := ih
+    use t1 :: ss'
     grind
 
+/-- Converts an execution into a multistep transition. -/
+@[scoped grind →]
+theorem LTS.isExecution_mTr (hexec : lts.IsExecution s1 μs s2 ss) :
+    lts.MTr s1 μs s2 := by
+  induction ss generalizing s1 μs
+  case nil => grind
+  case cons s1' ss ih =>
+    let ⟨hlen, hstart, hfinal, hexec'⟩ := hexec
+    have : s1' = s1 := by grind
+    rw [this] at hexec' hexec
+    cases μs
+    · grind
+    case cons μ μs =>
+      specialize ih (s1 := ss[0]'(by grind)) (μs := μs)
+      apply LTS.isExecution_cons_invert at hexec
+      apply LTS.MTr.stepL
+      · have : lts.Tr s1 μ (ss[0]'(by grind)) := by grind
+        apply this
+      · grind
+
+/-- Correspondence of multistep transitions and executions. -/
+@[scoped grind =]
+theorem LTS.mTr_isExecution_iff : lts.MTr s1 μs s2 ↔
+    ∃ ss : List State, lts.IsExecution s1 μs s2 ss := by
+  grind
+
 /-- A state `s1` can reach a state `s2` if there exists a multistep transition from
 `s1` to `s2`. -/
 @[scoped grind =]
@@ -262,7 +322,7 @@ theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0
 /-- Prepends an infinite execution with a finite execution. -/
 theorem LTS.ωTr.append (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs)
     (hm : ss 0 = t) : ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t := by
-  obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states hmtr
+  obtain ⟨sl, _, _, _, _⟩ := LTS.mTr_isExecution hmtr
   refine ⟨sl ++ω ss.drop 1, ?_, by grind [get_append_left], by grind [get_append_left]⟩
   intro n
   by_cases n < μl.length