diff --git a/.github/copilot-instructions.md b/AGENTS.md similarity index 75% rename from .github/copilot-instructions.md rename to AGENTS.md index 991077d49..afa747661 100644 --- a/.github/copilot-instructions.md +++ b/AGENTS.md @@ -1,4 +1,4 @@ -# Copilot Instructions for CSLib +# Project Instructions ## Repository Overview @@ -18,12 +18,12 @@ | 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 @@ -31,7 +31,7 @@ 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 diff --git a/Cslib.lean b/Cslib.lean index db3afa862..e3df7bf0b 100644 --- a/Cslib.lean +++ b/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 diff --git a/Cslib/Algorithms/CCS/VendingMachine.lean b/Cslib/Algorithms/CCS/VendingMachine.lean new file mode 100644 index 000000000..08bb84251 --- /dev/null +++ b/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 diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index b1f864f89..4c77f9e1b 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/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_not_lto (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 diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index d49a11a04..74c96fa18 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -95,6 +95,38 @@ theorem IsBisimulation.follow_snd ∃ s₁', lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂' := (hb hr μ).2 _ 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 + grind [follow_snd hb hr] + +/-- 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₂' := by + obtain ⟨s₂', htr₂, hr₂⟩ := follow_fst hb hr htr + exists s₂' + grind + +/-- 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₂' := by + obtain ⟨s₁', htr₁, hr₁⟩ := follow_snd hb hr htr + exists s₁' + grind + /-! ## Relation to simulation -/ /-- Any bisimulation is also a simulation. -/ diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index d71ece490..1d0f7ff47 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/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 diff --git a/Cslib/Languages/CCS/Semantics.lean b/Cslib/Languages/CCS/Semantics.lean index 7a5670fde..d300ea0bd 100644 --- a/Cslib/Languages/CCS/Semantics.lean +++ b/Cslib/Languages/CCS/Semantics.lean @@ -20,14 +20,12 @@ public import Cslib.Languages.CCS.Basic @[expose] public section -namespace Cslib +namespace Cslib.CCS variable {Name : Type u} {Constant : Type v} - {defs : Constant → (CCS.Process Name Constant) → Prop} - -namespace CCS + {defs : Constant → Option (Process Name Constant)} open Process @@ -43,7 +41,7 @@ inductive Tr : Process Name Constant → Act Name → Process Name Constant → | choiceL : Tr p μ p' → Tr (choice p q) μ p' | choiceR : Tr q μ q' → Tr (choice p q) μ q' | res : μ ≠ Act.name a → μ ≠ Act.coname a → Tr p μ p' → Tr (res a p) μ (res a p') - | const : defs k p → Tr p μ p' → Tr (const k) μ p' + | const : defs k = some p → Tr p μ p' → Tr (const k) μ p' instance : HasTau (Act Name) where τ := Act.τ @@ -55,6 +53,59 @@ inductive Terminated : Process Name Constant → Prop where | choice : Terminated p → Terminated q → Terminated (choice p q) | res : Terminated p → Terminated (res a p) -end CCS +open LTS + +/-- A terminated process has no outgoing transitions. -/ +@[scoped grind ⇒] +theorem terminated_not_tr (h : Terminated p) : ¬(lts (defs := defs)).Tr p μ p' := by + intro htr + induction htr <;> grind [Terminated] + +/-- Inversion lemma for prefix transitions. -/ +@[scoped grind →] +theorem pre_tr (h : (lts (defs := defs)).Tr (pre μ p) μ' p') : μ = μ' ∧ p = p' := by + cases h + simp + +/-- Inversion lemma for constant transitions. -/ +@[scoped grind →] +theorem const_tr (h : (lts (defs := defs)).Tr (const k) μ p') : + ∃ p, defs k = some p ∧ (lts (defs := defs)).Tr p μ p' := by + cases h + case const p hdef htr => + exists p + +/-- Prefixes are deterministic. -/ +@[scoped grind .] +theorem pre_deterministicState : DeterministicState (lts (defs := defs)) (pre μ p) := by + grind + +/-- Constants are deterministic if their definition is deterministic. -/ +@[scoped grind .] +theorem const_deterministicStateLabel (hdef : defs k = some p) + (h : DeterministicStateLabel (lts (defs := defs)) p μ) : + DeterministicStateLabel (lts (defs := defs)) (const k) μ := by + intro p₁ p₂ h₁ h₂ + cases h₁ + cases h₂ + case const.const q₁ hdef₁ htr₁ q₂ hdef₂ htr₂ => + have hq₁ : q₁ = p := by grind only + have hq₂ : q₂ = p := by grind only + rw [hq₁] at htr₁ + rw [hq₂] at htr₂ + apply h p₁ p₂ htr₁ htr₂ + +/-- Restriction is deterministic if its subterm is deterministic. -/ +@[scoped grind .] +theorem res_deterministicStateLabel + (h : DeterministicStateLabel (lts (defs := defs)) p μ) : + DeterministicStateLabel (lts (defs := defs)) (res μ' p) μ := by + intro p₁ p₂ h₁ h₂ + cases h₁ + cases h₂ + case res.res q₁ h₁ h₂ htr₁ q₂ h₃ h₄ htr₂ => + have hq₁q₂ : q₁ = q₂ := by + apply h _ _ htr₁ htr₂ + rw [hq₁q₂] -end Cslib +end Cslib.CCS diff --git a/CslibTests.lean b/CslibTests.lean index ed3063209..87ab72a89 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -1,5 +1,6 @@ import CslibTests.Bisimulation import CslibTests.CCS +import CslibTests.CCS.VendingMachine import CslibTests.CLL import CslibTests.DFA import CslibTests.FreeMonad diff --git a/CslibTests/CCS.lean b/CslibTests/CCS.lean index af9837705..6478b842b 100644 --- a/CslibTests/CCS.lean +++ b/CslibTests/CCS.lean @@ -13,7 +13,7 @@ open Cslib open CCS Process @[lts ltsNat "ₙ"] -def TrNat := @CCS.Tr ℕ ℕ (fun _ _ => False) +def TrNat := @CCS.Tr ℕ ℕ (fun _ => none) def p : Process ℕ ℕ := (pre Act.τ (pre (Act.name 1) nil)) diff --git a/CslibTests/CCS/VendingMachine.lean b/CslibTests/CCS/VendingMachine.lean new file mode 100644 index 000000000..7771ec301 --- /dev/null +++ b/CslibTests/CCS/VendingMachine.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +import Cslib.Algorithms.CCS.VendingMachine + +namespace CslibTests + +open Cslib CCS Process Algorithms.CCS.VendingMachine + +/-- The deterministic vending machine can perform a coin action. -/ +example : ltsD.Tr vm Coin (choice (pre Tea (const .vm)) (pre Coffee (const .vm))) := + Tr.const rfl Tr.pre + +end CslibTests diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index deba30056..53e833189 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -33,8 +33,8 @@ open_scoped_all Cslib #grind_lint skip Cslib.FinFun.fromFun_eq #grind_lint skip Cslib.FinFun.fromFun_idem #grind_lint skip Cslib.FinFun.fromFun_inter -#grind_lint skip Cslib.LTS.deterministic_not_lto -#grind_lint skip Cslib.LTS.deterministic_tr_image_singleton +#grind_lint skip Cslib.LTS.deterministicStateLabel_not_lto +#grind_lint skip Cslib.LTS.deterministicStateLabel_tr_image_singleton #grind_lint skip Cslib.LTS.Execution.refl #grind_lint skip Cslib.LTS.mem_saturate_image_τ #grind_lint skip Cslib.ωSequence.drop_const