Define the category of LTSs by ayberkt · Pull Request #391 · leanprover/cslib

ayberkt · 2026-03-02T23:09:17Z

This PR resolves #387.

Cslib/Foundations/Semantics/LTS/Category.lean

fmontesi · 2026-03-03T07:35:20Z

Cslib/Foundations/Semantics/LTS/Category.lean

+variable (lts₁ : LTS State₁ Label₁)
+variable (lts₂ : LTS State₂ Label₂)
+variable (lts₃ : LTS State₃ Label₃)
+


From what I see below, you don't need these lts variables that much? Consider removing them maybe?

fmontesi · 2026-03-03T07:37:20Z

Cslib/Foundations/Semantics/LTS/Category.lean

+
+@[expose] public section
+
+variable {State Label State₃ Label₃ State₁ State₂ Label₁ Label₂ : Type}


Type is too restrictive here, you want each type to be in its own universe to state the definitions below more generally. I suggest uᵢ for the States and vᵢ for the labels.

fmontesi · 2026-03-03T07:37:48Z

Cslib/Foundations/Semantics/LTS/Category.lean

+
+/-- A morphism between two labelled transition systems, consisting of a function on states, a
+function on labels, and a proof that transitions are preserved. -/
+structure LTSMorphism (lts₁ : LTS State₁ Label₁) (lts₂ : LTS State₂ Label₂) : Type where


The resulting type should live in the max of the universes of the params.

Cslib/Foundations/Semantics/LTS/Category.lean

fmontesi · 2026-03-03T07:47:25Z

Cslib/Foundations/Semantics/LTS/Category.lean

+/-- A morphism between two labelled transition systems, consisting of a function on states, a
+function on labels, and a proof that transitions are preserved. -/
+structure LTSMorphism (lts₁ : LTS State₁ Label₁) (lts₂ : LTS State₂ Label₂) : Type where
+  toFun : State₁ → State₂


I'm a bit confused by the names. I suggest: stateMap, labelMap, and labelMap_tr.

fmontesi · 2026-03-03T07:48:02Z

Cslib/Foundations/Semantics/LTS/Category.lean

+function on labels, and a proof that transitions are preserved. -/
+structure LTSMorphism (lts₁ : LTS State₁ Label₁) (lts₂ : LTS State₂ Label₂) : Type where
+  toFun : State₁ → State₂
+  labelMap : Label₁ → Label₂


Reading from the reference you provided on Zulip, this function is supposed to be partial. Is it a conscious decision to make it total here?

Good point. I wasn’t sure about this. I’ve definitely seen it defined like this elsewhere, but it might be better to stick with the definitions from the Winskel and Nielsen reference as it is quite standard. I will update the definition.

I am also looking at Daniel Mroz’s PhD thesis and the category of LTSs there is over a fixed label set.

It is common in category theory formalization to have some encoding of partial functions though dependent types, so I wasn't particularly surprised by this definition. Please see my reviews below however, I believe these definitions have a more fundamental problem.

fmontesi · 2026-03-03T07:48:15Z

Cslib/Foundations/Semantics/LTS/Category.lean

+variable (lts₃ : LTS State₃ Label₃)
+
+/-!
+# Category of Labelled Transition Systems


Would be good to add a reference.

fmontesi · 2026-03-03T07:49:45Z

Not urgent, but please fix the title of the PR at some point to start with the required feat: prefix, or CI won't let us merge this.

chenson2018 · 2026-03-03T11:41:50Z

Cslib/Foundations/Semantics/LTS/Category.lean

+def LTS.Morphism.id (lts : LTS State Label) : LTS.Morphism lts lts :=
+  { toFun                     := _root_.id
+  , labelMap                  := _root_.id
+  , fun_preserves_transitions := fun _ _ _ h => h
+  }


A couple of style points:

you can use where with def as well for better readability

please eliminate the extra whitespace here and everywhere else. I personally like it too aesthetically, but we prioritize the uniformity of the Mathlib style.

For fun_preserves_transitions move parameters to the left for clarity

All together this gives:

Suggested change

def LTS.Morphism.id (lts : LTS State Label) : LTS.Morphism lts lts :=

{ toFun := _root_.id

, labelMap := _root_.id

, fun_preserves_transitions := fun _ _ _ h => h

}

def LTS.Morphism.id (lts : LTS State Label) : LTS.Morphism lts lts where

toFun := _root_.id

labelMap := _root_.id

fun_preserves_transitions _ _ _ h := h

chenson2018 · 2026-03-03T12:02:55Z

Cslib/Foundations/Semantics/LTS/Category.lean

+
+/-- A morphism between two labelled transition systems, consisting of a function on states, a
+function on labels, and a proof that transitions are preserved. -/
+structure LTS.Morphism (lts₁ : LTS State₁ Label₁) (lts₂ : LTS State₂ Label₂) : Type where


More significantly this needs to follow suit with Mathlib's concrete categories such as AddMonCat, AlgCat, GrpCat, etc. As I describe below, I think you end up formalizing a definition different from what you are intending.

I would expect this structure to follow their naming and to similarly bundle a separately defined type of LTS homomorphism.

chenson2018 · 2026-03-03T12:05:17Z

Cslib/Foundations/Semantics/LTS/Category.lean

+  fun_preserves_transitions : (s s' : State₁)
+                            → (l : Label₁)
+                            → lts₁.Tr s l s'
+                            → lts₂.Tr (toFun s) (labelMap l) (toFun s')


Style-wise this should go mostly on one line

Suggested change

fun_preserves_transitions : (s s' : State₁)

→ (l : Label₁)

→ lts₁.Tr s l s'

→ lts₂.Tr (toFun s) (labelMap l) (toFun s')

fun_preserves_transitions (s s' : State₁) (l : Label₁) :

lts₁.Tr s l s' → lts₂.Tr (toFun s) (labelMap l) (toFun s')

chenson2018 · 2026-03-03T12:07:43Z

Cslib/Foundations/Semantics/LTS/Category.lean

+/-! ## LTSs and LTS morphisms form a category -/
+
+/-- `LTS.Morphism` provides a category structure on the `LTS` type. -/
+instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) where


You shouldn't define this separately from the Category instance.

chenson2018 · 2026-03-03T12:16:42Z

Cslib/Foundations/Semantics/LTS/Category.lean

+  comp {lts₁} {lts₂} {lts₃} := LTS.Morphism.comp lts₁ lts₂ lts₃
+
+/-- Proof that the above structure actually forms a category. -/
+instance {State Label : Type} : CategoryTheory.Category (LTS State Label) where


You'll see in the examples I link above that they would define a fully bundled equivalent

structure LTSCat where State : Type u Label : Type v str : LTS State Label

Otherwise, we aren't talking about the category of LTSs where morphisms are between LTS with different states/labels, because a polymorphic instance like this is defining a category for each state/label type.

It might be best also to go ahead and have the module structure match up as Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean since it looks like you have immediate plans to extend this further.

ctchou · 2026-03-03T13:39:58Z

Cslib/Foundations/Semantics/LTS/Category.lean

+
+/- Remark: I do not like the name 'bundled LTS'; and LTS is already the bundled notion. The name
+   `LTS` for the transition relation on a fixed set of states and labels is what is confusing here.
+    I propose to change that to `LTS-Structure` and call the above `LTS`.


I hope not. LTS is used in many, many places already. We should keep its short name.

Rest assured we will not change this name. As I say above, in alignment with Mathlib it should be LTSCat. (And will not affect any of your existing work)

Also

LTS is already the bundled notion

makes me think we have a mismatch in terminology that might be a Lean colloquialism. Could you clarify what you mean by this @ayberkt?

ayberkt added 7 commits March 2, 2026 22:50

Write down the structure of the category of LTSs

99efff2

Prove that these form a category

ec7b48e

Replace unused variable names with underscores

28840c2

Improve cosmetics

33d6785

Add comment

528040d

Add Markdown sections

691b443

Improve naming

3a7993f

ayberkt requested review from chenson2018 and fmontesi as code owners March 2, 2026 23:09

fmontesi requested changes Mar 3, 2026

View reviewed changes

ayberkt added 2 commits March 3, 2026 11:07

Re-order variables

dc216e3

Put LTSMorphism under the LTS namespace

2d068c3

chenson2018 requested changes Mar 3, 2026

View reviewed changes

ayberkt added 3 commits March 3, 2026 13:13

Fix the definition of the category of LTSs

487c4f3

Use the notion of BundledLTS everywhere

c942d95

Tweak

dc6ba49

ctchou reviewed Mar 3, 2026

View reviewed changes


		@[expose] public section

		variable {State Label State₃ Label₃ State₁ State₂ Label₁ Label₂ : Type}

Conversation

ayberkt commented Mar 2, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chenson2018 Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fmontesi commented Mar 3, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

chenson2018 Mar 3, 2026 •

edited

Loading