From 46281db6f60bfbb2544264e4c48ff4e4768db3a8 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Wed, 18 Mar 2026 12:27:57 -0700 Subject: [PATCH] chore: rename definitions and theorems about LTS.Execution and LTS.OmegaExecution --- Cslib/Computability/Automata/NA/Basic.lean | 2 +- Cslib/Computability/Automata/NA/Concat.lean | 10 +- Cslib/Computability/Automata/NA/Loop.lean | 8 +- Cslib/Computability/Automata/NA/Pair.lean | 11 +- Cslib/Computability/Automata/NA/Sum.lean | 2 +- Cslib/Computability/Automata/NA/Total.lean | 4 +- .../Congruences/BuchiCongruence.lean | 27 ++-- Cslib/Foundations/Semantics/LTS/Basic.lean | 150 +++++++++--------- CslibTests/GrindLint.lean | 2 +- 9 files changed, 115 insertions(+), 101 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Basic.lean b/Cslib/Computability/Automata/NA/Basic.lean index 88ee3901f..97059fab4 100644 --- a/Cslib/Computability/Automata/NA/Basic.lean +++ b/Cslib/Computability/Automata/NA/Basic.lean @@ -47,7 +47,7 @@ variable {State Symbol : Type*} /-- Infinite run. -/ structure Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) where start : ss 0 ∈ na.start - trans : na.ωTr ss xs + trans : na.OmegaExecution ss xs /-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/ structure FinAcc (State Symbol : Type*) extends NA State Symbol where diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index 0454f909d..ba9b69a94 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/Cslib/Computability/Automata/NA/Concat.lean @@ -97,15 +97,15 @@ theorem concat_run_exists {xs1 : List Symbol} {xs2 : ωSequence Symbol} {ss2 : ∃ ss, (concat na1 na2).Run (xs1 ++ω xs2) ss ∧ ss.drop xs1.length = ss2.map inr := by by_cases h_xs1 : xs1.length = 0 · 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⟩ + refine ⟨ss2.map inr, by simp only [concat]; grind [Run, LTS.OmegaExecution], by simp⟩ · obtain ⟨s0, _, _, _, h_mtr⟩ := h1 - obtain ⟨ss1, _, _, _, _⟩ := LTS.mTr_extract_isExecution h_mtr + obtain ⟨ss1, _, _, _, _⟩ := LTS.execution_of_mTr 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, LTS.IsExecution] + grind [Run, LTS.OmegaExecution, get_append_right', get_append_left, LTS.Execution] · grind [drop_append_of_le_length] namespace Buchi @@ -156,7 +156,7 @@ theorem finConcat_language_eq [Inhabited Symbol] : ext xl constructor · rintro ⟨s, _, t, h_acc, h_mtr⟩ - obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr h_mtr + obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_omegaExecution h_mtr have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run] have hr : (ss xl.length).isRight := by grind obtain ⟨n, _⟩ := concat_run_proj hc hr @@ -173,7 +173,7 @@ theorem finConcat_language_eq [Inhabited Symbol] : grind [ finConcat, List.length_append, take_append_of_le_length, extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss, - LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length)) + LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length)) ] end FinAcc diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean index 111b4646c..5858a60ed 100644 --- a/Cslib/Computability/Automata/NA/Loop.lean +++ b/Cslib/Computability/Automata/NA/Loop.lean @@ -99,7 +99,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_extract_isExecution h_mtr + obtain ⟨sl, _, _, _, _⟩ := LTS.execution_of_mTr h_mtr by_cases xl.length = 0 · use [inl ()] grind @@ -128,7 +128,7 @@ theorem loop_run_exists [Inhabited Symbol] {xls : ωSequence (List Symbol)} let ts := ωSequence.const (inl () : Unit ⊕ State) have h_mtr (k : ℕ) : na.loop.MTr (ts k) (xls k) (ts (k + 1)) := by grind [loop_fin_run_mtr] have h_pos (k : ℕ) : (xls k).length > 0 := by grind - obtain ⟨ss, _, _⟩ := LTS.ωTr.flatten h_mtr h_pos + obtain ⟨ss, _, _⟩ := LTS.OmegaExecution.flatten_mTr h_mtr h_pos use ss grind [Run.mk, FinAcc.loop, cumLen_zero (ls := xls)] @@ -186,7 +186,7 @@ theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) : · have : Nonempty na.start := by obtain ⟨_, s0, _, _⟩ := nonempty_iff_ne_empty.mpr h use s0 - obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr h_mtr + obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_omegaExecution h_mtr have h_run : na.finLoop.Run (xl ++ω xs) ss := by grind [Run] obtain ⟨h1, h2⟩ : 0 < xl.length ∧ (ss xl.length).isLeft := by simp only [mem_singleton_iff] at h_acc @@ -195,7 +195,7 @@ theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) : left; refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩ · grind [totalize_language_eq, take_append_of_le_length] · refine ⟨ss n, by grind, ss xl.length, by grind, ?_⟩ - have := LTS.ωTr_mTr h_ωtr' (show 0 ≤ xl.length - n by grind) + have := LTS.OmegaExecution.extract_mTr h_ωtr' (show 0 ≤ xl.length - n by grind) have : n + (xl.length - n) = xl.length := by grind have : ((xl ++ω xs).drop n).extract 0 (xl.length - n) = xl.drop n := by grind [extract_eq_take, drop_append_of_le_length, take_append_of_le_length] diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean index 6b1540426..3a450925d 100644 --- a/Cslib/Computability/Automata/NA/Pair.lean +++ b/Cslib/Computability/Automata/NA/Pair.lean @@ -112,7 +112,8 @@ theorem language_eq_fin_iSup_hmul_omegaPow use ss 0, by grind [NA.Run], t, h_acc obtain ⟨f, h_mono, h_f⟩ := frequently_iff_strictMono.mp h_t refine ⟨xs.take (f 0), ?_, xs.drop (f 0), ?_, by grind⟩ - · have : na.MTr (ss 0) (xs.extract 0 (f 0)) (ss (f 0)) := by grind [LTS.ωTr_mTr, NA.Run] + · have : na.MTr (ss 0) (xs.extract 0 (f 0)) (ss (f 0)) := by + grind [LTS.OmegaExecution.extract_mTr, NA.Run] grind [extract_eq_drop_take] · simp only [omegaPow_seq_prop, LTS.mem_pairLang] use (f · - f 0) @@ -121,7 +122,8 @@ theorem language_eq_fin_iSup_hmul_omegaPow · simp · intro n have mono_f (k : ℕ) : f 0 ≤ f (n + k) := h_mono.monotone (by grind) - grind [extract_drop, mono_f 0, LTS.ωTr_mTr h_run.trans <| h_mono.monotone (?_ : n ≤ n + 1)] + grind [extract_drop, mono_f 0, + LTS.OmegaExecution.extract_mTr h_run.trans <| h_mono.monotone (?_ : n ≤ n + 1)] · rintro ⟨s, _, t, _, yl, h_yl, zs, h_zs, rfl⟩ obtain ⟨zls, rfl, h_zls⟩ := mem_omegaPow.mp h_zs let ts := ωSequence.const t @@ -129,9 +131,10 @@ theorem language_eq_fin_iSup_hmul_omegaPow grind [Language.mem_sub_one, LTS.mem_pairLang] have h_pos (n : ℕ) : (zls n).length > 0 := by grind [Language.mem_sub_one, List.eq_nil_iff_length_eq_zero] - obtain ⟨zss, h_zss, _⟩ := LTS.ωTr.flatten h_mtr h_pos + obtain ⟨zss, h_zss, _⟩ := LTS.OmegaExecution.flatten_mTr h_mtr h_pos have (n : ℕ) : zss (zls.cumLen n) = t := by grind - obtain ⟨xss, _, _, _, _⟩ := LTS.ωTr.append h_yl h_zss (by grind [cumLen_zero (ls := zls)]) + obtain ⟨xss, _, _, _, _⟩ := LTS.OmegaExecution.append h_yl h_zss + (by grind [cumLen_zero (ls := zls)]) use xss, by grind [NA.Run] apply (drop_frequently_iff_frequently yl.length).mp apply frequently_iff_strictMono.mpr diff --git a/Cslib/Computability/Automata/NA/Sum.lean b/Cslib/Computability/Automata/NA/Sum.lean index 9fa33116d..541e15243 100644 --- a/Cslib/Computability/Automata/NA/Sum.lean +++ b/Cslib/Computability/Automata/NA/Sum.lean @@ -51,7 +51,7 @@ theorem iSum_run_iff {na : (i : I) → NA (State i) Symbol} constructor · simp only [iSum, get_map, mem_iUnion] grind [NA.Run] - · simp only [LTS.ωTr] + · simp only [LTS.OmegaExecution] grind [NA.Run] namespace Buchi diff --git a/Cslib/Computability/Automata/NA/Total.lean b/Cslib/Computability/Automata/NA/Total.lean index 3462a82bc..18d1756fd 100644 --- a/Cslib/Computability/Automata/NA/Total.lean +++ b/Cslib/Computability/Automata/NA/Total.lean @@ -38,14 +38,14 @@ theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (State ⊕ Un refine ⟨?_, by grind⟩ -- TODO: `grind` does not use congruence relations with `na.totalize.MTr` rw [← LTS.totalize.mtr_left_iff, ← extract_eq_take, eq₁, ← eq₂] - exact LTS.ωTr_mTr h.trans (by grind) + exact LTS.OmegaExecution.extract_mTr h.trans (by grind) /-- Any finite execution of the original NA can be extended to an infinite execution of `NA.totalize`, provided that the alphabet is inbabited. -/ theorem totalize_mtr_run [Inhabited Symbol] {xl : List Symbol} {s t : State} (hs : s ∈ na.start) (hm : na.MTr s xl t) : ∃ xs ss, na.totalize.Run (xl ++ω xs) ss ∧ ss 0 = inl s ∧ ss xl.length = inl t := by - grind [totalize, Run, LTS.Total.mTr_ωTr <| LTS.totalize.mtr_left_iff.mpr hm] + grind [totalize, Run, LTS.Total.mTr_omegaExecution <| LTS.totalize.mtr_left_iff.mpr hm] namespace FinAcc diff --git a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean index c9b0be95c..a562de9b4 100644 --- a/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/BuchiCongruence.lean @@ -81,16 +81,16 @@ if `xl` makes `na` go through an accepting state of `na`, then so can `yl`. -/ lemma buchiCongruence_transfer {a : Quotient na.BuchiCongruence.eq} {xl yl : List Symbol} {s t : State} (hc : xl ∈ na.BuchiCongruence.eqvCls a) (hc' : yl ∈ na.BuchiCongruence.eqvCls a) - (hp : xl ∈ na.pairLang s t) : ∃ sl, na.IsExecution s yl t sl ∧ + (hp : xl ∈ na.pairLang s t) : ∃ sl, na.Execution s yl t sl ∧ ( xl ∈ na.pairViaLang na.accept s t → ∃ r ∈ na.accept, r ∈ sl ) := by have h_eq : na.BuchiCongruence.eq xl yl := by apply Quotient.exact grind have := h_eq s t have h_yl : yl ∈ na.pairLang s t := by grind - have := LTS.mTr_extract_isExecution h_yl - grind [LTS.mem_pairViaLang, LTS.IsExecution, → LTS.IsExecution.comp, - → LTS.mTr_extract_isExecution] + have := LTS.execution_of_mTr h_yl + grind [LTS.mem_pairViaLang, LTS.Execution, → LTS.Execution.comp, + → LTS.execution_of_mTr] /-- `na.buchiFamily` is a family of ω-languages indexed by a pair of equivalence classes of `na.BuchiCongruence` which will turn out to saturate the ω-language accepted by `na` @@ -110,7 +110,8 @@ theorem mem_buchiFamily [Inhabited Symbol] -- because that proof was too big and kept exceeding the default `maxHeartbeats`. private lemma frequently_via_accept [Inhabited Symbol] {xl : List Symbol} {xls : ωSequence (List Symbol)} {ss : ωSequence State} - (h_acc : ∃ᶠ (k : ℕ) in atTop, ss k ∈ na.accept) (h_exec : na.ωTr ss (xl ++ω xls.flatten)) + (h_acc : ∃ᶠ (k : ℕ) in atTop, ss k ∈ na.accept) + (h_exec : na.OmegaExecution ss (xl ++ω xls.flatten)) (h_xls_p : ∀ (k : ℕ), (xls k).length > 0) (f : ℕ → ℕ) (h_f : f = fun k => xl.length + xls.cumLen k) (ts : ωSequence State) (h_ts : ts = ωSequence.mk (fun k ↦ ss (f k))) : @@ -121,7 +122,8 @@ private lemma frequently_via_accept [Inhabited Symbol] apply LTS.mem_pairViaLang.mpr use ss (f n + k), by grind, (xls n).take k, (xls n).drop k have := extract_flatten h_xls_p n - have exec {m n} (h : m ≤ n) := LTS.isExecution_mTr na.toLTS <| LTS.ωTr_isExecution h_exec h + have exec {m n} (h : m ≤ n) := + LTS.mTr_of_execution na.toLTS <| LTS.OmegaExecution.extract_execution h_exec h split_ands · have h : f n ≤ f n + k := by lia specialize exec h @@ -141,24 +143,25 @@ theorem buchiFamily_saturation [Inhabited Symbol] : Saturates na.buchiFamily (la let ts := ωSequence.mk (fun k ↦ ss (f k)) have h_xls_p (k : ℕ) : (xls k).length > 0 := by grind [Language.mem_sub_one] have h_xls_e (k : ℕ) : xls k ∈ na.pairLang (ts k) (ts (k + 1)) := by - grind [LTS.ωTr_mTr h_exec (?_ : f k ≤ f (k + 1)), LTS.mem_pairLang, extract_append_right_right, - add_tsub_cancel_left] + grind [LTS.OmegaExecution.extract_mTr h_exec (?_ : f k ≤ f (k + 1)), LTS.mem_pairLang, + extract_append_right_right, add_tsub_cancel_left] have h_yls (k : ℕ) := buchiCongruence_transfer ((h_xls_c k).left) ((h_yls_c k).left) (h_xls_e k) choose sls h_yls_e h_yls_a using h_yls have h_yls_p (k : ℕ) : (yls k).length > 0 := by grind [Language.mem_sub_one] - obtain ⟨ss1, h_ss1_run, h_ss1_seg⟩ := LTS.IsExecution.flatten h_yls_e h_yls_p + obtain ⟨ss1, h_ss1_run, h_ss1_seg⟩ := LTS.OmegaExecution.flatten_execution h_yls_e h_yls_p suffices ∃ᶠ (k : ℕ) in atTop, ss1 k ∈ na.accept by have h_xl_e : xl ∈ na.pairLang (ss 0) (ts 0) := by - grind [LTS.ωTr_mTr h_exec (?_ : 0 ≤ xl.length), extract_append_zero_right, LTS.mem_pairLang] + grind [LTS.OmegaExecution.extract_mTr h_exec (?_ : 0 ≤ xl.length), + extract_append_zero_right, LTS.mem_pairLang] have h_yl_e : yl ∈ na.pairLang (ss 0) (ts 0) := by - grind [buchiCongruence_transfer h_xl_c h_yl_c h_xl_e, LTS.mem_pairLang, LTS.isExecution_mTr] + grind [buchiCongruence_transfer h_xl_c h_yl_c h_xl_e, LTS.mem_pairLang, LTS.mTr_of_execution] have h_ss1_ts : ss1 0 = ts 0 := by have h : 0 < yls.cumLen 1 - yls.cumLen 0 := by grind have : 0 < (sls 0).length := by grind have : ss1 0 = (sls 0)[0] := by grind [get_extract (xs := ss1) h] have : (sls 0)[0] = ts 0 := h_yls_e 0 |>.choose_spec |>.1 grind - obtain ⟨ss2, _, _, _, _⟩ := LTS.ωTr.append h_yl_e h_ss1_run h_ss1_ts + obtain ⟨ss2, _, _, _, _⟩ := LTS.OmegaExecution.append h_yl_e h_ss1_run h_ss1_ts use ss2 have := @drop_frequently_iff_frequently _ ss2 na.accept yl.length grind [Run.mk] diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 2de27ef11..3490f3a79 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -140,30 +140,30 @@ theorem LTS.MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by cases h rfl -/-- A finite execution, or sequence of transitions. -/ +/-- LTS.Execution extends LTS.MTr by providing the intermediate states of a multistep transition. -/ @[scoped grind =] -def LTS.IsExecution (lts : LTS State Label) (s1 : State) (μs : List Label) (s2 : State) +def LTS.Execution (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. -/ +/-- Every execution has at least one intermediate state. -/ @[scoped grind →] -theorem LTS.isExecution_nonEmpty_states (h : lts.IsExecution s1 μs s2 ss) : +theorem LTS.execution_nonEmpty_states (h : lts.Execution 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 +theorem LTS.Execution.refl (lts : LTS State Label) (s : State) : lts.Execution s [] s [s] := by grind /-- Equivalent of `MTr.stepL` for executions. -/ -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 +theorem LTS.Execution.stepL {lts : LTS State Label} (htr : lts.Tr s1 μ s2) + (hexec : lts.Execution s2 μs s3 ss) : lts.Execution s1 (μ :: μs) s3 (s1 :: ss) := by grind /-- Deconstruction of executions with `List.cons`. -/ -theorem LTS.isExecution_cons_invert (h : lts.IsExecution s1 (μ :: μs) s2 (s1 :: ss)) : - lts.IsExecution (ss[0]'(by grind)) μs s2 ss := by +theorem LTS.execution_cons_invert (h : lts.Execution s1 (μ :: μs) s2 (s1 :: ss)) : + lts.Execution (ss[0]'(by grind)) μs s2 ss := by obtain ⟨_, _, _, h4⟩ := h exists (by grind) constructorm* _∧_ @@ -172,12 +172,12 @@ theorem LTS.isExecution_cons_invert (h : lts.IsExecution s1 (μ :: μs) s2 (s1 : · intro k valid specialize h4 k <;> grind -open scoped LTS.IsExecution in +open scoped LTS.Execution in /-- A multistep transition implies the existence of an execution. -/ @[scoped grind →] -theorem LTS.mTr_extract_isExecution {lts : LTS State Label} +theorem LTS.execution_of_mTr {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 + (h : lts.MTr s1 μs s2) : ∃ ss : List State, lts.Execution s1 μs s2 ss := by induction h case refl t => use [t] @@ -189,7 +189,7 @@ theorem LTS.mTr_extract_isExecution {lts : LTS State Label} /-- Converts an execution into a multistep transition. -/ @[scoped grind →] -theorem LTS.isExecution_mTr (hexec : lts.IsExecution s1 μs s2 ss) : +theorem LTS.mTr_of_execution (hexec : lts.Execution s1 μs s2 ss) : lts.MTr s1 μs s2 := by induction ss generalizing s1 μs case nil => grind @@ -201,7 +201,7 @@ theorem LTS.isExecution_mTr (hexec : lts.IsExecution s1 μs s2 ss) : · grind case cons μ μs => specialize ih (s1 := ss[0]'(by grind)) (μs := μs) - apply LTS.isExecution_cons_invert at hexec + apply LTS.execution_cons_invert at hexec apply LTS.MTr.stepL · have : lts.Tr s1 μ (ss[0]'(by grind)) := by grind apply this @@ -209,13 +209,13 @@ theorem LTS.isExecution_mTr (hexec : lts.IsExecution s1 μs s2 ss) : /-- Correspondence of multistep transitions and executions. -/ @[scoped grind =] -theorem LTS.mTr_extract_isExecution_iff : lts.MTr s1 μs s2 ↔ - ∃ ss : List State, lts.IsExecution s1 μs s2 ss := by +theorem LTS.mTr_iff_execution : + lts.MTr s1 μs s2 ↔ ∃ ss : List State, lts.Execution s1 μs s2 ss := by grind -lemma LTS.IsExecution.comp_helper +private lemma LTS.Execution.comp_helper {lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State} - (h1 : lts.IsExecution s μs1 r ss1) (h2 : lts.IsExecution r μs2 t ss2) + (h1 : lts.Execution s μs1 r ss1) (h2 : lts.Execution r μs2 t ss2) (k : ℕ) (h_k : k < ss2.length) : (ss1 ++ ss2.tail)[μs1.length + k]'(by grind) = ss2[k] := by by_cases h : k = 0 @@ -226,38 +226,38 @@ lemma LTS.IsExecution.comp_helper grind /-- The composition of two executions is an execution. -/ -theorem LTS.IsExecution.comp +theorem LTS.Execution.comp {lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State} - (h1 : lts.IsExecution s μs1 r ss1) (h2 : lts.IsExecution r μs2 t ss2) : - lts.IsExecution s (μs1 ++ μs2) t (ss1 ++ ss2.tail) := by + (h1 : lts.Execution s μs1 r ss1) (h2 : lts.Execution r μs2 t ss2) : + lts.Execution s (μs1 ++ μs2) t (ss1 ++ ss2.tail) := by have h0 : (ss1 ++ ss2.tail).length = (μs1 ++ μs2).length + 1 := by grind use h0 split_ands · grind - · have := LTS.IsExecution.comp_helper h1 h2 μs2.length - grind only [IsExecution, = List.length_append] + · have := LTS.Execution.comp_helper h1 h2 μs2.length + grind only [Execution, = List.length_append] · intro k h_k by_cases k < μs1.length - · grind only [IsExecution, = List.getElem_append] - · have := LTS.IsExecution.comp_helper h1 h2 (k - μs1.length) - have := LTS.IsExecution.comp_helper h1 h2 (k - μs1.length + 1) + · grind only [Execution, = List.getElem_append] + · have := LTS.Execution.comp_helper h1 h2 (k - μs1.length) + have := LTS.Execution.comp_helper h1 h2 (k - μs1.length + 1) grind /-- An execution can be split at any intermediate state into two executions. -/ -theorem LTS.IsExecution.split +theorem LTS.Execution.split {lts : LTS State Label} {s t : State} {μs : List Label} {ss : List State} - (he : lts.IsExecution s μs t ss) (n : ℕ) (hn : n ≤ μs.length) : - lts.IsExecution s (μs.take n) (ss[n]'(by grind)) (ss.take (n + 1)) ∧ - lts.IsExecution (ss[n]'(by grind)) (μs.drop n) t (ss.drop n) := by + (he : lts.Execution s μs t ss) (n : ℕ) (hn : n ≤ μs.length) : + lts.Execution s (μs.take n) (ss[n]'(by grind)) (ss.take (n + 1)) ∧ + lts.Execution (ss[n]'(by grind)) (μs.drop n) t (ss.drop n) := by have : n + (ss.length - n - 1) = ss.length - 1 := by grind - simp [IsExecution] + simp [Execution] grind /-- A multistep transition over a concatenation can be split into two multistep transitions. -/ theorem LTS.MTr.split {lts : LTS State Label} {s0 : State} {μs1 μs2 : List Label} {s2 : State} (h : lts.MTr s0 (μs1 ++ μs2) s2) : ∃ s1, lts.MTr s0 μs1 s1 ∧ lts.MTr s1 μs2 s2 := by - obtain ⟨ss, h_ss⟩ := LTS.mTr_extract_isExecution h - have := LTS.IsExecution.split h_ss μs1.length + obtain ⟨ss, h_ss⟩ := LTS.execution_of_mTr h + have := LTS.Execution.split h_ss μs1.length grind /-- A state `s1` can reach a state `s2` if there exists a multistep transition from @@ -333,40 +333,44 @@ end MultiStep section ωMultiStep /-! ## Infinite sequences of transitions - -This section treats infinite executions as ω-sequences of transitions. -/ -/-- Definition of an infinite execution, or ω-sequence of transitions. -/ +/-- An infinite execution is conceptually an infinite sequence of transitions. But it is +technically more convenient to separate the states and the labels into two ω-sequences. -/ @[scoped grind] -def LTS.ωTr (lts : LTS State Label) (ss : ωSequence State) (μs : ωSequence Label) : - Prop := ∀ i, lts.Tr (ss i) (μs i) (ss (i + 1)) +def LTS.OmegaExecution (lts : LTS State Label) + (ss : ωSequence State) (μs : ωSequence Label) : Prop := + ∀ i, lts.Tr (ss i) (μs i) (ss (i + 1)) variable {lts : LTS State Label} open ωSequence /-- Any finite execution extracted from an infinite execution is valid. -/ -theorem LTS.ωTr_isExecution (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) : - lts.IsExecution (ss n) (μs.extract n m) (ss m) (ss.extract n (m + 1)) := by +theorem LTS.OmegaExecution.extract_execution + (h : lts.OmegaExecution ss μs) {n m : ℕ} (hnm : n ≤ m) : + lts.Execution (ss n) (μs.extract n m) (ss m) (ss.extract n (m + 1)) := by grind /-- Any multistep transition extracted from an infinite execution is valid. -/ -theorem LTS.ωTr_mTr (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) : +theorem LTS.OmegaExecution.extract_mTr + (h : lts.OmegaExecution ss μs) {n m : ℕ} (hnm : n ≤ m) : lts.MTr (ss n) (μs.extract n m) (ss m) := by - grind [LTS.ωTr_isExecution h hnm] + grind [LTS.OmegaExecution.extract_execution h hnm] /-- Prepends an infinite execution with a transition. -/ -theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) : - lts.ωTr (s ::ω ss) (μ ::ω μs) := by +theorem LTS.OmegaExecution.cons (htr : lts.Tr s μ t) + (hωtr : lts.OmegaExecution ss μs) (hm : ss 0 = t) : + lts.OmegaExecution (s ::ω ss) (μ ::ω μs) := by intro i induction i <;> grind /-- 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 ∧ ss'.drop μl.length = ss := by - obtain ⟨sl, _, _, _, _⟩ := LTS.mTr_extract_isExecution hmtr +theorem LTS.OmegaExecution.append + (hmtr : lts.MTr s μl t) (hωtr : lts.OmegaExecution ss μs) (hm : ss 0 = t) : + ∃ ss', lts.OmegaExecution ss' (μl ++ω μs) ∧ + ss' 0 = s ∧ ss' μl.length = t ∧ ss'.drop μl.length = ss := by + obtain ⟨sl, _, _, _, _⟩ := LTS.execution_of_mTr hmtr use sl.take μl.length ++ω ss split_ands · intro n @@ -381,11 +385,11 @@ theorem LTS.ωTr.append open Nat in /-- Concatenating an infinite sequence of finite executions. -/ -theorem LTS.IsExecution.flatten [Inhabited Label] +theorem LTS.OmegaExecution.flatten_execution [Inhabited Label] {ts : ωSequence State} {μls : ωSequence (List Label)} {sls : ωSequence (List State)} - (hexec : ∀ k, lts.IsExecution (ts k) (μls k) (ts (k + 1)) (sls k)) + (hexec : ∀ k, lts.Execution (ts k) (μls k) (ts (k + 1)) (sls k)) (hpos : ∀ k, (μls k).length > 0) : - ∃ ss, lts.ωTr ss μls.flatten ∧ + ∃ ss, lts.OmegaExecution ss μls.flatten ∧ ∀ k, ss.extract (μls.cumLen k) (μls.cumLen (k + 1)) = (sls k).take (μls k).length := by have : Inhabited State := by exact {default := ts 0} let segs := ωSequence.mk fun k ↦ (sls k).take (μls k).length @@ -398,7 +402,7 @@ theorem LTS.IsExecution.flatten [Inhabited Label] split_ands · intro n simp only [h_len, flatten_def] - simp only [LTS.IsExecution] at hexec + simp only [LTS.Execution] at hexec have := segment_lower_bound h_mono h_zero n by_cases h_n : n + 1 < segs.cumLen (segment segs.cumLen n + 1) · have := segment_range_val h_mono (by grind) h_n @@ -419,11 +423,12 @@ theorem LTS.IsExecution.flatten [Inhabited Label] · simp [h_len, extract_flatten h_pos, segs] /-- Concatenating an infinite sequence of multistep transitions. -/ -theorem LTS.ωTr.flatten [Inhabited Label] {ts : ωSequence State} {μls : ωSequence (List Label)} +theorem LTS.OmegaExecution.flatten_mTr [Inhabited Label] + {ts : ωSequence State} {μls : ωSequence (List Label)} (hmtr : ∀ k, lts.MTr (ts k) (μls k) (ts (k + 1))) (hpos : ∀ k, (μls k).length > 0) : - ∃ ss, lts.ωTr ss μls.flatten ∧ ∀ k, ss (μls.cumLen k) = ts k := by - choose sls h_sls using fun k ↦ LTS.mTr_extract_isExecution (hmtr k) - obtain ⟨ss, h_ss, h_seg⟩ := LTS.IsExecution.flatten h_sls hpos + ∃ ss, lts.OmegaExecution ss μls.flatten ∧ ∀ k, ss (μls.cumLen k) = ts k := by + choose sls h_sls using fun k ↦ LTS.execution_of_mTr (hmtr k) + obtain ⟨ss, h_ss, h_seg⟩ := LTS.OmegaExecution.flatten_execution h_sls hpos use ss, h_ss intro k have h1 : 0 < (ss.extract (μls.cumLen k) (μls.cumLen (k + 1))).length := by grind @@ -453,27 +458,28 @@ theorem LTS.chooseFLTS.total (lts : LTS State Label) [h : lts.Total] (s : State) lts.Tr s μ (lts.chooseFLTS.tr s μ) := Classical.choose_spec <| h.total s μ -/-- `LTS.chooseωTr` builds an infinite execution of a total LTS from any starting state and -over any infinite sequence of labels. -/ -noncomputable def LTS.chooseωTr (lts : LTS State Label) [lts.Total] +/-- `LTS.chooseOmegaExecution` builds an infinite execution of a total LTS from any starting state +and over any infinite sequence of labels. -/ +noncomputable def LTS.chooseOmegaExecution (lts : LTS State Label) [lts.Total] (s : State) (μs : ωSequence Label) : ℕ → State | 0 => s - | n + 1 => lts.chooseFLTS.tr (lts.chooseωTr s μs n) (μs n) + | n + 1 => lts.chooseFLTS.tr (lts.chooseOmegaExecution s μs n) (μs n) /-- If a LTS is total, then there exists an infinite execution from any starting state and over any infinite sequence of labels. -/ -theorem LTS.Total.ωTr_exists [h : lts.Total] (s : State) (μs : ωSequence Label) : - ∃ ss, lts.ωTr ss μs ∧ ss 0 = s := by - use lts.chooseωTr s μs - grind [LTS.chooseωTr, LTS.chooseFLTS.total] +theorem LTS.Total.omegaExecution_exists [h : lts.Total] (s : State) (μs : ωSequence Label) : + ∃ ss, lts.OmegaExecution ss μs ∧ ss 0 = s := by + use lts.chooseOmegaExecution s μs + grind [LTS.chooseOmegaExecution, LTS.chooseFLTS.total] /-- If a LTS is total, then any finite execution can be extended to an infinite execution, provided that the label type is inbabited. -/ -theorem LTS.Total.mTr_ωTr [Inhabited Label] [ht : lts.Total] {μl : List Label} {s t : State} - (hm : lts.MTr s μl t) : ∃ μs ss, lts.ωTr ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t := by +theorem LTS.Total.mTr_omegaExecution [Inhabited Label] [ht : lts.Total] + {μl : List Label} {s t : State} (hm : lts.MTr s μl t) : + ∃ μs ss, lts.OmegaExecution ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t := by let μs : ωSequence Label := .const default - obtain ⟨ss', ho, h0⟩ := LTS.Total.ωTr_exists (h := ht) t μs - grind [LTS.ωTr.append hm ho h0] + obtain ⟨ss', ho, h0⟩ := LTS.Total.omegaExecution_exists (h := ht) t μs + grind [LTS.OmegaExecution.append hm ho h0] /-- `LTS.totalize` constructs a total LTS from any given LTS by adding a sink state. -/ def LTS.totalize (lts : LTS State Label) : LTS (State ⊕ Unit) Label where @@ -603,7 +609,8 @@ variable {State : Type u} {Label : Type v} (lts : LTS State Label) label. -/ @[scoped grind] class LTS.Deterministic (lts : LTS State Label) where - deterministic (s1 : State) (μ : Label) (s2 s3 : State) : lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3 + deterministic (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`. -/ @[scoped grind =] @@ -612,7 +619,8 @@ def LTS.image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ /-- The `μs`-image of a state `s`, where `μs` is a list of labels, is the set of all `μs`-derivatives of `s`. -/ @[scoped grind =] -def LTS.imageMultistep (s : State) (μs : List Label) : Set State := { s' : State | lts.MTr s μs 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`. -/ @[scoped grind =] @@ -917,7 +925,7 @@ def LTS.DivergentTrace [HasTau Label] (μs : ωSequence Label) := ∀ i, μs i = /-- A state is divergent if there is a divergent execution from it. -/ def LTS.Divergent [HasTau Label] (lts : LTS State Label) (s : State) : Prop := - ∃ ss μs, lts.ωTr ss μs ∧ ss 0 = s ∧ DivergentTrace μs + ∃ ss μs, lts.OmegaExecution ss μs ∧ ss 0 = s ∧ DivergentTrace μs /-- If a trace is divergent, then any 'suffix' is also divergent. -/ @[scoped grind ⇒] diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index 8c456a6c2..c3594585e 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -35,7 +35,7 @@ open_scoped_all Cslib #grind_lint skip Cslib.FinFun.fromFun_inter #grind_lint skip Cslib.LTS.deterministic_not_lto #grind_lint skip Cslib.LTS.deterministic_tr_image_singleton -#grind_lint skip Cslib.LTS.IsExecution.refl +#grind_lint skip Cslib.LTS.Execution.refl #grind_lint skip Cslib.LTS.mem_saturate_image_τ #grind_lint skip Cslib.ωSequence.drop_const #grind_lint skip Cslib.ωSequence.get_cons_append_zero