feat(LTS/Spectrum): may- and must-testing equivalence as Galois-closed points - #752
Closed
patchwright wants to merge 12 commits into
Closed
feat(LTS/Spectrum): may- and must-testing equivalence as Galois-closed points#752patchwright wants to merge 12 commits into
patchwright wants to merge 12 commits into
Conversation
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).
…ing + authors 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.
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.
Addresses ctchou's review on leanprover#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.
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.
…te lattice 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.
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.
Per ctchou's 2026-07-19 review of leanprover#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).
…um point Follow-up to leanprover#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.
…utation-based 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.
Generated by 'lake exe mk_all --check' verification (confirmed: no diff after this edit — the manual insertion matches the auto-generated order).
…redefinition 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 leanprover#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.
Collaborator
|
Please see my comments on #713 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
A follow-up to #713 (van Glabbeek spectrum as a Galois connection). Adds two
more named points to the spectrum: may-testing and must-testing
equivalence [De Nicola & Hennessy, 1984] — the classical testing-equivalence
pair that gives the framework in #713 its name.
What's added
Two new modules in
Cslib.Foundations.Semantics.LTS.Spectrum(imports wiredinto
Cslib.lean,lake exe mk_all --checkconfirms no diff):MayTestingPoint.lean—MayEquiv_testable: may-testing equivalence(
pmay-passes the same tests asq) is Galois-closed. Definitional, likeTracePoint: it isinducedof the may-test observer class.MustTestingPoint.lean—MustEquiv_testable: must-testing equivalence(every maximal computation of
p ∥ Tsucceeds) is Galois-closed. Alsodefinitional. "Maximal computation" covers both finite-and-stuck and
infinite (
OmegaExecution) runs, so divergence-without-success anddeadlock-without-success both correctly fail
must.Both are instantiated concretely over CCS (
Cslib.Languages.CCS), matchingthe existing point files' pattern.
Why it's additive
#713established the Galois-connection framework and two points (trace,bisimilarity). May- and must-testing are the equivalences the testing
literature is actually about — De Nicola–Hennessy is the paper the framework
is named after — so this is the natural next pair, not a new direction. It
does not touch
Galois.leanor either existing point file.Scope notes / honesty
TracePoint— no theorem does theconnective work
BisimPoint's Hennessy–Milner step does. That's expected:may/must-testing equivalences are defined as induced-by-test-observers in
the source literature, unlike bisimilarity.
must's "maximal computation" clause requires both the finite-stuck caseand the
OmegaExecutioncase to succeed, matching the standard must-testingdefinition (no silent divergence escape).
mustPass's "stuck" condition reusesCslib.LTS.Stuck(fromFoundations/Semantics/LTS/Termination.lean), instantiated withTerminated := fun _ => False, rather than introducing a second localnotion — testing has no independent designated-terminal-state concept, so
a state is a testing endpoint exactly when it has no outgoing transition,
and
¬False ∧ P ↔ Pmakes the instantiation propositionally exact.Verification
Full
lake build: 0 errors, 2764/2764 jobs.lake exe mk_all --check: nodiff.
lake exe checkInitImports: clean. 0sorry/ 0axiomin both newfiles.
AI use disclosure
Per CSLib's AI policy (following Mathlib): this contribution was developed
with AI assistance, same disclosure as #713.
Open questions for maintainers
Galois.leanAPI change lands there first — this PR doesn't depend on anypending change to feat(LTS/Spectrum): van Glabbeek spectrum as a Galois connection #713, but a rename there would need a follow-up here.