From 99efff2385903b393902bba52d9c551ed71f09c8 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 22:50:01 +0000 Subject: [PATCH 01/12] Write down the structure of the category of LTSs --- Cslib/Foundations/Semantics/LTS/Category.lean | 54 +++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 Cslib/Foundations/Semantics/LTS/Category.lean diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean new file mode 100644 index 00000000..a1b2b18f --- /dev/null +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -0,0 +1,54 @@ +/- +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ayberk Tosun +-/ + +module + +public import Cslib.Foundations.Semantics.LTS.Basic +public import Mathlib.CategoryTheory.Category.Basic +open Cslib + +@[expose] public section + +variable {State Label State₃ Label₃ State₁ State₂ Label₁ Label₂ : Type} +variable (lts₁ : LTS State₁ Label₁) +variable (lts₂ : LTS State₂ Label₂) +variable (lts₃ : LTS State₃ Label₃) + +/-! +# Category of Labelled Transition Systems +-/ + +/-- 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₂ + lam : Label₁ → Label₂ + fun_preserves_transitions : (s s' : State₁) + → (l : Label₁) + → lts₁.Tr s l s' + → lts₂.Tr (toFun s) (lam l) (toFun s') + +/-- The identity LTS morphism. -/ +def LTSMorphism.id (lts : LTS State Label) : LTSMorphism lts lts := + { toFun := _root_.id + , lam := _root_.id + , fun_preserves_transitions := fun _ _ _ h => h + } + +/-- Composition of LTS morphisms. -/ +def LTSMorphism.comp : LTSMorphism lts₁ lts₂ → LTSMorphism lts₂ lts₃ → LTSMorphism lts₁ lts₃ := + fun ⟨f, μ, p⟩ ⟨g, ν, q⟩ => + let r := by intros s s' l h + apply q + apply p + exact h + ⟨g ∘ f, ν ∘ μ, r⟩ + +/-- `LTSMorphism` provides a category structure on the `LTS` type. -/ +instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) := + { Hom := LTSMorphism + , id := LTSMorphism.id + , comp {lts₁} {lts₂} {lts₃} := LTSMorphism.comp lts₁ lts₂ lts₃ + } From ec7b48e13cb984b0da1e0a4d43e5bc63a63dbc46 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 22:56:18 +0000 Subject: [PATCH 02/12] Prove that these form a category --- Cslib/Foundations/Semantics/LTS/Category.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index a1b2b18f..462fbe59 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -52,3 +52,19 @@ instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) , id := LTSMorphism.id , comp {lts₁} {lts₂} {lts₃} := LTSMorphism.comp lts₁ lts₂ lts₃ } + +instance {State Label : Type} : CategoryTheory.Category (LTS State Label) where + id_comp := by + intro _ _ f + cases f + rfl + comp_id := by + intro _ _ f + cases f + rfl + assoc := by + intro _ _ _ _ f g h + cases f + cases g + cases h + rfl From 28840c2f6d44ecc8240d07c5ad9df00880795030 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 22:56:33 +0000 Subject: [PATCH 03/12] Replace unused variable names with underscores --- Cslib/Foundations/Semantics/LTS/Category.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 462fbe59..dd33b713 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -40,7 +40,7 @@ def LTSMorphism.id (lts : LTS State Label) : LTSMorphism lts lts := /-- Composition of LTS morphisms. -/ def LTSMorphism.comp : LTSMorphism lts₁ lts₂ → LTSMorphism lts₂ lts₃ → LTSMorphism lts₁ lts₃ := fun ⟨f, μ, p⟩ ⟨g, ν, q⟩ => - let r := by intros s s' l h + let r := by intros _ _ _ h apply q apply p exact h From 33d6785ee782552dd757350e4b125540826644f9 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 22:57:17 +0000 Subject: [PATCH 04/12] Improve cosmetics --- Cslib/Foundations/Semantics/LTS/Category.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index dd33b713..4eae6f06 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -47,11 +47,10 @@ def LTSMorphism.comp : LTSMorphism lts₁ lts₂ → LTSMorphism lts₂ lts₃ ⟨g ∘ f, ν ∘ μ, r⟩ /-- `LTSMorphism` provides a category structure on the `LTS` type. -/ -instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) := - { Hom := LTSMorphism - , id := LTSMorphism.id - , comp {lts₁} {lts₂} {lts₃} := LTSMorphism.comp lts₁ lts₂ lts₃ - } +instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) where + Hom := LTSMorphism + id := LTSMorphism.id + comp {lts₁} {lts₂} {lts₃} := LTSMorphism.comp lts₁ lts₂ lts₃ instance {State Label : Type} : CategoryTheory.Category (LTS State Label) where id_comp := by From 528040dca80d3d95490188300a4ab8c1184fdaca Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 22:59:40 +0000 Subject: [PATCH 05/12] Add comment --- Cslib/Foundations/Semantics/LTS/Category.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 4eae6f06..f376f002 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -52,6 +52,7 @@ instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) id := LTSMorphism.id comp {lts₁} {lts₂} {lts₃} := LTSMorphism.comp lts₁ lts₂ lts₃ +/-- Proof that the above structure actually forms a category. -/ instance {State Label : Type} : CategoryTheory.Category (LTS State Label) where id_comp := by intro _ _ f From 691b4432ded4ccbfd2002e65d1af767007bfd9a6 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 23:04:15 +0000 Subject: [PATCH 06/12] Add Markdown sections --- Cslib/Foundations/Semantics/LTS/Category.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index f376f002..3e20f771 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -20,6 +20,8 @@ variable (lts₃ : LTS State₃ Label₃) # Category of Labelled Transition Systems -/ +/-! ## Definition of LTS morphism -/ + /-- 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 @@ -46,6 +48,8 @@ def LTSMorphism.comp : LTSMorphism lts₁ lts₂ → LTSMorphism lts₂ lts₃ exact h ⟨g ∘ f, ν ∘ μ, r⟩ +/-! ## LTSs and LTS morphisms form a category -/ + /-- `LTSMorphism` provides a category structure on the `LTS` type. -/ instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) where Hom := LTSMorphism From 3a7993f491f710328386f218638831b0b51be2f6 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Mon, 2 Mar 2026 23:07:51 +0000 Subject: [PATCH 07/12] Improve naming --- Cslib/Foundations/Semantics/LTS/Category.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 3e20f771..f7e9a254 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -26,16 +26,16 @@ variable (lts₃ : LTS State₃ Label₃) 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₂ - lam : Label₁ → Label₂ + labelMap : Label₁ → Label₂ fun_preserves_transitions : (s s' : State₁) → (l : Label₁) → lts₁.Tr s l s' - → lts₂.Tr (toFun s) (lam l) (toFun s') + → lts₂.Tr (toFun s) (labelMap l) (toFun s') /-- The identity LTS morphism. -/ def LTSMorphism.id (lts : LTS State Label) : LTSMorphism lts lts := { toFun := _root_.id - , lam := _root_.id + , labelMap := _root_.id , fun_preserves_transitions := fun _ _ _ h => h } From dc216e372efe8ce07a27d994f49fa8c9e7ec627f Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 3 Mar 2026 11:07:40 +0000 Subject: [PATCH 08/12] Re-order variables --- Cslib/Foundations/Semantics/LTS/Category.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index f7e9a254..2c814a08 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -11,7 +11,7 @@ open Cslib @[expose] public section -variable {State Label State₃ Label₃ State₁ State₂ Label₁ Label₂ : Type} +variable {State Label State₁ State₂ State₃ Label₁ Label₂ Label₃ : Type} variable (lts₁ : LTS State₁ Label₁) variable (lts₂ : LTS State₂ Label₂) variable (lts₃ : LTS State₃ Label₃) From 2d068c350d1839628f92fd4666c10d428e646a81 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 3 Mar 2026 11:12:59 +0000 Subject: [PATCH 09/12] Put `LTSMorphism` under the `LTS` namespace --- Cslib/Foundations/Semantics/LTS/Category.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 2c814a08..2ca3423d 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -24,7 +24,7 @@ variable (lts₃ : LTS State₃ Label₃) /-- 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 +structure LTS.Morphism (lts₁ : LTS State₁ Label₁) (lts₂ : LTS State₂ Label₂) : Type where toFun : State₁ → State₂ labelMap : Label₁ → Label₂ fun_preserves_transitions : (s s' : State₁) @@ -33,14 +33,15 @@ structure LTSMorphism (lts₁ : LTS State₁ Label₁) (lts₂ : LTS State₂ La → lts₂.Tr (toFun s) (labelMap l) (toFun s') /-- The identity LTS morphism. -/ -def LTSMorphism.id (lts : LTS State Label) : LTSMorphism lts lts := +def LTS.Morphism.id (lts : LTS State Label) : LTS.Morphism lts lts := { toFun := _root_.id , labelMap := _root_.id , fun_preserves_transitions := fun _ _ _ h => h } /-- Composition of LTS morphisms. -/ -def LTSMorphism.comp : LTSMorphism lts₁ lts₂ → LTSMorphism lts₂ lts₃ → LTSMorphism lts₁ lts₃ := +def LTS.Morphism.comp : + LTS.Morphism lts₁ lts₂ → LTS.Morphism lts₂ lts₃ → LTS.Morphism lts₁ lts₃ := fun ⟨f, μ, p⟩ ⟨g, ν, q⟩ => let r := by intros _ _ _ h apply q @@ -50,11 +51,11 @@ def LTSMorphism.comp : LTSMorphism lts₁ lts₂ → LTSMorphism lts₂ lts₃ /-! ## LTSs and LTS morphisms form a category -/ -/-- `LTSMorphism` provides a category structure on the `LTS` type. -/ +/-- `LTS.Morphism` provides a category structure on the `LTS` type. -/ instance {State Label : Type} : CategoryTheory.CategoryStruct (LTS State Label) where - Hom := LTSMorphism - id := LTSMorphism.id - comp {lts₁} {lts₂} {lts₃} := LTSMorphism.comp lts₁ lts₂ lts₃ + Hom := LTS.Morphism + id := LTS.Morphism.id + 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 From 487c4f3eb46f8a4db1eef55f38e75f9512a6d99c Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 3 Mar 2026 13:13:49 +0000 Subject: [PATCH 10/12] Fix the definition of the category of LTSs --- Cslib/Foundations/Semantics/LTS/Category.lean | 50 +++++++++++-------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 2ca3423d..7316d8a0 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -9,6 +9,8 @@ public import Cslib.Foundations.Semantics.LTS.Basic public import Mathlib.CategoryTheory.Category.Basic open Cslib +universe u v + @[expose] public section variable {State Label State₁ State₂ State₃ Label₁ Label₂ Label₃ : Type} @@ -51,25 +53,33 @@ def LTS.Morphism.comp : /-! ## 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 - Hom := LTS.Morphism - id := LTS.Morphism.id - comp {lts₁} {lts₂} {lts₃} := LTS.Morphism.comp lts₁ lts₂ lts₃ +/-- The notion of labelled transition system -/ +structure BundledLTS where + State : Type u + Label : Type v + lts : LTS State Label + +/- 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`. +-/ + +/-- `LTS.Morphism` provides a category structure on bundled LTSs. -/ +instance : CategoryTheory.CategoryStruct BundledLTS where + Hom X Y := LTS.Morphism X.lts Y.lts + id X := LTS.Morphism.id X.lts + comp {X} {Y} {Z} f g := LTS.Morphism.comp X.lts Y.lts Z.lts f g /-- Proof that the above structure actually forms a category. -/ -instance {State Label : Type} : CategoryTheory.Category (LTS State Label) where - id_comp := by - intro _ _ f - cases f - rfl - comp_id := by - intro _ _ f - cases f - rfl - assoc := by - intro _ _ _ _ f g h - cases f - cases g - cases h - rfl +instance : CategoryTheory.Category BundledLTS where + id_comp := by intro _ _ f + cases f + rfl + comp_id := by intro _ _ f + cases f + rfl + assoc := by intro _ _ _ _ f g h + cases f + cases g + cases h + rfl From c942d95472c00172e520cca50227e7e024f12a1a Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 3 Mar 2026 13:21:09 +0000 Subject: [PATCH 11/12] Use the notion of `BundledLTS` everywhere --- Cslib/Foundations/Semantics/LTS/Category.lean | 62 +++++++++---------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 7316d8a0..7a4554b6 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -13,36 +13,48 @@ universe u v @[expose] public section -variable {State Label State₁ State₂ State₃ Label₁ Label₂ Label₃ : Type} -variable (lts₁ : LTS State₁ Label₁) -variable (lts₂ : LTS State₂ Label₂) -variable (lts₃ : LTS State₃ Label₃) +variable {State Label : Type} /-! # Category of Labelled Transition Systems -/ +/-! ## LTSs and LTS morphisms form a category -/ + +/-- The notion of labelled transition system -/ +structure BundledLTS where + State : Type u + Label : Type v + lts : LTS State Label + +/- 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`. +-/ + /-! ## Definition of LTS morphism -/ -/-- 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 - toFun : State₁ → State₂ - labelMap : Label₁ → Label₂ - fun_preserves_transitions : (s s' : State₁) - → (l : Label₁) - → lts₁.Tr s l s' - → lts₂.Tr (toFun s) (labelMap l) (toFun s') +/-- +A morphism between two labelled transition systems consists of a function on +states, a function on labels, and a proof that transitions are preserved. +-/ +structure LTS.Morphism (lts₁ lts₂ : BundledLTS) : Type where + toFun : lts₁.State → lts₂.State + labelMap : lts₁.Label → lts₂.Label + fun_preserves_transitions : (s s' : lts₁.State) + → (l : lts₁.Label) + → lts₁.lts.Tr s l s' + → lts₂.lts.Tr (toFun s) (labelMap l) (toFun s') /-- The identity LTS morphism. -/ -def LTS.Morphism.id (lts : LTS State Label) : LTS.Morphism lts lts := +def LTS.Morphism.id (lts : BundledLTS) : LTS.Morphism lts lts := { toFun := _root_.id , labelMap := _root_.id , fun_preserves_transitions := fun _ _ _ h => h } /-- Composition of LTS morphisms. -/ -def LTS.Morphism.comp : +def LTS.Morphism.comp {lts₁ lts₂ lts₃ : BundledLTS} : LTS.Morphism lts₁ lts₂ → LTS.Morphism lts₂ lts₃ → LTS.Morphism lts₁ lts₃ := fun ⟨f, μ, p⟩ ⟨g, ν, q⟩ => let r := by intros _ _ _ h @@ -51,24 +63,12 @@ def LTS.Morphism.comp : exact h ⟨g ∘ f, ν ∘ μ, r⟩ -/-! ## LTSs and LTS morphisms form a category -/ - -/-- The notion of labelled transition system -/ -structure BundledLTS where - State : Type u - Label : Type v - lts : LTS State Label - -/- 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`. --/ - /-- `LTS.Morphism` provides a category structure on bundled LTSs. -/ instance : CategoryTheory.CategoryStruct BundledLTS where - Hom X Y := LTS.Morphism X.lts Y.lts - id X := LTS.Morphism.id X.lts - comp {X} {Y} {Z} f g := LTS.Morphism.comp X.lts Y.lts Z.lts f g + Hom lts₁ lts₂ := LTS.Morphism lts₁ lts₂ + id lts := LTS.Morphism.id lts + comp {lts₁} {lts₂} {lts₃} f g := + LTS.Morphism.comp (lts₁ := lts₁) (lts₂ := lts₂) (lts₃ := lts₃) f g /-- Proof that the above structure actually forms a category. -/ instance : CategoryTheory.Category BundledLTS where From dc6ba49028193be4f3950039a0b131be674f4c72 Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Tue, 3 Mar 2026 13:22:03 +0000 Subject: [PATCH 12/12] Tweak --- Cslib/Foundations/Semantics/LTS/Category.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Category.lean b/Cslib/Foundations/Semantics/LTS/Category.lean index 7a4554b6..0ab23377 100644 --- a/Cslib/Foundations/Semantics/LTS/Category.lean +++ b/Cslib/Foundations/Semantics/LTS/Category.lean @@ -67,8 +67,7 @@ def LTS.Morphism.comp {lts₁ lts₂ lts₃ : BundledLTS} : instance : CategoryTheory.CategoryStruct BundledLTS where Hom lts₁ lts₂ := LTS.Morphism lts₁ lts₂ id lts := LTS.Morphism.id lts - comp {lts₁} {lts₂} {lts₃} f g := - LTS.Morphism.comp (lts₁ := lts₁) (lts₂ := lts₂) (lts₃ := lts₃) f g + comp {lts₁} {lts₂} {lts₃} f g := @LTS.Morphism.comp lts₁ lts₂ lts₃ f g /-- Proof that the above structure actually forms a category. -/ instance : CategoryTheory.Category BundledLTS where