leanprover · ctchou · Mar 18, 2026
@@ -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

@@ -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

@@ -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]

@@ -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,17 +122,19 @@ 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
     have h_mtr (n : ℕ) : na.MTr (ts n) (zls n) (ts (n + 1)) := by
       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

@@ -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

@@ -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
 

@@ -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]