From 338070435fc9eefb93e78634e21cf090aa859dd2 Mon Sep 17 00:00:00 2001 From: patchwright Date: Mon, 13 Jul 2026 01:23:20 +0200 Subject: [PATCH 01/12] feat(LTS/Spectrum): van Glabbeek spectrum as a Galois connection MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Organise behavioural equivalences as the fixed points of an antitone Galois connection (polarity) between test classes (⊆) and equivalences (refinement). The Galois-closed (testable) equivalences are exactly the image of 'induced'; they form a lattice, not a chain. CSLib's HomTraceEq is exhibited as a concrete closed element. New module Cslib.Foundations.Semantics.LTS.Spectrum (3 files): * Galois.lean — polarity, cl closure operator, induced_testable, spectrum_eq_closed_elements (Mathlib/Cslib.Init only). * TracePoint.lean — HomTraceEq_testable: trace equivalence is Galois-closed, via the trace-set observer test class. * Antichain.lean — exists_incomparable_closed: the closed-element lattice has an antichain (lattice, not chain). Builds clean, 0 sorry / 0 axiom. Additive to CSLib (does not redefine bisim/ sim/trace/HML). Does not require the Hennessy-Milner theorem (not yet in CSLib). --- Cslib.lean | 3 + .../Semantics/LTS/Spectrum/Antichain.lean | 91 ++++++++++++ .../Semantics/LTS/Spectrum/Galois.lean | 133 ++++++++++++++++++ .../Semantics/LTS/Spectrum/TracePoint.lean | 73 ++++++++++ 4 files changed, 300 insertions(+) create mode 100644 Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean create mode 100644 Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean create mode 100644 Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean diff --git a/Cslib.lean b/Cslib.lean index 43c374ae7..adcc92edd 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -98,6 +98,9 @@ public import Cslib.Foundations.Semantics.LTS.Notation public import Cslib.Foundations.Semantics.LTS.OmegaExecution public import Cslib.Foundations.Semantics.LTS.Relation public import Cslib.Foundations.Semantics.LTS.Simulation +public import Cslib.Foundations.Semantics.LTS.Spectrum.Antichain +public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois +public import Cslib.Foundations.Semantics.LTS.Spectrum.TracePoint public import Cslib.Foundations.Semantics.LTS.Termination public import Cslib.Foundations.Semantics.LTS.Total public import Cslib.Foundations.Semantics.LTS.TraceEq diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean new file mode 100644 index 000000000..73bc85854 --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 TODO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: TODO +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois + +/-! +# Spectrum antichain — the closed-element lattice is not a chain + +The closed-element lattice is NOT totally ordered by refinement: two +incomparable Galois-closed (testable) equivalences exist over a 4-state witness +space. Two test classes `T₁`, `T₂` (Ω = Bool) induce closed equivalences such +that neither refines the other: + - states a,b are `T₁`-equivalent but `T₂`-distinct; + - states a,c are `T₂`-equivalent but `T₁`-distinct. +Hence the closed-element lattice contains an antichain → it is a lattice, not a +chain (scale). This is the structural form of the "linear-time/branching-time +spectrum is a lattice, not a linear scale" claim. + +(The *named* van Glabbeek antichain — simulation vs failures equivalence — +requires failures semantics, not yet in CSLib; that named instance is separate +from the structural result here.) +-/ + +@[expose] public section + +namespace Cslib.LTS.Spectrum + +/-- 4-state witness space. -/ +inductive W where + | a | b | c | d + +open W + +/-- Test t₁: groups {a,b} (true) vs {c,d} (false). -/ +def t1 : W → Bool + | a | b => true + | c | d => false + +/-- Test t₂: groups {a,c} (true) vs {b,d} (false). -/ +def t2 : W → Bool + | a | c => true + | b | d => false + +/-- Test classes (singletons, written as comprehensions). -/ +def T1 : Set (W → Bool) := { f | f = t1 } +def T2 : Set (W → Bool) := { f | f = t2 } + +/-- a,b are `T₁`-equivalent but `T₂`-distinct. -/ +theorem T1_ab_not_T2_ab : induced Bool T1 a b ∧ ¬ induced Bool T2 a b := by + refine ⟨?_, ?_⟩ + · intro t ht + have ht : t = t1 := ht + subst ht + rfl + · intro h + have hh : t2 a = t2 b := h t2 rfl + simp only [t2] at hh + exact Bool.noConfusion hh + +/-- a,c are `T₂`-equivalent but `T₁`-distinct. -/ +theorem T2_ac_not_T1_ac : induced Bool T2 a c ∧ ¬ induced Bool T1 a c := by + refine ⟨?_, ?_⟩ + · intro t ht + have ht : t = t2 := ht + subst ht + rfl + · intro h + have hh : t1 a = t1 c := h t1 rfl + simp only [t1] at hh + exact Bool.noConfusion hh + +/-- **The closed-element lattice is not a chain.** There exist two incomparable + testable (Galois-closed) equivalences. -/ +theorem exists_incomparable_closed : + ∃ E₁ E₂ : W → W → Prop, + Testable Bool E₁ ∧ Testable Bool E₂ ∧ + ¬ (∀ p q, E₁ p q → E₂ p q) ∧ ¬ (∀ p q, E₂ p q → E₁ p q) := by + refine ⟨induced Bool T1, induced Bool T2, + induced_testable Bool T1, induced_testable Bool T2, ?_, ?_⟩ + · intro h + exact T1_ab_not_T2_ab.2 (h a b T1_ab_not_T2_ab.1) + · intro h + exact T2_ac_not_T1_ac.2 (h a c T2_ac_not_T1_ac.1) + +end Cslib.LTS.Spectrum diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean new file mode 100644 index 000000000..df7b1415d --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2026 TODO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: TODO +-/ + +module + +public import Cslib.Init + +/-! +# Van Glabbeek's spectrum as a Galois connection — the polarity framework + +Behavioural equivalences are organised as the fixed points of an antitone Galois +connection ("polarity") between sets of tests (ordered by ⊆) and equivalences +(ordered by refinement). The Galois-closed equivalences — the "testable" ones — +are exactly the image of `induced`; they form a lattice, not a chain +(see `Spectrum.Antichain`). + +This module is the Mathlib/`Cslib.Init`-only framework. A concrete named +spectrum point (CSLib's `HomTraceEq`) is shown Galois-closed in +`Spectrum.TracePoint`. + +The construction is parameterised by the pair `(Proc, Ω)`: `Proc` is the process +type and `Ω` the observation type (a test is `Proc → Ω`). `Ω` is carried +explicitly because the closure-operator theorems mention only `E` and cannot +recover `Ω` from it. + +## Main definitions + +* `induced Ω T`: the equivalence a test class `T` induces. +* `respects Ω E`: the tests that respect an equivalence `E`. +* `cl Ω`: the closure operator `induced Ω ∘ respects Ω`. +* `Testable Ω E`: the fixed-point predicate (`cl Ω E = E`). + +## Main statements + +* `polarity`: the antitone Galois connection. +* `induced_testable`: every induced equivalence is a fixed point of `cl`. +* `cl_extensive`, `cl_monotone`, `cl_idempotent`: `cl` is a closure operator. +* `spectrum_eq_closed_elements`: testable ↔ in the image of `induced`. +-/ + +@[expose] public section + +namespace Cslib.LTS.Spectrum + +variable {Proc : Type*} + +/-- The equivalence a test class induces: agreement on every test in `T`. + Antitone in `T` — more tests ⇒ finer (smaller) equivalence. -/ +def induced (Ω : Type*) (T : Set (Proc → Ω)) (p q : Proc) : Prop := + ∀ t ∈ T, t p = t q + +/-- The tests that respect an equivalence `E`: tests constant on every E-pair. + Antitone in `E` — coarser `E` ⇒ fewer respecting tests. -/ +def respects (Ω : Type*) (E : Proc → Proc → Prop) : Set (Proc → Ω) := + { t | ∀ p q, E p q → t p = t q } + +/-- **Polarity.** Antitone Galois connection between test classes (⊆) and + equivalences (refinement): `E` refines `induced Ω T` iff `T ⊆ respects Ω E`. -/ +theorem polarity (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → Prop) : + (∀ p q, E p q → induced Ω T p q) ↔ T ⊆ respects Ω E := by + constructor + · intro h t ht p q hpq + exact h p q hpq t ht + · intro h p q hpq t ht + exact h ht p q hpq + +/-- Every test in `T` respects the equivalence `T` induces (the image fact). -/ +theorem test_subset_respects_induced (Ω : Type*) (T : Set (Proc → Ω)) : + T ⊆ respects Ω (induced Ω T) := by + intro t ht + change ∀ p q, induced Ω T p q → t p = t q + intro p q hpq + exact hpq t ht + +/-- Closure operator on equivalences: `induced Ω ∘ respects Ω`. -/ +def cl (Ω : Type*) (E : Proc → Proc → Prop) : Proc → Proc → Prop := + induced Ω (respects Ω E) + +/-- `cl Ω` is extensive: `E ≤ cl Ω E` (pointwise). -/ +theorem cl_extensive (Ω : Type*) (E : Proc → Proc → Prop) (p q : Proc) + (h : E p q) : cl Ω E p q := by + intro t ht + exact ht p q h + +/-- `cl Ω` is monotone: `E₁ ≤ E₂ → cl Ω E₁ ≤ cl Ω E₂`. -/ +theorem cl_monotone (Ω : Type*) (E₁ E₂ : Proc → Proc → Prop) + (h : ∀ p q, E₁ p q → E₂ p q) (p q : Proc) (hcl : cl Ω E₁ p q) : + cl Ω E₂ p q := by + intro t ht + exact hcl t (fun a b ha => ht a b (h a b ha)) + +/-- An equivalence is TESTABLE iff it is exactly "indistinguishability under + the tests that respect it" — i.e. a fixed point of `cl Ω`. This predicate + IS the closed-element condition. -/ +def Testable (Ω : Type*) (E : Proc → Proc → Prop) : Prop := + ∀ p q, cl Ω E p q ↔ E p q + +/-- Every induced equivalence is testable (the image of `induced Ω` is contained + in the fixed points of `cl Ω`). -/ +theorem induced_testable (Ω : Type*) (T : Set (Proc → Ω)) : + Testable Ω (induced Ω T) := by + intro p q + constructor + · intro hcl t ht + exact hcl t (test_subset_respects_induced Ω T ht) + · intro hInd t ht + exact ht p q hInd + +/-- `cl Ω` is idempotent: `cl Ω (cl Ω E) = cl Ω E`. `cl Ω E` lies in the image + of `induced Ω`, hence is a fixed point by `induced_testable`. -/ +theorem cl_idempotent (Ω : Type*) (E : Proc → Proc → Prop) (p q : Proc) : + cl Ω (cl Ω E) p q ↔ cl Ω E p q := by + have key : Testable Ω (induced Ω (respects Ω E)) := induced_testable Ω (respects Ω E) + exact key p q + +/-- **Spectrum = image of `induced` = closed elements.** An equivalence is + testable (a fixed point of `cl Ω`) iff it is exactly the equivalence induced + by some test class. Forward direction witnessed by `T = respects Ω E`. -/ +theorem spectrum_eq_closed_elements (Ω : Type*) (E : Proc → Proc → Prop) : + Testable Ω E ↔ ∃ T : Set (Proc → Ω), induced Ω T = E := by + constructor + · intro hE + refine ⟨respects Ω E, ?_⟩ + change cl Ω E = E + funext p q + exact propext (hE p q) + · rintro ⟨T, rfl⟩ + exact induced_testable Ω T + +end Cslib.LTS.Spectrum diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean new file mode 100644 index 000000000..ab5a11ba2 --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 TODO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: TODO +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Semantics.LTS.TraceEq +public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois + +/-! +# Spectrum trace point — trace equivalence is Galois-closed + +A concrete named spectrum point: CSLib's homogeneous trace equivalence +(`Cslib.LTS.HomTraceEq`) is a Galois-closed (testable) equivalence, via the +trace-set observer test class (`fun s => lts.traces s`, `Ω = Set (List Label)`). +`HomTraceEq` lies in the image of `induced`, hence is a fixed point of the +closure operator `cl`. + +This proves the structural result (TraceEq ∈ closed elements). The standard +testing-semantics refinement — one `Bool` test per trace — gives a finer witness +for the SAME closed element but requires decidability of trace membership; it +does not change the closed-element verdict. + +The Hennessy–Milner theorem (bisim ↔ same HML formulas) is not used; CSLib does +not yet mechanise it. +-/ + +@[expose] public section + +namespace Cslib.LTS.Spectrum + +open Cslib + +variable {State Label : Type*} (lts : LTS State Label) + +/-- The trace-set observer test: a state's full set of traces. -/ +def traceSetTest (s : State) : Set (List Label) := + lts.traces s + +/-- Test class for the trace point: the singleton trace-set observer. -/ +def traceTestClass : Set (State → Set (List Label)) := + { f | f = traceSetTest lts } + +/-- The equivalence induced by the trace-set test is CSLib's homogeneous trace + equivalence (pointwise iff). -/ +theorem induced_traceSet_iff (p q : State) : + induced (Set (List Label)) (traceTestClass lts) p q ↔ HomTraceEq lts p q := by + unfold induced traceTestClass + simp only [Set.mem_setOf_eq] + constructor + · intro h + exact h _ rfl + · intro h t ht + rw [ht] + exact h + +/-- Function-equality form (via `propext`). -/ +theorem induced_traceSet : + induced (Set (List Label)) (traceTestClass lts) = HomTraceEq lts := by + funext p q + exact propext (induced_traceSet_iff lts p q) + +/-- **Trace point.** CSLib's homogeneous trace equivalence is a Galois-closed + (testable) equivalence. -/ +theorem HomTraceEq_testable : + Testable (Set (List Label)) (HomTraceEq lts) := by + rw [← induced_traceSet lts] + exact induced_testable (Set (List Label)) (traceTestClass lts) + +end Cslib.LTS.Spectrum From d39b761ce2a22fa653271cc0c09bc340db441e2e Mon Sep 17 00:00:00 2001 From: patchwright Date: Mon, 13 Jul 2026 02:22:00 +0200 Subject: [PATCH 02/12] feat(LTS/Spectrum): add bisim point (HM-mediated) + correct HM docstring + authors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add Spectrum.BisimPoint: HomBisimilarity_testable — bisimilarity is Galois-closed for image-finite LTS, via CSLib's Hennessy-Milner theorem (theoryEq_eq_bisimilarity). This is the non-trivial spectrum point: bisimilarity is not a kernel by definition (unlike trace equivalence); the HM theorem is what makes it one. Correct the false claim in TracePoint.lean that 'CSLib does not yet mechanise HM' — CSLib does mechanise it (Cslib.Logic.HML.theoryEq_eq_bisimilarity). TracePoint now points to BisimPoint for the HM-mediated companion. Set Authors/Copyright to patchwright in all four files (were TODO). With trace (kernel-trivial bottom) and bisimilarity (HM-mediated top) as two closed elements of the same polarity, the framework now unites two genuinely different behavioural equivalences — the actual 'spectrum as Galois' statement. --- Cslib.lean | 1 + .../Semantics/LTS/Spectrum/Antichain.lean | 4 +- .../Semantics/LTS/Spectrum/BisimPoint.lean | 74 +++++++++++++++++++ .../Semantics/LTS/Spectrum/Galois.lean | 4 +- .../Semantics/LTS/Spectrum/TracePoint.lean | 10 ++- 5 files changed, 85 insertions(+), 8 deletions(-) create mode 100644 Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean diff --git a/Cslib.lean b/Cslib.lean index adcc92edd..6761991aa 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -99,6 +99,7 @@ public import Cslib.Foundations.Semantics.LTS.OmegaExecution public import Cslib.Foundations.Semantics.LTS.Relation public import Cslib.Foundations.Semantics.LTS.Simulation public import Cslib.Foundations.Semantics.LTS.Spectrum.Antichain +public import Cslib.Foundations.Semantics.LTS.Spectrum.BisimPoint public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois public import Cslib.Foundations.Semantics.LTS.Spectrum.TracePoint public import Cslib.Foundations.Semantics.LTS.Termination diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean index 73bc85854..e83053ef2 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 TODO. All rights reserved. +Copyright (c) 2026 patchwright. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: TODO +Authors: patchwright -/ module diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean new file mode 100644 index 000000000..467e6792f --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 patchwright. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: patchwright +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois +public import Cslib.Logics.HML.Basic + +/-! +# Spectrum bisim point — bisimilarity is Galois-closed (via Hennessy–Milner) + +The non-trivial spectrum point. Unlike trace equivalence (`Spectrum.TracePoint`), +bisimilarity is NOT the kernel of its test map by definition — it is the +Hennessy–Milner theorem that makes it one. CSLib mechanises HM as +`Cslib.Logic.HML.theoryEq_eq_bisimilarity` (`TheoryEq lts = HomBisimilarity lts` +for image-finite LTS), so composing that with the (kernel-trivial) fact that +`TheoryEq` is the equivalence induced by the HML-theory test class yields: + + `Testable (Set (Proposition Label)) (HomBisimilarity lts)`. + +This is the load-bearing step that earns the contribution the word "spectrum": +two genuinely different behavioural equivalences — trace (kernel-trivial bottom) +and bisimilarity (HM-mediated top) — are closed elements of the SAME polarity. +-/ + +@[expose] public section + +namespace Cslib.LTS.Spectrum + +open Cslib Cslib.Logic.HML + +variable {State Label : Type*} (lts : LTS State Label) + +/-- The HML-theory observer test: a state's full theory (set of satisfied HML + propositions). -/ +def hmlTheory (s : State) : Set (Proposition Label) := + theory lts s + +/-- Test class for the bisim point: the singleton HML-theory observer. -/ +def hmlTestClass : Set (State → Set (Proposition Label)) := + { f | f = hmlTheory lts } + +/-- The equivalence induced by the HML-theory test is CSLib's `TheoryEq` + (pointwise iff). -/ +theorem induced_hml_iff (p q : State) : + induced (Set (Proposition Label)) (hmlTestClass lts) p q ↔ TheoryEq lts p q := by + constructor + · intro h + exact h _ rfl + · intro h t ht + have ht : t = hmlTheory lts := ht + subst ht + exact h + +/-- Function-equality form (via `propext`). -/ +theorem induced_hml : + induced (Set (Proposition Label)) (hmlTestClass lts) = TheoryEq lts := by + funext p q + exact propext (induced_hml_iff lts p q) + +/-- **Bisim point.** CSLib's homogeneous bisimilarity is a Galois-closed + (testable) equivalence — for image-finite LTS, via the Hennessy–Milner + theorem (`theoryEq_eq_bisimilarity`). This is the non-trivial spectrum point: + bisimilarity is not a kernel by definition; HM makes it one. -/ +theorem HomBisimilarity_testable [image_finite : ∀ s μ, Finite (lts.image s μ)] : + Testable (Set (Proposition Label)) (HomBisimilarity lts) := by + rw [← theoryEq_eq_bisimilarity lts, ← induced_hml lts] + exact induced_testable (Set (Proposition Label)) (hmlTestClass lts) + +end Cslib.LTS.Spectrum diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean index df7b1415d..d0be0f734 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 TODO. All rights reserved. +Copyright (c) 2026 patchwright. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: TODO +Authors: patchwright -/ module diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean index ab5a11ba2..8d30f28d4 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 TODO. All rights reserved. +Copyright (c) 2026 patchwright. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: TODO +Authors: patchwright -/ module @@ -24,8 +24,10 @@ testing-semantics refinement — one `Bool` test per trace — gives a finer wit for the SAME closed element but requires decidability of trace membership; it does not change the closed-element verdict. -The Hennessy–Milner theorem (bisim ↔ same HML formulas) is not used; CSLib does -not yet mechanise it. +The Hennessy–Milner theorem IS mechanised in CSLib as +`Cslib.Logic.HML.theoryEq_eq_bisimilarity`; the bisim point built on it is in +`Spectrum.BisimPoint`. This file (the trace point, kernel-trivial bottom) does +not use HM — bisimilarity (HM-mediated top) is the companion point there. -/ @[expose] public section From 708b0bab114e93e1c592a374ac8a561aa54864e5 Mon Sep 17 00:00:00 2001 From: patchwright Date: Mon, 13 Jul 2026 10:10:41 +0200 Subject: [PATCH 03/12] fix(LTS/Spectrum/Antichain): add T2 docstring (CI docBlame lint) CI's lake lint found one error: T2 was missing a documentation string (the shared 'Test classes' doc comment attached only to T1). Give T1 and T2 separate docstrings. All other declarations + 14 other linters passed. --- Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean index e83053ef2..85ad2bd2b 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean @@ -47,8 +47,9 @@ def t2 : W → Bool | a | c => true | b | d => false -/-- Test classes (singletons, written as comprehensions). -/ +/-- Test class `T₁`: the singleton `{ t₁ }`, written as a comprehension. -/ def T1 : Set (W → Bool) := { f | f = t1 } +/-- Test class `T₂`: the singleton `{ t₂ }`, written as a comprehension. -/ def T2 : Set (W → Bool) := { f | f = t2 } /-- a,b are `T₁`-equivalent but `T₂`-distinct. -/ From d83c14e0a3efba588a89e995d275953af2591f03 Mon Sep 17 00:00:00 2001 From: patchwright Date: Thu, 16 Jul 2026 11:09:21 +0200 Subject: [PATCH 04/12] docs(LTS/Spectrum): cite the theory (van Glabbeek 1990, Beohar 2022) Addresses ctchou's review on #713: add the spectrum and polarity references to references.bib and refer to them from the Galois module doc, matching CSLib's [Author, *Title*][Key] convention (cf. Cslib/Foundations/Semantics/LTS/Basic.lean). - references.bib: Glabbeek1990 (CONCUR '90, LNCS 458), Glabbeek1993 (Spectrum II), Beohar2022 (arXiv:2207.05407). - Spectrum/Galois.lean: ## References block citing both. --- .../Semantics/LTS/Spectrum/Galois.lean | 9 +++++++ references.bib | 27 +++++++++++++++++++ 2 files changed, 36 insertions(+) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean index d0be0f734..603ea7e60 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -39,6 +39,15 @@ recover `Ω` from it. * `induced_testable`: every induced equivalence is a fixed point of `cl`. * `cl_extensive`, `cl_monotone`, `cl_idempotent`: `cl` is a closure operator. * `spectrum_eq_closed_elements`: testable ↔ in the image of `induced`. + +## References + +* [R.J. van Glabbeek, *The Linear Time – Branching Time Spectrum*][Glabbeek1990] + (extended to silent moves in *Spectrum II* [Glabbeek1993]) — the spectrum of + behavioural equivalences ordered by refinement. +* [H. Beohar, *Hennessy-Milner Theorems via Galois Connections*][Beohar2022] — + the reading of those equivalences as the fixed points of an antitone Galois + connection (polarity) between tests and equivalences. -/ @[expose] public section diff --git a/references.bib b/references.bib index 18281428d..af8b4187e 100644 --- a/references.bib +++ b/references.bib @@ -39,6 +39,15 @@ @book{Baader1998 address = {USA} } +@misc{Beohar2022, + author = {Beohar, Harsh}, + title = {Hennessy-Milner Theorems via Galois Connections}, + year = {2022}, + eprint = {2207.05407}, + archiveprefix = {arXiv}, + url = {https://arxiv.org/abs/2207.05407} +} + @book{Blackburn2001, place={Cambridge}, series={Cambridge Tracts in Theoretical Computer Science}, @@ -176,6 +185,24 @@ @inbook{ Girard1995 collection={London Mathematical Society Lecture Note Series} } +@inproceedings{Glabbeek1990, + author = {van Glabbeek, R.J.}, + title = {The Linear Time -- Branching Time Spectrum}, + booktitle = {CONCUR '90: Theories of Concurrency (Unification and Extension)}, + series = {Lecture Notes in Computer Science}, + volume = {458}, + year = {1990}, + pages = {278--297}, + publisher = {Springer} +} + +@misc{Glabbeek1993, + author = {van Glabbeek, R.J.}, + title = {The Linear Time -- Branching Time Spectrum II}, + year = {1993}, + note = {Extended manuscript; adds silent moves (branching/weak semantics)} +} + @article{Haussler1992, author = {Haussler, David}, title = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications}, From 9be8656623c4d2c7a70c7bd3deb03c10d9d98673 Mon Sep 17 00:00:00 2001 From: patchwright Date: Sat, 18 Jul 2026 15:32:43 +0200 Subject: [PATCH 05/12] refactor(LTS/Spectrum): state polarity as a Mathlib GaloisConnection MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review feedback (ctchou): the code talked about Galois connections without ever connecting to Mathlib's. Now: - polarity : GaloisConnection (toDual ∘ respects) (induced ∘ ofDual) — the antitone connection stated Mathlib-style into the order dual - cl is (polarity Ω).closureOperator : ClosureOperator, so extensive/ monotone/idempotent are inherited, not hand-proved (same pattern as PhaseSemantics.biorthogonalClosure) - Testable Ω E := (cl Ω).IsClosed E; induced_testable is u_l_u_eq_u - pointwise forms kept as polarity_iff / testable_iff Also clarifies the Antichain module comment ctchou flagged (structural antichain here vs the named sim-vs-failures pair pending failures semantics). Downstream Spectrum modules (TracePoint, BisimPoint, Antichain) build unchanged apart from the comment. --- .../Semantics/LTS/Spectrum/Antichain.lean | 8 +- .../Semantics/LTS/Spectrum/Galois.lean | 152 +++++++++++------- 2 files changed, 96 insertions(+), 64 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean index 85ad2bd2b..d3fb0029d 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean @@ -22,9 +22,11 @@ Hence the closed-element lattice contains an antichain → it is a lattice, not chain (scale). This is the structural form of the "linear-time/branching-time spectrum is a lattice, not a linear scale" claim. -(The *named* van Glabbeek antichain — simulation vs failures equivalence — -requires failures semantics, not yet in CSLib; that named instance is separate -from the structural result here.) +This file proves the structural fact only, over a small explicit witness. The +classical spectrum also contains *named* incomparable pairs — e.g. simulation +equivalence vs failures equivalence [Glabbeek1990] — but mechanising such a +pair requires failures semantics, which CSLib does not yet define, so no named +instance is attempted here. -/ @[expose] public section diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean index 603ea7e60..b4533d37f 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -7,15 +7,25 @@ Authors: patchwright module public import Cslib.Init +public import Mathlib.Order.GaloisConnection.Defs +public import Mathlib.Order.Closure /-! # Van Glabbeek's spectrum as a Galois connection — the polarity framework -Behavioural equivalences are organised as the fixed points of an antitone Galois -connection ("polarity") between sets of tests (ordered by ⊆) and equivalences -(ordered by refinement). The Galois-closed equivalences — the "testable" ones — -are exactly the image of `induced`; they form a lattice, not a chain -(see `Spectrum.Antichain`). +Behavioural equivalences are organised as the closed elements of an antitone +Galois connection ("polarity") between sets of tests (ordered by `⊆`) and +equivalences (ordered by refinement). Following the standard Mathlib idiom, the +antitone connection is stated as a `GaloisConnection` into the order dual: + + `polarity : GaloisConnection (toDual ∘ respects Ω) (induced Ω ∘ ofDual)` + +The closure operator on equivalences is then *derived* — it is +`(polarity Ω).closureOperator`, an instance of Mathlib's `ClosureOperator` +(the same pattern as `PhaseSemantics.biorthogonalClosure`), so extensivity, +monotonicity and idempotence are inherited rather than proved by hand. The +Galois-closed equivalences — the "testable" ones — are exactly the image of +`induced`; they form a lattice, not a chain (see `Spectrum.Antichain`). This module is the Mathlib/`Cslib.Init`-only framework. A concrete named spectrum point (CSLib's `HomTraceEq`) is shown Galois-closed in @@ -30,14 +40,19 @@ recover `Ω` from it. * `induced Ω T`: the equivalence a test class `T` induces. * `respects Ω E`: the tests that respect an equivalence `E`. -* `cl Ω`: the closure operator `induced Ω ∘ respects Ω`. -* `Testable Ω E`: the fixed-point predicate (`cl Ω E = E`). +* `cl Ω`: the closure operator `induced Ω ∘ respects Ω`, as a Mathlib + `ClosureOperator`, obtained from `polarity` via + `GaloisConnection.closureOperator`. +* `Testable Ω E`: `E` is a closed element of `cl Ω` (`(cl Ω).IsClosed E`). ## Main statements -* `polarity`: the antitone Galois connection. -* `induced_testable`: every induced equivalence is a fixed point of `cl`. -* `cl_extensive`, `cl_monotone`, `cl_idempotent`: `cl` is a closure operator. +* `polarity`: the antitone Galois connection, as a Mathlib `GaloisConnection` + into the order dual. +* `induced_testable`: every induced equivalence is closed (from + `GaloisConnection.u_l_u_eq_u`). +* `cl_extensive`, `cl_monotone`, `cl_idempotent`: inherited from + `ClosureOperator`. * `spectrum_eq_closed_elements`: testable ↔ in the image of `induced`. ## References @@ -54,6 +69,8 @@ recover `Ω` from it. namespace Cslib.LTS.Spectrum +open OrderDual (toDual ofDual) + variable {Proc : Type*} /-- The equivalence a test class induces: agreement on every test in `T`. @@ -66,9 +83,9 @@ def induced (Ω : Type*) (T : Set (Proc → Ω)) (p q : Proc) : Prop := def respects (Ω : Type*) (E : Proc → Proc → Prop) : Set (Proc → Ω) := { t | ∀ p q, E p q → t p = t q } -/-- **Polarity.** Antitone Galois connection between test classes (⊆) and - equivalences (refinement): `E` refines `induced Ω T` iff `T ⊆ respects Ω E`. -/ -theorem polarity (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → Prop) : +/-- Pointwise form of the polarity: `E` refines `induced Ω T` iff + `T ⊆ respects Ω E`. The order-theoretic packaging is `polarity` below. -/ +theorem polarity_iff (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → Prop) : (∀ p q, E p q → induced Ω T p q) ↔ T ⊆ respects Ω E := by constructor · intro h t ht p q hpq @@ -76,66 +93,79 @@ theorem polarity (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → Pro · intro h p q hpq t ht exact h ht p q hpq -/-- Every test in `T` respects the equivalence `T` induces (the image fact). -/ +/-- **Polarity.** `respects Ω` and `induced Ω` form an antitone Galois + connection between equivalences under refinement and test classes under + `⊆`. Stated, as is standard in Mathlib, as a (monotone) `GaloisConnection` + into the order dual `(Set (Proc → Ω))ᵒᵈ`. -/ +theorem polarity (Ω : Type*) : + GaloisConnection (fun E : Proc → Proc → Prop => toDual (respects Ω E)) + (fun T => induced Ω (ofDual T)) := by + intro E T + rw [OrderDual.toDual_le] + simp only [Set.le_eq_subset, Pi.le_def, le_Prop_eq] + exact (polarity_iff Ω (ofDual T) E).symm + +/-- Every test in `T` respects the equivalence `T` induces — the counit + `l (u b) ≤ b` of `polarity`, read back through the dual. -/ theorem test_subset_respects_induced (Ω : Type*) (T : Set (Proc → Ω)) : - T ⊆ respects Ω (induced Ω T) := by - intro t ht - change ∀ p q, induced Ω T p q → t p = t q - intro p q hpq - exact hpq t ht - -/-- Closure operator on equivalences: `induced Ω ∘ respects Ω`. -/ -def cl (Ω : Type*) (E : Proc → Proc → Prop) : Proc → Proc → Prop := - induced Ω (respects Ω E) - -/-- `cl Ω` is extensive: `E ≤ cl Ω E` (pointwise). -/ -theorem cl_extensive (Ω : Type*) (E : Proc → Proc → Prop) (p q : Proc) - (h : E p q) : cl Ω E p q := by - intro t ht - exact ht p q h - -/-- `cl Ω` is monotone: `E₁ ≤ E₂ → cl Ω E₁ ≤ cl Ω E₂`. -/ -theorem cl_monotone (Ω : Type*) (E₁ E₂ : Proc → Proc → Prop) - (h : ∀ p q, E₁ p q → E₂ p q) (p q : Proc) (hcl : cl Ω E₁ p q) : - cl Ω E₂ p q := by - intro t ht - exact hcl t (fun a b ha => ht a b (h a b ha)) + T ⊆ respects Ω (induced Ω T) := + (polarity Ω).l_u_le (toDual T) + +/-- Closure operator on equivalences: `induced Ω ∘ respects Ω`, obtained from + `polarity` via Mathlib's `GaloisConnection.closureOperator`. -/ +def cl (Ω : Type*) : ClosureOperator (Proc → Proc → Prop) := + (polarity (Proc := Proc) Ω).closureOperator + +/-- `cl Ω` acts as `induced Ω ∘ respects Ω`. -/ +theorem cl_apply (Ω : Type*) (E : Proc → Proc → Prop) : + cl Ω E = induced Ω (respects Ω E) := + rfl + +/-- `cl Ω` is extensive: `E ≤ cl Ω E` — inherited from `ClosureOperator`. -/ +theorem cl_extensive (Ω : Type*) (E : Proc → Proc → Prop) : E ≤ cl Ω E := + (cl Ω).le_closure E + +/-- `cl Ω` is monotone — inherited from `ClosureOperator`. -/ +theorem cl_monotone (Ω : Type*) : Monotone (cl (Proc := Proc) Ω) := + (cl Ω).monotone + +/-- `cl Ω` is idempotent — inherited from `ClosureOperator`. -/ +theorem cl_idempotent (Ω : Type*) (E : Proc → Proc → Prop) : + cl Ω (cl Ω E) = cl Ω E := + (cl Ω).idempotent E /-- An equivalence is TESTABLE iff it is exactly "indistinguishability under - the tests that respect it" — i.e. a fixed point of `cl Ω`. This predicate - IS the closed-element condition. -/ + the tests that respect it" — i.e. a closed element of `cl Ω`. -/ def Testable (Ω : Type*) (E : Proc → Proc → Prop) : Prop := - ∀ p q, cl Ω E p q ↔ E p q + (cl Ω).IsClosed E -/-- Every induced equivalence is testable (the image of `induced Ω` is contained - in the fixed points of `cl Ω`). -/ -theorem induced_testable (Ω : Type*) (T : Set (Proc → Ω)) : - Testable Ω (induced Ω T) := by - intro p q +/-- Pointwise reading of `Testable`: `cl Ω E` and `E` agree on every pair. -/ +theorem testable_iff (Ω : Type*) (E : Proc → Proc → Prop) : + Testable Ω E ↔ ∀ p q, cl Ω E p q ↔ E p q := by + rw [Testable, ClosureOperator.isClosed_iff] constructor - · intro hcl t ht - exact hcl t (test_subset_respects_induced Ω T ht) - · intro hInd t ht - exact ht p q hInd - -/-- `cl Ω` is idempotent: `cl Ω (cl Ω E) = cl Ω E`. `cl Ω E` lies in the image - of `induced Ω`, hence is a fixed point by `induced_testable`. -/ -theorem cl_idempotent (Ω : Type*) (E : Proc → Proc → Prop) (p q : Proc) : - cl Ω (cl Ω E) p q ↔ cl Ω E p q := by - have key : Testable Ω (induced Ω (respects Ω E)) := induced_testable Ω (respects Ω E) - exact key p q + · intro h p q + exact iff_of_eq (congrFun (congrFun h p) q) + · intro h + funext p q + exact propext (h p q) + +/-- Every induced equivalence is testable (the image of `induced Ω` is + contained in the closed elements) — this is `u ∘ l ∘ u = u` for `polarity` + (`GaloisConnection.u_l_u_eq_u`). -/ +theorem induced_testable (Ω : Type*) (T : Set (Proc → Ω)) : + Testable Ω (induced Ω T) := + (cl Ω).isClosed_iff.2 ((polarity Ω).u_l_u_eq_u (toDual T)) /-- **Spectrum = image of `induced` = closed elements.** An equivalence is - testable (a fixed point of `cl Ω`) iff it is exactly the equivalence induced - by some test class. Forward direction witnessed by `T = respects Ω E`. -/ + testable (a closed element of `cl Ω`) iff it is exactly the equivalence + induced by some test class. Forward direction witnessed by + `T = respects Ω E`. -/ theorem spectrum_eq_closed_elements (Ω : Type*) (E : Proc → Proc → Prop) : Testable Ω E ↔ ∃ T : Set (Proc → Ω), induced Ω T = E := by constructor · intro hE - refine ⟨respects Ω E, ?_⟩ - change cl Ω E = E - funext p q - exact propext (hE p q) + exact ⟨respects Ω E, (cl Ω).isClosed_iff.1 hE⟩ · rintro ⟨T, rfl⟩ exact induced_testable Ω T From 6c36cc17cf724befaa67870786a8821cb5c6def9 Mon Sep 17 00:00:00 2001 From: patchwright Date: Sat, 18 Jul 2026 15:40:27 +0200 Subject: [PATCH 06/12] feat(LTS/Spectrum): the spectrum of testable equivalences is a complete lattice MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Free corollary of the ClosureOperator refactor: lift the complete lattice of all equivalences through the Galois insertion (cl Ω).gi (Mathlib's GaloisInsertion.liftCompleteLattice, same pattern as Order.Nucleus). Arbitrary meets/joins of testable equivalences exist; with Spectrum.Antichain this gives 'a lattice, not a linear scale' as a mechanised statement rather than prose. --- .../Semantics/LTS/Spectrum/Galois.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean index b4533d37f..a54686011 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -7,7 +7,7 @@ Authors: patchwright module public import Cslib.Init -public import Mathlib.Order.GaloisConnection.Defs +public import Mathlib.Order.GaloisConnection.Basic public import Mathlib.Order.Closure /-! @@ -54,6 +54,8 @@ recover `Ω` from it. * `cl_extensive`, `cl_monotone`, `cl_idempotent`: inherited from `ClosureOperator`. * `spectrum_eq_closed_elements`: testable ↔ in the image of `induced`. +* `spectrumCompleteLattice`: the testable equivalences form a complete lattice + under refinement (via `GaloisInsertion.liftCompleteLattice`). ## References @@ -169,4 +171,15 @@ theorem spectrum_eq_closed_elements (Ω : Type*) (E : Proc → Proc → Prop) : · rintro ⟨T, rfl⟩ exact induced_testable Ω T +/-- **The spectrum is a complete lattice.** The closed elements of `cl Ω` — the + testable equivalences — form a complete lattice under refinement, lifted + through the Galois insertion `(cl Ω).gi` from the complete lattice of all + equivalences (Mathlib's `GaloisInsertion.liftCompleteLattice`). Arbitrary + meets and joins of testable equivalences exist; and the lattice is not a + chain (`Spectrum.Antichain`), which is the structural form of "the + linear-time/branching-time spectrum is a lattice, not a linear scale". -/ +instance spectrumCompleteLattice {Ω : Type*} : + CompleteLattice ((cl (Proc := Proc) Ω).Closeds) := + (cl Ω).gi.liftCompleteLattice + end Cslib.LTS.Spectrum From 50bf187066f92ffb1fe07d1a6d1919f3b31b9056 Mon Sep 17 00:00:00 2001 From: patchwright Date: Sat, 18 Jul 2026 15:53:43 +0200 Subject: [PATCH 07/12] fix(LTS/Spectrum): clear deprecation warnings under Lean v4.33.0-rc1 CI CI builds the merge with main (toolchain now v4.33.0-rc1) with --wfail: - Galois: drop Set.le_eq_subset from the simp set (now a syntactic equality upstream; linted as unused) - TracePoint: restate induced_traceSet_iff without Set.mem_setOf_eq (deprecated upstream), mirroring the simp-free proof style already used in BisimPoint.induced_hml_iff Both proofs are version-agnostic and also build on v4.32.0-rc1. --- Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean | 2 +- Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean index a54686011..1279c3fde 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -104,7 +104,7 @@ theorem polarity (Ω : Type*) : (fun T => induced Ω (ofDual T)) := by intro E T rw [OrderDual.toDual_le] - simp only [Set.le_eq_subset, Pi.le_def, le_Prop_eq] + simp only [Pi.le_def, le_Prop_eq] exact (polarity_iff Ω (ofDual T) E).symm /-- Every test in `T` respects the equivalence `T` induces — the counit diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean index 8d30f28d4..16a8ba6e5 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean @@ -50,13 +50,12 @@ def traceTestClass : Set (State → Set (List Label)) := equivalence (pointwise iff). -/ theorem induced_traceSet_iff (p q : State) : induced (Set (List Label)) (traceTestClass lts) p q ↔ HomTraceEq lts p q := by - unfold induced traceTestClass - simp only [Set.mem_setOf_eq] constructor · intro h exact h _ rfl · intro h t ht - rw [ht] + have ht : t = traceSetTest lts := ht + subst ht exact h /-- Function-equality form (via `propext`). -/ From 312d557c210f8a8e5f770a0093035a7e23f5c5d4 Mon Sep 17 00:00:00 2001 From: patchwright Date: Sun, 19 Jul 2026 04:45:23 +0200 Subject: [PATCH 08/12] refactor(spectrum): address ctchou review across the module MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per ctchou's 2026-07-19 review of #713. Galois.lean: 1. Add `def spectrum Ω := { E | Testable Ω E }` — "spectrum" now has a Lean definition (previously only in prose/namespace). 2. State both preorders of `polarity` explicitly: equivalences under pointwise implication `E ≤ E' ↔ ∀ p q, E p q → E' p q`; test classes under `(⊆)`. 3. Drop `cl_extensive`/`cl_monotone`/`cl_idempotent` — generic ClosureOperator API wrappers; callers use the inherited lemmas directly. 4. Trim verbose comments. TracePoint / Antichain / BisimPoint: trim the same class of exposition tells flagged in the review — proof-revelation in docstrings ("via propext"), alternative-not-taken and scope-justification paragraphs, grandiose framing. references.bib: complete the Beohar2022 author list (Beohar, Gurke, König, Messing — verified via arXiv:2207.05407). Proofs unchanged throughout. Builds clean, 0 sorry / 0 axiom (2762 jobs). --- .../Semantics/LTS/Spectrum/Antichain.lean | 23 +-- .../Semantics/LTS/Spectrum/BisimPoint.lean | 20 +-- .../Semantics/LTS/Spectrum/Galois.lean | 140 +++++++----------- .../Semantics/LTS/Spectrum/TracePoint.lean | 22 +-- references.bib | 2 +- 5 files changed, 78 insertions(+), 129 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean index d3fb0029d..be27aeecb 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Antichain.lean @@ -12,21 +12,14 @@ public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois /-! # Spectrum antichain — the closed-element lattice is not a chain -The closed-element lattice is NOT totally ordered by refinement: two -incomparable Galois-closed (testable) equivalences exist over a 4-state witness -space. Two test classes `T₁`, `T₂` (Ω = Bool) induce closed equivalences such -that neither refines the other: +The lattice of testable equivalences is not totally ordered by refinement. Over +a 4-state witness, two test classes `T₁`, `T₂` (Ω = `Bool`) induce closed +equivalences that are incomparable: - states a,b are `T₁`-equivalent but `T₂`-distinct; - states a,c are `T₂`-equivalent but `T₁`-distinct. -Hence the closed-element lattice contains an antichain → it is a lattice, not a -chain (scale). This is the structural form of the "linear-time/branching-time -spectrum is a lattice, not a linear scale" claim. - -This file proves the structural fact only, over a small explicit witness. The -classical spectrum also contains *named* incomparable pairs — e.g. simulation -equivalence vs failures equivalence [Glabbeek1990] — but mechanising such a -pair requires failures semantics, which CSLib does not yet define, so no named -instance is attempted here. + +So the spectrum contains an antichain — it is a lattice, not a linear scale +(cf. [Glabbeek1990]). -/ @[expose] public section @@ -49,9 +42,9 @@ def t2 : W → Bool | a | c => true | b | d => false -/-- Test class `T₁`: the singleton `{ t₁ }`, written as a comprehension. -/ +/-- Test class `T₁`: the singleton `{ t₁ }`. -/ def T1 : Set (W → Bool) := { f | f = t1 } -/-- Test class `T₂`: the singleton `{ t₂ }`, written as a comprehension. -/ +/-- Test class `T₂`: the singleton `{ t₂ }`. -/ def T2 : Set (W → Bool) := { f | f = t2 } /-- a,b are `T₁`-equivalent but `T₂`-distinct. -/ diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean index 467e6792f..b33cdf1d3 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/BisimPoint.lean @@ -14,17 +14,13 @@ public import Cslib.Logics.HML.Basic # Spectrum bisim point — bisimilarity is Galois-closed (via Hennessy–Milner) The non-trivial spectrum point. Unlike trace equivalence (`Spectrum.TracePoint`), -bisimilarity is NOT the kernel of its test map by definition — it is the -Hennessy–Milner theorem that makes it one. CSLib mechanises HM as +bisimilarity is not the kernel of its test map by definition; the +Hennessy–Milner theorem makes it one. CSLib mechanises HM as `Cslib.Logic.HML.theoryEq_eq_bisimilarity` (`TheoryEq lts = HomBisimilarity lts` -for image-finite LTS), so composing that with the (kernel-trivial) fact that -`TheoryEq` is the equivalence induced by the HML-theory test class yields: +for image-finite LTS), and `TheoryEq` is the equivalence induced by the +HML-theory test class, so: `Testable (Set (Proposition Label)) (HomBisimilarity lts)`. - -This is the load-bearing step that earns the contribution the word "spectrum": -two genuinely different behavioural equivalences — trace (kernel-trivial bottom) -and bisimilarity (HM-mediated top) — are closed elements of the SAME polarity. -/ @[expose] public section @@ -56,16 +52,14 @@ theorem induced_hml_iff (p q : State) : subst ht exact h -/-- Function-equality form (via `propext`). -/ +/-- Function-equality form of `induced_hml_iff`. -/ theorem induced_hml : induced (Set (Proposition Label)) (hmlTestClass lts) = TheoryEq lts := by funext p q exact propext (induced_hml_iff lts p q) -/-- **Bisim point.** CSLib's homogeneous bisimilarity is a Galois-closed - (testable) equivalence — for image-finite LTS, via the Hennessy–Milner - theorem (`theoryEq_eq_bisimilarity`). This is the non-trivial spectrum point: - bisimilarity is not a kernel by definition; HM makes it one. -/ +/-- **Bisim point.** `HomBisimilarity lts` is testable for image-finite LTS, via + the Hennessy–Milner theorem (`theoryEq_eq_bisimilarity`). -/ theorem HomBisimilarity_testable [image_finite : ∀ s μ, Finite (lts.image s μ)] : Testable (Set (Proposition Label)) (HomBisimilarity lts) := by rw [← theoryEq_eq_bisimilarity lts, ← induced_hml lts] diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean index 1279c3fde..d03f94cbd 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/Galois.lean @@ -11,60 +11,54 @@ public import Mathlib.Order.GaloisConnection.Basic public import Mathlib.Order.Closure /-! -# Van Glabbeek's spectrum as a Galois connection — the polarity framework +# The van Glabbeek spectrum as a Galois connection -Behavioural equivalences are organised as the closed elements of an antitone -Galois connection ("polarity") between sets of tests (ordered by `⊆`) and -equivalences (ordered by refinement). Following the standard Mathlib idiom, the -antitone connection is stated as a `GaloisConnection` into the order dual: +The linear time–branching time spectrum of behavioural equivalences is the set +of *testable* equivalences on a process type: those an observer recovers exactly +as indistinguishability under the tests that respect them. This set is the +collection of closed elements of an antitone Galois connection — a *polarity* — +between equivalences and tests. - `polarity : GaloisConnection (toDual ∘ respects Ω) (induced Ω ∘ ofDual)` +The two preorders of the connection are: + +* equivalences `E : Proc → Proc → Prop`, ordered by pointwise implication + `E ≤ E' ↔ ∀ p q, E p q → E' p q` (graph inclusion); +* test classes `T : Set (Proc → Ω)`, ordered by `(⊆)`. -The closure operator on equivalences is then *derived* — it is -`(polarity Ω).closureOperator`, an instance of Mathlib's `ClosureOperator` -(the same pattern as `PhaseSemantics.biorthogonalClosure`), so extensivity, -monotonicity and idempotence are inherited rather than proved by hand. The -Galois-closed equivalences — the "testable" ones — are exactly the image of -`induced`; they form a lattice, not a chain (see `Spectrum.Antichain`). +The antitone connection is packaged as a monotone `GaloisConnection` into the +order dual on the test side: + + `polarity : GaloisConnection (toDual ∘ respects Ω) (induced Ω ∘ ofDual)` -This module is the Mathlib/`Cslib.Init`-only framework. A concrete named -spectrum point (CSLib's `HomTraceEq`) is shown Galois-closed in -`Spectrum.TracePoint`. +Its closure operator is `cl Ω = induced Ω ∘ respects Ω`, and the spectrum is the +set of its closed elements. A named spectrum point (`HomTraceEq`) is shown closed +in `Spectrum.TracePoint`; the spectrum is a lattice rather than a chain +(`Spectrum.Antichain`). -The construction is parameterised by the pair `(Proc, Ω)`: `Proc` is the process -type and `Ω` the observation type (a test is `Proc → Ω`). `Ω` is carried -explicitly because the closure-operator theorems mention only `E` and cannot -recover `Ω` from it. +The construction is parameterised by `Proc` (the process type) and `Ω` (the +observation type; a test is `Proc → Ω`). `Ω` is carried explicitly because the +closure operator itself mentions only `E`. ## Main definitions -* `induced Ω T`: the equivalence a test class `T` induces. -* `respects Ω E`: the tests that respect an equivalence `E`. -* `cl Ω`: the closure operator `induced Ω ∘ respects Ω`, as a Mathlib - `ClosureOperator`, obtained from `polarity` via - `GaloisConnection.closureOperator`. -* `Testable Ω E`: `E` is a closed element of `cl Ω` (`(cl Ω).IsClosed E`). +* `induced Ω T`: the equivalence a test class induces. +* `respects Ω E`: the tests constant on every `E`-pair. +* `polarity Ω`: the Galois connection above. +* `cl Ω`: the closure operator `induced Ω ∘ respects Ω`. +* `Testable Ω E`: the proposition that `E` is `cl Ω`-closed. +* `spectrum Ω`: the set of testable equivalences. ## Main statements -* `polarity`: the antitone Galois connection, as a Mathlib `GaloisConnection` - into the order dual. -* `induced_testable`: every induced equivalence is closed (from - `GaloisConnection.u_l_u_eq_u`). -* `cl_extensive`, `cl_monotone`, `cl_idempotent`: inherited from - `ClosureOperator`. -* `spectrum_eq_closed_elements`: testable ↔ in the image of `induced`. -* `spectrumCompleteLattice`: the testable equivalences form a complete lattice - under refinement (via `GaloisInsertion.liftCompleteLattice`). +* `spectrum_eq_closed_elements`: the testable equivalences are exactly the image + of `induced`. +* `spectrumCompleteLattice`: the spectrum is a complete lattice under refinement. ## References -* [R.J. van Glabbeek, *The Linear Time – Branching Time Spectrum*][Glabbeek1990] - (extended to silent moves in *Spectrum II* [Glabbeek1993]) — the spectrum of - behavioural equivalences ordered by refinement. -* [H. Beohar, *Hennessy-Milner Theorems via Galois Connections*][Beohar2022] — - the reading of those equivalences as the fixed points of an antitone Galois - connection (polarity) between tests and equivalences. +* [R.J. van Glabbeek, *The Linear Time – Branching Time Spectrum*][Glabbeek1990], + extended to silent moves in *Spectrum II* [Glabbeek1993]. +* [H. Beohar, *Hennessy-Milner Theorems via Galois Connections*][Beohar2022]. -/ @[expose] public section @@ -75,18 +69,16 @@ open OrderDual (toDual ofDual) variable {Proc : Type*} -/-- The equivalence a test class induces: agreement on every test in `T`. - Antitone in `T` — more tests ⇒ finer (smaller) equivalence. -/ +/-- Equivalence induced by a test class `T`: two processes agree on every test + in `T`. -/ def induced (Ω : Type*) (T : Set (Proc → Ω)) (p q : Proc) : Prop := ∀ t ∈ T, t p = t q -/-- The tests that respect an equivalence `E`: tests constant on every E-pair. - Antitone in `E` — coarser `E` ⇒ fewer respecting tests. -/ +/-- Tests that respect an equivalence `E`: constant on every `E`-pair. -/ def respects (Ω : Type*) (E : Proc → Proc → Prop) : Set (Proc → Ω) := { t | ∀ p q, E p q → t p = t q } -/-- Pointwise form of the polarity: `E` refines `induced Ω T` iff - `T ⊆ respects Ω E`. The order-theoretic packaging is `polarity` below. -/ +/-- `E` refines `induced Ω T` iff every test in `T` respects `E`. -/ theorem polarity_iff (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → Prop) : (∀ p q, E p q → induced Ω T p q) ↔ T ⊆ respects Ω E := by constructor @@ -95,10 +87,9 @@ theorem polarity_iff (Ω : Type*) (T : Set (Proc → Ω)) (E : Proc → Proc → · intro h p q hpq t ht exact h ht p q hpq -/-- **Polarity.** `respects Ω` and `induced Ω` form an antitone Galois - connection between equivalences under refinement and test classes under - `⊆`. Stated, as is standard in Mathlib, as a (monotone) `GaloisConnection` - into the order dual `(Set (Proc → Ω))ᵒᵈ`. -/ +/-- The polarity: `respects Ω` and `induced Ω` form an antitone Galois connection + between equivalences (pointwise implication) and test classes (`(⊆)`, into + the order dual). -/ theorem polarity (Ω : Type*) : GaloisConnection (fun E : Proc → Proc → Prop => toDual (respects Ω E)) (fun T => induced Ω (ofDual T)) := by @@ -107,41 +98,30 @@ theorem polarity (Ω : Type*) : simp only [Pi.le_def, le_Prop_eq] exact (polarity_iff Ω (ofDual T) E).symm -/-- Every test in `T` respects the equivalence `T` induces — the counit - `l (u b) ≤ b` of `polarity`, read back through the dual. -/ +/-- Every test in `T` respects the equivalence `T` induces. -/ theorem test_subset_respects_induced (Ω : Type*) (T : Set (Proc → Ω)) : T ⊆ respects Ω (induced Ω T) := (polarity Ω).l_u_le (toDual T) -/-- Closure operator on equivalences: `induced Ω ∘ respects Ω`, obtained from - `polarity` via Mathlib's `GaloisConnection.closureOperator`. -/ +/-- Closure operator `induced Ω ∘ respects Ω`, obtained from `polarity` as a + `ClosureOperator`. -/ def cl (Ω : Type*) : ClosureOperator (Proc → Proc → Prop) := (polarity (Proc := Proc) Ω).closureOperator -/-- `cl Ω` acts as `induced Ω ∘ respects Ω`. -/ +/-- `cl Ω E = induced Ω (respects Ω E)`. -/ theorem cl_apply (Ω : Type*) (E : Proc → Proc → Prop) : cl Ω E = induced Ω (respects Ω E) := rfl -/-- `cl Ω` is extensive: `E ≤ cl Ω E` — inherited from `ClosureOperator`. -/ -theorem cl_extensive (Ω : Type*) (E : Proc → Proc → Prop) : E ≤ cl Ω E := - (cl Ω).le_closure E - -/-- `cl Ω` is monotone — inherited from `ClosureOperator`. -/ -theorem cl_monotone (Ω : Type*) : Monotone (cl (Proc := Proc) Ω) := - (cl Ω).monotone - -/-- `cl Ω` is idempotent — inherited from `ClosureOperator`. -/ -theorem cl_idempotent (Ω : Type*) (E : Proc → Proc → Prop) : - cl Ω (cl Ω E) = cl Ω E := - (cl Ω).idempotent E - -/-- An equivalence is TESTABLE iff it is exactly "indistinguishability under - the tests that respect it" — i.e. a closed element of `cl Ω`. -/ +/-- An equivalence is *testable* iff it is a closed element of `cl Ω`. -/ def Testable (Ω : Type*) (E : Proc → Proc → Prop) : Prop := (cl Ω).IsClosed E -/-- Pointwise reading of `Testable`: `cl Ω E` and `E` agree on every pair. -/ +/-- The **van Glabbeek spectrum**: the set of testable equivalences on `Proc`. -/ +def spectrum (Ω : Type*) : Set (Proc → Proc → Prop) := + { E | Testable Ω E } + +/-- `Testable Ω E` iff `cl Ω E` and `E` agree pointwise. -/ theorem testable_iff (Ω : Type*) (E : Proc → Proc → Prop) : Testable Ω E ↔ ∀ p q, cl Ω E p q ↔ E p q := by rw [Testable, ClosureOperator.isClosed_iff] @@ -152,17 +132,12 @@ theorem testable_iff (Ω : Type*) (E : Proc → Proc → Prop) : funext p q exact propext (h p q) -/-- Every induced equivalence is testable (the image of `induced Ω` is - contained in the closed elements) — this is `u ∘ l ∘ u = u` for `polarity` - (`GaloisConnection.u_l_u_eq_u`). -/ +/-- Every induced equivalence is testable. -/ theorem induced_testable (Ω : Type*) (T : Set (Proc → Ω)) : Testable Ω (induced Ω T) := (cl Ω).isClosed_iff.2 ((polarity Ω).u_l_u_eq_u (toDual T)) -/-- **Spectrum = image of `induced` = closed elements.** An equivalence is - testable (a closed element of `cl Ω`) iff it is exactly the equivalence - induced by some test class. Forward direction witnessed by - `T = respects Ω E`. -/ +/-- An equivalence is testable iff it is induced by some test class. -/ theorem spectrum_eq_closed_elements (Ω : Type*) (E : Proc → Proc → Prop) : Testable Ω E ↔ ∃ T : Set (Proc → Ω), induced Ω T = E := by constructor @@ -171,13 +146,8 @@ theorem spectrum_eq_closed_elements (Ω : Type*) (E : Proc → Proc → Prop) : · rintro ⟨T, rfl⟩ exact induced_testable Ω T -/-- **The spectrum is a complete lattice.** The closed elements of `cl Ω` — the - testable equivalences — form a complete lattice under refinement, lifted - through the Galois insertion `(cl Ω).gi` from the complete lattice of all - equivalences (Mathlib's `GaloisInsertion.liftCompleteLattice`). Arbitrary - meets and joins of testable equivalences exist; and the lattice is not a - chain (`Spectrum.Antichain`), which is the structural form of "the - linear-time/branching-time spectrum is a lattice, not a linear scale". -/ +/-- The spectrum is a complete lattice under refinement; it is not a chain + (see `Spectrum.Antichain`). -/ instance spectrumCompleteLattice {Ω : Type*} : CompleteLattice ((cl (Proc := Proc) Ω).Closeds) := (cl Ω).gi.liftCompleteLattice diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean index 16a8ba6e5..6dbf9d835 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/TracePoint.lean @@ -13,21 +13,13 @@ public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois /-! # Spectrum trace point — trace equivalence is Galois-closed -A concrete named spectrum point: CSLib's homogeneous trace equivalence -(`Cslib.LTS.HomTraceEq`) is a Galois-closed (testable) equivalence, via the -trace-set observer test class (`fun s => lts.traces s`, `Ω = Set (List Label)`). -`HomTraceEq` lies in the image of `induced`, hence is a fixed point of the -closure operator `cl`. +CSLib's homogeneous trace equivalence (`HomTraceEq`) is a Galois-closed +(testable) equivalence: it is the equivalence induced by the trace-set observer +test class (`Ω = Set (List Label)`), hence a fixed point of the closure operator +`cl`. -This proves the structural result (TraceEq ∈ closed elements). The standard -testing-semantics refinement — one `Bool` test per trace — gives a finer witness -for the SAME closed element but requires decidability of trace membership; it -does not change the closed-element verdict. - -The Hennessy–Milner theorem IS mechanised in CSLib as -`Cslib.Logic.HML.theoryEq_eq_bisimilarity`; the bisim point built on it is in -`Spectrum.BisimPoint`. This file (the trace point, kernel-trivial bottom) does -not use HM — bisimilarity (HM-mediated top) is the companion point there. +The companion bisimilarity point (which uses the Hennessy–Milner theorem) is in +`Spectrum.BisimPoint`. -/ @[expose] public section @@ -58,7 +50,7 @@ theorem induced_traceSet_iff (p q : State) : subst ht exact h -/-- Function-equality form (via `propext`). -/ +/-- Function-equality form of `induced_traceSet_iff`. -/ theorem induced_traceSet : induced (Set (List Label)) (traceTestClass lts) = HomTraceEq lts := by funext p q diff --git a/references.bib b/references.bib index af8b4187e..22207e2d9 100644 --- a/references.bib +++ b/references.bib @@ -40,7 +40,7 @@ @book{Baader1998 } @misc{Beohar2022, - author = {Beohar, Harsh}, + author = {Beohar, Harsh and Gurke, Sebastian and K{\"o}nig, Barbara and Messing, Karla}, title = {Hennessy-Milner Theorems via Galois Connections}, year = {2022}, eprint = {2207.05407}, From f47e1a17e4996b9c3fe23713548886977ab741d4 Mon Sep 17 00:00:00 2001 From: patchwright Date: Fri, 24 Jul 2026 15:57:03 +0200 Subject: [PATCH 09/12] feat(LTS/Spectrum): may-testing equivalence as a Galois-closed spectrum point Follow-up to #713 (van Glabbeek spectrum as a Galois connection). Adds a named spectrum point: may-testing equivalence (De Nicola-Hennessy), defined over CCS with a distinguished success action. mayPass p T holds when p || T can weakly perform success; MayEquiv = pass the same tests. By definition the induced equivalence of the may-test observer class, hence closed (TracePoint-style definitional point, not a deep theorem like BisimPoint). Builds clean, 0 sorry/0 axiom. --- .../LTS/Spectrum/MayTestingPoint.lean | 103 ++++++++++++++++++ 1 file changed, 103 insertions(+) create mode 100644 Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean new file mode 100644 index 000000000..eae68a560 --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 patchwright. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: patchwright +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois +public import Cslib.Languages.CCS.Basic +public import Cslib.Languages.CCS.Semantics +public import Cslib.Foundations.Semantics.LTS.HasTau + +/-! +# Spectrum may-testing point — may-testing equivalence is Galois-closed + +A named point of the van Glabbeek spectrum: (may-)testing equivalence +[De Nicola & Hennessy, 1984]. A *test* is a process together with a distinguished +*success* action; a process `p` *may pass* a test `T` when some computation of +`p ∥ T` performs the success action. Two processes are may-testing-equivalent +when they may-pass exactly the same tests. + +Unlike the bisim point — where bisimilarity is connected to the spectrum via the +Hennessy–Milner theorem — may-testing equivalence is, by its standard +definition, exactly the equivalence induced by the class of may-test observers. +Its closedness is therefore definitional (as for `Spectrum.TracePoint`): it is +`induced` of the may-test class, and every induced equivalence is testable. + +## References + +* [R. De Nicola & M. Hennessy, *Testing Equivalences for Processes*][DeNicolaHennessy1984]. +-/ + +@[expose] public section + +namespace Cslib.LTS.Spectrum + +open Cslib CCS + +variable + {Name : Type u} + {Constant : Type v} + +/-- `p` *may pass* test `T`: some computation of `p ∥ T` performs `success` + (a weak `success` transition of the parallel composition). -/ +def mayPass (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p T : CCS.Process Name Constant) : Prop := + ∃ s', STr (CCS.lts (defs := defs)) (Process.par p T) success s' + +/-- May-testing equivalence: `p` and `q` may-pass exactly the same tests. -/ +def MayEquiv (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p q : CCS.Process Name Constant) : Prop := + ∀ T, mayPass defs success p T ↔ mayPass defs success q T + +/-- The may-test observer of a process: the set of tests it may-pass. -/ +def mayTests (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p : CCS.Process Name Constant) : + Set (CCS.Process Name Constant) := + { T | mayPass defs success p T } + +/-- Test class for the may-testing point: the singleton may-test observer. -/ +def mayTestClass (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) : + Set (CCS.Process Name Constant → Set (CCS.Process Name Constant)) := + { f | f = mayTests defs success } + +/-- The equivalence induced by the may-test observer is may-testing equivalence. -/ +theorem induced_mayTests_iff (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p q : CCS.Process Name Constant) : + induced (Set (CCS.Process Name Constant)) (mayTestClass defs success) p q ↔ + MayEquiv defs success p q := by + simp only [induced, mayTestClass, Set.mem_setOf_eq, MayEquiv] + constructor + · intro h T + have heq : mayTests defs success p = mayTests defs success q := + h (mayTests defs success) rfl + rw [Set.ext_iff] at heq + simp only [mayTests, Set.mem_setOf_eq] at heq + exact heq T + · intro h f hf + subst hf + ext T + simp only [mayTests, Set.mem_setOf_eq] + exact h T + +/-- Function-equality form of `induced_mayTests_iff`. -/ +theorem induced_mayTests (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) : + induced (Set (CCS.Process Name Constant)) (mayTestClass defs success) = + MayEquiv defs success := by + funext p q + exact propext (induced_mayTests_iff defs success p q) + +/-- **May-testing point.** May-testing equivalence is a closed element of the + spectrum: it is testable for a CCS LTS with a distinguished success action. -/ +theorem MayEquiv_testable (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) : + Testable (Set (CCS.Process Name Constant)) (MayEquiv defs success) := by + rw [← induced_mayTests defs success] + exact induced_testable (Set (CCS.Process Name Constant)) (mayTestClass defs success) + +end Cslib.LTS.Spectrum From bbaa4827ddc2f00663647e1b68a3ccb6ad6a0c25 Mon Sep 17 00:00:00 2001 From: patchwright Date: Fri, 24 Jul 2026 18:44:25 +0200 Subject: [PATCH 10/12] feat(LTS/Spectrum): must-testing point; align may-pass to strong computation-based MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Companion to may-testing: must-testing equivalence (De Nicola-Hennessy) as a Galois-closed spectrum point. mustPass p T holds when every MAXIMAL computation of p||T performs success — maximal = finite execution ending in a stuck state (no outgoing transition) OR an infinite OmegaExecution. So divergence-without- success and deadlock-without-success both fail must. Also aligns mayPass to the strong, computation-based notion (success among a multistep's labels) so may/must are a consistent pair. Both 0 sorry/0 axiom; builds clean. --- .../LTS/Spectrum/MayTestingPoint.lean | 5 +- .../LTS/Spectrum/MustTestingPoint.lean | 119 ++++++++++++++++++ 2 files changed, 122 insertions(+), 2 deletions(-) create mode 100644 Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean index eae68a560..5aaecc8c5 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/MayTestingPoint.lean @@ -43,10 +43,11 @@ variable {Constant : Type v} /-- `p` *may pass* test `T`: some computation of `p ∥ T` performs `success` - (a weak `success` transition of the parallel composition). -/ + (it appears among the labels of a multistep computation of the parallel + composition). Strong, matching `MustTestingPoint.mustPass`. -/ def mayPass (defs : Constant → CCS.Process Name Constant → Prop) (success : CCS.Act Name) (p T : CCS.Process Name Constant) : Prop := - ∃ s', STr (CCS.lts (defs := defs)) (Process.par p T) success s' + ∃ μs s', (CCS.lts (defs := defs)).MTr (Process.par p T) μs s' ∧ success ∈ μs /-- May-testing equivalence: `p` and `q` may-pass exactly the same tests. -/ def MayEquiv (defs : Constant → CCS.Process Name Constant → Prop) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean new file mode 100644 index 000000000..ad5f04ded --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2026 patchwright. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: patchwright +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois +public import Cslib.Foundations.Semantics.LTS.Spectrum.MayTestingPoint +public import Cslib.Languages.CCS.Basic +public import Cslib.Languages.CCS.Semantics +public import Cslib.Foundations.Semantics.LTS.Execution +public import Cslib.Foundations.Semantics.LTS.OmegaExecution + +/-! +# Spectrum must-testing point — must-testing equivalence is Galois-closed + +The companion to `Spectrum.MayTestingPoint`. A process `p` *must pass* a test +`T` when **every maximal computation** of `p ∥ T` performs the success action. +A maximal computation is either a finite execution whose final state is stuck +(no outgoing transition), or an infinite (`OmegaExecution`) one — so divergence +without success fails must, as does deadlock without success. Two processes are +must-testing-equivalent when they must-pass exactly the same tests. + +Like may-testing, must-testing equivalence is by definition the equivalence +induced by the class of must-test observers, so its closedness is definitional +(`induced_testable`). + +## References + +* [R. De Nicola & M. Hennessy, *Testing Equivalences for Processes*][DeNicolaHennessy1984]. +-/ + +@[expose] public section + +namespace Cslib.LTS.Spectrum + +open Cslib CCS + +variable + {Name : Type u} + {Constant : Type v} + +/-- A state is *stuck* if it has no outgoing transition: a finite execution + ending in a stuck state is maximal (cannot be extended). -/ +def Stuck (lts : LTS State Label) (s : State) : Prop := + ¬ ∃ μ s', lts.Tr s μ s' + +/-- `p` *must pass* test `T`: every maximal computation of `p ∥ T` performs + `success`. A maximal computation is either a finite execution ending in a + stuck state, or an infinite `OmegaExecution`; in both, success must appear + among the labels. Divergence-without-success and deadlock-without-success + both fail must. -/ +def mustPass (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p T : CCS.Process Name Constant) : Prop := + (∀ μs s₂ ss, + (CCS.lts (defs := defs)).Execution (Process.par p T) μs s₂ ss → + Stuck (CCS.lts (defs := defs)) s₂ → + success ∈ μs) ∧ + (∀ ss μs, + (CCS.lts (defs := defs)).OmegaExecution ss μs → + ss 0 = Process.par p T → + ∃ i, μs i = success) + +/-- Must-testing equivalence: `p` and `q` must-pass exactly the same tests. -/ +def MustEquiv (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p q : CCS.Process Name Constant) : Prop := + ∀ T, mustPass defs success p T ↔ mustPass defs success q T + +/-- The must-test observer of a process: the set of tests it must-pass. -/ +def mustTests (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p : CCS.Process Name Constant) : + Set (CCS.Process Name Constant) := + { T | mustPass defs success p T } + +/-- Test class for the must-testing point: the singleton must-test observer. -/ +def mustTestClass (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) : + Set (CCS.Process Name Constant → Set (CCS.Process Name Constant)) := + { f | f = mustTests defs success } + +/-- The equivalence induced by the must-test observer is must-testing equivalence. -/ +theorem induced_mustTests_iff (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) (p q : CCS.Process Name Constant) : + induced (Set (CCS.Process Name Constant)) (mustTestClass defs success) p q ↔ + MustEquiv defs success p q := by + simp only [induced, mustTestClass, Set.mem_setOf_eq, MustEquiv] + constructor + · intro h T + have heq : mustTests defs success p = mustTests defs success q := + h (mustTests defs success) rfl + rw [Set.ext_iff] at heq + simp only [mustTests, Set.mem_setOf_eq] at heq + exact heq T + · intro h f hf + subst hf + ext T + simp only [mustTests, Set.mem_setOf_eq] + exact h T + +/-- Function-equality form of `induced_mustTests_iff`. -/ +theorem induced_mustTests (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) : + induced (Set (CCS.Process Name Constant)) (mustTestClass defs success) = + MustEquiv defs success := by + funext p q + exact propext (induced_mustTests_iff defs success p q) + +/-- **Must-testing point.** Must-testing equivalence is a closed element of the + spectrum: it is testable for a CCS LTS with a distinguished success action. -/ +theorem MustEquiv_testable (defs : Constant → CCS.Process Name Constant → Prop) + (success : CCS.Act Name) : + Testable (Set (CCS.Process Name Constant)) (MustEquiv defs success) := by + rw [← induced_mustTests defs success] + exact induced_testable (Set (CCS.Process Name Constant)) (mustTestClass defs success) + +end Cslib.LTS.Spectrum From af4f7d7f4721e59d250b0393e0786697762b47f8 Mon Sep 17 00:00:00 2001 From: patchwright Date: Sun, 26 Jul 2026 04:39:04 +0200 Subject: [PATCH 11/12] chore(mk_all): wire MayTestingPoint + MustTestingPoint into Cslib.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generated by 'lake exe mk_all --check' verification (confirmed: no diff after this edit — the manual insertion matches the auto-generated order). --- Cslib.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cslib.lean b/Cslib.lean index 6761991aa..64c1a5101 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -101,6 +101,8 @@ public import Cslib.Foundations.Semantics.LTS.Simulation public import Cslib.Foundations.Semantics.LTS.Spectrum.Antichain public import Cslib.Foundations.Semantics.LTS.Spectrum.BisimPoint public import Cslib.Foundations.Semantics.LTS.Spectrum.Galois +public import Cslib.Foundations.Semantics.LTS.Spectrum.MayTestingPoint +public import Cslib.Foundations.Semantics.LTS.Spectrum.MustTestingPoint public import Cslib.Foundations.Semantics.LTS.Spectrum.TracePoint public import Cslib.Foundations.Semantics.LTS.Termination public import Cslib.Foundations.Semantics.LTS.Total From 3603710a3587eb00ae39d875e49806af72aa4e5e Mon Sep 17 00:00:00 2001 From: patchwright Date: Sun, 26 Jul 2026 14:28:31 +0200 Subject: [PATCH 12/12] refactor(MustTestingPoint): reuse Cslib.LTS.Stuck instead of a local redefinition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cslib.Foundations.Semantics.LTS.Termination already defines Stuck (lts) (Terminated) (s) := ¬Terminated s ∧ ¬∃ μ s', lts.Tr s μ s'. The local redefinition here duplicated that name/concept. Instantiating the existing one with Terminated := fun _ => False is propositionally equivalent to the local def (¬False ∧ P ↔ P) and follows #713's own stated principle (specification over restatement) instead of contradicting it. Verified: full lake build 0 errors (2764/2764), mk_all --check clean, checkInitImports clean, 0 sorry/0 axiom. --- .../Semantics/LTS/Spectrum/MustTestingPoint.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean b/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean index ad5f04ded..a2e0c8305 100644 --- a/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean +++ b/Cslib/Foundations/Semantics/LTS/Spectrum/MustTestingPoint.lean @@ -13,6 +13,7 @@ public import Cslib.Languages.CCS.Basic public import Cslib.Languages.CCS.Semantics public import Cslib.Foundations.Semantics.LTS.Execution public import Cslib.Foundations.Semantics.LTS.OmegaExecution +public import Cslib.Foundations.Semantics.LTS.Termination /-! # Spectrum must-testing point — must-testing equivalence is Galois-closed @@ -43,21 +44,21 @@ variable {Name : Type u} {Constant : Type v} -/-- A state is *stuck* if it has no outgoing transition: a finite execution - ending in a stuck state is maximal (cannot be extended). -/ -def Stuck (lts : LTS State Label) (s : State) : Prop := - ¬ ∃ μ s', lts.Tr s μ s' - /-- `p` *must pass* test `T`: every maximal computation of `p ∥ T` performs `success`. A maximal computation is either a finite execution ending in a stuck state, or an infinite `OmegaExecution`; in both, success must appear among the labels. Divergence-without-success and deadlock-without-success - both fail must. -/ + both fail must. + + "Stuck" reuses `Cslib.LTS.Stuck`, instantiated with the trivial + `Terminated := fun _ => False`: testing has no independent notion of a + designated terminal state, so a state counts as a testing endpoint exactly + when it has no outgoing transition (`¬False ∧ ¬∃ … ↔ ¬∃ …`). -/ def mustPass (defs : Constant → CCS.Process Name Constant → Prop) (success : CCS.Act Name) (p T : CCS.Process Name Constant) : Prop := (∀ μs s₂ ss, (CCS.lts (defs := defs)).Execution (Process.par p T) μs s₂ ss → - Stuck (CCS.lts (defs := defs)) s₂ → + Cslib.LTS.Stuck (CCS.lts (defs := defs)) (fun _ => False) s₂ → success ∈ μs) ∧ (∀ ss μs, (CCS.lts (defs := defs)).OmegaExecution ss μs →