From 17081ca59762c2df22cf4882950c0f5510e08656 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Fri, 27 Mar 2026 13:48:30 +0100 Subject: [PATCH 1/8] Heterogeneous behavioural equivalences --- Cslib/Foundations/Data/Relation.lean | 3 + .../Semantics/LTS/Bisimulation.lean | 416 +++++++++--------- .../Foundations/Semantics/LTS/Simulation.lean | 119 ++--- Cslib/Foundations/Semantics/LTS/TraceEq.lean | 84 ++-- Cslib/Languages/CCS/BehaviouralTheory.lean | 10 +- Cslib/Logics/HML/Basic.lean | 10 +- 6 files changed, 345 insertions(+), 297 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index ed3f7e76a..d984e4a4c 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -31,6 +31,9 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou -/ +/-- The empty (heterogeneous) relation, which always returns `False`. -/ +def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False + namespace Relation attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index d41eafe71..047aa99f0 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -15,7 +15,7 @@ public import Cslib.Foundations.Semantics.LTS.TraceEq /-! # Bisimulation and Bisimilarity -A bisimulation is a binary relation on the states of an `LTS`, which establishes a tight semantic +A bisimulation is a binary relation on the states of two `LTS`s, which establishes a tight semantic correspondence. More specifically, if two states `s1` and `s2` are related by a bisimulation, then `s1` can mimic all transitions of `s2` and vice versa. Furthermore, the derivatives reaches through these transitions remain related by the bisimulation. @@ -68,100 +68,104 @@ equivalence coincide. namespace Cslib.LTS -universe u v - section Bisimulation -variable {State : Type u} {Label : Type v} {lts : LTS State Label} - -/-- A relation is a bisimulation if, whenever it relates two states in an lts, +/-- A relation is a bisimulation if, whenever it relates two states, the transitions originating from these states mimic each other and the reached derivatives are themselves related. -/ @[scoped grind =] -def IsBisimulation (lts : LTS State Label) (r : State → State → Prop) : Prop := +def IsBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : Prop := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2') + (∀ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s1' s2') ∧ - (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2') + (∀ s2', lts₂.Tr s2 μ s2' → ∃ s1', lts₁.Tr s1 μ s1' ∧ r s1' s2') ) +/-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/ +abbrev IsHomBisimulation (lts : LTS State Label) := IsBisimulation lts lts + /-- Helper for following a transition by the first state in a pair of a `Bisimulation`. -/ theorem IsBisimulation.follow_fst - (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') : - ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' := + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) (htr : lts₁.Tr s1 μ s1') : + ∃ s2', lts₂.Tr s2 μ s2' ∧ r s1' s2' := (hb hr μ).1 _ htr /-- Helper for following a transition by the second state in a pair of a `Bisimulation`. -/ theorem IsBisimulation.follow_snd - (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') : - ∃ s1', lts.Tr s1 μ s1' ∧ r s1' s2' := + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) (htr : lts₂.Tr s2 μ s2') : + ∃ s1', lts₁.Tr s1 μ s1' ∧ r s1' s2' := (hb hr μ).2 _ htr /-- Two states are bisimilar if they are related by some bisimulation. -/ @[scoped grind =] -def Bisimilarity (lts : LTS State Label) : State → State → Prop := - fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsBisimulation r +def Bisimilarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := + fun s1 s2 => ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsBisimulation lts₁ lts₂ r /-- Notation for bisimilarity. -Differently from standard pen-and-paper presentations, we require the lts to be mentioned +Differently from standard pen-and-paper presentations, we require the LTSs to be mentioned explicitly. -/ -notation s:max " ~[" lts "] " s':max => Bisimilarity lts s s' +scoped notation s:max " ~[" lts₁ "," lts₂ "] " s':max => Bisimilarity lts₁ lts₂ s s' + +/-- Homogeneous bisimilarity is bisimilarity where the underlying LTSs are the same. -/ +abbrev HomBisimilarity (lts : LTS State Label) := Bisimilarity lts lts + +/-- Notation for homogeneous bisimilarity. -/ +scoped notation s:max " ~[" lts "] " s':max => HomBisimilarity lts s s' -open LTS in -/-- Bisimilarity is reflexive. -/ +/-- Homogeneous bisimilarity is reflexive. -/ @[scoped grind ., refl] -theorem Bisimilarity.refl (s : State) : s ~[lts] s := by +theorem HomBisimilarity.refl (s : State) : s ~[lts] s := by exists Eq grind /-- The inverse of a bisimulation is a bisimulation. -/ @[scoped grind →] -theorem IsBisimulation.inv (h : lts.IsBisimulation r) : - lts.IsBisimulation (flip r) := by grind [flip] +theorem IsBisimulation.inv (h : IsBisimulation lts₁ lts₂ r) : + IsBisimulation lts₂ lts₁ (flip r) := by grind [flip] open scoped IsBisimulation in /-- Bisimilarity is symmetric. -/ @[scoped grind →, symm] -theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1 := by +theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts₁,lts₂] s2) : s2 ~[lts₂,lts₁] s1 := by grind [flip] /-- The composition of two bisimulations is a bisimulation. -/ @[scoped grind .] theorem IsBisimulation.comp - (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) : - lts.IsBisimulation (Relation.Comp r1 r2) := by grind [Relation.Comp] + (h1 : IsBisimulation lts₁ lts₂ r1) (h2 : IsBisimulation lts₂ lts₃ r2) : + IsBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by grind [Relation.Comp] -open LTS in /-- Bisimilarity is transitive. -/ @[scoped grind →] theorem Bisimilarity.trans - (h1 : s1 ~[lts] s2) (h2 : s2 ~[lts] s3) : - s1 ~[lts] s3 := by + (h1 : s1 ~[lts₁,lts₂] s2) (h2 : s2 ~[lts₂,lts₃] s3) : + s1 ~[lts₁,lts₃] s3 := by obtain ⟨r1, _, _⟩ := h1 obtain ⟨r2, _, _⟩ := h2 exists Relation.Comp r1 r2 grind [Relation.Comp] -/-- Bisimilarity is an equivalence relation. -/ -theorem Bisimilarity.eqv : - Equivalence (Bisimilarity lts) := { - refl := Bisimilarity.refl +/-- Homogeneous bisimilarity is an equivalence relation. -/ +theorem HomBisimilarity.eqv : + Equivalence (HomBisimilarity lts) := { + refl := HomBisimilarity.refl symm := Bisimilarity.symm trans := Bisimilarity.trans } -instance : IsEquiv State (Bisimilarity lts) where - refl := Bisimilarity.refl +instance : IsEquiv State (HomBisimilarity lts) where + refl := HomBisimilarity.refl symm _ _ := Bisimilarity.symm trans _ _ _ := Bisimilarity.trans /-- The union of two bisimulations is a bisimulation. -/ @[scoped grind .] -theorem Bisimulation.union (hrb : lts.IsBisimulation r) (hsb : lts.IsBisimulation s) : - lts.IsBisimulation (r ⊔ s) := by +theorem Bisimulation.union (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisimulation lts₁ lts₂ s) : + IsBisimulation lts₁ lts₂ (r ⊔ s) := by intro s1 s2 hrs μ cases hrs case inl h => @@ -201,39 +205,38 @@ theorem Bisimulation.union (hrb : lts.IsBisimulation r) (hsb : lts.IsBisimulatio right exact hs' -open LTS in /-- Bisimilarity is a bisimulation. -/ @[scoped grind .] -theorem Bisimilarity.is_bisimulation : lts.IsBisimulation (Bisimilarity lts) := by grind +theorem Bisimilarity.is_bisimulation : IsBisimulation lts₁ lts₂ (Bisimilarity lts₁ lts₂) := by grind /-- Bisimilarity is the largest bisimulation. -/ @[scoped grind →] -theorem Bisimilarity.largest_bisimulation (h : lts.IsBisimulation r) : - Subrelation r (Bisimilarity lts) := by +theorem Bisimilarity.largest_bisimulation (h : IsBisimulation lts₁ lts₂ r) : + Subrelation r (Bisimilarity lts₁ lts₂) := by intro s1 s2 hr exists r /-- The union of bisimilarity with any bisimulation is bisimilarity. -/ @[scoped grind =, simp] -theorem Bisimilarity.gfp (r : State → State → Prop) (h : lts.IsBisimulation r) : - (Bisimilarity lts) ⊔ r = Bisimilarity lts := by +theorem Bisimilarity.gfp (r : State₁ → State₂ → Prop) (h : IsBisimulation lts₁ lts₂ r) : + (Bisimilarity lts₁ lts₂) ⊔ r = Bisimilarity lts₁ lts₂ := by funext s1 s2 - simp only [max, SemilatticeSup.sup, eq_iff_iff, or_iff_left_iff_imp] - apply Bisimilarity.largest_bisimulation h + simp only [max, SemilatticeSup.sup] + grind /-- `calc` support for bisimilarity. -/ -instance : Trans (Bisimilarity lts) (Bisimilarity lts) (Bisimilarity lts) where +instance : Trans (Bisimilarity lts₁ lts₂) (Bisimilarity lts₂ lts₃) (Bisimilarity lts₁ lts₃) where trans := Bisimilarity.trans section Order /-! ## Order properties -/ -instance : Max {r // lts.IsBisimulation r} where +instance : Max {r // IsBisimulation lts₁ lts₂ r} where max r s := ⟨r.1 ⊔ s.1, Bisimulation.union r.2 s.2⟩ /-- Bisimulations equipped with union form a join-semilattice. -/ -instance : SemilatticeSup {r // lts.IsBisimulation r} where +instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where sup r s := r ⊔ s le_sup_left r s := by simp only [LE.le] @@ -257,9 +260,9 @@ instance : SemilatticeSup {r // lts.IsBisimulation r} where case inr h => apply h2 _ _ h -/-- The empty relation is a bisimulation. -/ +/-- The empty (heterogeneous) relation is a bisimulation. -/ @[scoped grind .] -theorem Bisimulation.emptyRelation_bisimulation : lts.IsBisimulation emptyRelation := by +theorem Bisimulation.emptyHRelation_bisimulation : IsBisimulation lts₁ lts₂ emptyHRelation := by intro s1 s2 hr cases hr @@ -268,13 +271,13 @@ theorem Bisimulation.emptyRelation_bisimulation : lts.IsBisimulation emptyRelati - The empty relation is the bottom element. - Bisimilarity is the top element. -/ -instance : BoundedOrder {r // lts.IsBisimulation r} where - top := ⟨Bisimilarity lts, Bisimilarity.is_bisimulation⟩ - bot := ⟨emptyRelation, Bisimulation.emptyRelation_bisimulation⟩ +instance : BoundedOrder {r // IsBisimulation lts₁ lts₂ r} where + top := ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ + bot := ⟨emptyHRelation, Bisimulation.emptyHRelation_bisimulation⟩ le_top r := by intro s1 s2 simp only [LE.le] - apply Bisimilarity.largest_bisimulation r.2 + grind bot_le r := by intro s1 s2 simp only [LE.le] @@ -285,21 +288,29 @@ end Order /-! ## Bisimulation up-to -/ -/-- A relation `r` is a bisimulation up to bisimilarity if, whenever it relates two +/-- Lifts a relation `r` to homogeneous bisimilarities on its types. -/ +def UpToHomBisimilarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : State₁ → State₂ → Prop := + Relation.Comp (HomBisimilarity lts₁) (Relation.Comp r (HomBisimilarity lts₂)) + +/-- A relation `r` is a bisimulation up to homogeneous bisimilarity if, whenever it relates two states in an lts, the transitions originating from these states mimic each other and the reached derivatives are themselves related by `r` up to bisimilarity. -/ @[scoped grind] -def IsBisimulationUpTo (lts : LTS State Label) (r : State → State → Prop) : Prop := +def IsBisimulationUpTo (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : Prop := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ Relation.UpTo r (Bisimilarity lts) s1' s2') + (∀ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.Tr s2 μ s2' ∧ + (UpToHomBisimilarity lts₁ lts₂ r) s1' s2') ∧ - (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.Tr s1 μ s1' ∧ Relation.UpTo r (Bisimilarity lts) s1' s2') + (∀ s2', lts₂.Tr s2 μ s2' → ∃ s1', lts₁.Tr s1 μ s1' ∧ + (UpToHomBisimilarity lts₁ lts₂ r) s1' s2') ) /-- Any bisimulation up to bisimilarity is a bisimulation. -/ @[scoped grind →] -theorem IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) : - lts.IsBisimulation (Relation.UpTo r (Bisimilarity lts)) := by +theorem IsBisimulationUpTo.is_bisimulation (h : IsBisimulationUpTo lts₁ lts₂ r) : + IsBisimulation lts₁ lts₂ (UpToHomBisimilarity lts₁ lts₂ r) := by intro s1 s2 hr μ rcases hr with ⟨s1b, hr1b, s2b, hrb, hr2b⟩ obtain ⟨r1, hr1, hr1b⟩ := hr1b @@ -349,9 +360,9 @@ theorem IsBisimulationUpTo.isBisimulation (h : lts.IsBisimulationUpTo r) : /-- If two states are related by a bisimulation, they can mimic each other's multi-step transitions. -/ -theorem Bisimulation.bisim_trace - (hb : lts.IsBisimulation r) (hr : r s1 s2) : - ∀ μs s1', lts.MTr s1 μs s1' → ∃ s2', lts.MTr s2 μs s2' ∧ r s1' s2' := by +theorem IsBisimulation.bisim_trace + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) : + ∀ μs s1', lts₁.MTr s1 μs s1' → ∃ s2', lts₂.MTr s2 μs s2' ∧ r s1' s2' := by intro μs induction μs generalizing s1 s2 case nil => @@ -384,27 +395,27 @@ theorem Bisimulation.bisim_trace /-- Any bisimulation implies trace equivalence. -/ @[scoped grind =>] theorem IsBisimulation.traceEq - (hb : lts.IsBisimulation r) (hr : r s1 s2) : - s1 ~tr[lts] s2 := by + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) : + s1 ~tr[lts₁,lts₂] s2 := by funext μs simp only [eq_iff_iff] constructor case mp => intro h obtain ⟨s1', h⟩ := h - obtain ⟨s2', hmtr⟩ := Bisimulation.bisim_trace hb hr μs s1' h + obtain ⟨s2', hmtr⟩ := IsBisimulation.bisim_trace hb hr μs s1' h exists s2' exact hmtr.1 case mpr => intro h obtain ⟨s2', h⟩ := h - obtain ⟨s1', hmtr⟩ := Bisimulation.bisim_trace hb.inv hr μs s2' h + obtain ⟨s1', hmtr⟩ := IsBisimulation.bisim_trace hb.inv hr μs s2' h exists s1' exact hmtr.1 /-- Bisimilarity is included in trace equivalence. -/ @[scoped grind .] -theorem Bisimilarity.le_traceEq : Bisimilarity lts ≤ TraceEq lts := by +theorem Bisimilarity.le_traceEq : Bisimilarity lts₁ lts₂ ≤ TraceEq lts₁ lts₂ := by intro s1 s2 h obtain ⟨r, hr, hb⟩ := h apply hb.traceEq hr @@ -426,7 +437,7 @@ private inductive BisimMotTr : ℕ → Char → ℕ → Prop where example `Bisimulation.deterministic_trace_eq_is_bisim`). -/ theorem Bisimulation.traceEq_not_bisim : ∃ (State : Type) (Label : Type) (lts : LTS State Label), - ¬(lts.IsBisimulation (TraceEq lts)) := by + ¬(IsHomBisimulation lts (HomTraceEq lts)) := by exists ℕ exists Char let lts := LTS.mk BisimMotTr @@ -693,27 +704,30 @@ theorem Bisimulation.traceEq_not_bisim : /-- In general, bisimilarity and trace equivalence are distinct. -/ theorem Bisimilarity.bisimilarity_neq_traceEq : - ∃ (State : Type) (Label : Type) (lts : LTS State Label), Bisimilarity lts ≠ TraceEq lts := by + ∃ (State : Type) (Label : Type) (lts : LTS State Label), + HomBisimilarity lts ≠ HomTraceEq lts := by obtain ⟨State, Label, lts, h⟩ := Bisimulation.traceEq_not_bisim exists State; exists Label; exists lts intro heq - have hb := Bisimilarity.is_bisimulation (lts := lts) + have hb := Bisimilarity.is_bisimulation (lts₁ := lts) (lts₂ := lts) + simp only [HomBisimilarity] at heq rw [heq] at hb contradiction /-- In any deterministic LTS, trace equivalence is a bisimulation. -/ theorem Bisimulation.deterministic_traceEq_is_bisim - [lts.Deterministic] : - (lts.IsBisimulation (TraceEq lts)) := by + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + [lts₁.Deterministic] [lts₂.Deterministic] : + (IsBisimulation lts₁ lts₂ (TraceEq lts₁ lts₂)) := by simp only [IsBisimulation] intro s1 s2 hteq μ constructor case left => - apply TraceEq.deterministic_sim lts s1 s2 hteq + apply TraceEq.deterministic_isSimulation s1 s2 hteq case right => intro s2' htr apply TraceEq.symm at hteq - have h := TraceEq.deterministic_sim lts s2 s1 hteq μ s2' htr + have h := TraceEq.deterministic_isSimulation s2 s1 hteq μ s2' htr obtain ⟨s1', h⟩ := h exists s1' constructor @@ -722,20 +736,21 @@ theorem Bisimulation.deterministic_traceEq_is_bisim case right => apply h.2.symm -/-- In any deterministic LTS, trace equivalence implies bisimilarity. -/ -theorem Bisimilarity.deterministic_traceEq_bisim - [lts.Deterministic] (h : s1 ~tr[lts] s2) : - (s1 ~[lts] s2) := by - exists TraceEq lts +/-- 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 : s1 ~tr[lts₁,lts₂] s2) : + (s1 ~[lts₁,lts₂] s2) := by + exists TraceEq lts₁ lts₂ constructor case left => exact h case right => apply Bisimulation.deterministic_traceEq_is_bisim -/-- In any deterministic LTS, bisimilarity and trace equivalence coincide. -/ -theorem Bisimilarity.deterministic_bisim_eq_traceEq [lts.Deterministic] : - Bisimilarity lts = TraceEq lts := by +/-- 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 s1 s2 simp only [eq_iff_iff] constructor @@ -746,36 +761,32 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq [lts.Deterministic] : /-! ## Relation to simulation -/ -open LTS in /-- Any bisimulation is also a simulation. -/ -theorem Bisimulation.is_simulation {lts : LTS State Label} {r : State → State → Prop} : - lts.IsBisimulation r → Simulation lts r := by - grind [Simulation] +theorem Bisimulation.isSimulation : IsBisimulation lts₁ lts₂ r → IsSimulation lts₁ lts₂ r := by + grind [IsSimulation] -open LTS in /-- A relation is a bisimulation iff both it and its inverse are simulations. -/ -theorem Bisimulation.simulation_iff {lts : LTS State Label} {r : State → State → Prop} : - lts.IsBisimulation r ↔ (Simulation lts r ∧ Simulation lts (flip r)) := by +theorem Bisimulation.simulation_iff : + IsBisimulation lts₁ lts₂ r ↔ (IsSimulation lts₁ lts₂ r ∧ IsSimulation lts₂ lts₁ (flip r)) := by have _ (s1 s2) : r s1 s2 → flip r s2 s1 := id - grind [Simulation, flip] + grind [IsSimulation, flip] -open LTS in -/-- Bisimilarity can also be characterized through symmetric simulations. -/ -theorem Bisimilarity.symm_simulation {lts : LTS State Label} : - Bisimilarity lts = - fun s1 s2 => ∃ r, r s1 s2 ∧ Std.Symm r ∧ Simulation lts r := by +/-- Homogeneous bisimilarity can also be characterized through symmetric simulations. -/ +theorem HomBisimilarity.symm_simulation : + HomBisimilarity lts = + fun s1 s2 => ∃ r, r s1 s2 ∧ Std.Symm r ∧ IsHomSimulation lts r := by funext s1 s2 apply Iff.eq apply Iff.intro · intro h - have bisim : Bisimilarity lts s1 s2 ∧ Std.Symm (Bisimilarity lts) - ∧ Simulation lts (Bisimilarity lts) := by - grind [Std.Symm, Bisimilarity.symm, Bisimulation.is_simulation] + have bisim : HomBisimilarity lts s1 s2 ∧ Std.Symm (HomBisimilarity lts) + ∧ IsHomSimulation lts (HomBisimilarity lts) := by + grind [Std.Symm, Bisimilarity.symm, Bisimulation.isSimulation] grind · intro ⟨r, hr, hsymm, hsim⟩ have : r = (flip r) := by grind [flip, Std.Symm] - have : lts.IsBisimulation r := by + have : IsHomBisimulation lts r := by grind [Bisimulation.simulation_iff] grind @@ -786,77 +797,87 @@ section WeakBisimulation /-! ## Weak bisimulation and weak bisimilarity -/ /-- A weak bisimulation is similar to a `Bisimulation`, but allows for the related processes to do -internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTS. -/ -def IsWeakBisimulation [HasTau Label] (lts : LTS State Label) - (r : State → State → Prop) := - lts.saturate.IsBisimulation r +internal work. Technically, this is defined as a `Bisimulation` on the saturation of the LTSs. -/ +def IsWeakBisimulation [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) := + IsBisimulation (lts₁.saturate) (lts₂.saturate) r + +/-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/ +abbrev IsHomWeakBisimulation [HasTau Label] (lts : LTS State Label) := IsWeakBisimulation lts lts /-- Two states are weakly bisimilar if they are related by some weak bisimulation. -/ -def WeakBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop := +def WeakBisimilarity [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + State₁ → State₂ → Prop := fun s1 s2 => - ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsWeakBisimulation r + ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsWeakBisimulation lts₁ lts₂ r /-- Notation for weak bisimilarity. -/ -notation s:max " ≈[" lts "] " s':max => WeakBisimilarity lts s s' +scoped notation s:max " ≈[" lts₁ "," lts₂ "] " s':max => WeakBisimilarity lts₁ lts₂ s s' + +/-- Homogeneous bisimilarity is bisimilarity where the underlying LTSs are the same. -/ +abbrev HomWeakBisimilarity [HasTau Label] (lts : LTS State Label) := WeakBisimilarity lts lts + +/-- Notation for homogeneous bisimilarity. -/ +scoped notation s:max " ≈[" lts "] " s':max => HomWeakBisimilarity lts s s' /-- An `SWBisimulation` is a more convenient definition of weak bisimulation, because the challenge is a single transition. We prove later that this technique is sound, following a strategy inspired by [Sangiorgi2011]. -/ -def IsSWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) : Prop := +def IsSWBisimulation [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (r : State₁ → State₂ → Prop) : Prop := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts.Tr s1 μ s1' → ∃ s2', lts.STr s2 μ s2' ∧ r s1' s2') + (∀ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.STr s2 μ s2' ∧ r s1' s2') ∧ - (∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.STr s1 μ s1' ∧ r s1' s2') + (∀ s2', lts₂.Tr s2 μ s2' → ∃ s1', lts₁.STr s1 μ s1' ∧ r s1' s2') ) /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (first component). -/ -theorem SWBisimulation.follow_internal_fst - [HasTau Label] {lts : LTS State Label} - (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.τSTr s1 s1') : - ∃ s2', lts.τSTr s2 s2' ∧ r s1' s2' := by - induction hstr - case refl => - exists s2 - constructor; constructor - exact hr - case tail sb hrsb htrsb ih1 ih2 => - obtain ⟨sb2, htrsb2, hrb⟩ := ih2 - have h := (hswb hrb HasTau.τ).left _ ih1 - obtain ⟨sb2', htrsb2', hrb'⟩ := h - exists sb2' - constructor - · simp only [sTr_τSTr] at htrsb htrsb2' - exact Relation.ReflTransGen.trans htrsb2 htrsb2' - · exact hrb' +theorem IsSWBisimulation.follow_internal_fst + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s1 s2) (hstr : lts₁.τSTr s1 s1') : + ∃ s2', lts₂.τSTr s2 s2' ∧ r s1' s2' := by + induction hstr + case refl => + exists s2 + constructor; constructor + exact hr + case tail sb hrsb htrsb ih1 ih2 => + obtain ⟨sb2, htrsb2, hrb⟩ := ih2 + have h := (hswb hrb HasTau.τ).left _ ih1 + obtain ⟨sb2', htrsb2', hrb'⟩ := h + exists sb2' + constructor + · simp only [sTr_τSTr] at htrsb htrsb2' + exact Relation.ReflTransGen.trans htrsb2 htrsb2' + · exact hrb' /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (second component). -/ -theorem SWBisimulation.follow_internal_snd - [HasTau Label] {lts : LTS State Label} - (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.τSTr s2 s2') : - ∃ s1', lts.τSTr s1 s1' ∧ r s1' s2' := by - induction hstr - case refl => - exists s1 - constructor; constructor - exact hr - case tail sb hrsb htrsb ih1 ih2 => - obtain ⟨sb2, htrsb2, hrb⟩ := ih2 - have h := (hswb hrb HasTau.τ).right _ ih1 - obtain ⟨sb2', htrsb2', hrb'⟩ := h - exists sb2' - constructor - · simp only [sTr_τSTr] at htrsb htrsb2' - exact Relation.ReflTransGen.trans htrsb2 htrsb2' - · exact hrb' - +theorem IsSWBisimulation.follow_internal_snd + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s1 s2) (hstr : lts₂.τSTr s2 s2') : + ∃ s1', lts₁.τSTr s1 s1' ∧ r s1' s2' := by + induction hstr + case refl => + exists s1 + constructor; constructor + exact hr + case tail sb hrsb htrsb ih1 ih2 => + obtain ⟨sb2, htrsb2, hrb⟩ := ih2 + have h := (hswb hrb HasTau.τ).right _ ih1 + obtain ⟨sb2', htrsb2', hrb'⟩ := h + exists sb2' + constructor + · simp only [sTr_τSTr] at htrsb htrsb2' + exact Relation.ReflTransGen.trans htrsb2 htrsb2' + · exact hrb' /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`. This formalises lemma 4.2.10 in [Sangiorgi2011]. -/ theorem isWeakBisimulation_iff_isSWBisimulation - [HasTau Label] {lts : LTS State Label} : - lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r := by + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} : + IsWeakBisimulation lts₁ lts₂ r ↔ IsSWBisimulation lts₁ lts₂ r := by apply Iff.intro case mp => intro h s1 s2 hr μ @@ -864,13 +885,13 @@ theorem isWeakBisimulation_iff_isSWBisimulation case left => intro s1' htr specialize h hr μ - have h' := h.1 s1' (STr.single lts htr) + have h' := h.1 s1' (STr.single lts₁ htr) obtain ⟨s2', htr2, hr2⟩ := h' exists s2' case right => intro s2' htr specialize h hr μ - have h' := h.2 s2' (STr.single lts htr) + have h' := h.2 s2' (STr.single lts₂ htr) obtain ⟨s1', htr1, hr1⟩ := h' exists s1' case mpr => @@ -886,13 +907,13 @@ theorem isWeakBisimulation_iff_isSWBisimulation case tr sb sb' hstr1 htr hstr2 => rw [←sTr_τSTr] at hstr1 hstr2 simp only [sTr_τSTr] at hstr1 hstr2 - obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_fst h hr hstr1 + obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_fst h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).left _ htr - obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2 + obtain ⟨s1', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2 rw [←sTr_τSTr] at hstr1' hstr1b exists s1' constructor - · exact STr.comp lts hstr1b hstr1b' hstr1' + · exact STr.comp lts₂ hstr1b hstr1b' hstr1' · exact hrb2 case right => intro s2' hstr @@ -904,74 +925,77 @@ theorem isWeakBisimulation_iff_isSWBisimulation case tr sb sb' hstr1 htr hstr2 => rw [←sTr_τSTr] at hstr1 hstr2 simp only [sTr_τSTr] at hstr1 hstr2 - obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_snd h hr hstr1 + obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_snd h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).right _ htr - obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2 + obtain ⟨s1', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2 rw [←sTr_τSTr] at hstr1' hstr1b exists s1' constructor - · exact STr.comp lts hstr1b hstr1b' hstr1' + · exact STr.comp lts₁ hstr1b hstr1b' hstr1' · exact hrb2 -theorem WeakBisimulation.toSwBisimulation - [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsWeakBisimulation r) : - lts.IsSWBisimulation r := isWeakBisimulation_iff_isSWBisimulation.1 h +theorem IsWeakBisimulation.isSwBisimulation + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} + (h : IsWeakBisimulation lts₁ lts₂ r) : + IsSWBisimulation lts₁ lts₂ r := isWeakBisimulation_iff_isSWBisimulation.1 h -theorem SWBisimulation.toWeakBisimulation - [HasTau Label] {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsSWBisimulation r) : - lts.IsWeakBisimulation r := isWeakBisimulation_iff_isSWBisimulation.2 h +theorem IsSWBisimulation.isWeakBisimulation + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} + (h : IsSWBisimulation lts₁ lts₂ r) : + IsWeakBisimulation lts₁ lts₂ r := isWeakBisimulation_iff_isSWBisimulation.2 h /-- Weak bisimilarity can also be characterized through sw-bisimulations. -/ @[scoped grind =] -theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts : LTS State Label) : - WeakBisimilarity lts = - fun s1 s2 => ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsSWBisimulation r := by +theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] + (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + WeakBisimilarity lts₁ lts₂ = + fun s1 s2 => ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsSWBisimulation lts₁ lts₂ r := by grind [WeakBisimilarity, isWeakBisimulation_iff_isSWBisimulation.1, isWeakBisimulation_iff_isSWBisimulation.2] -/-- Weak bisimilarity is reflexive. -/ -theorem WeakBisimilarity.refl [HasTau Label] (lts : LTS State Label) (s : State) : +/-- Homogeneous weak bisimilarity is reflexive. -/ +theorem HomWeakBisimilarity.refl [HasTau Label] {lts : LTS State Label} (s : State) : s ≈[lts] s := by - rw [WeakBisimilarity.weakBisim_eq_swBisim lts] + simp only [HomWeakBisimilarity] + rw [WeakBisimilarity.weakBisim_eq_swBisim lts lts] exists Eq grind [IsSWBisimulation, STr.single] /-- The inverse of a weak bisimulation is a weak bisimulation. -/ -theorem WeakBisimulation.inv [HasTau Label] (lts : LTS State Label) - (r : State → State → Prop) (h : lts.IsWeakBisimulation r) : - lts.IsWeakBisimulation (flip r) := by - grind [WeakBisimulation.toSwBisimulation, IsSWBisimulation, - flip, SWBisimulation.toWeakBisimulation] +theorem IsWeakBisimulation.inv [HasTau Label] + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (r : State₁ → State₂ → Prop) (h : IsWeakBisimulation lts₁ lts₂ r) : + IsWeakBisimulation lts₂ lts₁ (flip r) := by + grind [IsWeakBisimulation.isSwBisimulation, IsSWBisimulation, + flip, IsSWBisimulation.isWeakBisimulation] /-- Weak bisimilarity is symmetric. -/ -theorem WeakBisimilarity.symm [HasTau Label] (lts : LTS State Label) (h : s1 ≈[lts] s2) : - s2 ≈[lts] s1 := by +theorem WeakBisimilarity.symm [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + (h : s1 ≈[lts₁,lts₂] s2) : s2 ≈[lts₂,lts₁] s1 := by obtain ⟨r, hr, hrh⟩ := h exists (flip r) - grind [WeakBisimulation.inv, flip] + grind [IsWeakBisimulation.inv, flip] /-- The composition of two weak bisimulations is a weak bisimulation. -/ -theorem WeakBisimulation.comp - [HasTau Label] - (lts : LTS State Label) - (r1 r2 : State → State → Prop) - (h1 : lts.IsWeakBisimulation r1) (h2 : lts.IsWeakBisimulation r2) : - lts.IsWeakBisimulation (Relation.Comp r1 r2) := by +theorem IsWeakBisimulation.comp + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} + (h1 : IsWeakBisimulation lts₁ lts₂ r1) (h2 : IsWeakBisimulation lts₂ lts₃ r2) : + IsWeakBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by simp_all only [IsWeakBisimulation] exact h1.comp h2 /-- The composition of two sw-bisimulations is an sw-bisimulation. -/ -theorem SWBisimulation.comp - [HasTau Label] - (lts : LTS State Label) - (r1 r2 : State → State → Prop) (h1 : lts.IsSWBisimulation r1) (h2 : lts.IsSWBisimulation r2) : - lts.IsSWBisimulation (Relation.Comp r1 r2) := by +theorem IsSWBisimulation.comp + [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} + (h1 : IsSWBisimulation lts₁ lts₂ r1) (h2 : IsSWBisimulation lts₂ lts₃ r2) : + IsSWBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by simp_all only [isWeakBisimulation_iff_isSWBisimulation.symm] - apply WeakBisimulation.comp lts r1 r2 h1 h2 + apply IsWeakBisimulation.comp h1 h2 /-- Weak bisimilarity is transitive. -/ -theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State} - (lts : LTS State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3 := by +theorem WeakBisimilarity.trans [HasTau Label] + {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} + (h1 : s1 ≈[lts₁,lts₂] s2) (h2 : s2 ≈[lts₂,lts₃] s3) : s1 ≈[lts₁,lts₃] s3 := by obtain ⟨r1, hr1, hr1b⟩ := h1 obtain ⟨r2, hr2, hr2b⟩ := h2 exists Relation.Comp r1 r2 @@ -979,14 +1003,14 @@ theorem WeakBisimilarity.trans [HasTau Label] {s1 s2 s3 : State} case left => exists s2 case right => - apply WeakBisimulation.comp lts r1 r2 hr1b hr2b + apply IsWeakBisimulation.comp hr1b hr2b -/-- Weak bisimilarity is an equivalence relation. -/ +/-- Homogeneous weak bisimilarity is an equivalence relation. -/ theorem WeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : - Equivalence (WeakBisimilarity lts) where - refl := WeakBisimilarity.refl lts - symm := WeakBisimilarity.symm lts - trans := WeakBisimilarity.trans lts + Equivalence (HomWeakBisimilarity lts) where + refl := HomWeakBisimilarity.refl + symm := WeakBisimilarity.symm + trans := WeakBisimilarity.trans end WeakBisimulation diff --git a/Cslib/Foundations/Semantics/LTS/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean index 3c894ae95..f9e74f067 100644 --- a/Cslib/Foundations/Semantics/LTS/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -10,33 +10,36 @@ public import Cslib.Foundations.Semantics.LTS.Basic @[expose] public section -/-! # Simulation and Similarity +/-! # IsSimulation and Similarity -A simulation is a binary relation on the states of an `LTS`: if two states `s1` and `s2` are -related by a simulation, then `s2` can mimic all transitions of `s1`. Furthermore, the derivatives -reaches through these transitions remain related by the simulation. +A simulation is a binary relation on the states of two `LTS`s: if two states `s1` and `s2` are +related by a simulation, then `s2` can mimic all transitions of `s1` in their respective LTSs. +Furthermore, the derivatives reaches through these transitions remain related by the simulation. Similarity is the largest simulation: given an `LTS`, it relates any two states that are related by a simulation for that LTS. +The module provides abbreviations for the homogeneous case of comparing states in the same LTS. + For an introduction to theory of simulation, we refer to [Sangiorgi2011]. ## Main definitions -- `Simulation lts r`: the relation `r` on the states of the LTS `lts` is a simulation. -- `Similarity lts` is the binary relation on the states of `lts` that relates any two states -related by some simulation on `lts`. -- `SimulationEquiv lts` is the binary relation on the states of `lts` that relates any two states -similar to each other. +- `IsSimulation lts₁ lts₂ r`: the relation `r` on the states of `lts₁` and `lts₂` is a simulation. +- `Similarity lts₁ lts₂` is the binary relation that relates any two states related by some +simulation on `lts₁` and `lts₂`. +- `SimulationEquiv lts₁ lts₂` is the binary relation on the states of `lts₁` and `lts₂` that relates +any two states similar to each other. ## Notations -- `s1 ≤[lts] s2`: the states `s1` and `s2` are similar in the LTS `lts`. -- `s1 ≤≥[lts] s2`: the states `s1` and `s2` are simulation equivalent in the LTS `lts`. +- `s1 ≤[lts₁, lts₂] s2`: the states `s1` and `s2` are similar under `lts₁` and `lts₂`. +- `s1 ≤≥[lts₁, lts₂] s2`: the states `s1` and `s2` are simulation equivalent under `lts₁` and +`lts₂`. ## Main statements -- `SimulationEquiv.eqv`: simulation equivalence is an equivalence relation. +- `HomSimulationEquiv.eqv`: homogeneous simulation equivalence is an equivalence relation. -/ @@ -46,18 +49,20 @@ universe u v section Simulation -variable {State : Type u} {Label : Type v} (lts : LTS State Label) - /-- A relation is a simulation if, whenever it relates two states in an lts, any transition originating from the first state is mimicked by a transition from the second state and the reached derivatives are themselves related. -/ -def Simulation (lts : LTS State Label) (r : State → State → Prop) : Prop := - ∀ s1 s2, r s1 s2 → ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ r s1' s2' +def IsSimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : + Prop := + ∀ s1 s2, r s1 s2 → ∀ μ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s1' s2' + +/-- A homogeneous simulation is a simulation where the underlying LTSs are the same. -/ +abbrev IsHomSimulation (lts : LTS State Label) := IsSimulation lts lts /-- Two states are similar if they are related by some simulation. -/ -def Similarity (lts : LTS State Label) : State → State → Prop := +def Similarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := fun s1 s2 => - ∃ r : State → State → Prop, r s1 s2 ∧ Simulation lts r + ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsSimulation lts₁ lts₂ r /-- Notation for similarity. @@ -65,18 +70,26 @@ Notation for similarity. Differently from standard pen-and-paper presentations, we require the lts to be mentioned explicitly. -/ -notation s:max " ≤[" lts "] " s':max => Similarity lts s s' +scoped notation s:max " ≤[" lts₁ "," lts₂ "] " s':max => Similarity lts₁ lts₂ s s' + +/-- Homogeneous similarity is similarity where the underlying LTSs are the same. -/ +abbrev HomSimilarity (lts : LTS State Label) := Similarity lts lts -/-- Similarity is reflexive. -/ -theorem Similarity.refl (s : State) : s ≤[lts] s := by +/-- Notation for homogeneous similarity. -/ +scoped notation s:max " ≤[" lts "] " s':max => HomSimilarity lts s s' + +/-- Homogeneous similarity is reflexive. -/ +theorem HomSimilarity.refl (s : State) : s ≤[lts] s := by exists Eq - grind [Simulation] + grind [IsSimulation] /-- The composition of two simulations is a simulation. -/ -theorem Simulation.comp - (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) : - Simulation lts (Relation.Comp r1 r2) := by - simp_all only [Simulation] +theorem IsSimulation.comp + (r1 : State₁ → State₂ → Prop) + (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 s1 s2 hrc μ s1' htr rcases hrc with ⟨sb, hr1, hr2⟩ specialize h1 s1 sb hr1 μ @@ -91,7 +104,8 @@ theorem Simulation.comp · exists s1'' /-- Similarity is transitive. -/ -theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lts] s3 := by +theorem Similarity.trans (h1 : s1 ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,lts₃] s3) : + s1 ≤[lts₁,lts₃] s3 := by obtain ⟨r1, hr1, hr1s⟩ := h1 obtain ⟨r2, hr2, hr2s⟩ := h2 exists Relation.Comp r1 r2 @@ -99,47 +113,52 @@ theorem Similarity.trans (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lt case left => exists s2 case right => - apply Simulation.comp lts r1 r2 hr1s hr2s + apply IsSimulation.comp r1 r2 hr1s hr2s -/-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts] s2` and -`s2 ≤[lts] s1`. -/ -def SimulationEquiv (lts : LTS State Label) : State → State → Prop := +/-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts₁ lts₂] s2` and +`s2 ≤[lts₂ lts₁] s1`. -/ +def SimulationEquiv (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + State₁ → State₂ → Prop := fun s1 s2 => - s1 ≤[lts] s2 ∧ s2 ≤[lts] s1 + s1 ≤[lts₁, lts₂] s2 ∧ s2 ≤[lts₂, lts₁] s1 /-- Notation for simulation equivalence. -/ -notation s:max " ≤≥[" lts "] " s':max => SimulationEquiv lts s s' +scoped notation s:max " ≤≥[" lts₁ "," lts₂ "] " s':max => SimulationEquiv lts₁ lts₂ s s' + +/-- Homogeneous simulation equivalence. -/ +abbrev HomSimulationEquiv (lts : LTS State Label) := SimulationEquiv lts lts + +/-- Notation for homogeneous simulation equivalence. -/ +scoped notation s:max " ≤≥[" lts "] " s':max => HomSimulationEquiv lts s s' -/-- Simulation equivalence is reflexive. -/ -theorem SimulationEquiv.refl (s : State) : s ≤≥[lts] s := by - grind [SimulationEquiv, Similarity.refl] +/-- Homogeneous simulation equivalence is reflexive. -/ +theorem HomSimulationEquiv.refl (s : State) : s ≤≥[lts] s := by + grind [SimulationEquiv, HomSimilarity.refl] /-- Simulation equivalence is symmetric. -/ -theorem SimulationEquiv.symm {s1 s2 : State} (h : s1 ≤≥[lts] s2) : s2 ≤≥[lts] s1 := by +theorem SimulationEquiv.symm {s1 s2 : State} (h : s1 ≤≥[lts₁,lts₂] s2) : s2 ≤≥[lts₂, lts₁] s1 := by grind [SimulationEquiv] /-- Simulation equivalence is transitive. -/ -theorem SimulationEquiv.trans {s1 s2 s3 : State} (h1 : s1 ≤≥[lts] s2) (h2 : s2 ≤≥[lts] s3) : - s1 ≤≥[lts] s3 := by +theorem SimulationEquiv.trans (h1 : s1 ≤≥[lts₁,lts₂] s2) (h2 : s2 ≤≥[lts₂,lts₃] s3) : + s1 ≤≥[lts₁,lts₃] s3 := by grind [SimulationEquiv, Similarity.trans] -/-- Simulation equivalence is an equivalence relation. -/ -theorem SimulationEquiv.eqv (lts : LTS State Label) : - Equivalence (SimulationEquiv lts) := { - refl := SimulationEquiv.refl lts - symm := SimulationEquiv.symm lts - trans := SimulationEquiv.trans lts - } +/-- Homogeneous simulation equivalence is an equivalence relation. -/ +theorem HomSimulationEquiv.eqv : Equivalence (· ≤≥[lts] ·) where + refl := HomSimulationEquiv.refl + symm := SimulationEquiv.symm + trans := SimulationEquiv.trans /-- `calc` support for simulation equivalence. -/ instance : Trans - (SimulationEquiv lts) - (SimulationEquiv lts) - (SimulationEquiv lts) where - trans := SimulationEquiv.trans lts + (SimulationEquiv lts₁ lts₂) + (SimulationEquiv lts₂ lts₃) + (SimulationEquiv lts₁ lts₃) where + trans := SimulationEquiv.trans end Simulation diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index f4036ec20..d12398dc2 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -7,6 +7,7 @@ Authors: Fabrizio Montesi module public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.LTS.Simulation @[expose] public section @@ -33,70 +34,71 @@ Definitions and results on trace equivalence for `LTS`s. namespace Cslib.LTS -universe u v - -variable {State : Type u} {Label : Type v} (lts : LTS State Label) - /-- The traces of a state `s` is the set of all lists of labels `μs` such that there is a multi-step transition labelled by `μs` originating from `s`. -/ -def traces (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } +def traces (lts : LTS State Label) (s : State) := { μs : List Label | ∃ s', lts.MTr s μs s' } /-- If there is a multi-step transition from `s` labelled by `μs`, then `μs` is in the traces of `s`. -/ -theorem traces_in (s : State) (μs : List Label) (s' : State) (h : lts.MTr s μs s') : - μs ∈ lts.traces s := by - exists s' +theorem traces_in {lts : LTS State Label} (h : lts.MTr s μs s') : μs ∈ lts.traces s := by exists s' /-- Two states are trace equivalent if they have the same set of traces. -/ -def TraceEq (s1 s2 : State) := lts.traces s1 = lts.traces s2 +def TraceEq (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) + (s1 : State₁) (s2 : State₂) := + lts₁.traces s1 = lts₂.traces s2 /-- Notation for trace equivalence. -Differently from standard pen-and-paper presentations, we require the lts to be mentioned +Differently from standard pen-and-paper presentations, we require the LTSs to be mentioned explicitly. -/ -notation s " ~tr[" lts "] " s' => TraceEq lts s s' +scoped notation s " ~tr[" lts₁ "," lts₂ "] " s' => TraceEq lts₁ lts₂ s s' + +/-- Homogeneous trace equivalence compares states on the same LTS. -/ +abbrev HomTraceEq (lts : LTS State Label) := TraceEq lts lts + +/-- Notation for homogeneous trace equivalence. -/ +scoped notation s:max " ~tr[" lts "] " s':max => HomTraceEq lts s s' -/-- Trace equivalence is reflexive. -/ -theorem TraceEq.refl (s : State) : s ~tr[lts] s := by +/-- Homogeneous trace equivalence is reflexive. -/ +theorem HomTraceEq.refl (s : State) : s ~tr[lts] s := by simp only [TraceEq] /-- Trace equivalence is symmetric. -/ -theorem TraceEq.symm (lts : LTS State Label) {s1 s2 : State} (h : s1 ~tr[lts] s2) : - s2 ~tr[lts] s1 := by +theorem TraceEq.symm (h : s1 ~tr[lts₁,lts₂] s2) : s2 ~tr[lts₂,lts₁] s1 := by simp only [TraceEq] at h simp only [TraceEq] rw [h] /-- Trace equivalence is transitive. -/ -theorem TraceEq.trans {s1 s2 s3 : State} (h1 : s1 ~tr[lts] s2) (h2 : s2 ~tr[lts] s3) : - s1 ~tr[lts] s3 := by +theorem TraceEq.trans (h1 : s1 ~tr[lts₁,lts₂] s2) (h2 : s2 ~tr[lts₂,lts₃] s3) : + s1 ~tr[lts₁,lts₃] s3 := by simp only [TraceEq] at * rw [h1, h2] -/-- Trace equivalence is an equivalence relation. -/ -theorem TraceEq.eqv (lts : LTS State Label) : Equivalence (TraceEq lts) where - refl := TraceEq.refl lts - symm := TraceEq.symm lts - trans := TraceEq.trans lts +/-- Homogeneous trace equivalence is an equivalence relation. -/ +theorem HomTraceEq.eqv : Equivalence (· ~tr[lts] ·) where + refl := HomTraceEq.refl + symm := TraceEq.symm + trans := TraceEq.trans /-- `calc` support for simulation equivalence. -/ -instance : Trans (TraceEq lts) (TraceEq lts) (TraceEq lts) where - trans := TraceEq.trans lts - -/-- In a deterministic LTS, trace equivalence is a simulation. -/ -theorem TraceEq.deterministic_sim - (lts : LTS State Label) [hdet : lts.Deterministic] (s1 s2 : State) (h : s1 ~tr[lts] s2) : - ∀ μ s1', lts.Tr s1 μ s1' → ∃ s2', lts.Tr s2 μ s2' ∧ s1' ~tr[lts] s2' := by - intro μ s1' htr1 - have hmtr1 := MTr.single lts htr1 - have hin := traces_in lts s1 [μ] s1' hmtr1 +instance : Trans (TraceEq lts₁ lts₂) (TraceEq lts₂ lts₃) (TraceEq lts₁ lts₃) where + trans := TraceEq.trans + +/-- In deterministic LTSs, trace equivalence is a simulation. -/ +theorem TraceEq.deterministic_isSimulation {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] : + IsSimulation lts₁ lts₂ (TraceEq lts₁ lts₂) := by + intro s1 s2 h μ s1' htr1 + have hmtr1 := MTr.single lts₁ htr1 + have hin := traces_in hmtr1 rw [h] at hin obtain ⟨s2', hmtr2⟩ := hin exists s2' constructor - · apply MTr.single_invert lts _ _ _ hmtr2 + · apply MTr.single_invert lts₂ _ _ _ hmtr2 · simp only [TraceEq, traces] funext μs' simp only [eq_iff_iff] @@ -105,29 +107,29 @@ theorem TraceEq.deterministic_sim case mp => intro hmtr1' obtain ⟨s1'', hmtr1'⟩ := hmtr1' - have hmtr1comp := MTr.comp lts hmtr1 hmtr1' - have hin := traces_in lts s1 ([μ] ++ μs') s1'' hmtr1comp + have hmtr1comp := MTr.comp lts₁ hmtr1 hmtr1' + have hin := traces_in hmtr1comp rw [h] at hin obtain ⟨s', hmtr2'⟩ := hin cases hmtr2' case stepL s2'' htr2 hmtr2' => exists s' - have htr2' := MTr.single_invert lts _ _ _ hmtr2 - have hdets2 := hdet.deterministic s2 μ s2' s2'' htr2' htr2 + have htr2' := MTr.single_invert lts₂ _ _ _ hmtr2 + have hdets2 := hdet₂.deterministic s2 μ s2' s2'' htr2' htr2 rw [hdets2] exact hmtr2' case mpr => intro hmtr2' obtain ⟨s2'', hmtr2'⟩ := hmtr2' - have hmtr2comp := MTr.comp lts hmtr2 hmtr2' - have hin := traces_in lts s2 ([μ] ++ μs') s2'' hmtr2comp + have hmtr2comp := MTr.comp lts₂ hmtr2 hmtr2' + have hin := traces_in hmtr2comp rw [← h] at hin obtain ⟨s', hmtr1'⟩ := hin cases hmtr1' case stepL s1'' htr1 hmtr1' => exists s' - have htr1' := MTr.single_invert lts _ _ _ hmtr1 - have hdets1 := hdet.deterministic s1 μ s1' s1'' htr1' htr1 + have htr1' := MTr.single_invert lts₁ _ _ _ hmtr1 + have hdets1 := hdet₁.deterministic s1 μ s1' s1'' htr1' htr1 rw [hdets1] exact hmtr1' diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 08a9b002e..83850eb12 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -204,14 +204,14 @@ theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q constructor · unfold lts cases htr with grind - · grind [ChoiceComm] + · grind [HomBisimilarity.refl, ChoiceComm] case right => intro s1' htr exists s1' constructor · unfold lts cases htr with grind - · grind [ChoiceComm] + · grind [HomBisimilarity.refl, ChoiceComm] case bisim h => grind [ChoiceComm] @@ -326,7 +326,7 @@ theorem bisimilarity_congr_choice : constructor · apply Tr.choiceR htr · constructor - apply Bisimilarity.refl + apply HomBisimilarity.refl case bisim hbisim => obtain ⟨rel, hr, hb⟩ := hbisim obtain ⟨s2', htr2, hr2⟩ := hb.follow_fst hr htr @@ -353,7 +353,7 @@ theorem bisimilarity_congr_choice : constructor · apply Tr.choiceR htr · constructor - apply Bisimilarity.refl + apply HomBisimilarity.refl case bisim hbisim => obtain ⟨rel, hr, hb⟩ := hbisim obtain ⟨s1', htr1, hr1⟩ := hb.follow_snd hr htr @@ -435,7 +435,7 @@ theorem bisimilarity_is_congruence /-- Bisimilarity is a congruence in CCS. -/ instance bisimilarityCongruence : - Congruence (Process Name Constant) (Bisimilarity (lts (defs := defs))) where + Congruence (Process Name Constant) (HomBisimilarity (lts (defs := defs))) where covariant := ⟨by grind [Covariant, bisimilarity_is_congruence]⟩ end CCS diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean index 3b887a237..9d7478a5a 100644 --- a/Cslib/Logics/HML/Basic.lean +++ b/Cslib/Logics/HML/Basic.lean @@ -116,7 +116,7 @@ abbrev theory (lts : LTS State Label) (s : State) : Set (Proposition Label) := abbrev TheoryEq (lts : LTS State Label) (s1 s2 : State) := theory lts s1 = theory lts s2 -open Proposition LTS Bisimulation Simulation +open Proposition LTS /-- Characterisation theorem for the denotational semantics. -/ @[scoped grind =] @@ -201,7 +201,7 @@ end ImageToPropositions @[scoped grind ⇒] theorem theoryEq_isBisimulation (lts : LTS State Label) [image_finite : ∀ s μ, Finite (lts.image s μ)] : - lts.IsBisimulation (TheoryEq lts) := by + lts.IsHomBisimulation (TheoryEq lts) := by intro s1 s2 h μ let (s : State) := @Fintype.ofFinite (lts.image s μ) (image_finite s μ) constructor @@ -237,7 +237,7 @@ theorem theoryEq_isBisimulation (lts : LTS State Label) well. -/ @[scoped grind ⇒] lemma bisimulation_satisfies {lts : LTS State Label} - {hrb : lts.IsBisimulation r} + {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) (a : Proposition Label) (hs : Satisfies lts s1 a) : Satisfies lts s2 a := by induction a generalizing s1 s2 with @@ -245,7 +245,7 @@ lemma bisimulation_satisfies {lts : LTS State Label} | _ => grind lemma bisimulation_TheoryEq {lts : LTS State Label} - {hrb : lts.IsBisimulation r} + {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) : TheoryEq lts s1 s2 := by have : s2 ~[lts] s1 := by grind [Bisimilarity.symm] @@ -254,7 +254,7 @@ lemma bisimulation_TheoryEq {lts : LTS State Label} /-- Theory equivalence and bisimilarity coincide for image-finite LTSs. -/ theorem theoryEq_eq_bisimilarity (lts : LTS State Label) [image_finite : ∀ s μ, Finite (lts.image s μ)] : - TheoryEq lts = Bisimilarity lts := by + TheoryEq lts = HomBisimilarity lts := by ext s1 s2 apply Iff.intro <;> intro h · exists TheoryEq lts From a2154485f98be814f60cdd7e348a582630a628c2 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 12:56:37 +0200 Subject: [PATCH 2/8] switch to subscripts --- .../Semantics/LTS/Bisimulation.lean | 270 +++++++++--------- .../Foundations/Semantics/LTS/Simulation.lean | 44 +-- Cslib/Foundations/Semantics/LTS/TraceEq.lean | 36 +-- 3 files changed, 175 insertions(+), 175 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 047aa99f0..cc1b6949f 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -16,8 +16,8 @@ public import Cslib.Foundations.Semantics.LTS.TraceEq /-! # Bisimulation and Bisimilarity A bisimulation is a binary relation on the states of two `LTS`s, which establishes a tight semantic -correspondence. More specifically, if two states `s1` and `s2` are related by a bisimulation, then -`s1` can mimic all transitions of `s2` and vice versa. Furthermore, the derivatives reaches through +correspondence. More specifically, if two states `s₁` and `s₂` are related by a bisimulation, then +`s₁` can mimic all transitions of `s₂` and vice versa. Furthermore, the derivatives reaches through these transitions remain related by the bisimulation. Bisimilarity is the largest bisimulation: given an `LTS`, it relates any two states that are related @@ -45,8 +45,8 @@ we prove to be sound and complete. ## Notations -- `s1 ~[lts] s2`: the states `s1` and `s2` are bisimilar in the LTS `lts`. -- `s1 ≈[lts] s2`: the states `s1` and `s2` are weakly bisimilar in the LTS `lts`. +- `s₁ ~[lts] s₂`: the states `s₁` and `s₂` are bisimilar in the LTS `lts`. +- `s₁ ≈[lts] s₂`: the states `s₁` and `s₂` are weakly bisimilar in the LTS `lts`. ## Main statements @@ -76,10 +76,10 @@ derivatives are themselves related. -/ @[scoped grind =] def IsBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop := - ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s1' s2') + ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( + (∀ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂') ∧ - (∀ s2', lts₂.Tr s2 μ s2' → ∃ s1', lts₁.Tr s1 μ s1' ∧ r s1' s2') + (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂') ) /-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/ @@ -87,20 +87,20 @@ abbrev IsHomBisimulation (lts : LTS State Label) := IsBisimulation lts lts /-- Helper for following a transition by the first state in a pair of a `Bisimulation`. -/ theorem IsBisimulation.follow_fst - (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) (htr : lts₁.Tr s1 μ s1') : - ∃ s2', lts₂.Tr s2 μ s2' ∧ r s1' s2' := + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (htr : lts₁.Tr s₁ μ s₁') : + ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂' := (hb hr μ).1 _ htr /-- Helper for following a transition by the second state in a pair of a `Bisimulation`. -/ theorem IsBisimulation.follow_snd - (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) (htr : lts₂.Tr s2 μ s2') : - ∃ s1', lts₁.Tr s1 μ s1' ∧ r s1' s2' := + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (htr : lts₂.Tr s₂ μ s₂') : + ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂' := (hb hr μ).2 _ htr /-- Two states are bisimilar if they are related by some bisimulation. -/ @[scoped grind =] def Bisimilarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := - fun s1 s2 => ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsBisimulation lts₁ lts₂ r + fun s₁ s₂ => ∃ r : State₁ → State₂ → Prop, r s₁ s₂ ∧ IsBisimulation lts₁ lts₂ r /-- Notation for bisimilarity. @@ -130,7 +130,7 @@ theorem IsBisimulation.inv (h : IsBisimulation lts₁ lts₂ r) : open scoped IsBisimulation in /-- Bisimilarity is symmetric. -/ @[scoped grind →, symm] -theorem Bisimilarity.symm {s1 s2 : State} (h : s1 ~[lts₁,lts₂] s2) : s2 ~[lts₂,lts₁] s1 := by +theorem Bisimilarity.symm {s₁ s₂ : State} (h : s₁ ~[lts₁,lts₂] s₂) : s₂ ~[lts₂,lts₁] s₁ := by grind [flip] /-- The composition of two bisimulations is a bisimulation. -/ @@ -142,8 +142,8 @@ theorem IsBisimulation.comp /-- Bisimilarity is transitive. -/ @[scoped grind →] theorem Bisimilarity.trans - (h1 : s1 ~[lts₁,lts₂] s2) (h2 : s2 ~[lts₂,lts₃] s3) : - s1 ~[lts₁,lts₃] s3 := by + (h1 : s₁ ~[lts₁,lts₂] s₂) (h2 : s₂ ~[lts₂,lts₃] s₃) : + s₁ ~[lts₁,lts₃] s₃ := by obtain ⟨r1, _, _⟩ := h1 obtain ⟨r2, _, _⟩ := h2 exists Relation.Comp r1 r2 @@ -166,21 +166,21 @@ instance : IsEquiv State (HomBisimilarity lts) where @[scoped grind .] theorem Bisimulation.union (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisimulation lts₁ lts₂ s) : IsBisimulation lts₁ lts₂ (r ⊔ s) := by - intro s1 s2 hrs μ + intro s₁ s₂ hrs μ cases hrs case inl h => constructor - · intro s1' htr - obtain ⟨s2', htr', hr'⟩ := hrb.follow_fst h htr - exists s2' + · intro s₁' htr + obtain ⟨s₂', htr', hr'⟩ := hrb.follow_fst h htr + exists s₂' constructor · assumption · simp only [max, SemilatticeSup.sup] left exact hr' - · intro s2' htr - obtain ⟨s1', htr', hr'⟩ := hrb.follow_snd h htr - exists s1' + · intro s₂' htr + obtain ⟨s₁', htr', hr'⟩ := hrb.follow_snd h htr + exists s₁' constructor · assumption · simp only [max, SemilatticeSup.sup] @@ -188,17 +188,17 @@ theorem Bisimulation.union (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisim exact hr' case inr h => constructor - · intro s1' htr - obtain ⟨s2', htr', hs'⟩ := hsb.follow_fst h htr - exists s2' + · intro s₁' htr + obtain ⟨s₂', htr', hs'⟩ := hsb.follow_fst h htr + exists s₂' constructor · assumption · simp only [max, SemilatticeSup.sup] right exact hs' - · intro s2' htr - obtain ⟨s1', htr', hs'⟩ := hsb.follow_snd h htr - exists s1' + · intro s₂' htr + obtain ⟨s₁', htr', hs'⟩ := hsb.follow_snd h htr + exists s₁' constructor · assumption · simp only [max, SemilatticeSup.sup] @@ -213,14 +213,14 @@ theorem Bisimilarity.is_bisimulation : IsBisimulation lts₁ lts₂ (Bisimilarit @[scoped grind →] theorem Bisimilarity.largest_bisimulation (h : IsBisimulation lts₁ lts₂ r) : Subrelation r (Bisimilarity lts₁ lts₂) := by - intro s1 s2 hr + intro s₁ s₂ hr exists r /-- The union of bisimilarity with any bisimulation is bisimilarity. -/ @[scoped grind =, simp] theorem Bisimilarity.gfp (r : State₁ → State₂ → Prop) (h : IsBisimulation lts₁ lts₂ r) : (Bisimilarity lts₁ lts₂) ⊔ r = Bisimilarity lts₁ lts₂ := by - funext s1 s2 + funext s₁ s₂ simp only [max, SemilatticeSup.sup] grind @@ -240,20 +240,20 @@ instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where sup r s := r ⊔ s le_sup_left r s := by simp only [LE.le] - intro s1 s2 hr + intro s₁ s₂ hr simp only [max, SemilatticeSup.sup] left exact hr le_sup_right r s := by simp only [LE.le] - intro s1 s2 hs + intro s₁ s₂ hs simp only [max, SemilatticeSup.sup] right exact hs sup_le r s t := by intro h1 h2 simp only [LE.le, max, SemilatticeSup.sup] - intro s1 s2 h + intro s₁ s₂ h cases h case inl h => apply h1 _ _ h @@ -263,7 +263,7 @@ instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where /-- The empty (heterogeneous) relation is a bisimulation. -/ @[scoped grind .] theorem Bisimulation.emptyHRelation_bisimulation : IsBisimulation lts₁ lts₂ emptyHRelation := by - intro s1 s2 hr + intro s₁ s₂ hr cases hr /-- In the inclusion order on bisimulations: @@ -275,11 +275,11 @@ instance : BoundedOrder {r // IsBisimulation lts₁ lts₂ r} where top := ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ bot := ⟨emptyHRelation, Bisimulation.emptyHRelation_bisimulation⟩ le_top r := by - intro s1 s2 + intro s₁ s₂ simp only [LE.le] grind bot_le r := by - intro s1 s2 + intro s₁ s₂ simp only [LE.le] intro hr cases hr @@ -299,89 +299,89 @@ derivatives are themselves related by `r` up to bisimilarity. -/ @[scoped grind] def IsBisimulationUpTo (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop := - ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.Tr s2 μ s2' ∧ - (UpToHomBisimilarity lts₁ lts₂ r) s1' s2') + ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( + (∀ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ + (UpToHomBisimilarity lts₁ lts₂ r) s₁' s₂') ∧ - (∀ s2', lts₂.Tr s2 μ s2' → ∃ s1', lts₁.Tr s1 μ s1' ∧ - (UpToHomBisimilarity lts₁ lts₂ r) s1' s2') + (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ + (UpToHomBisimilarity lts₁ lts₂ r) s₁' s₂') ) /-- Any bisimulation up to bisimilarity is a bisimulation. -/ @[scoped grind →] theorem IsBisimulationUpTo.is_bisimulation (h : IsBisimulationUpTo lts₁ lts₂ r) : IsBisimulation lts₁ lts₂ (UpToHomBisimilarity lts₁ lts₂ r) := by - intro s1 s2 hr μ - rcases hr with ⟨s1b, hr1b, s2b, hrb, hr2b⟩ + intro s₁ s₂ hr μ + rcases hr with ⟨s₁b, hr1b, s₂b, hrb, hr2b⟩ obtain ⟨r1, hr1, hr1b⟩ := hr1b obtain ⟨r2, hr2, hr2b⟩ := hr2b constructor case left => - intro s1' htr1 - obtain ⟨s1b', hs1b'tr, hs1b'r⟩ := (hr1b hr1 μ).1 s1' htr1 - obtain ⟨s2b', hs2b'tr, hs2b'r⟩ := (h hrb μ).1 s1b' hs1b'tr - obtain ⟨s2', hs2btr, hs2br⟩ := (hr2b hr2 μ).1 _ hs2b'tr - exists s2' + intro s₁' htr1 + obtain ⟨s₁b', hs₁b'tr, hs₁b'r⟩ := (hr1b hr1 μ).1 s₁' htr1 + obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := (h hrb μ).1 s₁b' hs₁b'tr + obtain ⟨s₂', hs₂btr, hs₂br⟩ := (hr2b hr2 μ).1 _ hs₂b'tr + exists s₂' constructor case left => - exact hs2btr + exact hs₂btr case right => - obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs2b'r + obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₂b'r constructor constructor - · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b hs1b'r) + · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b hs₁b'r) hsmidb · exists smid2 constructor · exact hsmidr · apply Bisimilarity.trans hsmidrb - apply Bisimilarity.largest_bisimulation hr2b hs2br + apply Bisimilarity.largest_bisimulation hr2b hs₂br case right => - intro s2' htr2 - obtain ⟨s2b', hs2b'tr, hs2b'r⟩ := (hr2b hr2 μ).2 s2' htr2 - obtain ⟨s1b', hs1b'tr, hs1b'r⟩ := (h hrb μ).2 s2b' hs2b'tr - obtain ⟨s1', hs1btr, hs1br⟩ := (hr1b hr1 μ).2 _ hs1b'tr - exists s1' + intro s₂' htr2 + obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := (hr2b hr2 μ).2 s₂' htr2 + obtain ⟨s₁b', hs₁b'tr, hs₁b'r⟩ := (h hrb μ).2 s₂b' hs₂b'tr + obtain ⟨s₁', hs₁btr, hs₁br⟩ := (hr1b hr1 μ).2 _ hs₁b'tr + exists s₁' constructor case left => - exact hs1btr + exact hs₁btr case right => - obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs1b'r + obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₁b'r constructor constructor · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b _) hsmidb - · exact hs1br + · exact hs₁br · exists smid2 constructor · exact hsmidr · apply Bisimilarity.trans hsmidrb apply Bisimilarity.largest_bisimulation hr2b _ - exact hs2b'r + exact hs₂b'r /-- 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 s1 s2) : - ∀ μs s1', lts₁.MTr s1 μs s1' → ∃ s2', lts₂.MTr s2 μs s2' ∧ r s1' s2' := by + (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₂' := by intro μs - induction μs generalizing s1 s2 + induction μs generalizing s₁ s₂ case nil => - intro s1' hmtr1 - exists s2 + intro s₁' hmtr1 + exists s₂ cases hmtr1 constructor constructor exact hr case cons μ μs' ih => - intro s1' hmtr1 + intro s₁' hmtr1 cases hmtr1 - case stepL s1'' htr hmtr => + case stepL s₁'' htr hmtr => specialize hb hr μ - have hf := hb.1 s1'' htr - obtain ⟨s2'', htr2, hb2⟩ := hf - specialize ih hb2 s1' hmtr - obtain ⟨s2', hmtr2, hr'⟩ := ih - exists s2' + have hf := hb.1 s₁'' htr + obtain ⟨s₂'', htr2, hb2⟩ := hf + specialize ih hb2 s₁' hmtr + obtain ⟨s₂', hmtr2, hr'⟩ := ih + exists s₂' constructor case left => constructor @@ -395,28 +395,28 @@ theorem IsBisimulation.bisim_trace /-- Any bisimulation implies trace equivalence. -/ @[scoped grind =>] theorem IsBisimulation.traceEq - (hb : IsBisimulation lts₁ lts₂ r) (hr : r s1 s2) : - s1 ~tr[lts₁,lts₂] s2 := by + (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) : + s₁ ~tr[lts₁,lts₂] s₂ := by funext μs simp only [eq_iff_iff] constructor case mp => intro h - obtain ⟨s1', h⟩ := h - obtain ⟨s2', hmtr⟩ := IsBisimulation.bisim_trace hb hr μs s1' h - exists s2' + obtain ⟨s₁', h⟩ := h + obtain ⟨s₂', hmtr⟩ := IsBisimulation.bisim_trace hb hr μs s₁' h + exists s₂' exact hmtr.1 case mpr => intro h - obtain ⟨s2', h⟩ := h - obtain ⟨s1', hmtr⟩ := IsBisimulation.bisim_trace hb.inv hr μs s2' h - exists s1' + obtain ⟨s₂', h⟩ := h + obtain ⟨s₁', hmtr⟩ := IsBisimulation.bisim_trace hb.inv hr μs s₂' h + exists s₁' exact hmtr.1 /-- Bisimilarity is included in trace equivalence. -/ @[scoped grind .] theorem Bisimilarity.le_traceEq : Bisimilarity lts₁ lts₂ ≤ TraceEq lts₁ lts₂ := by - intro s1 s2 h + intro s₁ s₂ h obtain ⟨r, hr, hb⟩ := h apply hb.traceEq hr @@ -446,7 +446,7 @@ theorem Bisimulation.traceEq_not_bisim : -- specialize h 1 5 have htreq : (1 ~tr[lts] 5) := by simp [TraceEq] - have htraces1 : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by + have htraces₁ : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -495,7 +495,7 @@ theorem Bisimulation.traceEq_not_bisim : · apply BisimMotTr.one2two · apply MTr.single apply BisimMotTr.two2four - have htraces2 : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by + have htraces₂ : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -556,16 +556,16 @@ theorem Bisimulation.traceEq_not_bisim : · apply BisimMotTr.five2eight · apply MTr.single; apply BisimMotTr.eight2nine - simp [htraces1, htraces2] + simp [htraces₁, htraces₂] specialize h htreq specialize h 'a' obtain ⟨h1, h2⟩ := h specialize h1 2 (by constructor) - obtain ⟨s2', htr5, cih⟩ := h1 + obtain ⟨s₂', htr5, cih⟩ := h1 cases htr5 case five2six => simp [TraceEq] at cih - have htraces2 : lts.traces 2 = {[], ['b'], ['c']} := by + have htraces₂ : lts.traces 2 = {[], ['b'], ['c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -630,7 +630,7 @@ theorem Bisimulation.traceEq_not_bisim : grind case five2eight => simp only [TraceEq] at cih - have htraces2 : lts.traces 2 = {[], ['b'], ['c']} := by + have htraces₂ : lts.traces 2 = {[], ['b'], ['c']} := by apply Set.ext_iff.2 intro μs apply Iff.intro @@ -692,7 +692,7 @@ theorem Bisimulation.traceEq_not_bisim : simp at h simp [h] repeat constructor - rw [htraces2, htraces8] at cih + rw [htraces₂, htraces8] at cih apply Set.ext_iff.1 at cih specialize cih ['b'] obtain ⟨cih1, cih2⟩ := cih @@ -720,16 +720,16 @@ theorem Bisimulation.deterministic_traceEq_is_bisim [lts₁.Deterministic] [lts₂.Deterministic] : (IsBisimulation lts₁ lts₂ (TraceEq lts₁ lts₂)) := by simp only [IsBisimulation] - intro s1 s2 hteq μ + intro s₁ s₂ hteq μ constructor case left => - apply TraceEq.deterministic_isSimulation s1 s2 hteq + apply TraceEq.deterministic_isSimulation s₁ s₂ hteq case right => - intro s2' htr + intro s₂' htr apply TraceEq.symm at hteq - have h := TraceEq.deterministic_isSimulation s2 s1 hteq μ s2' htr - obtain ⟨s1', h⟩ := h - exists s1' + have h := TraceEq.deterministic_isSimulation s₂ s₁ hteq μ s₂' htr + obtain ⟨s₁', h⟩ := h + exists s₁' constructor case left => exact h.1 @@ -738,8 +738,8 @@ theorem Bisimulation.deterministic_traceEq_is_bisim /-- 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 : s1 ~tr[lts₁,lts₂] s2) : - (s1 ~[lts₁,lts₂] s2) := by + [lts₁.Deterministic] [lts₂.Deterministic] (h : s₁ ~tr[lts₁,lts₂] s₂) : + (s₁ ~[lts₁,lts₂] s₂) := by exists TraceEq lts₁ lts₂ constructor case left => @@ -751,7 +751,7 @@ theorem Bisimilarity.deterministic_traceEq_bisim {lts₁ : LTS State₁ Label} { 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 s1 s2 + funext s₁ s₂ simp only [eq_iff_iff] constructor case mp => @@ -768,18 +768,18 @@ theorem Bisimulation.isSimulation : IsBisimulation lts₁ lts₂ r → IsSimulat /-- A relation is a bisimulation iff both it and its inverse are simulations. -/ theorem Bisimulation.simulation_iff : IsBisimulation lts₁ lts₂ r ↔ (IsSimulation lts₁ lts₂ r ∧ IsSimulation lts₂ lts₁ (flip r)) := by - have _ (s1 s2) : r s1 s2 → flip r s2 s1 := id + have _ (s₁ s₂) : r s₁ s₂ → flip r s₂ s₁ := id grind [IsSimulation, flip] /-- Homogeneous bisimilarity can also be characterized through symmetric simulations. -/ theorem HomBisimilarity.symm_simulation : HomBisimilarity lts = - fun s1 s2 => ∃ r, r s1 s2 ∧ Std.Symm r ∧ IsHomSimulation lts r := by - funext s1 s2 + fun s₁ s₂ => ∃ r, r s₁ s₂ ∧ Std.Symm r ∧ IsHomSimulation lts r := by + funext s₁ s₂ apply Iff.eq apply Iff.intro · intro h - have bisim : HomBisimilarity lts s1 s2 ∧ Std.Symm (HomBisimilarity lts) + have bisim : HomBisimilarity lts s₁ s₂ ∧ Std.Symm (HomBisimilarity lts) ∧ IsHomSimulation lts (HomBisimilarity lts) := by grind [Std.Symm, Bisimilarity.symm, Bisimulation.isSimulation] grind @@ -808,8 +808,8 @@ abbrev IsHomWeakBisimulation [HasTau Label] (lts : LTS State Label) := IsWeakBis /-- Two states are weakly bisimilar if they are related by some weak bisimulation. -/ def WeakBisimilarity [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := - fun s1 s2 => - ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsWeakBisimulation lts₁ lts₂ r + fun s₁ s₂ => + ∃ r : State₁ → State₂ → Prop, r s₁ s₂ ∧ IsWeakBisimulation lts₁ lts₂ r /-- Notation for weak bisimilarity. -/ scoped notation s:max " ≈[" lts₁ "," lts₂ "] " s':max => WeakBisimilarity lts₁ lts₂ s s' @@ -825,21 +825,21 @@ is a single transition. We prove later that this technique is sound, following a by [Sangiorgi2011]. -/ def IsSWBisimulation [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop := - ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, ( - (∀ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.STr s2 μ s2' ∧ r s1' s2') + ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( + (∀ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.STr s₂ μ s₂' ∧ r s₁' s₂') ∧ - (∀ s2', lts₂.Tr s2 μ s2' → ∃ s1', lts₁.STr s1 μ s1' ∧ r s1' s2') + (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.STr s₁ μ s₁' ∧ r s₁' s₂') ) /-- Utility theorem for 'following' internal transitions using an `SWBisimulation` (first component). -/ theorem IsSWBisimulation.follow_internal_fst [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} - (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s1 s2) (hstr : lts₁.τSTr s1 s1') : - ∃ s2', lts₂.τSTr s2 s2' ∧ r s1' s2' := by + (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (hstr : lts₁.τSTr s₁ s₁') : + ∃ s₂', lts₂.τSTr s₂ s₂' ∧ r s₁' s₂' := by induction hstr case refl => - exists s2 + exists s₂ constructor; constructor exact hr case tail sb hrsb htrsb ih1 ih2 => @@ -856,11 +856,11 @@ theorem IsSWBisimulation.follow_internal_fst (second component). -/ theorem IsSWBisimulation.follow_internal_snd [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} - (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s1 s2) (hstr : lts₂.τSTr s2 s2') : - ∃ s1', lts₁.τSTr s1 s1' ∧ r s1' s2' := by + (hswb : IsSWBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) (hstr : lts₂.τSTr s₂ s₂') : + ∃ s₁', lts₁.τSTr s₁ s₁' ∧ r s₁' s₂' := by induction hstr case refl => - exists s1 + exists s₁ constructor; constructor exact hr case tail sb hrsb htrsb ih1 ih2 => @@ -880,28 +880,28 @@ theorem isWeakBisimulation_iff_isSWBisimulation IsWeakBisimulation lts₁ lts₂ r ↔ IsSWBisimulation lts₁ lts₂ r := by apply Iff.intro case mp => - intro h s1 s2 hr μ + intro h s₁ s₂ hr μ apply And.intro case left => - intro s1' htr + intro s₁' htr specialize h hr μ - have h' := h.1 s1' (STr.single lts₁ htr) - obtain ⟨s2', htr2, hr2⟩ := h' - exists s2' + have h' := h.1 s₁' (STr.single lts₁ htr) + obtain ⟨s₂', htr2, hr2⟩ := h' + exists s₂' case right => - intro s2' htr + intro s₂' htr specialize h hr μ - have h' := h.2 s2' (STr.single lts₂ htr) - obtain ⟨s1', htr1, hr1⟩ := h' - exists s1' + have h' := h.2 s₂' (STr.single lts₂ htr) + obtain ⟨s₁', htr1, hr1⟩ := h' + exists s₁' case mpr => - intro h s1 s2 hr μ + intro h s₁ s₂ hr μ apply And.intro case left => - intro s1' hstr + intro s₁' hstr cases hstr case refl => - exists s2 + exists s₂ constructor; constructor exact hr case tr sb sb' hstr1 htr hstr2 => @@ -909,17 +909,17 @@ theorem isWeakBisimulation_iff_isSWBisimulation simp only [sTr_τSTr] at hstr1 hstr2 obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_fst h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).left _ htr - obtain ⟨s1', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2 + obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2 rw [←sTr_τSTr] at hstr1' hstr1b - exists s1' + exists s₁' constructor · exact STr.comp lts₂ hstr1b hstr1b' hstr1' · exact hrb2 case right => - intro s2' hstr + intro s₂' hstr cases hstr case refl => - exists s1 + exists s₁ constructor; constructor exact hr case tr sb sb' hstr1 htr hstr2 => @@ -927,9 +927,9 @@ theorem isWeakBisimulation_iff_isSWBisimulation simp only [sTr_τSTr] at hstr1 hstr2 obtain ⟨sb1, hstr1b, hrb⟩ := IsSWBisimulation.follow_internal_snd h hr hstr1 obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).right _ htr - obtain ⟨s1', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2 + obtain ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2 rw [←sTr_τSTr] at hstr1' hstr1b - exists s1' + exists s₁' constructor · exact STr.comp lts₁ hstr1b hstr1b' hstr1' · exact hrb2 @@ -949,7 +949,7 @@ theorem IsSWBisimulation.isWeakBisimulation theorem WeakBisimilarity.weakBisim_eq_swBisim [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : WeakBisimilarity lts₁ lts₂ = - fun s1 s2 => ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsSWBisimulation lts₁ lts₂ r := by + fun s₁ s₂ => ∃ r : State₁ → State₂ → Prop, r s₁ s₂ ∧ IsSWBisimulation lts₁ lts₂ r := by grind [WeakBisimilarity, isWeakBisimulation_iff_isSWBisimulation.1, isWeakBisimulation_iff_isSWBisimulation.2] @@ -971,7 +971,7 @@ theorem IsWeakBisimulation.inv [HasTau Label] /-- Weak bisimilarity is symmetric. -/ theorem WeakBisimilarity.symm [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} - (h : s1 ≈[lts₁,lts₂] s2) : s2 ≈[lts₂,lts₁] s1 := by + (h : s₁ ≈[lts₁,lts₂] s₂) : s₂ ≈[lts₂,lts₁] s₁ := by obtain ⟨r, hr, hrh⟩ := h exists (flip r) grind [IsWeakBisimulation.inv, flip] @@ -995,13 +995,13 @@ theorem IsSWBisimulation.comp /-- Weak bisimilarity is transitive. -/ theorem WeakBisimilarity.trans [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} - (h1 : s1 ≈[lts₁,lts₂] s2) (h2 : s2 ≈[lts₂,lts₃] s3) : s1 ≈[lts₁,lts₃] s3 := by + (h1 : s₁ ≈[lts₁,lts₂] s₂) (h2 : s₂ ≈[lts₂,lts₃] s₃) : s₁ ≈[lts₁,lts₃] s₃ := by obtain ⟨r1, hr1, hr1b⟩ := h1 obtain ⟨r2, hr2, hr2b⟩ := h2 exists Relation.Comp r1 r2 constructor case left => - exists s2 + exists s₂ case right => apply IsWeakBisimulation.comp hr1b hr2b diff --git a/Cslib/Foundations/Semantics/LTS/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean index f9e74f067..f39cf449f 100644 --- a/Cslib/Foundations/Semantics/LTS/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -12,8 +12,8 @@ public import Cslib.Foundations.Semantics.LTS.Basic /-! # IsSimulation and Similarity -A simulation is a binary relation on the states of two `LTS`s: if two states `s1` and `s2` are -related by a simulation, then `s2` can mimic all transitions of `s1` in their respective LTSs. +A simulation is a binary relation on the states of two `LTS`s: if two states `s₁` and `s2` are +related by a simulation, then `s2` can mimic all transitions of `s₁` in their respective LTSs. Furthermore, the derivatives reaches through these transitions remain related by the simulation. Similarity is the largest simulation: given an `LTS`, it relates any two states that are related @@ -33,8 +33,8 @@ any two states similar to each other. ## Notations -- `s1 ≤[lts₁, lts₂] s2`: the states `s1` and `s2` are similar under `lts₁` and `lts₂`. -- `s1 ≤≥[lts₁, lts₂] s2`: the states `s1` and `s2` are simulation equivalent under `lts₁` and +- `s₁ ≤[lts₁, lts₂] s₂`: the states `s₁` and `s2` are similar under `lts₁` and `lts₂`. +- `s₁ ≤≥[lts₁, lts₂] s2`: the states `s₁` and `s2` are simulation equivalent under `lts₁` and `lts₂`. ## Main statements @@ -54,15 +54,15 @@ any transition originating from the first state is mimicked by a transition from and the reached derivatives are themselves related. -/ def IsSimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop := - ∀ s1 s2, r s1 s2 → ∀ μ s1', lts₁.Tr s1 μ s1' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s1' s2' + ∀ s₁ s2, r s₁ s2 → ∀ μ s₁', lts₁.Tr s₁ μ s₁' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s₁' s2' /-- A homogeneous simulation is a simulation where the underlying LTSs are the same. -/ abbrev IsHomSimulation (lts : LTS State Label) := IsSimulation lts lts /-- Two states are similar if they are related by some simulation. -/ def Similarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := - fun s1 s2 => - ∃ r : State₁ → State₂ → Prop, r s1 s2 ∧ IsSimulation lts₁ lts₂ r + fun s₁ s2 => + ∃ r : State₁ → State₂ → Prop, r s₁ s2 ∧ IsSimulation lts₁ lts₂ r /-- Notation for similarity. @@ -90,22 +90,22 @@ theorem IsSimulation.comp (h1 : IsSimulation lts₁ lts₂ r1) (h2 : IsSimulation lts₂ lts₃ r2) : IsSimulation lts₁ lts₃ (Relation.Comp r1 r2) := by simp_all only [IsSimulation] - intro s1 s2 hrc μ s1' htr + intro s₁ s2 hrc μ s₁' htr rcases hrc with ⟨sb, hr1, hr2⟩ - specialize h1 s1 sb hr1 μ + specialize h1 s₁ sb hr1 μ specialize h2 sb s2 hr2 μ - have h1' := h1 s1' htr - obtain ⟨s1'', h1'tr, h1'⟩ := h1' - have h2' := h2 s1'' h1'tr + 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 s1'' + · exists s₁'' /-- Similarity is transitive. -/ -theorem Similarity.trans (h1 : s1 ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,lts₃] s3) : - s1 ≤[lts₁,lts₃] s3 := by +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 @@ -115,12 +115,12 @@ theorem Similarity.trans (h1 : s1 ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,lts case right => apply IsSimulation.comp r1 r2 hr1s hr2s -/-- Simulation equivalence relates all states `s1` and `s2` such that `s1 ≤[lts₁ lts₂] s2` and -`s2 ≤[lts₂ lts₁] s1`. -/ +/-- Simulation equivalence relates all states `s₁` and `s2` such that `s₁ ≤[lts₁ lts₂] s2` and +`s2 ≤[lts₂ lts₁] s₁`. -/ def SimulationEquiv (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop := - fun s1 s2 => - s1 ≤[lts₁, lts₂] s2 ∧ s2 ≤[lts₂, lts₁] s1 + fun s₁ s2 => + s₁ ≤[lts₁, lts₂] s2 ∧ s2 ≤[lts₂, lts₁] s₁ /-- Notation for simulation equivalence. @@ -138,12 +138,12 @@ theorem HomSimulationEquiv.refl (s : State) : s ≤≥[lts] s := by grind [SimulationEquiv, HomSimilarity.refl] /-- Simulation equivalence is symmetric. -/ -theorem SimulationEquiv.symm {s1 s2 : State} (h : s1 ≤≥[lts₁,lts₂] s2) : s2 ≤≥[lts₂, lts₁] s1 := by +theorem SimulationEquiv.symm {s₁ s2 : State} (h : s₁ ≤≥[lts₁,lts₂] s2) : s2 ≤≥[lts₂, lts₁] s₁ := by grind [SimulationEquiv] /-- Simulation equivalence is transitive. -/ -theorem SimulationEquiv.trans (h1 : s1 ≤≥[lts₁,lts₂] s2) (h2 : s2 ≤≥[lts₂,lts₃] s3) : - s1 ≤≥[lts₁,lts₃] s3 := by +theorem SimulationEquiv.trans (h1 : s₁ ≤≥[lts₁,lts₂] s2) (h2 : s2 ≤≥[lts₂,lts₃] s₃) : + s₁ ≤≥[lts₁,lts₃] s₃ := by grind [SimulationEquiv, Similarity.trans] /-- Homogeneous simulation equivalence is an equivalence relation. -/ diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index d12398dc2..913372a66 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -19,11 +19,11 @@ Definitions and results on trace equivalence for `LTS`s. ## Main definitions - `LTS.traces`: the set of traces of a state. -- `TraceEq s1 s2`: `s1` and `s2` are trace equivalent, i.e., they have the same sets of traces. +- `TraceEq s₁ s₂`: `s₁` and `s₂` are trace equivalent, i.e., they have the same sets of traces. ## Notations -- `s1 ~tr[lts] s2`: the states `s1` and `s2` are trace equivalent in `lts`. +- `s₁ ~tr[lts] s₂`: the states `s₁` and `s₂` are trace equivalent in `lts`. ## Main statements @@ -44,8 +44,8 @@ theorem traces_in {lts : LTS State Label} (h : lts.MTr s μs s') : μs ∈ lts.t /-- Two states are trace equivalent if they have the same set of traces. -/ def TraceEq (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) - (s1 : State₁) (s2 : State₂) := - lts₁.traces s1 = lts₂.traces s2 + (s₁ : State₁) (s₂ : State₂) := + lts₁.traces s₁ = lts₂.traces s₂ /-- Notation for trace equivalence. @@ -66,14 +66,14 @@ theorem HomTraceEq.refl (s : State) : s ~tr[lts] s := by simp only [TraceEq] /-- Trace equivalence is symmetric. -/ -theorem TraceEq.symm (h : s1 ~tr[lts₁,lts₂] s2) : s2 ~tr[lts₂,lts₁] s1 := by +theorem TraceEq.symm (h : s₁ ~tr[lts₁,lts₂] s₂) : s₂ ~tr[lts₂,lts₁] s₁ := by simp only [TraceEq] at h simp only [TraceEq] rw [h] /-- Trace equivalence is transitive. -/ -theorem TraceEq.trans (h1 : s1 ~tr[lts₁,lts₂] s2) (h2 : s2 ~tr[lts₂,lts₃] s3) : - s1 ~tr[lts₁,lts₃] s3 := by +theorem TraceEq.trans (h1 : s₁ ~tr[lts₁,lts₂] s₂) (h2 : s₂ ~tr[lts₂,lts₃] s₃) : + s₁ ~tr[lts₁,lts₃] s₃ := by simp only [TraceEq] at * rw [h1, h2] @@ -91,12 +91,12 @@ instance : Trans (TraceEq lts₁ lts₂) (TraceEq lts₂ lts₃) (TraceEq lts₁ theorem TraceEq.deterministic_isSimulation {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] : IsSimulation lts₁ lts₂ (TraceEq lts₁ lts₂) := by - intro s1 s2 h μ s1' htr1 + intro s₁ s₂ h μ s₁' htr1 have hmtr1 := MTr.single lts₁ htr1 have hin := traces_in hmtr1 rw [h] at hin - obtain ⟨s2', hmtr2⟩ := hin - exists s2' + obtain ⟨s₂', hmtr2⟩ := hin + exists s₂' constructor · apply MTr.single_invert lts₂ _ _ _ hmtr2 · simp only [TraceEq, traces] @@ -106,31 +106,31 @@ theorem TraceEq.deterministic_isSimulation {lts₁ : LTS State₁ Label} {lts₂ constructor case mp => intro hmtr1' - obtain ⟨s1'', hmtr1'⟩ := hmtr1' + obtain ⟨s₁'', hmtr1'⟩ := hmtr1' have hmtr1comp := MTr.comp lts₁ hmtr1 hmtr1' have hin := traces_in hmtr1comp rw [h] at hin obtain ⟨s', hmtr2'⟩ := hin cases hmtr2' - case stepL s2'' htr2 hmtr2' => + case stepL s₂'' htr2 hmtr2' => exists s' have htr2' := MTr.single_invert lts₂ _ _ _ hmtr2 - have hdets2 := hdet₂.deterministic s2 μ s2' s2'' htr2' htr2 - rw [hdets2] + have hdets₂ := hdet₂.deterministic s₂ μ s₂' s₂'' htr2' htr2 + rw [hdets₂] exact hmtr2' case mpr => intro hmtr2' - obtain ⟨s2'', hmtr2'⟩ := hmtr2' + obtain ⟨s₂'', hmtr2'⟩ := hmtr2' have hmtr2comp := MTr.comp lts₂ hmtr2 hmtr2' have hin := traces_in hmtr2comp rw [← h] at hin obtain ⟨s', hmtr1'⟩ := hin cases hmtr1' - case stepL s1'' htr1 hmtr1' => + case stepL s₁'' htr1 hmtr1' => exists s' have htr1' := MTr.single_invert lts₁ _ _ _ hmtr1 - have hdets1 := hdet₁.deterministic s1 μ s1' s1'' htr1' htr1 - rw [hdets1] + have hdets₁ := hdet₁.deterministic s₁ μ s₁' s₁'' htr1' htr1 + rw [hdets₁] exact hmtr1' end Cslib.LTS From eeeaf26ef33bdd41183c57cc66d55365af81453d Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 13:04:00 +0200 Subject: [PATCH 3/8] fix names --- .../Semantics/LTS/Bisimulation.lean | 36 +++++++++++-------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index cc1b6949f..554edd18a 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -164,7 +164,7 @@ instance : IsEquiv State (HomBisimilarity lts) where /-- The union of two bisimulations is a bisimulation. -/ @[scoped grind .] -theorem Bisimulation.union (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisimulation lts₁ lts₂ s) : +theorem IsBisimulation.sup (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisimulation lts₁ lts₂ s) : IsBisimulation lts₁ lts₂ (r ⊔ s) := by intro s₁ s₂ hrs μ cases hrs @@ -233,7 +233,7 @@ section Order /-! ## Order properties -/ instance : Max {r // IsBisimulation lts₁ lts₂ r} where - max r s := ⟨r.1 ⊔ s.1, Bisimulation.union r.2 s.2⟩ + max r s := ⟨r.1 ⊔ s.1, IsBisimulation.sup r.2 s.2⟩ /-- Bisimulations equipped with union form a join-semilattice. -/ instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where @@ -262,21 +262,27 @@ instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where /-- The empty (heterogeneous) relation is a bisimulation. -/ @[scoped grind .] -theorem Bisimulation.emptyHRelation_bisimulation : IsBisimulation lts₁ lts₂ emptyHRelation := by +theorem IsBisimulation.bot : IsBisimulation lts₁ lts₂ emptyHRelation := by intro s₁ s₂ hr cases hr +instance : Bot {r // IsBisimulation lts₁ lts₂ r} := + ⟨emptyHRelation, IsBisimulation.bot⟩ + +instance : Top {r // IsBisimulation lts₁ lts₂ r} := + ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ + /-- In the inclusion order on bisimulations: - The empty relation is the bottom element. - Bisimilarity is the top element. -/ instance : BoundedOrder {r // IsBisimulation lts₁ lts₂ r} where - top := ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ - bot := ⟨emptyHRelation, Bisimulation.emptyHRelation_bisimulation⟩ + top := ⊤ + bot := ⊥ le_top r := by intro s₁ s₂ - simp only [LE.le] + simp only [LE.le, Top.top] grind bot_le r := by intro s₁ s₂ @@ -435,7 +441,7 @@ private inductive BisimMotTr : ℕ → Char → ℕ → Prop where /-- In general, trace equivalence is not a bisimulation (extra conditions are needed, see for example `Bisimulation.deterministic_trace_eq_is_bisim`). -/ -theorem Bisimulation.traceEq_not_bisim : +theorem IsBisimulation.traceEq_not_bisim : ∃ (State : Type) (Label : Type) (lts : LTS State Label), ¬(IsHomBisimulation lts (HomTraceEq lts)) := by exists ℕ @@ -706,7 +712,7 @@ theorem Bisimulation.traceEq_not_bisim : theorem Bisimilarity.bisimilarity_neq_traceEq : ∃ (State : Type) (Label : Type) (lts : LTS State Label), HomBisimilarity lts ≠ HomTraceEq lts := by - obtain ⟨State, Label, lts, h⟩ := Bisimulation.traceEq_not_bisim + obtain ⟨State, Label, lts, h⟩ := IsBisimulation.traceEq_not_bisim exists State; exists Label; exists lts intro heq have hb := Bisimilarity.is_bisimulation (lts₁ := lts) (lts₂ := lts) @@ -715,7 +721,7 @@ theorem Bisimilarity.bisimilarity_neq_traceEq : contradiction /-- In any deterministic LTS, trace equivalence is a bisimulation. -/ -theorem Bisimulation.deterministic_traceEq_is_bisim +theorem IsBisimulation.deterministic_traceEq_isBisimulation {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [lts₁.Deterministic] [lts₂.Deterministic] : (IsBisimulation lts₁ lts₂ (TraceEq lts₁ lts₂)) := by @@ -745,7 +751,7 @@ theorem Bisimilarity.deterministic_traceEq_bisim {lts₁ : LTS State₁ Label} { case left => exact h case right => - apply Bisimulation.deterministic_traceEq_is_bisim + apply IsBisimulation.deterministic_traceEq_isBisimulation /-- In deterministic LTSs, bisimilarity and trace equivalence coincide. -/ theorem Bisimilarity.deterministic_bisim_eq_traceEq @@ -762,11 +768,11 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq /-! ## Relation to simulation -/ /-- Any bisimulation is also a simulation. -/ -theorem Bisimulation.isSimulation : IsBisimulation lts₁ lts₂ r → IsSimulation lts₁ lts₂ r := by +theorem IsBisimulation.isSimulation : IsBisimulation lts₁ lts₂ r → IsSimulation lts₁ lts₂ r := by grind [IsSimulation] /-- A relation is a bisimulation iff both it and its inverse are simulations. -/ -theorem Bisimulation.simulation_iff : +theorem IsBisimulation.isSimulation_iff : IsBisimulation lts₁ lts₂ r ↔ (IsSimulation lts₁ lts₂ r ∧ IsSimulation lts₂ lts₁ (flip r)) := by have _ (s₁ s₂) : r s₁ s₂ → flip r s₂ s₁ := id grind [IsSimulation, flip] @@ -781,13 +787,13 @@ theorem HomBisimilarity.symm_simulation : · intro h have bisim : HomBisimilarity lts s₁ s₂ ∧ Std.Symm (HomBisimilarity lts) ∧ IsHomSimulation lts (HomBisimilarity lts) := by - grind [Std.Symm, Bisimilarity.symm, Bisimulation.isSimulation] + grind [Std.Symm, Bisimilarity.symm, IsBisimulation.isSimulation] grind · intro ⟨r, hr, hsymm, hsim⟩ have : r = (flip r) := by grind [flip, Std.Symm] have : IsHomBisimulation lts r := by - grind [Bisimulation.simulation_iff] + grind [IsBisimulation.isSimulation_iff] grind end Bisimulation @@ -1006,7 +1012,7 @@ theorem WeakBisimilarity.trans [HasTau Label] apply IsWeakBisimulation.comp hr1b hr2b /-- Homogeneous weak bisimilarity is an equivalence relation. -/ -theorem WeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : +theorem HomWeakBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : Equivalence (HomWeakBisimilarity lts) where refl := HomWeakBisimilarity.refl symm := WeakBisimilarity.symm From 6af4c570d2b383a3bb7eef7a929ee32e6f93b50a Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 13:45:17 +0200 Subject: [PATCH 4/8] fix hml test --- CslibTests/HML.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CslibTests/HML.lean b/CslibTests/HML.lean index 8f9d247b9..3e9346f2b 100644 --- a/CslibTests/HML.lean +++ b/CslibTests/HML.lean @@ -13,7 +13,7 @@ open Cslib open CCS Logic.HML LTS example [∀ p μ, Finite ((CCS.lts (defs := defs)).image p μ)] : - TheoryEq (CCS.lts (defs := defs)) = Bisimilarity (CCS.lts (defs := defs)) := + TheoryEq (CCS.lts (defs := defs)) = HomBisimilarity (CCS.lts (defs := defs)) := theoryEq_eq_bisimilarity .. end CslibTests From f3c9e62b432103cf65d9443ba7d8c432aac2f873 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 14:43:54 +0200 Subject: [PATCH 5/8] fix other tests --- CslibTests/Bisimulation.lean | 2 +- CslibTests/LTS.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CslibTests/Bisimulation.lean b/CslibTests/Bisimulation.lean index c33f2318c..4468a436a 100644 --- a/CslibTests/Bisimulation.lean +++ b/CslibTests/Bisimulation.lean @@ -8,7 +8,7 @@ import Cslib.Foundations.Semantics.LTS.Bisimulation namespace CslibTests -open Cslib +open Cslib LTS /- An LTS with two bisimilar states. -/ private inductive tr1 : ℕ → Char → ℕ → Prop where diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean index 88adf7ba7..34f3c3db9 100644 --- a/CslibTests/LTS.lean +++ b/CslibTests/LTS.lean @@ -12,7 +12,7 @@ import Cslib.Foundations.Semantics.LTS.Notation namespace CslibTests -open Cslib +open Cslib LTS -- A simple LTS on natural numbers From 74b61fa7f86b754cb20db5d9de4111cbb58714ac Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 14:52:30 +0200 Subject: [PATCH 6/8] fix namespace issue --- Cslib/Foundations/Data/Relation.lean | 4 ++-- Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index d984e4a4c..8d657c456 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -31,11 +31,11 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou -/ +namespace Relation + /-- The empty (heterogeneous) relation, which always returns `False`. -/ def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False -namespace Relation - attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := by diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 554edd18a..f048e1974 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -262,12 +262,12 @@ instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where /-- The empty (heterogeneous) relation is a bisimulation. -/ @[scoped grind .] -theorem IsBisimulation.bot : IsBisimulation lts₁ lts₂ emptyHRelation := by +theorem IsBisimulation.bot : IsBisimulation lts₁ lts₂ Relation.emptyHRelation := by intro s₁ s₂ hr cases hr instance : Bot {r // IsBisimulation lts₁ lts₂ r} := - ⟨emptyHRelation, IsBisimulation.bot⟩ + ⟨Relation.emptyHRelation, IsBisimulation.bot⟩ instance : Top {r // IsBisimulation lts₁ lts₂ r} := ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ From a13e611f438b2ad4b0567d6b28f1875e5914db31 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 18:09:49 +0200 Subject: [PATCH 7/8] unused args escape --- Cslib/Foundations/Data/Relation.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 8d657c456..0e3f65f6f 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -33,6 +33,7 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou namespace Relation +set_option linter.unusedVariables false in /-- The empty (heterogeneous) relation, which always returns `False`. -/ def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False From 5f26b99e60dfff9769746b624a0af8ef187d10a2 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Sun, 29 Mar 2026 18:58:07 +0200 Subject: [PATCH 8/8] fix unused args incantation --- Cslib/Foundations/Data/Relation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 0e3f65f6f..22a3d6787 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -33,8 +33,8 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou namespace Relation -set_option linter.unusedVariables false in /-- The empty (heterogeneous) relation, which always returns `False`. -/ +@[nolint unusedArguments] def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel