From 75181ad7517db1016cae68a28cd62b49abf783fc Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 13:46:36 +0200 Subject: [PATCH 1/9] start golfs --- .../Semantics/LTS/Bisimulation.lean | 166 ++++-------------- .../Foundations/Semantics/LTS/Simulation.lean | 22 +++ Cslib/Foundations/Semantics/LTS/TraceEq.lean | 4 + 3 files changed, 62 insertions(+), 130 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 21ffd67eb..c77645d71 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -68,6 +68,8 @@ equivalence coincide. namespace Cslib.LTS +variable {State₁ State₂ Label : Type*} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} + section Bisimulation /-- A relation is a bisimulation if, whenever it relates two states, @@ -82,6 +84,18 @@ def IsBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂') ) +/-! ## Relation to simulation -/ + +/-- Any bisimulation is also a simulation. -/ +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 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] + /-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/ abbrev IsHomBisimulation (lts : LTS State Label) := IsBisimulation lts lts @@ -130,7 +144,8 @@ theorem IsBisimulation.inv (h : IsBisimulation lts₁ lts₂ r) : open scoped IsBisimulation in /-- Bisimilarity is symmetric. -/ @[scoped grind →, symm] -theorem Bisimilarity.symm {s₁ s₂ : State} (h : s₁ ~[lts₁,lts₂] s₂) : s₂ ~[lts₂,lts₁] s₁ := by +theorem Bisimilarity.symm {lts₁ lts₂ : LTS State Label} {s₁ s₂ : State} + (h : s₁ ~[lts₁,lts₂] s₂) : s₂ ~[lts₂,lts₁] s₁ := by grind [flip] /-- The composition of two bisimulations is a bisimulation. -/ @@ -165,45 +180,10 @@ instance : IsEquiv State (HomBisimilarity lts) where /-- The union of two bisimulations is a bisimulation. -/ @[scoped grind .] 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 - case inl h => - constructor - · 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 s₂' htr - obtain ⟨s₁', htr', hr'⟩ := hrb.follow_snd h htr - exists s₁' - constructor - · assumption - · simp only [max, SemilatticeSup.sup] - left - exact hr' - case inr h => - constructor - · 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 s₂' htr - obtain ⟨s₁', htr', hs'⟩ := hsb.follow_snd h htr - exists s₁' - constructor - · assumption - · simp only [max, SemilatticeSup.sup] - right - exact hs' + IsBisimulation lts₁ lts₂ (r ⊔ s) := by + rw [IsBisimulation.isSimulation_iff] at hrb hsb ⊢ + rw [show flip (r ⊔ s) = flip r ⊔ flip s by ext; rfl] + exact ⟨hrb.1.sup hsb.1, hrb.2.sup hsb.2⟩ /-- Bisimilarity is a bisimulation. -/ @[scoped grind .] @@ -212,7 +192,7 @@ theorem Bisimilarity.is_bisimulation : IsBisimulation lts₁ lts₂ (Bisimilarit /-- Bisimilarity is the largest bisimulation. -/ @[scoped grind →] theorem Bisimilarity.largest_bisimulation (h : IsBisimulation lts₁ lts₂ r) : - Subrelation r (Bisimilarity lts₁ lts₂) := by + r ≤ (Bisimilarity lts₁ lts₂) := by intro s₁ s₂ hr exists r @@ -235,30 +215,15 @@ section Order instance : Max {r // IsBisimulation lts₁ lts₂ r} where max r s := ⟨r.1 ⊔ s.1, IsBisimulation.sup r.2 s.2⟩ +@[simp] lemma coe_sup (r s : {r // IsBisimulation lts₁ lts₂ r}) : + (↑(r ⊔ s) : State₁ → State₂ → Prop) = (r : State₁ → State₂ → Prop) ⊔ s := rfl + /-- Bisimulations equipped with union form a join-semilattice. -/ instance : SemilatticeSup {r // IsBisimulation lts₁ lts₂ r} where sup r s := r ⊔ s - le_sup_left r s := by - simp only [LE.le] - intro s₁ s₂ hr - simp only [max, SemilatticeSup.sup] - left - exact hr - le_sup_right r s := by - simp only [LE.le] - 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 s₁ s₂ h - cases h - case inl h => - apply h1 _ _ h - case inr h => - apply h2 _ _ h + le_sup_left r s := by simp [←Subtype.coe_le_coe] + le_sup_right r s := by simp [←Subtype.coe_le_coe] + sup_le r s t := by simp [←Subtype.coe_le_coe]; tauto /-- The empty (heterogeneous) relation is a bisimulation. -/ @[scoped grind .] @@ -280,15 +245,8 @@ instance : Top {r // IsBisimulation lts₁ lts₂ r} := instance : BoundedOrder {r // IsBisimulation lts₁ lts₂ r} where top := ⊤ bot := ⊥ - le_top r := by - intro s₁ s₂ - simp only [LE.le, Top.top] - grind - bot_le r := by - intro s₁ s₂ - simp only [LE.le] - intro hr - cases hr + le_top r := Bisimilarity.largest_bisimulation r.property + bot_le r := by simp [Bot.bot, LE.le] end Order @@ -335,13 +293,12 @@ theorem IsBisimulationUpTo.is_bisimulation (h : IsBisimulationUpTo lts₁ lts₂ obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₂b'r constructor constructor - · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b hs₁b'r) - hsmidb + · 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 hs₂br + apply Bisimilarity.largest_bisimulation hr2b _ _ hs₂br case right => intro s₂' htr2 obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := (hr2b hr2 μ).2 s₂' htr2 @@ -355,7 +312,7 @@ theorem IsBisimulationUpTo.is_bisimulation (h : IsBisimulationUpTo lts₁ lts₂ obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₁b'r constructor constructor - · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b _) hsmidb + · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b ..) hsmidb · exact hs₁br · exists smid2 constructor @@ -368,33 +325,8 @@ theorem IsBisimulationUpTo.is_bisimulation (h : IsBisimulationUpTo lts₁ lts₂ transitions. -/ theorem IsBisimulation.bisim_trace (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) : - ∀ μs s₁', lts₁.MTr s₁ μs s₁' → ∃ s₂', lts₂.MTr s₂ μs s₂' ∧ r s₁' s₂' := by - intro μs - induction μs generalizing s₁ s₂ - case nil => - intro s₁' hmtr1 - exists s₂ - cases hmtr1 - constructor - constructor - exact hr - case cons μ μs' ih => - intro s₁' hmtr1 - cases hmtr1 - case stepL s₁'' htr hmtr => - specialize hb hr μ - 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 - · exact htr2 - · exact hmtr2 - case right => - exact hr' + ∀ μs s₁', lts₁.MTr s₁ μs s₁' → ∃ s₂', lts₂.MTr s₂ μs s₂' ∧ r s₁' s₂' := + hb.isSimulation.sim_trace hr /-! ## Relation to trace equivalence -/ @@ -725,22 +657,8 @@ theorem IsBisimulation.deterministic_traceEq_isBisimulation {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [lts₁.Deterministic] [lts₂.Deterministic] : (IsBisimulation lts₁ lts₂ (TraceEq lts₁ lts₂)) := by - simp only [IsBisimulation] - intro s₁ s₂ hteq μ - constructor - case left => - apply TraceEq.deterministic_isSimulation s₁ s₂ hteq - case right => - intro s₂' htr - apply TraceEq.symm at hteq - have h := TraceEq.deterministic_isSimulation s₂ s₁ hteq μ s₂' htr - obtain ⟨s₁', h⟩ := h - exists s₁' - constructor - case left => - exact h.1 - case right => - apply h.2.symm + rw [IsBisimulation.isSimulation_iff, TraceEq.flip_eq] + exact ⟨TraceEq.deterministic_isSimulation, TraceEq.deterministic_isSimulation⟩ /-- In deterministic LTSs, trace equivalence implies bisimilarity. -/ theorem Bisimilarity.deterministic_traceEq_bisim {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} @@ -765,18 +683,6 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq case mpr => apply Bisimilarity.deterministic_traceEq_bisim -/-! ## Relation to simulation -/ - -/-- Any bisimulation is also a simulation. -/ -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 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] - set_option linter.tacticAnalysis.verifyGrindOnly false in /-- Homogeneous bisimilarity can also be characterized through symmetric simulations. -/ theorem HomBisimilarity.symm_simulation : diff --git a/Cslib/Foundations/Semantics/LTS/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean index cf401de04..4e642ebee 100644 --- a/Cslib/Foundations/Semantics/LTS/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -115,6 +115,28 @@ theorem Similarity.trans (h1 : s₁ ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,l case right => apply IsSimulation.comp r1 r2 hr1s hr2s +theorem IsSimulation.sup (hr : IsSimulation lts₁ lts₂ r) + (hs : IsSimulation lts₁ lts₂ s) : IsSimulation lts₁ lts₂ (r ⊔ s) := by + rintro s₁ s₂ (hrel | hrel) μ s₁' htr + · obtain ⟨s₂', htr', hrel'⟩ := hr s₁ s₂ hrel μ s₁' htr + use s₂', htr', Or.inl hrel' + · obtain ⟨s₂', htr', hrel'⟩ := hs s₁ s₂ hrel μ s₁' htr + use s₂', htr', Or.inr hrel' + +theorem IsSimulation.sim_trace (hr : IsSimulation lts₁ lts₂ r) (hrel : r s₁ s₂) : + ∀ μs s₁', lts₁.MTr s₁ μs s₁' → ∃ s₂', lts₂.MTr s₂ μs s₂' ∧ r s₁' s₂' := by + intro μs s₁' hmtr + induction μs generalizing s₁ s₂ with + | nil => + obtain rfl := hmtr.nil_eq + exact ⟨s₂, MTr.refl, hrel⟩ + | cons μ μs ih => + cases hmtr + case stepL s₁'' htr hmtr => + obtain ⟨s₂'', htr₂, hrel'⟩: ∃ s2', lts₂.Tr s₂ μ s2' ∧ r s₁'' s2' := hr _ _ hrel μ s₁'' htr + obtain ⟨s₂', hmtr₂, hrel'⟩ := ih hrel' hmtr + use s₂', hmtr₂.stepL htr₂, hrel' + /-- 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) : diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index 3e4dbebb4..6a5a6792b 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -71,6 +71,10 @@ theorem TraceEq.symm (h : s₁ ~tr[lts₁,lts₂] s₂) : s₂ ~tr[lts₂,lts₁ simp only [TraceEq] rw [h] +@[simp] theorem TraceEq.flip_eq : flip (TraceEq lts₁ lts₂) = TraceEq lts₂ lts₁ := by + ext s₁ s₂ + grind [flip, TraceEq.symm] + /-- Trace equivalence is transitive. -/ theorem TraceEq.trans (h1 : s₁ ~tr[lts₁,lts₂] s₂) (h2 : s₂ ~tr[lts₂,lts₃] s₃) : s₁ ~tr[lts₁,lts₃] s₃ := by From 3b0bca1b140a8ee3162514f51184e31c34db39ee Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 15:34:41 +0200 Subject: [PATCH 2/9] further golfs and simplifications --- .../Semantics/LTS/Bisimulation.lean | 109 +++++++----------- 1 file changed, 42 insertions(+), 67 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index c77645d71..788254df9 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -51,7 +51,7 @@ we prove to be sound and complete. - `LTS.IsBisimulation.inv`: the inverse of a bisimulation is a bisimulation. - `Bisimilarity.eqv`: bisimilarity is an equivalence relation (see `Equivalence`). - `Bisimilarity.isBisimulation`: bisimilarity is itself a bisimulation. -- `Bisimilarity.largest_bisimulation`: bisimilarity is the largest bisimulation. +- `Bisimilarity.le_bisimilarity_of_isBisimulation`: bisimilarity is the largest bisimulation. - `Bisimilarity.gfp`: the union of bisimilarity and any bisimulation is equal to bisimilarity. - `LTS.IsBisimulationUpTo.isBisimulation`: any bisimulation up to bisimilarity is a bisimulation. - `LTS.IsBisimulation.traceEq`: any bisimulation that relates two states implies that they are @@ -130,6 +130,14 @@ abbrev HomBisimilarity (lts : LTS State Label) := Bisimilarity lts lts /-- Notation for homogeneous bisimilarity. -/ scoped notation s:max " ~[" lts "] " s':max => HomBisimilarity lts s s' +/-- Helper for following a transition by the first state in a pair of a `Bisimilarity`. -/ +theorem Bisimilarity.follow_fst (hr : s₁ ~[lts₁,lts₂] s₂) (htr : lts₁.Tr s₁ μ s₁') : + ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ s₁' ~[lts₁,lts₂ ] s₂' := by grind + +/-- Helper for following a transition by the first state in a pair of a `Bisimilarity`. -/ +theorem Bisimilarity.follow_snd (hr : s₁ ~[lts₁,lts₂] s₂) (htr : lts₂.Tr s₂ μ s₂') : + ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ s₁' ~[lts₁,lts₂] s₂' := by grind + /-- Homogeneous bisimilarity is reflexive. -/ @[scoped grind ., refl] theorem HomBisimilarity.refl (s : State) : s ~[lts] s := by @@ -187,11 +195,12 @@ theorem IsBisimulation.sup (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisim /-- Bisimilarity is a bisimulation. -/ @[scoped grind .] -theorem Bisimilarity.is_bisimulation : IsBisimulation lts₁ lts₂ (Bisimilarity lts₁ lts₂) := by grind +theorem Bisimilarity.isBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : + IsBisimulation lts₁ lts₂ (Bisimilarity lts₁ lts₂) := by grind /-- Bisimilarity is the largest bisimulation. -/ @[scoped grind →] -theorem Bisimilarity.largest_bisimulation (h : IsBisimulation lts₁ lts₂ r) : +theorem IsBisimulation.le_bisimilarity (h : IsBisimulation lts₁ lts₂ r) : r ≤ (Bisimilarity lts₁ lts₂) := by intro s₁ s₂ hr exists r @@ -199,10 +208,7 @@ theorem Bisimilarity.largest_bisimulation (h : IsBisimulation lts₁ lts₂ 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 s₁ s₂ - simp only [max, SemilatticeSup.sup] - grind + (Bisimilarity lts₁ lts₂) ⊔ r = Bisimilarity lts₁ lts₂ := sup_eq_left.mpr h.le_bisimilarity /-- `calc` support for bisimilarity. -/ instance : Trans (Bisimilarity lts₁ lts₂) (Bisimilarity lts₂ lts₃) (Bisimilarity lts₁ lts₃) where @@ -235,7 +241,7 @@ instance : Bot {r // IsBisimulation lts₁ lts₂ r} := ⟨Relation.emptyHRelation, IsBisimulation.bot⟩ instance : Top {r // IsBisimulation lts₁ lts₂ r} := - ⟨Bisimilarity lts₁ lts₂, Bisimilarity.is_bisimulation⟩ + ⟨Bisimilarity lts₁ lts₂, Bisimilarity.isBisimulation ..⟩ /-- In the inclusion order on bisimulations: @@ -245,7 +251,7 @@ instance : Top {r // IsBisimulation lts₁ lts₂ r} := instance : BoundedOrder {r // IsBisimulation lts₁ lts₂ r} where top := ⊤ bot := ⊥ - le_top r := Bisimilarity.largest_bisimulation r.property + le_top r := r.property.le_bisimilarity bot_le r := by simp [Bot.bot, LE.le] end Order @@ -273,53 +279,29 @@ def IsBisimulationUpTo (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Labe /-- 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 +theorem IsBisimulationUpTo.isBisimulation (h : IsBisimulationUpTo lts₁ lts₂ r) : + IsBisimulation lts₁ lts₂ (UpToHomBisimilarity lts₁ lts₂ r) := by 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 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⟩ := hr1b.follow_fst 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 hs₂btr - case right => - obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₂b'r - constructor - constructor - · 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 _ _ hs₂br + obtain ⟨s₂', hs₂btr, hs₂br⟩ := hr2b.follow_fst hs₂b'tr + use s₂', hs₂btr + obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₂b'r + use smid1, hs₁b'r.trans hsmidb, smid2, hsmidr + exact hsmidrb.trans hs₂br case right => 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⟩ := hr2b.follow_snd 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 hs₁btr - case right => - obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₁b'r - constructor - constructor - · apply Bisimilarity.trans (Bisimilarity.largest_bisimulation hr1b ..) hsmidb - · exact hs₁br - · exists smid2 - constructor - · exact hsmidr - · apply Bisimilarity.trans hsmidrb - apply Bisimilarity.largest_bisimulation hr2b _ - exact hs₂b'r + obtain ⟨s₁', hs₁btr, hs₁br⟩ := hr1b.follow_snd hs₁b'tr + use s₁', hs₁btr + obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₁b'r + use smid1, hs₁br.trans hsmidb, smid2, hsmidr + exact hsmidrb.trans hs₂b'r /-- If two states are related by a bisimulation, they can mimic each other's multi-step transitions. -/ @@ -335,21 +317,18 @@ theorem IsBisimulation.bisim_trace theorem IsBisimulation.traceEq (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂) : s₁ ~tr[lts₁,lts₂] s₂ := by - funext μs - simp only [eq_iff_iff] + ext μs constructor case mp => intro h obtain ⟨s₁', h⟩ := h obtain ⟨s₂', hmtr⟩ := IsBisimulation.bisim_trace hb hr μs s₁' h - exists s₂' - exact hmtr.1 + use s₂', hmtr.1 case mpr => intro h obtain ⟨s₂', h⟩ := h obtain ⟨s₁', hmtr⟩ := IsBisimulation.bisim_trace hb.inv hr μs s₂' h - exists s₁' - exact hmtr.1 + use s₁', hmtr.1 /-- Bisimilarity is included in trace equivalence. -/ @[scoped grind .] @@ -645,9 +624,9 @@ theorem Bisimilarity.bisimilarity_neq_traceEq : ∃ (State : Type) (Label : Type) (lts : LTS State Label), HomBisimilarity lts ≠ HomTraceEq lts := by obtain ⟨State, Label, lts, h⟩ := IsBisimulation.traceEq_not_bisim - exists State; exists Label; exists lts + use State, Label, lts intro heq - have hb := Bisimilarity.is_bisimulation (lts₁ := lts) (lts₂ := lts) + have hb := Bisimilarity.isBisimulation lts lts simp only [HomBisimilarity] at heq rw [heq] at hb contradiction @@ -683,23 +662,19 @@ theorem Bisimilarity.deterministic_bisim_eq_traceEq case mpr => apply Bisimilarity.deterministic_traceEq_bisim -set_option linter.tacticAnalysis.verifyGrindOnly false in /-- Homogeneous bisimilarity can also be characterized through symmetric simulations. -/ theorem HomBisimilarity.symm_simulation : HomBisimilarity lts = fun s₁ s₂ => ∃ r, r s₁ s₂ ∧ Std.Symm r ∧ IsHomSimulation lts r := by - funext s₁ s₂ - apply Iff.eq - apply Iff.intro + ext s₁ s₂ + constructor · intro h - have bisim : HomBisimilarity lts s₁ s₂ ∧ Std.Symm (HomBisimilarity lts) - ∧ IsHomSimulation lts (HomBisimilarity lts) := by - grind [Std.Symm, Bisimilarity.symm, IsBisimulation.isSimulation] - grind - · intro ⟨r, hr, hsymm, hsim⟩ - have : r = (flip r) := by grind only [flip, Std.Symm] - have : IsHomBisimulation lts r := by grind [IsBisimulation.isSimulation_iff] - grind + use lts.HomBisimilarity, h + exact ⟨⟨fun _ _ => Bisimilarity.symm⟩, (Bisimilarity.isBisimulation lts lts).isSimulation⟩ + · intro ⟨r, hrel, ⟨hsymm⟩, hsim⟩ + use r, hrel + have : r = flip r := by ext; rw [flip]; grind + simpa [IsBisimulation.isSimulation_iff, ←this] end Bisimulation From bdbaffd25dd25e588538da7035f335affbc21770 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 15:39:21 +0200 Subject: [PATCH 3/9] fix docstring --- Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 788254df9..96e10c384 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -51,7 +51,7 @@ we prove to be sound and complete. - `LTS.IsBisimulation.inv`: the inverse of a bisimulation is a bisimulation. - `Bisimilarity.eqv`: bisimilarity is an equivalence relation (see `Equivalence`). - `Bisimilarity.isBisimulation`: bisimilarity is itself a bisimulation. -- `Bisimilarity.le_bisimilarity_of_isBisimulation`: bisimilarity is the largest bisimulation. +- `IsBisimulation.le_bisimilarity`: bisimilarity is the largest bisimulation. - `Bisimilarity.gfp`: the union of bisimilarity and any bisimulation is equal to bisimilarity. - `LTS.IsBisimulationUpTo.isBisimulation`: any bisimulation up to bisimilarity is a bisimulation. - `LTS.IsBisimulation.traceEq`: any bisimulation that relates two states implies that they are From f8d524aa362b7b9d35210e3acc21d4bcf4d96326 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 15:49:19 +0200 Subject: [PATCH 4/9] fix build --- Cslib/Languages/CCS/BehaviouralTheory.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 6e24dac12..9780f9347 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -262,7 +262,7 @@ theorem bisimilarity_congr_pre : case pre p' q' μ hbis => unfold lts constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind - case bisim => grind [Bisimilarity.largest_bisimulation] + case bisim => grind [IsBisimulation.le_bisimilarity] @[local grind] private inductive ResBisim : Process Name Constant → Process Name Constant → Prop where @@ -283,7 +283,7 @@ theorem bisimilarity_congr_res : case left => intro s1' htr cases htr with | res _ _ htr => - obtain ⟨q', _, bisim⟩ := Bisimilarity.is_bisimulation.follow_fst h htr + obtain ⟨q', _, bisim⟩ := h.follow_fst htr exists res a q' unfold lts at * #adaptation_note @@ -294,7 +294,7 @@ theorem bisimilarity_congr_res : case right => intro s2' htr cases htr with | res _ _ htr => - obtain ⟨p', _, bisim⟩ := Bisimilarity.is_bisimulation.follow_snd h htr + obtain ⟨p', _, bisim⟩ := h.follow_snd htr exists res a p' unfold lts at * #adaptation_note @@ -328,7 +328,7 @@ theorem bisimilarity_congr_choice : constructor · apply Tr.choiceL htr2 · constructor - apply Bisimilarity.largest_bisimulation hb hr2 + apply hb.le_bisimilarity _ _ hr2 case choiceR a b c htr => exists s1' constructor @@ -342,7 +342,7 @@ theorem bisimilarity_congr_choice : constructor · assumption constructor - apply Bisimilarity.largest_bisimulation hb hr2 + apply hb.le_bisimilarity _ _ hr2 case right => intro s2' htr cases r @@ -355,7 +355,7 @@ theorem bisimilarity_congr_choice : constructor · apply Tr.choiceL htr1 · constructor - apply Bisimilarity.largest_bisimulation hb hr1 + apply hb.le_bisimilarity _ _ hr1 case choiceR a b c htr => exists s2' constructor @@ -369,7 +369,7 @@ theorem bisimilarity_congr_choice : constructor · assumption · constructor - apply Bisimilarity.largest_bisimulation hb hr1 + apply hb.le_bisimilarity _ _ hr1 @[local grind] private inductive ParBisim : Process Name Constant → Process Name Constant → Prop where From e77618d332486815d4131a316b9898483bdbaee9 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 16:02:40 +0200 Subject: [PATCH 5/9] fix names in GrindLint --- CslibTests/GrindLint.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index 370e58db3..d04527c10 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -73,14 +73,14 @@ open_scoped_all Cslib /-- (changes from lean#13166) -/ #grind_lint skip Cslib.ωLanguage.map_id #grind_lint skip Cslib.LTS.Bisimilarity.gfp -#grind_lint skip Cslib.LTS.Bisimilarity.is_bisimulation -#grind_lint skip Cslib.LTS.Bisimilarity.largest_bisimulation +#grind_lint skip Cslib.LTS.Bisimilarity.isBisimulation +#grind_lint skip Cslib.LTS.IsBisimulation.le_bisimilarity #grind_lint skip Cslib.LTS.IsBisimulation.bot #grind_lint skip Cslib.LTS.IsBisimulation.comp #grind_lint skip Cslib.LTS.IsBisimulation.inv #grind_lint skip Cslib.LTS.IsBisimulation.sup #grind_lint skip Cslib.LTS.IsBisimulation.traceEq -#grind_lint skip Cslib.LTS.IsBisimulationUpTo.is_bisimulation +#grind_lint skip Cslib.LTS.IsBisimulationUpTo.isBisimulation #grind_lint skip Cslib.Logic.HML.theoryEq_isBisimulation #guard_msgs in From 3e74c080d3b4817b7f2c4da492fbaa52165e3580 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 16:13:58 +0200 Subject: [PATCH 6/9] remove grind annotations --- .../Semantics/LTS/Bisimulation.lean | 44 +++++++++---------- Cslib/Languages/CCS/BehaviouralTheory.lean | 4 +- Cslib/Logics/HML/Basic.lean | 2 +- 3 files changed, 24 insertions(+), 26 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 96e10c384..fe019e871 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -75,7 +75,6 @@ section Bisimulation /-- 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) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop := ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( @@ -84,33 +83,33 @@ def IsBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (∀ s₂', lts₂.Tr s₂ μ s₂' → ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂') ) +/-- 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 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 s₁ s₂) (htr : lts₂.Tr s₂ μ s₂') : + ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂' := + (hb hr μ).2 _ htr + /-! ## Relation to simulation -/ /-- Any bisimulation is also a simulation. -/ theorem IsBisimulation.isSimulation : IsBisimulation lts₁ lts₂ r → IsSimulation lts₁ lts₂ r := by - grind [IsSimulation] + grind [IsBisimulation, IsSimulation] /-- A relation is a bisimulation iff both it and its inverse are simulations. -/ 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] + grind [IsBisimulation, IsSimulation, flip] /-- 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 : 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 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 := @@ -132,22 +131,22 @@ scoped notation s:max " ~[" lts "] " s':max => HomBisimilarity lts s s' /-- Helper for following a transition by the first state in a pair of a `Bisimilarity`. -/ theorem Bisimilarity.follow_fst (hr : s₁ ~[lts₁,lts₂] s₂) (htr : lts₁.Tr s₁ μ s₁') : - ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ s₁' ~[lts₁,lts₂ ] s₂' := by grind + ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ s₁' ~[lts₁,lts₂ ] s₂' := by grind [IsBisimulation] /-- Helper for following a transition by the first state in a pair of a `Bisimilarity`. -/ theorem Bisimilarity.follow_snd (hr : s₁ ~[lts₁,lts₂] s₂) (htr : lts₂.Tr s₂ μ s₂') : - ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ s₁' ~[lts₁,lts₂] s₂' := by grind + ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ s₁' ~[lts₁,lts₂] s₂' := by grind [IsBisimulation] /-- Homogeneous bisimilarity is reflexive. -/ @[scoped grind ., refl] theorem HomBisimilarity.refl (s : State) : s ~[lts] s := by exists Eq - grind + grind [IsBisimulation] /-- The inverse of a bisimulation is a bisimulation. -/ @[scoped grind →] theorem IsBisimulation.inv (h : IsBisimulation lts₁ lts₂ r) : - IsBisimulation lts₂ lts₁ (flip r) := by grind [flip] + IsBisimulation lts₂ lts₁ (flip r) := by grind [IsBisimulation, flip] open scoped IsBisimulation in /-- Bisimilarity is symmetric. -/ @@ -160,7 +159,7 @@ theorem Bisimilarity.symm {lts₁ lts₂ : LTS State Label} {s₁ s₂ : State} @[scoped grind .] theorem IsBisimulation.comp (h1 : IsBisimulation lts₁ lts₂ r1) (h2 : IsBisimulation lts₂ lts₃ r2) : - IsBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by grind [Relation.Comp] + IsBisimulation lts₁ lts₃ (Relation.Comp r1 r2) := by grind [IsBisimulation, Relation.Comp] /-- Bisimilarity is transitive. -/ @[scoped grind →] @@ -170,7 +169,7 @@ theorem Bisimilarity.trans obtain ⟨r1, _, _⟩ := h1 obtain ⟨r2, _, _⟩ := h2 exists Relation.Comp r1 r2 - grind [Relation.Comp] + grind [IsBisimulation, Relation.Comp] /-- Homogeneous bisimilarity is an equivalence relation. -/ theorem HomBisimilarity.eqv : @@ -196,7 +195,7 @@ theorem IsBisimulation.sup (hrb : IsBisimulation lts₁ lts₂ r) (hsb : IsBisim /-- Bisimilarity is a bisimulation. -/ @[scoped grind .] theorem Bisimilarity.isBisimulation (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : - IsBisimulation lts₁ lts₂ (Bisimilarity lts₁ lts₂) := by grind + IsBisimulation lts₁ lts₂ (Bisimilarity lts₁ lts₂) := by grind [IsBisimulation] /-- Bisimilarity is the largest bisimulation. -/ @[scoped grind →] @@ -266,7 +265,6 @@ def UpToHomBisimilarity (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Lab /-- 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) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop := ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ( diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index 9780f9347..d71ece490 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -213,7 +213,7 @@ theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q cases htr with grind · grind [HomBisimilarity.refl, ChoiceComm] case bisim h => - grind [ChoiceComm] + grind [IsBisimulation, ChoiceComm] private inductive ChoiceAssoc : Process Name Constant → Process Name Constant → Prop where | assoc : ChoiceAssoc (choice p (choice q r)) (choice (choice p q) r) @@ -262,7 +262,7 @@ theorem bisimilarity_congr_pre : case pre p' q' μ hbis => unfold lts constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind - case bisim => grind [IsBisimulation.le_bisimilarity] + case bisim => grind [IsBisimulation, IsBisimulation.le_bisimilarity] @[local grind] private inductive ResBisim : Process Name Constant → Process Name Constant → Prop where diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean index f83709a78..de2efd0ca 100644 --- a/Cslib/Logics/HML/Basic.lean +++ b/Cslib/Logics/HML/Basic.lean @@ -242,7 +242,7 @@ lemma bisimulation_satisfies {lts : LTS State Label} Satisfies lts s2 a := by induction a generalizing s1 s2 with | diamond => cases hs with | diamond htr _ => grind [hrb.follow_fst hr htr] - | _ => grind + | _ => grind [IsBisimulation] lemma bisimulation_TheoryEq {lts : LTS State Label} {hrb : lts.IsHomBisimulation r} From 447c57ffd558aa74e7490d656a2b54f181f313c3 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 18:18:35 +0200 Subject: [PATCH 7/9] golf week bisimulation --- .../Semantics/LTS/Bisimulation.lean | 118 ++++-------------- Cslib/Foundations/Semantics/LTS/HasTau.lean | 3 + .../Foundations/Semantics/LTS/Simulation.lean | 37 +++++- 3 files changed, 63 insertions(+), 95 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index fe019e871..0dbc7875a 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi module public import Cslib.Foundations.Data.Relation -public import Cslib.Foundations.Semantics.LTS.HasTau public import Cslib.Foundations.Semantics.LTS.Simulation public import Cslib.Foundations.Semantics.LTS.TraceEq @@ -715,47 +714,22 @@ def IsSWBisimulation [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS (∀ 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 s₁ s₂) (hstr : lts₁.τSTr s₁ s₁') : - ∃ s₂', lts₂.τSTr s₂ s₂' ∧ r s₁' s₂' := by - induction hstr - case refl => - exists s₂ - 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 IsSWBisimulation.follow_internal_snd - [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} - (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 s₁ - 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' +lemma IsSWBisimulation.isSimulation [HasTau Label] (h : IsSWBisimulation lts₁ lts₂ r) : + IsSimulation lts₁ lts₂.saturate r := by + intro s₁ s₂ hr μ + exact (h hr μ).1 + +lemma IsSWBisimulation.isSimulation_flip [HasTau Label] (h : IsSWBisimulation lts₁ lts₂ r) : + IsSimulation lts₂ lts₁.saturate (flip r) := by + intro s₂ s₁ hr μ + exact (h hr μ).2 + +lemma IsSWBisimulation.iff_isSimulation [HasTau Label] : + IsSWBisimulation lts₁ lts₂ r ↔ + IsSimulation lts₁ lts₂.saturate r ∧ IsSimulation lts₂ lts₁.saturate (flip r) := by + refine ⟨fun h => ⟨h.isSimulation, h.isSimulation_flip⟩, ?_⟩ + intro ⟨h, hflip⟩ s₁ s₂ hr μ + exact ⟨h s₁ s₂ hr μ, hflip s₂ s₁ hr μ⟩ /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`. This formalises lemma 4.2.10 in [Sangiorgi2011]. -/ @@ -764,59 +738,15 @@ theorem isWeakBisimulation_iff_isSWBisimulation IsWeakBisimulation lts₁ lts₂ r ↔ IsSWBisimulation lts₁ lts₂ r := by apply Iff.intro case mp => - intro h s₁ s₂ hr μ - apply And.intro - case left => - intro s₁' htr - specialize h hr μ - have h' := h.1 s₁' (STr.single lts₁ htr) - obtain ⟨s₂', htr2, hr2⟩ := h' - exists s₂' - case right => - intro s₂' htr - specialize h hr μ - have h' := h.2 s₂' (STr.single lts₂ htr) - obtain ⟨s₁', htr1, hr1⟩ := h' - exists s₁' + intro h + rw [IsSWBisimulation.iff_isSimulation] + exact ⟨h.isSimulation.mono lts₁.tr_le_tr_saturate le_rfl, + h.inv.isSimulation.mono lts₂.tr_le_tr_saturate le_rfl⟩ case mpr => - intro h s₁ s₂ hr μ - apply And.intro - case left => - intro s₁' hstr - cases hstr - case refl => - exists s₂ - constructor; constructor - exact hr - case tr sb sb' hstr1 htr hstr2 => - rw [←sTr_τSTr] at hstr1 hstr2 - 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 ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_fst h hrb' hstr2 - rw [←sTr_τSTr] at hstr1' hstr1b - exists s₁' - constructor - · exact STr.comp lts₂ hstr1b hstr1b' hstr1' - · exact hrb2 - case right => - intro s₂' hstr - cases hstr - case refl => - exists s₁ - constructor; constructor - exact hr - case tr sb sb' hstr1 htr hstr2 => - rw [←sTr_τSTr] at hstr1 hstr2 - 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 ⟨s₁', hstr1', hrb2⟩ := IsSWBisimulation.follow_internal_snd h hrb' hstr2 - rw [←sTr_τSTr] at hstr1' hstr1b - exists s₁' - constructor - · exact STr.comp lts₁ hstr1b hstr1b' hstr1' - · exact hrb2 + intro h + rw [IsWeakBisimulation, IsBisimulation.isSimulation_iff] + exact ⟨h.isSimulation.isSimulation_saturate_left, + h.isSimulation_flip.isSimulation_saturate_left⟩ theorem IsWeakBisimulation.isSwBisimulation [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} diff --git a/Cslib/Foundations/Semantics/LTS/HasTau.lean b/Cslib/Foundations/Semantics/LTS/HasTau.lean index 9deb34d44..2b886a295 100644 --- a/Cslib/Foundations/Semantics/LTS/HasTau.lean +++ b/Cslib/Foundations/Semantics/LTS/HasTau.lean @@ -49,6 +49,9 @@ theorem STr.single [HasTau Label] (lts : LTS State Label) : intro h apply STr.tr .refl h .refl +lemma tr_le_tr_saturate [HasTau Label] (lts : LTS State Label) : lts.Tr ≤ lts.saturate.Tr := + fun _ _ _ => STr.single lts + /-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/ theorem sTr_τSTr [HasTau Label] (lts : LTS State Label) : lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by diff --git a/Cslib/Foundations/Semantics/LTS/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean index 4e642ebee..244c15b8f 100644 --- a/Cslib/Foundations/Semantics/LTS/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -6,7 +6,7 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.LTS.HasTau /-! # IsSimulation and Similarity @@ -182,6 +182,41 @@ instance : (SimulationEquiv lts₁ lts₃) where trans := SimulationEquiv.trans +/-- Utility theorem for following internal transitions along a saturated lts. -/ +lemma IsSimulation.follow_internal [HasTau Label] {lts₁ : LTS State₁ Label} + {lts₂ : LTS State₂ Label} (h : IsSimulation lts₁ lts₂.saturate r) (hr : r s₁ s₂) + (hstr : lts₁.τSTr s₁ s₁') : ∃ s₂', lts₂.τSTr s₂ s₂' ∧ r s₁' s₂' := by + induction hstr + case refl => + use s₂, .refl + case tail sb hrsb htrsb ih1 ih2 => + obtain ⟨sb2, htrsb2, hrb⟩ := ih2 + have ⟨sb2', htrsb2', hrb'⟩ := h _ _ hrb HasTau.τ _ ih1 + use sb2', htrsb2.trans (lts₂.sTr_τSTr.mp htrsb2') + +/-- If the right-hand lts is saturated, a simulation lifts along saturating the left-hand lts. -/ +theorem IsSimulation.isSimulation_saturate_left [HasTau Label] {lts₁ : LTS State₁ Label} + {lts₂ : LTS State₂ Label} (h : IsSimulation lts₁ lts₂.saturate r) : + IsSimulation lts₁.saturate lts₂.saturate r := by + intro s₁ s₂ hr μ s₁' h + cases h + case refl => + use s₂, .refl, hr + case tr sb sb' hstr1 htr hstr2 => + obtain ⟨sb1, hstr1b, hrb⟩ := IsSimulation.follow_internal h hr hstr1 + obtain ⟨sb2', hstr1b', hrb'⟩ := h _ _ hrb μ _ htr + obtain ⟨s₁', hstr1', hrb2⟩ := IsSimulation.follow_internal h hrb' hstr2 + rw [←sTr_τSTr] at hstr1' hstr1b + use s₁', STr.comp lts₂ hstr1b hstr1b' hstr1', hrb2 + +/-- Simulation is preserved by removing transitions on the left, and adding transitions on the +right. -/ +lemma IsSimulation.mono (h₁ : lts₁'.Tr ≤ lts₁.Tr) (h₂ : lts₂.Tr ≤ lts₂'.Tr) + (h : IsSimulation lts₁ lts₂ r) : IsSimulation lts₁' lts₂' r := by + intro s₁ s₂ hr μ s₁' htr + obtain ⟨s₂', htr', hr'⟩ := h s₁ s₂ hr μ s₁' (h₁ _ _ _ htr) + use s₂', h₂ _ _ _ htr', hr' + end Simulation end Cslib.LTS From 999df73d49caf543a88c8dd7fe33d8b7fe4213a5 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 19:38:10 +0200 Subject: [PATCH 8/9] golf IsBisimulation.traceEq_not_bisim --- .../Semantics/LTS/Bisimulation.lean | 294 +++--------------- 1 file changed, 37 insertions(+), 257 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 0dbc7875a..13897b0f7 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -352,269 +352,53 @@ example `Bisimulation.deterministic_trace_eq_is_bisim`). -/ theorem IsBisimulation.traceEq_not_bisim : ∃ (State : Type) (Label : Type) (lts : LTS State Label), ¬(IsHomBisimulation lts (HomTraceEq lts)) := by - exists ℕ - exists Char let lts := LTS.mk BisimMotTr - exists lts + exists ℕ, Char, lts intro h - -- specialize h 1 5 have htreq : (1 ~tr[lts] 5) := by - simp [TraceEq] have htraces₁ : lts.traces 1 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by - apply Set.ext_iff.2 - intro μs - apply Iff.intro + ext μs + constructor case mp => - intro h1 - obtain ⟨s', htr⟩ := h1 - cases htr - case refl => - simp - case stepL μ sb μs' htr hmtr => - cases htr - cases hmtr - case one2two.stepL μ sb μs' htr hmtr => - cases htr <;> cases hmtr <;> - simp only [↓Char.isValue, Set.mem_insert_iff, reduceCtorEq, List.cons.injEq, - List.cons_ne_self, and_false, Set.mem_singleton_iff, Char.reduceEq, and_true, - or_false, or_true] <;> - contradiction - simp + rintro ⟨_, (_ | ⟨⟨_⟩, (_ | ⟨(_ | _), (_ | ⟨⟨_⟩, _⟩)⟩)⟩)⟩ + all_goals simp case mpr => - intro h1 - cases h1 - case inl h1 => - simp only [h1] - exists 1 - constructor - case inr h1 => - cases h1 - case inl h1 => - simp only [h1] - exists 2 - apply MTr.single; constructor - case inr h1 => - cases h1 - case inl h1 => - simp only [h1] - exists 3 - constructor - · apply BisimMotTr.one2two - · apply MTr.single - apply BisimMotTr.two2three - case inr h1 => - cases h1 - exists 4 - constructor - · apply BisimMotTr.one2two - · apply MTr.single - apply BisimMotTr.two2four - have htraces₂ : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by - apply Set.ext_iff.2 - intro μs - apply Iff.intro + rintro (rfl | rfl | rfl | rfl) + · exact ⟨1, .refl⟩ + · exact ⟨2, MTr.single lts .one2two⟩ + · exact ⟨3, MTr.stepL .one2two <| MTr.single lts .two2three⟩ + · exact ⟨4, MTr.stepL .one2two <| MTr.single lts .two2four⟩ + have htraces₅ : lts.traces 5 = {[], ['a'], ['a', 'b'], ['a', 'c']} := by + ext μs + constructor case mp => - intro h1 - obtain ⟨s', htr⟩ := h1 - cases htr - case refl => - simp - case stepL μ sb μs' htr hmtr => - cases htr - case five2six => - cases hmtr - case refl => - simp - case stepL μ sb μs' htr hmtr => - cases htr - cases hmtr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - case five2eight => - cases hmtr - case refl => - simp - case stepL μ sb μs' htr hmtr => - cases htr - cases hmtr - case refl => right; right; simp - case stepL μ sb μs' htr hmtr => - cases htr + rintro ⟨_, (_ | ⟨(_ | _), (_ | ⟨⟨_⟩, (_ | ⟨⟨_⟩, _⟩)⟩)⟩)⟩ + all_goals simp case mpr => - intro h1 - cases h1 - case inl h1 => - simp only [h1] - exists 5 - constructor - case inr h1 => - cases h1 - case inl h1 => - simp only [h1] - exists 6 - apply MTr.single; constructor - case inr h1 => - cases h1 - case inl h1 => - simp only [h1] - exists 7 - constructor - · apply BisimMotTr.five2six - · apply MTr.single - apply BisimMotTr.six2seven - case inr h1 => - cases h1 - exists 9 - constructor - · apply BisimMotTr.five2eight - · apply MTr.single; - apply BisimMotTr.eight2nine - simp [htraces₁, htraces₂] - specialize h htreq - specialize h 'a' - obtain ⟨h1, h2⟩ := h - specialize h1 2 (by constructor) - obtain ⟨s₂', htr5, cih⟩ := h1 + rintro (rfl | rfl | rfl | rfl) + · exact ⟨5, .refl⟩ + · exact ⟨6, MTr.single lts .five2six⟩ + · exact ⟨7, MTr.stepL .five2six <| MTr.single lts .six2seven⟩ + · exact ⟨9, MTr.stepL .five2eight <| MTr.single lts .eight2nine⟩ + exact htraces₁.trans htraces₅.symm + obtain ⟨h1, h2⟩ := h htreq 'a' + obtain ⟨s₂', htr5, cih⟩ := h1 2 (by constructor) + have htraces₂ : {['b'], ['c']} ⊆ lts.traces 2 := by + intro μs h + rcases h with (rfl | rfl) + · exists 3; constructor; constructor; constructor + · exists 4; constructor; constructor; constructor cases htr5 case five2six => - simp [TraceEq] at cih - have htraces₂ : lts.traces 2 = {[], ['b'], ['c']} := by - apply Set.ext_iff.2 - intro μs - apply Iff.intro - case mp => - intro h - obtain ⟨s', htr⟩ := h - cases htr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - case two2three => - cases hmtr - case stepL μ sb μs' htr hmtr => cases htr - simp - case two2four => - cases hmtr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - case mpr => - intro h - cases h - case inl h => - exists 2 - simp [h] - constructor - case inr h => - cases h - case inl h => - exists 3; simp [h]; constructor; constructor; constructor - case inr h => - exists 4 - simp at h - simp [h] - constructor; constructor; constructor - have htraces6 : lts.traces 6 = {[], ['b']} := by - apply Set.ext_iff.2 - intro μs - apply Iff.intro - case mp => - intro h - obtain ⟨s', htr⟩ := h - cases htr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - cases hmtr - case stepL μ sb μs' htr hmtr => cases htr - simp - case mpr => - intro h - cases h - case inl h => - exists 6 - simp [h] - constructor - case inr h => - exists 7 - simp at h - simp [h] - constructor; constructor; constructor - grind + suffices ['c'] ∉ lts.traces 6 by grind [TraceEq] + intro ⟨_, h⟩ + cases h + case stepL h _ => cases h case five2eight => - simp only [TraceEq] at cih - have htraces₂ : lts.traces 2 = {[], ['b'], ['c']} := by - apply Set.ext_iff.2 - intro μs - apply Iff.intro - case mp => - intro h - obtain ⟨s', htr⟩ := h - cases htr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - case two2three => - cases hmtr - case stepL μ sb μs' htr hmtr => cases htr - simp - case two2four => - cases hmtr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - case mpr => - intro h - cases h - case inl h => - exists 2 - simp [h] - constructor - case inr h => - cases h - case inl h => - exists 3; simp [h]; constructor; constructor; constructor - case inr h => - exists 4 - simp at h - simp [h] - constructor; constructor; constructor - have htraces8 : lts.traces 8 = {[], ['c']} := by - apply Set.ext_iff.2 - intro μs - apply Iff.intro - case mp => - intro h - obtain ⟨s', htr⟩ := h - cases htr - case refl => simp - case stepL μ sb μs' htr hmtr => - cases htr - cases hmtr - case stepL μ sb μs' htr hmtr => cases htr - simp - case mpr => - intro h - cases h - case inl h => - exists 8 - simp [h] - constructor - case inr h => - exists 9 - simp at h - simp [h] - repeat constructor - rw [htraces₂, htraces8] at cih - apply Set.ext_iff.1 at cih - specialize cih ['b'] - obtain ⟨cih1, cih2⟩ := cih - have cih1h : ['b'] ∈ @insert - (List Char) (Set (List Char)) Set.instInsert [] {['b'], ['c']} := by - simp - specialize cih1 cih1h - simp at cih1 + suffices ['b'] ∉ lts.traces 8 by grind [TraceEq] + intro ⟨_, h⟩ + cases h + case stepL h _ => cases h /-- In general, bisimilarity and trace equivalence are distinct. -/ theorem Bisimilarity.bisimilarity_neq_traceEq : @@ -622,11 +406,7 @@ theorem Bisimilarity.bisimilarity_neq_traceEq : HomBisimilarity lts ≠ HomTraceEq lts := by obtain ⟨State, Label, lts, h⟩ := IsBisimulation.traceEq_not_bisim use State, Label, lts - intro heq - have hb := Bisimilarity.isBisimulation lts lts - simp only [HomBisimilarity] at heq - rw [heq] at hb - contradiction + grind [Bisimilarity.isBisimulation lts lts] /-- In any deterministic LTS, trace equivalence is a bisimulation. -/ theorem IsBisimulation.deterministic_traceEq_isBisimulation From aa789ea058ec8eb7b5e856f1770de9c74f06d035 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 3 Jun 2026 20:10:04 +0200 Subject: [PATCH 9/9] tidy up --- Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 13897b0f7..94175b8ee 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi +Authors: Fabrizio Montesi, Thomas Waring -/ module @@ -386,19 +386,17 @@ theorem IsBisimulation.traceEq_not_bisim : have htraces₂ : {['b'], ['c']} ⊆ lts.traces 2 := by intro μs h rcases h with (rfl | rfl) - · exists 3; constructor; constructor; constructor - · exists 4; constructor; constructor; constructor + · refine ⟨3, MTr.single lts .two2three⟩ + · refine ⟨4, MTr.single lts .two2four⟩ cases htr5 case five2six => suffices ['c'] ∉ lts.traces 6 by grind [TraceEq] - intro ⟨_, h⟩ + rintro ⟨_, (_ | h)⟩ cases h - case stepL h _ => cases h case five2eight => suffices ['b'] ∉ lts.traces 8 by grind [TraceEq] - intro ⟨_, h⟩ + rintro ⟨_, (_ | h)⟩ cases h - case stepL h _ => cases h /-- In general, bisimilarity and trace equivalence are distinct. -/ theorem Bisimilarity.bisimilarity_neq_traceEq :