chore: split the Relation module (#632)

This was already at ~1000 lines and growing. I've split this without
making any other changes with one exception: the `CoeDep` instances
previously specific to `dom` and `cod` are generalized as this makes
imports less awkward (and is also useful for another PR I will make
soon).

Author: chenson2018

Cslib.lean

@@ -66,12 +66,16 @@ public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
 public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.RelatesInSteps
-public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
+public import Cslib.Foundations.Relation.Attr
+public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Foundations.Relation.Defs
+public import Cslib.Foundations.Relation.Domain
+public import Cslib.Foundations.Relation.Euclidean
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS

Cslib/Computability/URM/Execution.lean

@@ -6,7 +6,7 @@ Authors: Jesse Alama
 module
 
 public import Cslib.Computability.URM.Defs
-public import Cslib.Foundations.Data.Relation
+public import Cslib.Foundations.Relation.Confluence
 public import Mathlib.Data.Part
 
 /-! # URM Execution Semantics