Zulip Chat Archive

Stream: general

Topic: Contributing AVL tree module

Henry Pearson (May 09 2022 at 15:19):

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 (May 09 2022 at 16:33):

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 (May 09 2022 at 16:40):

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 (May 09 2022 at 16:51):

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 (May 09 2022 at 17:09):

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

Last updated: Aug 03 2023 at 10:10 UTC