Advice on whether to use new Rel definition

Stream: new members

[Angelina Chen]

Hi, I'm working on a project in which I'm trying to formalize memglue, a cache coherence protocol, and the c11 memory model to prove that memglue upholds the c11 axioms. Currently, my c11 model relies on the old version of Rel, and I'm not sure whether it's worth rewriting everything to use the new Set version because the only benefit that is obvious to me is being able to reason about relations as Sets containing event pairs (e.g., can directly use set union to define relations formed from the union of other relations). On the other hand, if I were to use the new version of Rel, then I wouldn't be able to use Relation.Refl/TransGen directly anymore because Rel and Relation are now distinct types, which is problematic as I need to use those for some of the relations. I haven’t yet modified my code, so I’ve just been using the old definition along with custom instances of Union/Inter to make the notation less cumbersome. I was hoping to get some advice as to whether I should keep working with the old definition or if there are significant benefits to switching over to the new definition in terms of making it easier to prove the c11 axioms later. I couldn’t really understand the implementation notes for Rel and I’m sure that there are details I’m not seeing since I’m new to Lean and theorem proving, in general, so if someone could provide some guidance for my specific use case, that would be much appreciated. Thanks!
c11.lean
memglueO.lean

[Eric Wieser]

You can probably get by with abbrev Rel' (A B : Type*) := A -> B -> Prop, and the lattice notation should just work

[Eric Wieser]

But I've posted a message in #mathlib4 > Changing `Rel` to `Set (α × β)`, to help uniform spaces @ 💬 to suggest restoring at least the old Rel name to its former meaning

[Angelina Chen]

Got it, I'll look into lattice notation, thanks so much!