chore: split LTS/Basic.lean into more manageable pieces (#453)

This PR splits `Cslib/Foundations/Semantics/LTS/Basic.lean` into 7 files
with the following dependencies among them:
- Basic.lean
- Execution.lean, which imports Basic.lean
- OmegaExecution.lean, which imports Execution.lean
- Total.lean, which imports OmegaExecution.lean
- HasTau.lean, which imports Basic.lean
- Divergence.lean, which imports HasTau.lean and OmegaExecution.lean
- Union.lean, which imports Basic.lean

Other files which formerly import LTS/Basic.lean now import only the
"lowest" necessary file in the above hierarchy. LTS/Basic.lean now
imports only Cslib.Init and some mathlib files.

I also took the opportunity to rename a few theorems to more rational
and systematic names.

---------

Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: ctchou

Cslib.lean

@@ -62,8 +62,17 @@ public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
 public import Cslib.Foundations.Semantics.FLTS.Prod
 public import Cslib.Foundations.Semantics.LTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Bisimulation
+public import Cslib.Foundations.Semantics.LTS.Divergence
+public import Cslib.Foundations.Semantics.LTS.Execution
+public import Cslib.Foundations.Semantics.LTS.HasTau
+public import Cslib.Foundations.Semantics.LTS.Notation
+public import Cslib.Foundations.Semantics.LTS.OmegaExecution
+public import Cslib.Foundations.Semantics.LTS.Relation
 public import Cslib.Foundations.Semantics.LTS.Simulation
+public import Cslib.Foundations.Semantics.LTS.Termination
+public import Cslib.Foundations.Semantics.LTS.Total
 public import Cslib.Foundations.Semantics.LTS.TraceEq
+public import Cslib.Foundations.Semantics.LTS.Union
 public import Cslib.Foundations.Syntax.Congruence
 public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Syntax.HasAlphaEquiv

Cslib/Computability/Automata/EpsilonNA/Basic.lean

@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou
 module
 
 public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Semantics.LTS.HasTau
 
 @[expose] public section
 

Cslib/Computability/Automata/NA/Basic.lean

@@ -9,7 +9,7 @@ module
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
-public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 
 @[expose] public section
 

Cslib/Computability/Automata/NA/Concat.lean

@@ -99,7 +99,7 @@ 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.OmegaExecution], by simp⟩
   · obtain ⟨s0, _, _, _, h_mtr⟩ := h1
-    obtain ⟨ss1, _, _, _, _⟩ := LTS.execution_of_mTr 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]
@@ -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_omegaExecution h_mtr
+    obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.extend_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

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.execution_of_mTr h_mtr
+  obtain ⟨sl, _, _, _, _⟩ := LTS.Execution.of_mTr h_mtr
   by_cases xl.length = 0
   · use [inl ()]
     grind
@@ -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_omegaExecution h_mtr
+      obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.extend_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

Cslib/Computability/Automata/NA/Total.lean

@@ -7,6 +7,7 @@ Authors: Ching-Tsun Chou
 module
 
 public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Semantics.LTS.Total
 
 @[expose] public section
 
@@ -37,15 +38,15 @@ theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (State ⊕ Un
   use s, t
   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₂]
+  rw [← LTS.totalize.nonsink_mtr_iff, ← extract_eq_take, eq₁, ← eq₂]
   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_omegaExecution <| LTS.totalize.mtr_left_iff.mpr hm]
+  grind [totalize, Run, LTS.Total.extend_omegaExecution <| LTS.totalize.nonsink_mtr_iff.mpr hm]
 
 namespace FinAcc
 

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -87,9 +87,9 @@ lemma buchiCongruence_transfer
     grind
   have := h_eq s t
   have h_yl : yl ∈ na.pairLang s t := by grind
-  have := LTS.execution_of_mTr h_yl
+  have := LTS.Execution.of_mTr h_yl
   grind [LTS.mem_pairViaLang, LTS.Execution, → LTS.Execution.comp,
-    → LTS.execution_of_mTr]
+    → 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`
@@ -148,7 +148,7 @@ private lemma frequently_via_accept [Inhabited Symbol]
   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.mTr_of_execution na.toLTS <| LTS.OmegaExecution.extract_execution h_exec h
+    LTS.Execution.to_mTr <| LTS.OmegaExecution.extract_execution h_exec h
   split_ands
   · have h : f n ≤ f n + k := by lia
     specialize exec h
@@ -179,7 +179,7 @@ theorem buchiFamily_saturation [Inhabited Symbol] : Saturates na.buchiFamily (la
       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.mTr_of_execution]
+      grind [buchiCongruence_transfer h_xl_c h_yl_c h_xl_e, LTS.mem_pairLang, LTS.Execution.to_mTr]
     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

Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean

@@ -6,6 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
+public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Basic
 
 @[expose] public section

Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean

@@ -6,6 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
+public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Basic
 
 @[expose] public section