Switch to the standard type for relations.

Cslib.lean

@@ -1,6 +1,6 @@
 import Cslib.Semantics.LTS.Basic
 import Cslib.Semantics.LTS.Bisimulation
 import Cslib.Semantics.LTS.TraceEq
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 import Cslib.Computability.CombinatoryLogic.Defs
 import Cslib.Computability.CombinatoryLogic.Basic

Cslib/Computability/CombinatoryLogic/Confluence.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
 import Cslib.Computability.CombinatoryLogic.Defs
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 
 /-!
 # SKI reduction is confluent

Cslib/Computability/CombinatoryLogic/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Waring
 -/
 import Mathlib.Logic.Relation
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 
 /-!
 # SKI Combinatory Logic

Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean

@@ -7,7 +7,7 @@ Authors: Chris Henson
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBeta
-import Cslib.Utils.Relation
+import Cslib.Data.Relation
 
 /-! # β-confluence for the λ-calculus -/
 

Cslib/ConcurrencyTheory/CCS/BehaviouralTheory.lean

@@ -23,13 +23,13 @@ Additionally, some standard laws of bisimilarity for CCS, including:
 
 section CCS.BehaviouralTheory
 
-variable {Name : Type u} {Constant : Type v} {defs : Rel Constant (CCS.Process Name Constant)}
+variable {Name : Type u} {Constant : Type v} {defs : Constant → (CCS.Process Name Constant) → Prop}
 
 open CCS CCS.Process CCS.Act
 
 namespace CCS
 
-private inductive ParNil : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ParNil : (Process Name Constant) → (Process Name Constant) → Prop where
 | parNil : ParNil (par p nil) p
 
 /-- P | 𝟎 ~ P -/
@@ -60,7 +60,7 @@ theorem bisimilarity_par_nil (p : Process Name Constant) : (par p nil) ~[@lts Na
     case right =>
       constructor
 
-private inductive ParComm : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ParComm : (Process Name Constant) → (Process Name Constant) → Prop where
 | parComm : ParComm (par p q) (par q p)
 
 /-- P | Q ~ Q | P -/
@@ -114,7 +114,7 @@ theorem bisimilarity_par_comm (p q : Process Name Constant) : (par p q) ~[@lts N
             apply Tr.com htrq htrp
           . constructor
 
-private inductive ChoiceComm : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ChoiceComm : (Process Name Constant) → (Process Name Constant) → Prop where
 | choiceComm : ChoiceComm (choice p q) (choice q p)
 | bisim : (p ~[@lts Name Constant defs] q) → ChoiceComm p q
 
@@ -166,7 +166,7 @@ theorem bisimilarity_choice_comm : (choice p q) ~[@lts Name Constant defs] (choi
       apply And.intro htr1
       constructor; assumption
 
-private inductive PreBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive PreBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | pre : (p ~[@lts Name Constant defs] q) → PreBisim (pre μ p) (pre μ q)
 | bisim : (p ~[@lts Name Constant defs] q) → PreBisim p q
 
@@ -217,7 +217,7 @@ theorem bisimilarity_congr_pre : (p ~[@lts Name Constant defs] q) → (pre μ p)
       constructor
       apply Bisimilarity.largest_bisimulation _ r hbisim s1' s2' hr1
 
-private inductive ResBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ResBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | res : (p ~[@lts Name Constant defs] q) → ResBisim (res a p) (res a q)
 -- | bisim : (p ~[@lts Name Constant defs] q) → ResBisim p q
 
@@ -250,7 +250,7 @@ theorem bisimilarity_congr_res : (p ~[@lts Name Constant defs] q) → (res a p)
     constructor; constructor; repeat assumption
     constructor; assumption
 
-private inductive ChoiceBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ChoiceBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | choice : (p ~[@lts Name Constant defs] q) → ChoiceBisim (choice p r) (choice q r)
 | bisim : (p ~[@lts Name Constant defs] q) → ChoiceBisim p q
 
@@ -315,7 +315,7 @@ theorem bisimilarity_congr_choice : (p ~[@lts Name Constant defs] q) → (choice
       constructor
       apply Bisimilarity.largest_bisimulation _ _ hb _ _ hr1
 
-private inductive ParBisim : Rel (Process Name Constant) (Process Name Constant) where
+private inductive ParBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | par : (p ~[@lts Name Constant defs] q) → ParBisim (par p r) (par q r)
 
 /-- P ~ Q → P | R ~ Q | R-/

Cslib/ConcurrencyTheory/CCS/Semantics.lean

@@ -15,7 +15,10 @@ import Cslib.ConcurrencyTheory.CCS.Basic
 
 -/
 
-variable {Name : Type u} {Constant : Type v} {defs : Rel Constant (CCS.Process Name Constant)}
+variable
+  {Name : Type u}
+  {Constant : Type v}
+  {defs : Constant → (CCS.Process Name Constant) → Prop}
 
 namespace CCS
 

Cslib/Utils/Relation.lean → Cslib/Data/Relation.lean

@@ -1,13 +1,37 @@
 /-
-Copyright (c) 2025 Thomas Waring. All rights reserved.
+Copyright (c) 2025 Fabrizio Montesi and Thomas Waring. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Waring, Chris Henson
+Authors: Fabrizio Montesi, Thomas Waring, Chris Henson
 -/
+
 import Mathlib.Logic.Relation
 
-universe u
+/-! # Relations -/
+
+universe u v
+
+section Relation
+
+/-- Union of two relations. -/
+def Relation.union (r s : α → β → Prop) : α → β → Prop :=
+  fun x y => r x y ∨ s x y
+
+instance {α : Type u} {β : Type v} : Union (α → β → Prop) where
+  union := Relation.union
 
-variable {α : Type u} {R R' : α → α → Prop}
+/-- Inverse of a relation. -/
+def Relation.inv (r : α → β → Prop) : β → α → Prop := flip r
+
+-- /-- Composition of two relations. -/
+-- def Relation.comp (r : α → β → Prop) (s : β → γ → Prop) : α → γ → Prop :=
+--   fun x z => ∃ y, r x y ∧ s y z
+
+/-- The relation `r` 'up to' the relation `s`. -/
+def Relation.upTo (r s : α → α → Prop) : α → α → Prop := Relation.Comp s (Relation.Comp r s)
+
+/-- The identity relation. -/
+inductive Relation.Id : α → α → Prop where
+| id {x : α} : Id x x
 
 /-- A relation has the diamond property when all reductions with a common origin are joinable -/
 abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C → (∃ D, R B D ∧ R C D)
@@ -16,9 +40,9 @@ abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C →
 abbrev Confluence (R : α → α → Prop) := Diamond (Relation.ReflTransGen R)
 
 /-- Extending a multistep reduction by a single step preserves multi-joinability. -/
-lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) : 
-  Relation.ReflTransGen R A B → 
-  R A C → 
+lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) :
+  Relation.ReflTransGen R A B →
+  R A C →
   ∃ D, Relation.ReflTransGen R B D ∧ Relation.ReflTransGen R C D := by
   intros AB _
   revert C
@@ -75,3 +99,5 @@ theorem church_rosser_of_diamond {α : Type _} {r : α → α → Prop}
   constructor
   . exact Relation.ReflGen.single hd.1
   . exact Relation.ReflTransGen.single hd.2
+
+end Relation

Cslib/Semantics/LTS/Basic.lean

@@ -7,7 +7,6 @@ Authors: Fabrizio Montesi
 import Mathlib.Tactic.Lemma
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Fintype.Basic
-import Mathlib.Data.Rel
 import Mathlib.Logic.Function.Defs
 import Mathlib.Data.Set.Finite.Basic
 import Mathlib.Data.Stream.Defs
@@ -64,11 +63,12 @@ section Relation
 and `s2` such that `lts.Tr s1 μ s2`.
 
 This can be useful, for example, to see a reduction relation as an LTS. -/
-def LTS.toRel (lts : LTS State Label) (μ : Label) : Rel State State :=
+def LTS.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
   fun s1 s2 => lts.Tr s1 μ s2
 
 /-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/
-def Rel.toLTS [DecidableEq Label] (r : Rel State State) (μ : Label) : LTS State Label where
+def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) :
+  LTS State Label where
   Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False
 
 end Relation
@@ -576,9 +576,9 @@ elab "create_lts" lt:ident name:ident : command => do
       addTermInfo' name (.const name.getId params) (isBinder := true)
       addDeclarationRangesFromSyntax name.getId name
 
-/-- 
+/--
   This command adds notations for an `LTS.Tr`. This should not usually be called directly, but from
-  the `lts` attribute. 
+  the `lts` attribute.
 
   As an example `lts_reduction_notation foo "β"` will add the notations "[⬝]⭢β" and "[⬝]↠β"
 
@@ -588,12 +588,12 @@ elab "create_lts" lt:ident name:ident : command => do
 -/
 syntax "lts_reduction_notation" ident (Lean.Parser.Command.notationItem)? : command
 macro_rules
-  | `(lts_reduction_notation $lts $sym) => 
+  | `(lts_reduction_notation $lts $sym) =>
     `(
       notation:39 t "["μ"]⭢"$sym t' => (LTS.Tr $lts) t μ t'
       notation:39 t "["μ"]↠"$sym t' => (LTS.MTr $lts) t μ t'
      )
-  | `(lts_reduction_notation $lts) => 
+  | `(lts_reduction_notation $lts) =>
     `(
       notation:39 t "["μ"]⭢" t' => (LTS.Tr $lts) t μ t'
       notation:39 t "["μ"]↠" t' => (LTS.MTr $lts) t μ t'