From dc83a75e7fe6346e59a344d5d63999b368fde109 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 11 Jan 2026 13:15:39 +0100 Subject: [PATCH 1/3] feat: LTS.IsExecution --- Cslib/Computability/Automata/NA/Concat.lean | 4 +- Cslib/Computability/Automata/NA/Loop.lean | 2 +- Cslib/Foundations/Semantics/LTS/Basic.lean | 71 ++++++++++++++++++--- 3 files changed, 64 insertions(+), 13 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index a1846afd..b5d1d3ed 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/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 diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean index dc24fb30..8fa945ad 100644 --- a/Cslib/Computability/Automata/NA/Loop.lean +++ b/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 diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 18a81f82..2a4f6df0 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/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,71 @@ 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) + (ss : List State) (μs : List Label) : Prop := + ∃ hlen : ss.length = μs.length + 1, ∀ k, {valid : 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 ss μs) : 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] [] := by + exists (by grind) + intro k valid + cases valid + +/-- Equivalent of `MTr.stepL` for executions. -/ +@[scoped grind →] +theorem LTS.IsExecution.stepL {lts : LTS State Label} (htr : lts.Tr s1 μ s2) + (hexec : lts.IsExecution ss μs) (hjoin : ss[0]'(by grind) = s2) : + lts.IsExecution (s1 :: ss) (μ :: μs) := by + grind + +/-- Deconstruction of executions with `List.cons`. -/ +@[scoped grind →] +theorem LTS.isExecution_cons_invert (h : lts.IsExecution (s :: ss) (μ :: μs)) : + lts.IsExecution ss μs := by + obtain ⟨h1, h2⟩ := h + exists (by grind) + intro k valid + specialize h2 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, ∃ _ : ss.length = μs.length + 1, + ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧ lts.IsExecution ss μs := 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', hlen, ih⟩ := ih + use t1 :: ss' grind +/-- Converts an execution into a multistep transition. -/ +@[scoped grind →] +theorem LTS.isExecution_mTr (hexec : lts.IsExecution ss μs) : + lts.MTr (ss[0]'(by grind)) μs (ss[ss.length - 1]'(by grind)) := by + induction ss generalizing μs + case nil => grind + case cons s1 ss ih => + cases μs <;> grind + +/-- Correspondence of multistep transitions and executions. -/ +@[scoped grind =] +theorem LTS.mTr_isExecution_iff : lts.MTr s1 μs s2 ↔ + ∃ ss : List State, ∃ _ : ss.length = μs.length + 1, + ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧ lts.IsExecution ss μs := by + grind + /-- A state `s1` can reach a state `s2` if there exists a multistep transition from `s1` to `s2`. -/ @[scoped grind =] @@ -262,7 +313,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 From 2e667404d6a68cfc789533b9c3299bfbddf0df04 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Mon, 12 Jan 2026 17:17:15 +0100 Subject: [PATCH 2/3] simplify a proof --- Cslib/Foundations/Semantics/LTS/Basic.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 2a4f6df0..6e54afe6 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -154,16 +154,13 @@ theorem LTS.isExecution_nonEmpty_states (h : lts.IsExecution ss μs) : ss ≠ [] @[scoped grind ⇒] theorem LTS.IsExecution.refl (lts : LTS State Label) (s : State) : lts.IsExecution [s] [] := by - exists (by grind) - intro k valid - cases valid + 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 ss μs) (hjoin : ss[0]'(by grind) = s2) : - lts.IsExecution (s1 :: ss) (μ :: μs) := by - grind + lts.IsExecution (s1 :: ss) (μ :: μs) := by grind /-- Deconstruction of executions with `List.cons`. -/ @[scoped grind →] From d5cee8f6ff0c2f6007404e8c23ccf632176fb433 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 15 Jan 2026 10:31:37 +0100 Subject: [PATCH 3/3] add start and final states to IsExecution --- Cslib/Foundations/Semantics/LTS/Basic.lean | 60 +++++++++++++--------- 1 file changed, 36 insertions(+), 24 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 6e54afe6..acf0f05d 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -142,64 +142,76 @@ theorem LTS.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by /-- A finite execution, or sequence of transitions. -/ @[scoped grind =] -def LTS.IsExecution (lts : LTS State Label) - (ss : List State) (μs : List Label) : Prop := - ∃ hlen : ss.length = μs.length + 1, ∀ k, {valid : k < μs.length} → lts.Tr ss[k] μs[k] ss[k + 1] +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 ss μs) : ss ≠ [] := by 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] [] := by +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 ss μs) (hjoin : ss[0]'(by grind) = s2) : - lts.IsExecution (s1 :: ss) (μ :: μs) := by grind + (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 (s :: ss) (μ :: μs)) : - lts.IsExecution ss μs := by - obtain ⟨h1, h2⟩ := h +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) - intro k valid - specialize h2 k <;> 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, ∃ _ : ss.length = μs.length + 1, - ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧ lts.IsExecution ss μs := by +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 htr hmtr ih => - obtain ⟨ss', hlen, ih⟩ := ih + obtain ⟨ss', _⟩ := ih use t1 :: ss' grind /-- Converts an execution into a multistep transition. -/ @[scoped grind →] -theorem LTS.isExecution_mTr (hexec : lts.IsExecution ss μs) : - lts.MTr (ss[0]'(by grind)) μs (ss[ss.length - 1]'(by grind)) := by - induction ss generalizing μs +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 => - cases μs <;> 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, ∃ _ : ss.length = μs.length + 1, - ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧ lts.IsExecution ss μs := by + ∃ 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