feat(CCS): Milner's Vending Machine

.github/copilot-instructions.md → AGENTS.md

@@ -1,4 +1,4 @@
-# Copilot Instructions for CSLib
+# Project Instructions
 
 ## Repository Overview
 
@@ -18,20 +18,20 @@
 | Command | Purpose | When to Use |
 |---------|---------|-------------|
 | `lake build` | Build the library | After any code change |
-| `lake build --wfail --iofail` | Build with CI strictness (fails on warnings) | **Always use before committing** |
+| `lake build --wfail --iofail` | Build with CI strictness (fails on warnings) | Before committing |
 | `lake test` | Run all tests (builds CslibTests + checks init imports) | After changes to verify correctness |
 | `lake lint` | Run environment linters (Batteries/Mathlib) | Before committing |
 | `lake exe lint-style` | Run text-based style linters | Before committing |
-| `lake exe mk_all --module --check` | Verify Cslib.lean imports all modules | After adding new files |
-| `lake exe mk_all --module` | Auto-update Cslib.lean imports | After adding new files |
+| `lake exe mk_all --check` | Verify Cslib.lean imports all modules | After adding new files |
+| `lake exe mk_all` | Auto-update Cslib.lean imports | After adding new files |
 
 ### Full CI Validation Sequence
 
 Run these commands **in order** to replicate CI checks locally:
 
 ```bash
 lake build --wfail --iofail
-lake exe mk_all --module --check
+lake exe mk_all --check
 lake test
 lake lint
 lake exe lint-style
@@ -64,8 +64,7 @@ lake exe lint-style
 │   └── Logics/          # Logic formalisations (e.g., Linear Logic, Hennessy-Milner Logic)
 ├── CslibTests/          # Test files
 ├── scripts/             # Build and maintenance scripts
-│   ├── noshake.json     # Import exceptions for shake tool
-│   └── nolints.json     # Lint exceptions
+│   └── noshake.json     # Import exceptions for shake tool
 └── .github/workflows/   # CI workflows
 ```
 
@@ -79,9 +78,9 @@ Every file in `Cslib/` must transitively import `Cslib/Init.lean`. This sets up
 - `Cslib.Init` itself
 
 ### 2. New Files Must Be Added to Cslib.lean
-When creating a new `.lean` file in `Cslib/`, add its import to `Cslib.lean`. Run:
+When creating a new `.lean` file in `Cslib/`, add its import to `Cslib.lean` by running:
 ```bash
-lake exe mk_all --module
+lake exe mk_all
 ```
 
 ### 3. PR Title Convention
@@ -103,15 +102,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: $LIST_OF_AUTHORS
 -/
 ```
+where $YEAR should be replaced with the current year, $AUTHOR_NAME with the name of the file creator, and $LIST_OF_AUTHORS with the list of authors (this is just the file creator if there are no additional authors).
+
+### 5. Always Read Local README.md Files
+
+Before working on any file or directory, **always read** all `README.md` files in all directories throughout the entire repository.
+
+These files contain essential context that must be understood before making changes.
 
 ## Code Style
 
 - Follow everything written in /CONTRIBUTING.md
-- Follow [Mathlib style guide](https://leanprover-community.github.io/contribute/style.html)
-- Use domain-specific variable names (e.g., `State` for state types, `μ` for transition labels)
-- Keep proofs readable; golfing is welcome if proofs remain clear
-- Use existing typeclasses for common concepts (transitions, reductions)
-- Use `module` keyword at the start of files with `public import` statements
+- Follow the [Mathlib code style](https://leanprover-community.github.io/contribute/style.html)
+- Use domain-specific variable names when dealing with APIs that have a clear intention (e.g., `State` for state types, `μ` for transition labels).
+- Keep proofs readable; golfing is welcome if proofs remain clear.
+- Use existing typeclasses for common concepts (`Congruence`, `Context`, etc.).
+- Use the `module` keyword at the start of files with `public import` statements.
 
 ## Linter Configuration
 
@@ -122,18 +128,11 @@ Linters are configured in `lakefile.toml`.
 ### Creating a New Module
 1. Create file in appropriate `Cslib/` subdirectory
 2. Add `import Cslib.Init` (or import a module that imports it)
-3. Run `lake exe mk_all --module`
+3. Run `lake exe mk_all`
 4. Run `lake build --wfail --iofail`
 5. Run `lake test` to verify init imports
 
 ### Adding Tests
 1. Create or modify a file in `CslibTests/`
-2. Add import to `CslibTests.lean` if new file
+2. Add import to `CslibTests.lean` if it is a new file
 3. Run `lake test`
-
-## Trust These Instructions
-
-Only search for additional information if:
-- A command fails with an unexpected error
-- You need details about a specific module's API
-- The instructions appear incomplete for your specific task

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

@@ -213,16 +213,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. -/
@@ -304,24 +313,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_neq_tr (hdet : lts.DeterministicStateLabel s μ)
+    (hneq : 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_tr_image_singleton (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 [=_ deterministicStateLabel_tr_image_singleton]
 
-/-- 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 (h : lts.DeterministicStateLabel s μ) :
+    Finite (lts.image s μ) := by
+  have hDet := deterministicStateLabel_image_char lts h
   cases hDet
   case inl hDet =>
     obtain ⟨s', hDet'⟩ := hDet
@@ -331,6 +345,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 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,62 @@ 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 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 +530,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]. -/