Splay Tree Formalisation

[AntoineduFresne]

This PR introduces Splay Trees to CSLib, the algorithmic definitions, the correctness proofs, and the (amortised) complexity analysis.

Design & Architecture: The implementation is partitioned into four modules to isolate dependencies.

Basic: Core definitions (splay, splayUp, descend, Frame). Primitive rotations are upstreamed to BinaryTree.

Correctness:

• Splaying a binary search tree returns a binary search tree (IsBST_splay).
• Splaying a binary tree at a key q will return a binary tree with q at the root (splay_root_of_contains).

Complexity: We formalise the Sleator-Tarjan potential method.

• Per-operation bound: we prove the amortised cost of a single splay operation is bounded by 3log_2(n)+1 (splay_amortized_bound).
• Sequence bound: we establish the global sequence cost for m operations on an initial tree of size n. The total cost is bounded by m(3log_2(n) + 1) + n log_2(n) (nlogn_cost).

BSTAPI: A user-facing wrapper providing a bundled BST API. Users can splay binary search trees naturally without having to manually supply invariant proofs (for example that splaying a binary search tree returns automatically binary search tree).

Why Bottom-Up? (Comparison with Top-Down):
There is a complementary top-down implementation available for reference here. This PR utilises a bottom-up approach because it reduces the length of the formalisation:

• No "Broken" Trees: Top-down splaying partitions the tree into three disconnected pieces (Left, Right, Middle) while searching. This makes tracking the mathematical potential function more difficult, as the potential function φ expects a whole tree. Our bottom-up approach leaves the tree intact—it just records the search path on the way down, and applies local rotations on the way up. The tree is always whole.

• Odd vs. Even Paths: Splaying works by rotating edges in pairs (e.g., zig-zig). If a path has an odd number of edges, top-down requires, asymmetrical edge-case code to handle the leftover rotation while stitching the tree back together. By modelling the path as a list of Frames, our bottom-up approach processes pairs natively via list induction.

• Search first & Rotate after: Top-down tries to search and restructure at the exact same time. Bottom-up strictly separates the logic: descend purely finds the node, and splayUp purely rotates it. This allows us to prove things about path lengths and node existence completely independently of the rotation proofs.

• Symmetry Exploitation: The proofs utilise formalised mirror symmetry (mirror, flip). This allows left/right symmetric double rotations (like zig-zig vs. zag-zag) to be proven using generic transformations rather making things redundant by duplicating code with a "mirror" logic.

Co-authored-by: Anton Kovsharov antonkov@google.com
Co-authored-by: Antoine du Fresne von Hohenesche antoine@du-fresne.ch
Co-authored-by: Sorrachai Yingchareonthawornchai sorrachai.cp@gmail.com

[sorrachai]

Link to discussion thread: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Splay.20tree.20PR/with/595534315