porting `Data.RBTree.Init`

Stream: mathlib4

[Andrew Yang]

I'm would like to try and port Data.RBTree.Init. Should it go in Mathlib or Std?

[Moritz Doll]

probably mathlib4, we can move parts to Std4 later on

[Andrew Yang]

It seems like I do not have the permission to write to a non-master branch. Is it still standard to work on an non-master branch? If so, can someone grant the right to me? Thanks!

[Ruben Van de Velde]

@Andrew Yang note that there's also https://leanprover-community.github.io/mathlib4_docs/Std/Data/RBMap/Basic.html in std4, so I'm not sure what (if anything) still needs porting

[Andrew Yang]

Oh I didn't notice that. But that rbtree is (syntactically) different than the docs#rbtree in mathlib3, and we should probably do something to appease mathport? Is it possible to align them in this case?

[Mario Carneiro]

I think a suitable "port" of the data.rbtree is: make a list of all the theorems about rbtree that don't yet exist in Std.Data.RBMap, open an issue for them on std4, and then remove everything from the module except for #aligns if possible (if the types are too different, just leave them unaligned). Std.Data.RBMap intends to completely replace that directory.

[Scott Morrison]

@Andrew Yang, I've given you permissions for mathlib4.

[Lukas Miaskiwskyi]

I PR'd the RBTree.Init file a couple hours ago, thinking it'd be a simple job, but this thread showed me that it's a bit of a nonstandard endeavour :) I followed @Mario Carneiro's recommended approach trying to align the contents with the corresponding ones from std4, maybe someone can have a look if things make sense in there: https://github.com/leanprover-community/mathlib4/pull/1246

[Mario Carneiro]

Note: I have an incomplete port of the rbtree files in progress, although it is a relatively low priority so I'm not actively working on it now. As for the #aligns, most of them need to have \_x because they aren't exact defeq ports, and for something like depth which is more than a little different (such that it would not be reasonable to ask someone porting a downstream file to migrate from one definition to the other) it should either be #noaligned or #aligned to a depth' function that is defined as it is in mathlib3.

[Bulhwi Cha]

Mario Carneiro said:

Note: I have an incomplete port of the rbtree files in progress, although it is a relatively low priority so I'm not actively working on it now.

Can I have a look at these files so I can port them?

[Bulhwi Cha]

Um, perhaps there isn't anything left to port.

[Mario Carneiro]

The intention was to replicate the functionality of all the files in std, and then delete the mathlib files. I think it's about 80% there, but it's almost all unused by mathlib in the first place

[Mario Carneiro]

What is there is almost all already landed in Std.Data.RBMap.Lemmas