feat(CCS): Milner's Vending Machine

Cslib.lean

@@ -1,5 +1,6 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import Cslib.Algorithms.CCS.VendingMachine
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor

Cslib/Algorithms/CCS/VendingMachine.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Languages.CCS.Semantics
+public import Cslib.Foundations.Semantics.LTS.Bisimulation
+public import Cslib.Foundations.Semantics.LTS.TraceEq
+public import Mathlib.Tactic.FinCases
+
+/-! # Milner's Vending Machine
+
+This file formalises Milner's vending machine example for CCS.
+
+We formalise two versions:
+- A machine with a deterministic LTS: `coin.(tea.VM + coffee.VM)`.
+- A machine with a nondeterministic LTS: `coin.tea.VM + coin.coffee.VM`.
+
+We then prove the classical example that the two are not bisimilar.
+
+Future work on proving that the two vending machines are trace equivalent would be
+welcome.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.CCS.VendingMachine
+
+open Cslib.CCS Process Act
+open scoped LTS
+
+/-! Action names. -/
+
+/-- Insert a coin. -/
+abbrev Coin := name "coin"
+
+/-- Tea request. -/
+abbrev Tea := name "tea"
+
+/-- Coffee request. -/
+abbrev Coffee := name "coffee"
+
+/-- Constants. -/
+inductive Constant
+  | vm
+
+/-- The vending machine process. -/
+def vm : Process String Constant := const .vm
+
+/-! ## Deterministic vending machine -/
+
+/-- Constant definitions: vm = coin.(tea.VM + coffee.VM) -/
+@[local grind =]
+def vendingDefs : Constant → Option (Process String Constant)
+  | .vm => some <| pre Coin (choice (pre Tea (const .vm)) (pre Coffee (const .vm)))
+
+/-- The LTS of CCS for the deterministic vending machine. -/
+abbrev ltsD := CCS.lts (defs := vendingDefs)
+
+/-- VM can perform a coin action. -/
+example : ltsD.Tr vm Coin (choice (pre Tea (const .vm)) (pre Coffee (const .vm))) :=
+  Tr.const rfl Tr.pre
+
+/-! ## Nondeterministic vending machine -/
+
+/-- vm = coin.tea.VM + coin.coffee.VM -/
+def vendingDefsND : Constant → Option (Process String Constant)
+  | .vm => some <| (choice (pre Coin (pre Tea (const .vm))) (pre Coin (pre Coffee (const .vm))))
+
+/-- The LTS of CCS for the nondeterministic vending machine. -/
+abbrev ltsND := CCS.lts (defs := vendingDefsND)
+
+open LTS LTS.IsBisimulation LTS.Bisimilarity
+
+/-- The deterministic and nondeterministic vending machines are not bisimilar. -/
+theorem vm_ltsD_ltsND_not_bisim : ¬(vm ~[ltsD, ltsND] vm) := by
+  rintro ⟨r, hr, hbisim⟩
+  let p₁ := (choice (pre Tea (const Constant.vm)) (pre Coffee (const Constant.vm)))
+  let q₁ := (pre Tea (const Constant.vm))
+  have ltsD_vm_deterministic : ltsD.DeterministicStateLabel vm Coin := by
+    intro _ _ htr₁ htr₂
+    grind [const_tr htr₁, const_tr htr₂]
+  have h : r p₁ q₁ :=
+    match_deterministic
+      hbisim hr
+      ltsD_vm_deterministic
+      (.const rfl .pre)
+      (.const rfl (.choiceL .pre))
+  have hp₁q₁ : p₁ ~[ltsD, ltsND] q₁ := by grind
+  have hp₁coffee : ltsD.Tr p₁ Coffee (const Constant.vm) := .choiceR .pre
+  grind [hp₁q₁.follow_fst]
+
+end Cslib.Algorithms.CCS.VendingMachine

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -221,16 +221,25 @@ section Classes
 
 variable {State : Type u} {Label : Type v} (lts : LTS State Label)
 
-/-- An lts is deterministic if a state cannot reach different states with the same transition
-label. -/
+/-- A state `s` is deterministic for a label `μ` if `s` has at most one `μ`-derivative. -/
+@[scoped grind =]
+def DeterministicStateLabel (s : State) (μ : Label) : Prop :=
+  ∀ s₁ s₂, lts.Tr s μ s₁ → lts.Tr s μ s₂ → s₁ = s₂
+
+/-- A state `s` is deterministic if it is deterministic for all labels. -/
+@[scoped grind =]
+def DeterministicState (s : State) : Prop := ∀ μ, lts.DeterministicStateLabel s μ
+
+/-- An lts is deterministic if it is deterministic at every state. -/
 @[scoped grind]
 class Deterministic (lts : LTS State Label) where
-  deterministic (s1 : State) (μ : Label) (s2 s3 : State) :
-    lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3
+  /-- For all states and labels, there is at most one state reachable from a given state
+  with a given label. -/
+  deterministic : ∀ s, lts.DeterministicState s
 
-theorem Deterministic.eq_of_tr {lts : LTS State Label} [lts.Deterministic]
+theorem Deterministic.eq_of_tr {lts : LTS State Label} [h : lts.Deterministic]
     (htr : lts.Tr s1 μ s2) (htr' : lts.Tr s1 μ s2') : s2 = s2' :=
-  Deterministic.deterministic s1 μ s2 s2' htr htr'
+  h.deterministic s1 μ s2 s2' htr htr'
 
 /-- In a deterministic lts, multistep transitions with a given start state and trace reach a unique
 end state. -/
@@ -312,24 +321,29 @@ abbrev ImageFinite := ∀ s μ, Finite (lts.image s μ)
 
 /-- In a deterministic LTS, if a state has a `μ`-derivative, then it can have no other
 `μ`-derivative. -/
-@[scoped grind .]
-theorem deterministic_not_lto [h : lts.Deterministic] :
-  ∀ s μ s' s'', s' ≠ s'' → lts.Tr s μ s' → ¬lts.Tr s μ s'' := by grind
+@[scoped grind ⇒]
+theorem DeterministicStateLabel.not_tr_of_ne (hdet : lts.DeterministicStateLabel s μ)
+    (hne : s₁ ≠ s₂) (htr₁ : lts.Tr s μ s₁) : ¬lts.Tr s μ s₂ := by
+  grind
 
-@[scoped grind _=_]
-theorem deterministic_tr_image_singleton [lts.Deterministic] :
+@[scoped grind ⇒]
+theorem DeterministicStateLabel.image_singleton_iff_tr (h : lts.DeterministicStateLabel s μ) :
     lts.image s μ = {s'} ↔ lts.Tr s μ s' := by
   have := (lts.image s μ).eq_singleton_iff_unique_mem (a := s')
   grind
 
-/-- In a deterministic LTS, any image is either a singleton or the empty set. -/
-@[scoped grind .]
-theorem deterministic_image_char [lts.Deterministic] (s : State) (μ : Label) :
-    (∃ s', lts.image s μ = { s' }) ∨ (lts.image s μ = ∅) := by grind
+/-- If `s` is deterministic for `μ`, then the `μ`-image of `s` is either a singleton or the empty
+set. -/
+@[scoped grind →]
+theorem DeterministicStateLabel.image_char (h : lts.DeterministicStateLabel s μ) :
+    (∃ s', lts.image s μ = { s' }) ∨ (lts.image s μ = ∅) := by
+  grind [=_ image_singleton_iff_tr]
 
-/-- In a deterministic LTS, the image of any state-label combination is finite. -/
-instance [lts.Deterministic] (s : State) (μ : Label) : Finite (lts.image s μ) := by
-  have hDet := deterministic_image_char lts s μ
+/-- If `s` is deterministic at `μ`, then the `μ`-image of `s` is finite. -/
+@[scoped grind →]
+theorem DeterministicStateLabel.finite_image (h : lts.DeterministicStateLabel s μ) :
+    Finite (lts.image s μ) := by
+  have hDet := image_char lts h
   cases hDet
   case inl hDet =>
     obtain ⟨s', hDet'⟩ := hDet
@@ -339,6 +353,9 @@ instance [lts.Deterministic] (s : State) (μ : Label) : Finite (lts.image s μ)
     simp only [hDet]
     apply Set.finite_empty
 
+instance [h : lts.Deterministic] (s : State) (μ : Label) : Finite (lts.image s μ) :=
+  DeterministicStateLabel.finite_image lts (h.deterministic s μ)
+
 /-- Every deterministic LTS is also image-finite. -/
 instance deterministic_imageFinite [lts.Deterministic] : lts.ImageFinite := inferInstance
 

Cslib/Foundations/Semantics/LTS/Bisimulation.lean

@@ -83,30 +83,73 @@ 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 [IsBisimulation, IsSimulation]
 
+/-- The inverse of a bisimulation is a simulation. -/
+theorem IsBisimulation.flip_isSimulation :
+    IsBisimulation lts₁ lts₂ r → IsSimulation lts₂ lts₁ (flip r) := by
+  grind [IsBisimulation, IsSimulation, flip]
+
 /-- 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 [IsBisimulation, IsSimulation, flip]
 
+/-- 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₂' :=
+  IsSimulation.follow hb.isSimulation hr 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₂' :=
+  IsSimulation.follow hb.flip_isSimulation hr htr
+
+/-- If the unique transition of a state is matched by a related state in a bisimulation,
+then the derivatives are still in the bisimulation. -/
+theorem IsBisimulation.match_deterministic
+    (hb : IsBisimulation lts₁ lts₂ r)
+    (hr : r s₁ s₂)
+    (hdet : lts₁.DeterministicStateLabel s₁ μ)
+    (htr₁ : lts₁.Tr s₁ μ s₁')
+    (htr₂ : lts₂.Tr s₂ μ s₂') : r s₁' s₂' := by
+  have hr' : (flip r) s₂ s₁ := by grind [flip]
+  apply IsSimulation.match_deterministic hb.flip_isSimulation hr' hdet htr₂ htr₁
+
+/-- If the unique transition of a state is matched by a related state in the inverse of a
+bisimulation, then the derivatives are still in the bisimulation. -/
+theorem IsBisimulation.match_deterministic_flip
+    (hb : IsBisimulation lts₁ lts₂ r)
+    (hr : (flip r) s₂ s₁)
+    (hdet : lts₂.DeterministicStateLabel s₂ μ)
+    (htr₁ : lts₂.Tr s₂ μ s₂')
+    (htr₂ : lts₁.Tr s₁ μ s₁') : r s₁' s₂' := by
+  have hr' : r s₁ s₂ := by grind [flip]
+  apply IsSimulation.match_deterministic hb.isSimulation hr' hdet htr₂ htr₁
+
+/-- If a state is deterministic for `μ`, then any transition made by a related state in a
+bisimulation is matched by a unique transition (left variant). -/
+theorem IsBisimulation.follow_fst_deterministic (hb : IsBisimulation lts₁ lts₂ r) (hr : r s₁ s₂)
+    (hdet : lts₂.DeterministicStateLabel s₂ μ) (htr : lts₁.Tr s₁ μ s₁') :
+    ∃! s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂' :=
+  IsSimulation.follow_deterministic hb.isSimulation hr hdet htr
+
+/-- If a state is deterministic for `μ`, then any transition made by a related state in a
+bisimulation is matched by a unique transition (right variant). -/
+theorem IsBisimulation.follow_snd_deterministic
+    (hb : IsBisimulation lts₁ lts₂ r)
+    (hr : r s₁ s₂)
+    (hdet : lts₁.DeterministicStateLabel s₁ μ)
+    (htr : lts₂.Tr s₂ μ s₂') : ∃! s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂' :=
+  IsSimulation.follow_deterministic hb.flip_isSimulation hr hdet htr
+
 /-- A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same. -/
 abbrev IsHomBisimulation (lts : LTS State Label) := IsBisimulation lts lts
 
@@ -498,7 +541,7 @@ theorem IsSWBisimulation.iff_isSimulation [HasTau Label] :
       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 μ⟩
+  exact ⟨h hr μ, hflip hr μ⟩
 
 /-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`.
 This formalises lemma 4.2.10 in [Sangiorgi2011]. -/

Cslib/Foundations/Semantics/LTS/Simulation.lean

@@ -54,7 +54,7 @@ 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 :=
-  ∀ s₁ s2, r s₁ s2 → ∀ μ s₁', lts₁.Tr s₁ μ s₁' → ∃ s2', lts₂.Tr s2 μ s2' ∧ r s₁' s2'
+  ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ s₁', lts₁.Tr s₁ μ s₁' → ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂'
 
 /-- A homogeneous simulation is a simulation where the underlying LTSs are the same. -/
 abbrev IsHomSimulation (lts : LTS State Label) := IsSimulation lts lts
@@ -91,8 +91,8 @@ theorem IsSimulation.comp
     IsSimulation lts₁ lts₃ (Relation.Comp r1 r2) := by
   intro s₁ s2 hrc μ s₁' htr
   rcases hrc with ⟨sb, hr1, hr2⟩
-  obtain ⟨s₁'', h1'tr, h1'⟩ := h1 s₁ sb hr1 μ s₁' htr
-  obtain ⟨s2'', h2'tr, h2'⟩ := h2 sb s2 hr2 μ s₁'' h1'tr
+  obtain ⟨s₁'', h1'tr, h1'⟩ := h1 hr1 μ s₁' htr
+  obtain ⟨s2'', h2'tr, h2'⟩ := h2 hr2 μ s₁'' h1'tr
   use s2'', h2'tr, s₁'', h1', h2'
 
 /-- Similarity is transitive. -/
@@ -105,9 +105,9 @@ theorem Similarity.trans (h1 : s₁ ≤[lts₁,lts₂] s2) (h2 : s2 ≤[lts₂,l
 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
+  · obtain ⟨s₂', htr', hrel'⟩ := hr hrel μ s₁' htr
     use s₂', htr', Or.inl hrel'
-  · obtain ⟨s₂', htr', hrel'⟩ := hs s₁ s₂ hrel μ s₁' htr
+  · obtain ⟨s₂', htr', hrel'⟩ := hs hrel μ s₁' htr
     use s₂', htr', Or.inr hrel'
 
 theorem IsSimulation.sim_trace (hr : IsSimulation lts₁ lts₂ r) (hrel : r s₁ s₂) :
@@ -120,7 +120,7 @@ theorem IsSimulation.sim_trace (hr : IsSimulation lts₁ lts₂ r) (hrel : r s
   | 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₂'', 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'
 
@@ -169,6 +169,11 @@ instance :
     (SimulationEquiv lts₁ lts₃) where
   trans := SimulationEquiv.trans
 
+/-- Helper for following a transition by the first state in a pair of a simulation. -/
+theorem IsSimulation.follow
+    (hb : IsSimulation lts₁ lts₂ r) (hr : r s₁ s₂) (htr : lts₁.Tr s₁ μ s₁') :
+    ∃ s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂' := hb hr μ _ htr
+
 /-- 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₂)
@@ -178,7 +183,7 @@ lemma IsSimulation.follow_internal [HasTau Label] {lts₁ : LTS State₁ Label}
     use s₂, .refl
   case tail sb hrsb htrsb ih1 ih2 =>
     obtain ⟨sb2, htrsb2, hrb⟩ := ih2
-    have ⟨sb2', htrsb2', hrb'⟩ := h _ _ hrb HasTau.τ _ ih1
+    have ⟨sb2', htrsb2', hrb'⟩ := h hrb HasTau.τ _ ih1
     use sb2', htrsb2.trans (lts₂.sTr_τSTr_iff.mp htrsb2')
 
 /-- If the right-hand lts is saturated, a simulation lifts along saturating the left-hand lts. -/
@@ -191,7 +196,7 @@ theorem IsSimulation.isSimulation_saturate_left [HasTau Label] {lts₁ : LTS Sta
     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 ⟨sb2', hstr1b', hrb'⟩ := h hrb μ _ htr
     obtain ⟨s₁', hstr1', hrb2⟩ := IsSimulation.follow_internal h hrb' hstr2
     rw [←sTr_τSTr_iff] at hstr1' hstr1b
     use s₁', STr.comp hstr1b hstr1b' hstr1', hrb2
@@ -201,9 +206,25 @@ right. -/
 theorem 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)
+  obtain ⟨s₂', htr', hr'⟩ := h hr μ s₁' (h₁ _ _ _ htr)
   use s₂', h₂ _ _ _ htr', hr'
 
+/-- When a deterministic state matches a transition in a simulation, then the derivatives are still
+in the simulation. -/
+theorem IsSimulation.match_deterministic (hb : IsSimulation lts₁ lts₂ r) (hr : r s₁ s₂)
+    (hdet : lts₂.DeterministicStateLabel s₂ μ) (htr₁ : lts₁.Tr s₁ μ s₁') (htr₂ : lts₂.Tr s₂ μ s₂') :
+    r s₁' s₂' := by
+  grind [follow hb hr]
+
+/-- If a state is deterministic for `μ`, then any transition made by a related state in a
+simulation is matched by a unique transition. -/
+theorem IsSimulation.follow_deterministic (hb : IsSimulation lts₁ lts₂ r) (hr : r s₁ s₂)
+    (hdet : lts₂.DeterministicStateLabel s₂ μ) (htr : lts₁.Tr s₁ μ s₁') :
+    ∃! s₂', lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂' := by
+  obtain ⟨s₂', htr₂, hr₂⟩ := follow hb hr htr
+  exists s₂'
+  grind
+
 end Simulation
 
 end Cslib.LTS

Cslib/Languages/CCS/BehaviouralTheory.lean

@@ -30,7 +30,7 @@ section CCS.BehaviouralTheory
 
 open LTS
 
-variable {Name : Type u} {Constant : Type v} {defs : Constant → CCS.Process Name Constant → Prop}
+variable {Name : Type u} {Constant : Type v} {defs : Constant → Option (CCS.Process Name Constant)}
 
 namespace CCS