Lemmas on relations

Stream: general

[Eben Rogers]

Hi, another student at the TU Delft (@Luka Janjić ) and I recently did some work on formalizing memory consistency models in Lean. For this we had to work with a model that heavily relied on binary relations and permutations and combinations of them (transitive-, reflexive-, reflexive-transitive-closures, and also unions, intersections, and compositions). We did quite a bit of abstract boilerplate lemma proving pertaining to combinations of these operations on relations (e.g. (r1 or r2+)+ = (r1 or r2)+, where + is the transitive closure of a relation) and would love to contribute them to Mathlib. My Github username is @bigstep22 and Luka's is @sourceCode4. Would it be possible to contribute? What stream is best for discussing this?

[Eric Wieser]

Those sound like nice things to have in mathlib; I've added you both to mathlib3

[Eric Wieser]

Note that you're finding mathlib at an interesting time; we're in the process of converting to mathlib4 (see #port-dashboard to see our progress). If you've already written your code in Lean 3 though, I'd encourage you to make a PR to the Lean3 version of mathlib anyway to get some feedback!

[Eben Rogers]

Ok, thank you for the fast reply! I remember reading somewhere that Mathlib3 is some sort of a 'feature freeze'. So I'm assuming that eventually we'll have to contribute to both Mathlib3 and 4 for it to be merged? In the meantime, we'll get to work creating a PR.

[Eric Wieser]

Right now we are still accepting PRs to mathlib3; but once they're merged they'll appear on #outofsync the next day, which contains a best-effort translation of your changes to Lean4 that you'll have to assemble into a mathlib4 PR yourself. Depending on what exactly you intend to contribute, it _may_ make sense to skip lean3 and go straight to Lean4; but that can be decided in review

[Yaël Dillies]

Do have a look at #18286 and see whether I caught any of your lemmas there.