chore(LTS): add API for TraceEq and relatives (#617)

Follow-up to cslib#613 adding API & simplifying arguments related to
trace equivalence.

---

- [ ] depends on: cslib#613

---------

Co-authored-by: twwar <tom.waring@unimelb.edu.au>

Author: thomaskwaring

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -78,13 +78,22 @@ Definition of a multistep transition.
 rule. This makes working with lists of labels more convenient, because we follow the same
 construction. It is also similar to what is done in the `SimpleGraph` library in mathlib.)
 -/
-@[scoped grind]
+@[scoped grind, mk_iff]
 inductive MTr (lts : LTS State Label) : State → List Label → State → Prop where
   | refl {s : State} : lts.MTr s [] s
   | stepL {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} :
     lts.Tr s1 μ s2 → lts.MTr s2 μs s3 →
     lts.MTr s1 (μ :: μs) s3
 
+/-- In any zero-steps multistep transition, the origin and the derivative are the same. -/
+@[scoped grind .]
+theorem MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by
+  cases h
+  rfl
+
+@[simp] theorem MTr.nil_iff (s1 s2 : State) : lts.MTr s1 [] s2 ↔ s1 = s2 :=
+  ⟨nil_eq lts, fun h => h ▸ MTr.refl⟩
+
 /-- Any transition is also a multistep transition. -/
 @[scoped grind →]
 theorem MTr.single {s1 : State} {μ : Label} {s2 : State} :
@@ -94,6 +103,16 @@ theorem MTr.single {s1 : State} {μ : Label} {s2 : State} :
   · exact h
   · apply MTr.refl
 
+/-- A multistep transition along `μ :: μs` is a transition labelled by `μ` plus a multistep
+transition labelled by `μs`. -/
+theorem MTr.cons_iff {lts : LTS State Label} :
+    lts.MTr s1 (μ :: μs) s2 ↔ ∃ s, lts.Tr s1 μ s ∧ lts.MTr s μs s2 := by
+  constructor
+  · rintro (_ | ⟨htr, hmtr⟩)
+    exact ⟨_, htr, hmtr⟩
+  · intro ⟨s, htr, hmtr⟩
+    exact .stepL htr hmtr
+
 /-- Any multistep transition can be extended by adding a transition. -/
 theorem MTr.stepR {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} :
   lts.MTr s1 μs s2 → lts.Tr s2 μ s3 → lts.MTr s1 (μs ++ [μ]) s3 := by
@@ -128,11 +147,28 @@ theorem MTr.single_invert (s1 : State) (μ : Label) (s2 : State) :
     cases hmtr
     exact htr
 
-/-- In any zero-steps multistep transition, the origin and the derivative are the same. -/
-@[scoped grind .]
-theorem MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by
-  cases h
-  rfl
+/-- A 1-sized multistep transition is exactly a single transision with the given label. -/
+@[simp] theorem MTr.singleton_iff (s1 : State) (μ : Label) (s2 : State) :
+  lts.MTr s1 [μ] s2 ↔ lts.Tr s1 μ s2 := ⟨MTr.single_invert lts s1 μ s2, MTr.single lts⟩
+
+/-- A multistep transition over a concatenation can be split into two multistep transitions. -/
+theorem MTr.split {lts : LTS State Label} (h : lts.MTr s1 (μs ++ μs') s2) :
+    ∃ s, lts.MTr s1 μs s ∧ lts.MTr s μs' s2 := by
+  induction μs generalizing s1 s2 with
+  | nil => use s1, .refl, h
+  | cons μ μs ih =>
+    rw [List.cons_append] at h
+    cases h
+    case stepL s htr hmtr =>
+      obtain ⟨s', hmtr', hmtr''⟩ := ih hmtr
+      use s', .stepL htr hmtr', hmtr''
+
+/-- Multistep-transitions over `μs ++ μs'` are exactly multistep transitions over `μs` and `μs'`
+with a common end & start state (respectively). -/
+theorem MTr.append_iff : lts.MTr s1 (μs ++ μs') s2 ↔ ∃ s, lts.MTr s1 μs s ∧ lts.MTr s μs' s2 := by
+  refine ⟨MTr.split, ?_⟩
+  intro ⟨_, h, h'⟩
+  exact h.comp lts h'
 
 /-- A state `s1` can reach a state `s2` if there exists a multistep transition from
 `s1` to `s2`. -/
@@ -167,6 +203,21 @@ class Deterministic (lts : LTS State Label) where
   deterministic (s1 : State) (μ : Label) (s2 s3 : State) :
     lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3
 
+theorem Deterministic.eq_of_tr {lts : LTS State Label} [lts.Deterministic]
+    (htr : lts.Tr s1 μ s2) (htr' : lts.Tr s1 μ s2') : s2 = s2' :=
+  Deterministic.deterministic s1 μ s2 s2' htr htr'
+
+/-- In a deterministic lts, multistep transitions with a given start state and trace reach a unique
+end state. -/
+theorem Deterministic.eq_of_mTr {lts : LTS State Label} [lts.Deterministic]
+    (hmtr : lts.MTr s1 μs s2) (hmtr' : lts.MTr s1 μs s2') : s2 = s2' := by
+  induction μs generalizing s1 s2 s2' with
+  | nil => grind
+  | cons μ μs ih =>
+    rcases hmtr with (_ | ⟨htr, hmtr⟩); rcases hmtr' with (_ | ⟨htr', hmtr'⟩)
+    rw [eq_of_tr htr htr'] at hmtr
+    exact ih hmtr hmtr'
+
 /-- The `μ`-image of a state `s` is the set of all `μ`-derivatives of `s`. -/
 @[scoped grind =]
 def image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' }

Cslib/Foundations/Semantics/LTS/Bisimulation.lean

@@ -9,6 +9,7 @@ module
 public import Cslib.Foundations.Relation.Domain
 public import Cslib.Foundations.Semantics.LTS.Simulation
 public import Cslib.Foundations.Semantics.LTS.TraceEq
+public import Mathlib.Tactic.TFAE
 
 /-! # Bisimulation and Bisimilarity
 
@@ -183,6 +184,10 @@ instance : IsEquiv State (HomBisimilarity lts) where
   symm _ _ := Bisimilarity.symm
   trans _ _ _ := Bisimilarity.trans
 
+/-- Bisimulation implies simulation equivalence. -/
+theorem IsBisimulation.simulationEquiv (h : IsBisimulation lts₁ lts₂ r) (hrel : r s₁ s₂) :
+    s₁ ≤≥[lts₁,lts₂] s₂ := ⟨⟨r, hrel, h.isSimulation⟩, flip r, hrel, h.inv.isSimulation⟩
+
 /-- The union of two bisimulations is a bisimulation. -/
 @[scoped grind .]
 theorem IsBisimulation.sup (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisimulation lts₁ lts₂ s) :
@@ -302,30 +307,16 @@ theorem IsBisimulationUpTo.isBisimulation (h : IsBisimulationUpTo lts₁ lts₂
 
 /-- If two states are related by a bisimulation, they can mimic each other's multi-step
 transitions. -/
-theorem IsBisimulation.bisim_trace
-    (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) :
+theorem IsBisimulation.bisim_trace (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) :
     ∀ μs s₁', lts₁.MTr s₁ μs s₁' → ∃ s₂', lts₂.MTr s₂ μs s₂' ∧ r s₁' s₂' :=
   hb.isSimulation.sim_trace hr
 
 /-! ## Relation to trace equivalence -/
 
 /-- Any bisimulation implies trace equivalence. -/
 @[scoped grind =>]
-theorem IsBisimulation.traceEq
-    (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) :
-    s₁ ~tr[lts₁,lts₂] s₂ := by
-  ext μs
-  constructor
-  case mp =>
-    intro h
-    obtain ⟨s₁', h⟩ := h
-    obtain ⟨s₂', hmtr⟩ := IsBisimulation.bisim_trace hb hr μs s₁' h
-    use s₂', hmtr.1
-  case mpr =>
-    intro h
-    obtain ⟨s₂', h⟩ := h
-    obtain ⟨s₁', hmtr⟩ := IsBisimulation.bisim_trace hb.inv hr μs s₂' h
-    use s₁', hmtr.1
+theorem IsBisimulation.traceEq (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) :
+    s₁ ~tr[lts₁,lts₂] s₂ := (hb.simulationEquiv hr).traceEq
 
 /-- Bisimilarity is included in trace equivalence. -/
 @[scoped grind .]
@@ -412,30 +403,30 @@ theorem IsBisimulation.deterministic_traceEq_isBisimulation
     [lts₁.Deterministic] [lts₂.Deterministic] :
     (IsBisimulation lts₁ lts₂ (TraceEq lts₁ lts₂)) := by
   rw [IsBisimulation.isSimulation_iff, TraceEq.flip_eq]
-  exact ⟨TraceEq.deterministic_isSimulation, TraceEq.deterministic_isSimulation⟩
+  exact ⟨Deterministic.isSimulation_traceEq, Deterministic.isSimulation_traceEq⟩
 
 /-- In deterministic LTSs, trace equivalence implies bisimilarity. -/
 theorem Bisimilarity.deterministic_traceEq_bisim {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label}
     [lts₁.Deterministic] [lts₂.Deterministic] (h : s₁ ~tr[lts₁,lts₂] s₂) :
     (s₁ ~[lts₁,lts₂] s₂) := by
-  exists TraceEq lts₁ lts₂
-  constructor
-  case left =>
-    exact h
-  case right =>
-    apply IsBisimulation.deterministic_traceEq_isBisimulation
+  use TraceEq lts₁ lts₂, h, IsBisimulation.deterministic_traceEq_isBisimulation
+
+/-- In a deterministic lts, bisimilarity, trace equivalence, and simulation equivalence are
+equivalent to one-another. -/
+theorem Deterministic.bisim_tfae {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label}
+    [lts₁.Deterministic] [lts₂.Deterministic] (s₁ : State₁) (s₂ : State₂) :
+    [s₁ ~[lts₁,lts₂] s₂, s₁ ~tr[lts₁,lts₂] s₂, s₁ ≤≥[lts₁,lts₂] s₂].TFAE := by
+  tfae_have 2 ↔ 3 := Deterministic.traceEq_iff_simulationEquiv s₁ s₂
+  tfae_have 1 → 2 := Bisimilarity.le_traceEq s₁ s₂
+  tfae_have 2 → 1 := Bisimilarity.deterministic_traceEq_bisim
+  tfae_finish
 
 /-- In deterministic LTSs, bisimilarity and trace equivalence coincide. -/
 theorem Bisimilarity.deterministic_bisim_eq_traceEq
     {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label}
     [lts₁.Deterministic] [lts₂.Deterministic] : Bisimilarity lts₁ lts₂ = TraceEq lts₁ lts₂ := by
-  funext s₁ s₂
-  simp only [eq_iff_iff]
-  constructor
-  case mp =>
-    apply Bisimilarity.le_traceEq
-  case mpr =>
-    apply Bisimilarity.deterministic_traceEq_bisim
+  ext s₁ s₂
+  exact (Deterministic.bisim_tfae s₁ s₂).out 0 1
 
 /-- Homogeneous bisimilarity can also be characterized through symmetric simulations. -/
 theorem HomBisimilarity.symm_simulation :

Cslib/Foundations/Semantics/LTS/Execution.lean

@@ -131,11 +131,4 @@ theorem Execution.split
   simp [Execution]
   grind
 
-/-- A multistep transition over a concatenation can be split into two multistep transitions. -/
-theorem 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⟩ := Execution.of_mTr h
-  have := Execution.split h_ss μs1.length
-  grind
-
 end Cslib.LTS

Cslib/Foundations/Semantics/LTS/Simulation.lean

@@ -89,31 +89,18 @@ theorem IsSimulation.comp
     (r2 : State₂ → State₃ → Prop)
     (h1 : IsSimulation lts₁ lts₂ r1) (h2 : IsSimulation lts₂ lts₃ r2) :
     IsSimulation lts₁ lts₃ (Relation.Comp r1 r2) := by
-  simp_all only [IsSimulation]
   intro s₁ s2 hrc μ s₁' htr
   rcases hrc with ⟨sb, hr1, hr2⟩
-  specialize h1 s₁ sb hr1 μ
-  specialize h2 sb s2 hr2 μ
-  have h1' := h1 s₁' htr
-  obtain ⟨s₁'', h1'tr, h1'⟩ := h1'
-  have h2' := h2 s₁'' h1'tr
-  obtain ⟨s2'', h2'tr, h2'⟩ := h2'
-  exists s2''
-  constructor
-  · exact h2'tr
-  · exists s₁''
+  obtain ⟨s₁'', h1'tr, h1'⟩ := h1 s₁ sb hr1 μ s₁' htr
+  obtain ⟨s2'', h2'tr, h2'⟩ := h2 sb s2 hr2 μ s₁'' h1'tr
+  use s2'', h2'tr, s₁'', h1', h2'
 
 /-- Similarity is transitive. -/
 theorem Similarity.trans (h1 : s₁ ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,lts₃] s₃) :
     s₁ ≤[lts₁,lts₃] s₃ := by
   obtain ⟨r1, hr1, hr1s⟩ := h1
   obtain ⟨r2, hr2, hr2s⟩ := h2
-  exists Relation.Comp r1 r2
-  constructor
-  case left =>
-    exists s2
-  case right =>
-    apply IsSimulation.comp r1 r2 hr1s hr2s
+  use! Relation.Comp r1 r2, s2, hr1, hr2, IsSimulation.comp r1 r2 hr1s hr2s
 
 theorem IsSimulation.sup (hr : IsSimulation lts₁ lts₂ r)
     (hs : IsSimulation lts₁ lts₂ s) : IsSimulation lts₁ lts₂ (r ⊔ s) := by