unbundling `ReductionSystem`

Stream: CSLib

[Chris Henson]

I'd like to discuss unbundling relations from Cslib.ReductionSystem. Here are my thoughts:

• This is one of the oldest definitions first used by @Fabrizio Montesi and I at the very beginning of the library. I'm a bit fuzzy on if we talked it over much, but I think I agreed with this design at the time because I thought it might become an abstraction barrier similar to docs#Digraph or docs#SimpleGraph that also bundle relations
• In practice however, this is tightly coupled with Mathlib.Logic.Relation, Cslib.Foundations.Data.Relation, and even core. At the moment there is a growing amount of duplication from these modules. I have enforced that anything added here should directly correspond to the unbundled version definitionally, but this is still burdensome.
• Especially because there is notation involved, it is confusing when there are gaps in this duplicated API. In general, the ergonomics are frustrating.

As far as I can tell, there are no advantages to this bundling. I propose that we remove ReductionSystem entirely and refactor the reduction_sys attribute to just directly make notation for the relation it annotates. This change doesn't seem overly difficult and I think has the end result of simplifying the experience of working with reductions to the usual theorems about relations.

[Fabrizio Montesi]

This makes sense, generally speaking. How would things like MRed or the equivalent of LTS.OmegaExecution look like?
Making it easy to access derived motions was one of the main motivations, iirc.

[Chris Henson]

MRed will still be the reflexive transitive closure and use the same notation, just directly with the relation instead of paramaterized by the bundled structure. I think this will make it easier to work with because you don't have to keep in mind the bundling.

Can you point out LTS.OmegaExecution? I'm not seeing it.

[Fabrizio Montesi]

Sorry I meant this: https://api.cslib.io/docs/Cslib/Foundations/Semantics/LTS/Basic.html#Cslib.LTS.%CF%89Tr

[Chris Henson]

We haven't really needed this much for relations yet, but I don't think the (un)bundling is too relevant here. You can imagine something like docs#wellFounded_iff_isEmpty_descending_chain restated in terms of ωSequence.

[Fabrizio Montesi]

That looks fine, but is MRed gonna be an abbrev, or just replaced by ReflTransGen, or..?

[Chris Henson]

The notation currently used for MRed will just expand to ReflTransGen r. There is no need for a separate declaration when unbundled.

[Chris Henson]

I think this is preferable because then you just use the usual theorems on relations instead of needing to remember a possibly imperfectly duplicated API.

[Fabrizio Montesi]

It is definitely preferable, I agree, just trying to think of corner cases.

Re notation: we don't really have a notation for these relations, only their instances. So theorems about MRed and similar things on general relations won't use the notation. You'd get access to it only in specific developments, e.g., the reduction relation of lambda-calculus.

The idea sounds fine to me otherwise.

[Chris Henson]

I completely agree, though this is an existing problem. I've thought about defining local notation in Cslib.Foundations.Data.Relation, where we'd mirror the arrows we picked for the paramaterized notations.

[Chris Henson]

I have opened cslib#320. This seemed very straightforward and is a +125 -468 diff. The only oddity I encountered was a single strange grind failure, but this was very easily solved by calling simp on a hypothesis first.