Contributing AVL tree module

Stream: general

[Henry Pearson]

Hi, for the past few months I have been writing a formalisation of AVL trees as part of an undergraduate project. I was looking to potentially contribute this to mathlib - would anyone be able to help me with this process? My code for the project can be found here https://github.com/HenryPearson2001/avltree. Thanks!

[Jannis Limperg]

Looks cool! I'm afraid I can't help much with the contribution process, but I have one comment on the content: if you want your operations to be efficient, you need to cache the depth in each avlnode. Otherwise you recompute it all the time. Well-formedness then needs to be extended to include the invariant that the cached depth is correct. (I had a student last year who did a similar project and we made the same mistake. :innocent: )

[Henry Pearson]

Ah thanks for the message! I did consider this but decided not to cache the depth for simplicity, my reasoning for not needing it being that the module is not designed for practical usage of AVL trees, only to prove theorems involving AVL trees, so it only matters that the structure 'looks correct' if that makes sense.

[Jannis Limperg]

Sure! But the practical version (for which, I think, not much needs to change beyond the depth caching) would be much more interesting. Not so much for Lean 3 but in Lean 4, it would be really nice to have some verified and reasonably performant data structures.

[Henry Pearson]

Ah yeah that's true, I'll have a look at changing it