splay tree proofs

Stream: graph theory

[Derrick R Burns]

As a first experiment with Lean, I created proofs of correctness and amortized running time for various operations on splay trees. I used Claude to create the proofs. Is there any appetite for these proofs in Mathlib.

Specifically, I've implemented a complete formalization of splay trees for mathlib4:

- 6 modules with full proofs (no sorries)

- Amortized O(log n) complexity analysis

- Working set property, dynamic finger theorem

- Branch: https://github.com/derrickburns/mathlib4/tree/splay-mathlib4

If there is interest, what is the process?

[Kim Morrison]

I think splay trees are probably out of scope for mathlib itself. I'd ask in the #**CSLib> channel!

[Kim Morrison]

In any case, it doesn't look like this is ready for upstreaming anywhere. The very first thing I see is that you duplicate the existing definition of Tree (with just a permutation of arguments) instead of reusing.

[Derrick R Burns]

Thx! That is the kind of feedback that I’m looking for.

[Yuyang Zhao]

I haven't looked at everything in detail, but I don't think it proves the dynamic finger theorem. (upd: Sorry, I realized I should reply in another place.)

[Joscha Mennicken]

For context, there is a thread for this question in the CS channel at #computer science > Splay trees @ 💬