feat: add several definitions and theorems about reduction systems

[IvanRenison]

This PR adds some additional API to ReductionSystem. While it duplicates from the relation namespace, this seems like an acceptable tradeoff for unifying proofs that use the corresponding notation, and ultimately a user can still simplify to the underlying relation if they desire. (description added by Chris Henson)

[IvanRenison]

I don't know why the CI is failing Now the strange error was fixed

[chenson2018]

I don't know why the CI is failing Now the strange error was fixed

Yes, I retriggered CI manually a couple of times and it then passed, so I assume a transient runner issue.

[chenson2018]

This PR looks very nice in terms of adding API to ReductionSystem. I worry a bit about having to duplicate everything from Relation, but this all seems correct to me assuming this need. I will review fully probably next week.

[IvanRenison]

@chenson2018 don't forget about this pull request. The CI for the last commit was never run

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for 883298e against 7f88669 are in! @chenson2018

Small changes (1🟥)

• 🟥 build/module/Cslib.Foundations.Semantics.ReductionSystem.Basic//instructions: +3.0G (+36.5%)

[chenson2018]

@chenson2018 don't forget about this pull request. The CI for the last commit was never run

Thank you for your patience. I was very undecided about the idea of duplication from Relation, but with more examples where I think this will be useful have decided that this is a positive change. I have resolved merge conflicts and added a description.

[chenson2018]

Thanks again, I think this will be useful!

[IvanRenison]

Thank you!