From 6bf1e9faa4a78b4e32485ce37c1ed7a9934c17a4 Mon Sep 17 00:00:00 2001
From: Shreyas Srinivas <shreyasss94@gmail.com>
Date: Mon, 18 May 2026 22:49:00 +0200
Subject: [PATCH 1/3] Module system fixes and namespace Cslib

---
 Cslib/Foundations/Data/SplayTree/BSTAPI.lean      | 14 +++++++++++---
 Cslib/Foundations/Data/SplayTree/Basic.lean       | 12 +++++++++---
 Cslib/Foundations/Data/SplayTree/Complexity.lean  | 14 ++++++++++----
 Cslib/Foundations/Data/SplayTree/Correctness.lean | 10 ++++++++--
 4 files changed, 38 insertions(+), 12 deletions(-)

diff --git a/Cslib/Foundations/Data/SplayTree/BSTAPI.lean b/Cslib/Foundations/Data/SplayTree/BSTAPI.lean
index 3f1f583fd..112aabaf0 100644
--- a/Cslib/Foundations/Data/SplayTree/BSTAPI.lean
+++ b/Cslib/Foundations/Data/SplayTree/BSTAPI.lean
@@ -5,8 +5,10 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
   Sorrachai Yingchareonthawornchai
 -/
 
-import Cslib.Foundations.Data.SplayTree.Complexity
-import Cslib.Foundations.Data.SplayTree.Correctness
+module
+
+public import Cslib.Foundations.Data.SplayTree.Complexity
+public import Cslib.Foundations.Data.SplayTree.Correctness
 
 /-!
 # Splay Tree API for BST
@@ -17,13 +19,17 @@ proofs, allowing users to safely and cleanly manipulate BSTs without manually
 re-proving the `IsBST` invariant after every rotation.
 -/
 
-variable {α : Type} [LinearOrder α]
+@[expose] public section
+
+namespace Cslib
 
 namespace SplayTree.BSTAPI
 
 open SplayTree
 open BinaryTree
 
+variable {α : Type} [LinearOrder α]
+
 /-! ### Core Operation -/
 
 /--
@@ -85,3 +91,5 @@ theorem nlogn_cost (n m : ℕ) (X : Fin m → α)
   SplayTree.nlogn_cost n m X init.tree h_size
 
 end SplayTree.BSTAPI
+
+end Cslib
diff --git a/Cslib/Foundations/Data/SplayTree/Basic.lean b/Cslib/Foundations/Data/SplayTree/Basic.lean
index b7b2c274f..9d508fab8 100644
--- a/Cslib/Foundations/Data/SplayTree/Basic.lean
+++ b/Cslib/Foundations/Data/SplayTree/Basic.lean
@@ -5,8 +5,10 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
   Sorrachai Yingchareonthawornchai
 -/
 
-import Cslib.Foundations.Data.BinaryTree
-import Mathlib.Data.List.Sort
+module
+
+public import Cslib.Foundations.Data.BinaryTree
+public import Mathlib.Data.List.Sort
 
 /-!
 # Splay Tree Basic Definitions
@@ -16,7 +18,9 @@ rotation primitives, path frames, and the `splay` and `splayUp` functions.
 It also provides fundamental structural lemmas regarding tree size and descent paths.
 -/
 
-variable {α : Type}
+@[expose] public section
+
+namespace Cslib
 
 namespace SplayTree
 
@@ -374,3 +378,5 @@ lemma descend_go_length_le [LinearOrder α] (q : α) (t : BinaryTree α) (acc :
 end DescendLemmas
 
 end SplayTree
+
+end Cslib
diff --git a/Cslib/Foundations/Data/SplayTree/Complexity.lean b/Cslib/Foundations/Data/SplayTree/Complexity.lean
index 445f68e2c..7070f9ac0 100644
--- a/Cslib/Foundations/Data/SplayTree/Complexity.lean
+++ b/Cslib/Foundations/Data/SplayTree/Complexity.lean
@@ -5,9 +5,11 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
   Sorrachai Yingchareonthawornchai
 -/
 
-import Cslib.Foundations.Data.SplayTree.Basic
-import Mathlib.Data.Real.Basic
-import Mathlib.Analysis.SpecialFunctions.Log.Base
+module
+
+public import Cslib.Foundations.Data.SplayTree.Basic
+public import Mathlib.Data.Real.Basic
+public import Mathlib.Analysis.SpecialFunctions.Log.Base
 
 /-!
 # Amortized Complexity of Splay Trees
@@ -21,7 +23,9 @@ the classical O(m log n + n log n) total cost bound for a sequence of
 splay operations.
 -/
 
-variable {α : Type}
+@[expose] public section
+
+namespace Cslib
 
 namespace SplayTree
 
@@ -727,3 +731,5 @@ theorem nlogn_cost [LinearOrder α] (n m : ℕ) (X : Fin m → α)
 end SequenceCost
 
 end SplayTree
+
+end Cslib
diff --git a/Cslib/Foundations/Data/SplayTree/Correctness.lean b/Cslib/Foundations/Data/SplayTree/Correctness.lean
index 592ddad83..3a8d0caf9 100644
--- a/Cslib/Foundations/Data/SplayTree/Correctness.lean
+++ b/Cslib/Foundations/Data/SplayTree/Correctness.lean
@@ -5,7 +5,9 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
   Sorrachai Yingchareonthawornchai
 -/
 
-import Cslib.Foundations.Data.SplayTree.Basic
+module
+
+public import Cslib.Foundations.Data.SplayTree.Basic
 
 /-!
 # Splay Tree Correctness
@@ -15,7 +17,9 @@ It establishes that splaying preserves the binary search tree (BST) invariant
 and guarantees that querying an existing key successfully rotates it to the root.
 -/
 
-variable {α : Type}
+@[expose] public section
+
+namespace Cslib
 
 namespace SplayTree
 
@@ -256,3 +260,5 @@ theorem splay_root_of_contains [LinearOrder α] (t : BinaryTree α) (q : α)
 end RootOfContainedKey
 
 end SplayTree
+
+end Cslib

From 280db004fe06896698b09bb419916e82e399dce5 Mon Sep 17 00:00:00 2001
From: Shreyas Srinivas <shreyasss94@gmail.com>
Date: Mon, 18 May 2026 22:50:06 +0200
Subject: [PATCH 2/3] namespace Cslib and move @[expose] public section after
 module docstring

---
 Cslib/Foundations/Data/BinaryTree.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Cslib/Foundations/Data/BinaryTree.lean b/Cslib/Foundations/Data/BinaryTree.lean
index 28e8c0c24..90da41645 100644
--- a/Cslib/Foundations/Data/BinaryTree.lean
+++ b/Cslib/Foundations/Data/BinaryTree.lean
@@ -10,15 +10,15 @@ module
 public import Mathlib.Combinatorics.SimpleGraph.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Metric
 
-@[expose] public section
-
 /-!
 # Binary Tree
 
 In this file we introduce the `BinaryTree` data structure and its basic operations.
 -/
 
-variable {α : Type}
+@[expose] public section
+
+namespace Cslib
 
 inductive BinaryTree (α : Type) where
   | empty
@@ -256,3 +256,5 @@ def contains [LinearOrder α] (t : BST α) (q : α) : Prop :=
 end BST
 
 end BSTStructure
+
+end Cslib

From 03f3b46890f014986467d8fa0a0f6028c7b72591 Mon Sep 17 00:00:00 2001
From: Shreyas Srinivas <shreyasss94@gmail.com>
Date: Tue, 19 May 2026 01:00:43 +0200
Subject: [PATCH 3/3] Many errors to fix.

---
 Cslib/Foundations/Data/BinaryTree.lean      | 204 +++++++-------------
 Cslib/Foundations/Data/SplayTree/Basic.lean |  98 +++++-----
 2 files changed, 124 insertions(+), 178 deletions(-)

diff --git a/Cslib/Foundations/Data/BinaryTree.lean b/Cslib/Foundations/Data/BinaryTree.lean
index 90da41645..5079509f8 100644
--- a/Cslib/Foundations/Data/BinaryTree.lean
+++ b/Cslib/Foundations/Data/BinaryTree.lean
@@ -7,71 +7,38 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
 
 module
 
+public import Mathlib.Data.Tree.Basic
+public import Mathlib.Data.Tree.Traversable
+public import Mathlib.Control.Fold.Traversable
 public import Mathlib.Combinatorics.SimpleGraph.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Metric
 
 /-!
-# Binary Tree
+# Tree
 
-In this file we introduce the `BinaryTree` data structure and its basic operations.
+In this file we extend the `Tree` data structure from mathlib with basic operations.
 -/
 
 @[expose] public section
 
 namespace Cslib
 
-inductive BinaryTree (α : Type) where
-  | empty
-  | node (left : BinaryTree α) (key : α) (right : BinaryTree α)
-  deriving DecidableEq
+namespace Tree
 
-namespace BinaryTree
+open Cslib
 
-/-! ### Core Definitions -/
-section CoreDefs
-
-def left : BinaryTree α → BinaryTree α
-  | .empty => .empty
-  | .node l _ _ => l
-
-def right : BinaryTree α → BinaryTree α
-  | .empty => .empty
-  | .node _ _ r => r
-
-theorem non_empty_exist (s : BinaryTree α) (h : s ≠ .empty) :
-    ∃ A k B, s = .node A k B := by
-  induction s <;> grind
-
-def num_nodes : BinaryTree α → ℕ
-  | .empty => 0
-  | .node l _ r => 1 + num_nodes l + num_nodes r
-
-@[simp] lemma num_nodes_empty : num_nodes (empty : BinaryTree α) = 0 := rfl
-
-@[simp] lemma num_nodes_node (l : BinaryTree α) (k : α) (r : BinaryTree α) :
-    (node l k r).num_nodes = 1 + l.num_nodes + r.num_nodes := rfl
-
-/-- In-order traversal as a list of keys. -/
-def toKeyList : BinaryTree α → List α
-  | .empty => []
-  | .node l k r => l.toKeyList ++ [k] ++ r.toKeyList
-
-@[simp] lemma toKeyList_empty : toKeyList (empty : BinaryTree α) = [] := rfl
-
-@[simp] lemma toKeyList_node (l : BinaryTree α) (k : α) (r : BinaryTree α) :
-    (node l k r).toKeyList = l.toKeyList ++ [k] ++ r.toKeyList := rfl
 
 /-- Number of nodes on the search path for `q` in `t`. Zero on the empty
 tree; on a node this counts the root plus (if `q ≠ k`) the search path
 length in the appropriate subtree. -/
-def search_path_len [LinearOrder α] (t : BinaryTree α) (q : α) : ℕ :=
+def search_path_len [LinearOrder α] (t : Tree α) (q : α) : ℕ :=
   match t with
-  | .empty => 0
-  | .node l key r =>
+  | .nil => 0
+  | .node key l r =>
     if q < key then
-      1 + l.search_path_len q
+      1 + search_path_len l q
     else if key < q then
-      1 + r.search_path_len q
+      1 + search_path_len r q
     else
       1
 
@@ -84,68 +51,68 @@ If `contains t q` is true, then `q` is in `t`; but
 the converse need not necessarily hold true. The
 converse is true for a binary search tree.
 -/
-def contains [LinearOrder α] (t : BinaryTree α) (q : α) : Prop :=
+def containsBST [LinearOrder α] (t : Tree α) (q : α) : Prop :=
   match t with
-  | .empty => False
-  | .node l key r =>
+  | .nil => False
+  | .node key l r =>
     if q < key then
-      l.contains q
+      containsBST l q
     else if key < q then
-      r.contains q
+      containsBST r q
     else
       True
 
-end CoreDefs
-
 
 /-! ### Rotations and Mirroring -/
 section Transformations
 
-def rotateRight : BinaryTree α → BinaryTree α
-  | .node (.node a x b) y c => .node a x (.node b y c)
+def rotateRight : Tree α → Tree α
+  | .node y (.node x a b) c => .node x a (.node y b c)
   | t => t
 
-def rotateLeft : BinaryTree α → BinaryTree α
-  | .node a x (.node b y c) => .node (.node a x b) y c
+def rotateLeft : Tree α → Tree α
+  | .node x a (.node y b c) => .node y (.node x a b) c
   | t => t
 
 /-- Mirror a binary tree: swap every left and right subtree. -/
-def mirror : BinaryTree α → BinaryTree α
-  | .empty => .empty
-  | .node l k r => .node r.mirror k l.mirror
+def mirror : Tree α → Tree α
+  | .nil => .nil
+  | .node k l r => .node k (mirror r) (mirror l)
+
+@[simp] lemma mirror_empty : (.nil : Tree α).mirror = .nil := rfl
 
-@[simp] lemma mirror_empty : (empty : BinaryTree α).mirror = .empty := rfl
+@[simp] lemma mirror_node (k : α) (l : Tree α) (r : Tree α) :
+    (Tree.node k l r).mirror = .node k r.mirror l.mirror := rfl
 
-@[simp] lemma mirror_node (l : BinaryTree α) (k : α) (r : BinaryTree α) :
-    (node l k r).mirror = .node r.mirror k l.mirror := rfl
 
-@[simp] lemma mirror_mirror (t : BinaryTree α) : t.mirror.mirror = t := by
+@[simp] lemma mirror_mirror (t : Tree α) : t.mirror.mirror = t := by
   induction t <;> simp_all
 
-@[simp] lemma num_nodes_mirror (t : BinaryTree α) : t.mirror.num_nodes = t.num_nodes := by
-  induction t <;> simp_all [num_nodes]; omega
+@[simp] lemma size_mirror (t : Tree α) : t.mirror.numNodes = t.numNodes := by
+  induction t <;> simp_all [Tree.numNodes]; omega
 
-@[simp] lemma mirror_rotateRight (t : BinaryTree α) :
+@[simp] lemma mirror_rotateRight (t : Tree α) :
     (rotateRight t).mirror = rotateLeft t.mirror := by
-  cases t; · rfl
-  rename_i l _ _
-  cases l <;> rfl
+  cases t
+  · rfl
+  · rename_i _ l _
+    cases l <;> rfl
 
-@[simp] lemma mirror_rotateLeft (t : BinaryTree α) :
+@[simp] lemma mirror_rotateLeft (t : Tree α) :
     (rotateLeft t).mirror = rotateRight t.mirror := by
   cases t; · rfl
   rename_i _ _ r
   cases r <;> rfl
 
-@[simp] theorem num_nodes_rotateRight (t : BinaryTree α) :
-    (rotateRight t).num_nodes = t.num_nodes := by
-  rcases t with _ | ⟨(_ | ⟨ll, lk, lr⟩), k, r⟩ <;>
+@[simp] theorem size_rotateRight (t : Tree α) :
+    (rotateRight t).numNodes = t.numNodes := by
+  rcases t with _ | ⟨k, (_ | ⟨lk, ll, lr⟩), r⟩ <;>
     simp [rotateRight]; omega
 
-@[simp] theorem num_nodes_rotateLeft (t : BinaryTree α) :
-    (rotateLeft t).num_nodes = t.num_nodes := by
-  have h := num_nodes_rotateRight t.mirror
-  simp only [← mirror_rotateLeft, num_nodes_mirror] at h; exact h
+@[simp] theorem size_rotateLeft (t : Tree α) :
+    (rotateLeft t).numNodes = t.numNodes := by
+  have h := size_rotateRight t.mirror
+  simp only [← mirror_rotateLeft, size_mirror] at h; exact h
 
 end Transformations
 
@@ -154,24 +121,24 @@ end Transformations
 section ContainsLemmas
 
 @[simp] lemma not_contains_empty [LinearOrder α] (q : α) :
-    ¬ (empty : BinaryTree α).contains q := nofun
+    ¬ (Tree.nil : Tree α).containsBST q := nofun
 
-@[simp] lemma contains_node_lt [LinearOrder α] {l : BinaryTree α} {k q : α}
-    {r : BinaryTree α} (h : q < k) :
-    (node l k r).contains q ↔ l.contains q := by
-  simp [contains, h]
+@[simp] lemma contains_node_lt [LinearOrder α] {l : Tree α} {k q : α}
+    {r : Tree α} (h : q < k) :
+    (Tree.node k l r).containsBST q ↔ l.containsBST q := by
+  simp [containsBST, h]
 
-@[simp] lemma contains_node_gt [LinearOrder α] {l : BinaryTree α} {k q : α}
-    {r : BinaryTree α} (h : k < q) :
-    (node l k r).contains q ↔ r.contains q := by
-  simp [contains, h, not_lt_of_gt h]
+@[simp] lemma contains_node_gt [LinearOrder α] {l : Tree α} {k q : α}
+    {r : Tree α} (h : k < q) :
+    (Tree.node k l r).containsBST q ↔ r.containsBST q := by
+  simp [containsBST, h, not_lt_of_gt h]
 
 @[simp] lemma contains_node_not_eq_not_lt [LinearOrder α]
-    {l : BinaryTree α} {k q : α} {r : BinaryTree α}
+    {l : Tree α} {k q : α} {r : Tree α}
     (h1 : ¬ q = k) (h2 : ¬ q < k) :
-    (node l k r).contains q ↔ r.contains q := by
+    (Tree.node k l r).containsBST q ↔ r.containsBST q := by
   have hgt : k < q := lt_of_le_of_ne (Std.not_lt.mp h2) (Ne.symm (Ne.intro h1))
-  simp [contains, hgt, not_lt_of_gt hgt]
+  simp [containsBST, hgt, not_lt_of_gt hgt]
 
 end ContainsLemmas
 
@@ -179,21 +146,17 @@ end ContainsLemmas
 /-! ### Tree Invariants and BST Properties -/
 section Invariants
 
-inductive ForallTree (p : α → Prop) : BinaryTree α → Prop
-  | left : ForallTree p .empty
-  | node l key r :
-     ForallTree p l →
-     p key →
-     ForallTree p r →
-     ForallTree p (.node l key r)
-
-inductive IsBST [LinearOrder α] : BinaryTree α → Prop
-  | left : IsBST .empty
-  | node key l r :
-     ForallTree (fun k => k < key) l →
-     ForallTree (fun k => key < k) r →
-     IsBST l → IsBST r →
-     IsBST (.node l key r)
+
+def contains (t : Tree β) (p : β) : Prop :=
+  match t with
+  | .nil => False
+  | .node k l r => p = k ∨ Tree.contains l p ∨ Tree.contains r p
+
+instance : Membership β (Tree β) where
+  mem := Tree.contains
+
+def IsBST [LinearOrder α] (t : Tree α) : Prop :=
+  Traversable.foldl
 
 end Invariants
 
@@ -201,15 +164,15 @@ end Invariants
 /-! ### Accessor Lemmas for ForallTree -/
 section ForallTreeAccessors
 
-@[simp] lemma ForallTree.left_sub {p : α → Prop} {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma ForallTree.left_sub {p : α → Prop} {l : Tree α} {k : α} {r : Tree α}
     (h : ForallTree p (.node l k r)) : ForallTree p l := by
   cases h with | node _ _ _ hl _ _ => exact hl
 
-@[simp] lemma ForallTree.root {p : α → Prop} {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma ForallTree.root {p : α → Prop} {l : Tree α} {k : α} {r : Tree α}
     (h : ForallTree p (.node l k r)) : p k := by
   cases h with | node _ _ _ _ hk _ => exact hk
 
-@[simp] lemma ForallTree.right_sub {p : α → Prop} {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma ForallTree.right_sub {p : α → Prop} {l : Tree α} {k : α} {r : Tree α}
     (h : ForallTree p (.node l k r)) : ForallTree p r := by
   cases h with | node _ _ _ _ _ hr => exact hr
 
@@ -219,42 +182,25 @@ end ForallTreeAccessors
 /-! ### Accessor Lemmas for IsBST -/
 section IsBSTAccessors
 
-@[simp] lemma IsBST.forallTree_left [LinearOrder α] {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma IsBST.forallTree_left [LinearOrder α] {l : Tree α} {k : α} {r : Tree α}
     (h : IsBST (.node l k r)) : ForallTree (· < k) l := by
   cases h with | node _ _ _ hl _ _ _ => exact hl
 
-@[simp] lemma IsBST.forallTree_right [LinearOrder α] {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma IsBST.forallTree_right [LinearOrder α] {l : Tree α} {k : α} {r : Tree α}
     (h : IsBST (.node l k r)) : ForallTree (k < ·) r := by
   cases h with | node _ _ _ _ hr _ _ => exact hr
 
-@[simp] lemma IsBST.left_bst [LinearOrder α] {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma IsBST.left_bst [LinearOrder α] {l : Tree α} {k : α} {r : Tree α}
     (h : IsBST (.node l k r)) : IsBST l := by
   cases h with | node _ _ _ _ _ hl _ => exact hl
 
-@[simp] lemma IsBST.right_bst [LinearOrder α] {l : BinaryTree α} {k : α} {r : BinaryTree α}
+@[simp] lemma IsBST.right_bst [LinearOrder α] {l : Tree α} {k : α} {r : Tree α}
     (h : IsBST (.node l k r)) : IsBST r := by
   cases h with | node _ _ _ _ _ _ hr => exact hr
 
 end IsBSTAccessors
 
-end BinaryTree
-
-
-/-! ### BST Structure -/
-section BSTStructure
-
-structure BST (α : Type) [LinearOrder α] where
-  tree : BinaryTree α
-  hBST : BinaryTree.IsBST tree
-
-namespace BST
-
-/-- Checks if the BST contains a given key by delegating to the underlying tree. -/
-def contains [LinearOrder α] (t : BST α) (q : α) : Prop :=
-  t.tree.contains q
-
-end BST
 
-end BSTStructure
+end Tree
 
 end Cslib
diff --git a/Cslib/Foundations/Data/SplayTree/Basic.lean b/Cslib/Foundations/Data/SplayTree/Basic.lean
index 9d508fab8..087dd6bd9 100644
--- a/Cslib/Foundations/Data/SplayTree/Basic.lean
+++ b/Cslib/Foundations/Data/SplayTree/Basic.lean
@@ -7,7 +7,8 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche,
 
 module
 
-public import Cslib.Foundations.Data.BinaryTree
+public import Mathlib.Data.Tree.Basic
+public import Mathlib.Data.Tree.Traversable
 public import Mathlib.Data.List.Sort
 
 /-!
@@ -24,7 +25,6 @@ namespace Cslib
 
 namespace SplayTree
 
-open BinaryTree
 
 /-! ### Definitions -/
 section Definitions
@@ -45,12 +45,12 @@ def Dir.flip : Dir → Dir
 
 /-- Single primitive rotation that brings the `d`-child of the root up one
 level. `L` ↦ `rotateRight`, `R` ↦ `rotateLeft`. -/
-def Dir.bringUp : Dir → BinaryTree α → BinaryTree α
+def Dir.bringUp : Dir → Tree α → Tree α
   | .L => rotateRight
   | .R => rotateLeft
 
 /-- Apply `op` to the `d`-child of the root, leaving everything else fixed. -/
-def applyChild (d : Dir) (op : BinaryTree α → BinaryTree α) : BinaryTree α → BinaryTree α
+def applyChild (d : Dir) (op : Tree α → Tree α) : Tree α → Tree α
   | .node l k r =>
     match d with
     | .L => .node (op l) k r
@@ -62,15 +62,15 @@ its key, and the subtree we did *not* descend into. -/
 structure Frame α where
   dir : Dir
   key : α
-  sibling : BinaryTree α
+  sibling : Tree α
 
 /-- Re-attach a subtree `c` below the ancestor described by `f`. -/
-def Frame.attach (c : BinaryTree α) (f : Frame α) : BinaryTree α :=
+def Frame.attach (c : Tree α) (f : Frame α) : Tree α :=
   match f.dir with
   | .L => .node c f.key f.sibling
   | .R => .node f.sibling f.key c
 
-@[simp] lemma mirror_bringUp (d : Dir) (t : BinaryTree α) :
+@[simp] lemma mirror_bringUp (d : Dir) (t : Tree α) :
     (d.bringUp t).mirror = d.flip.bringUp t.mirror := by
   cases d <;> simp [Dir.bringUp, Dir.flip]
 
@@ -78,13 +78,13 @@ def Frame.attach (c : BinaryTree α) (f : Frame α) : BinaryTree α :=
 def Frame.flip (f : Frame α) : Frame α :=
   { dir := f.dir.flip, key := f.key, sibling := f.sibling.mirror }
 
-@[simp] lemma mirror_attach (c : BinaryTree α) (f : Frame α) :
+@[simp] lemma mirror_attach (c : Tree α) (f : Frame α) :
     (f.attach c).mirror = f.flip.attach c.mirror := by
   cases f with | mk d k s =>
     cases d <;> simp [Frame.attach, Frame.flip, Dir.flip]
 
 @[simp] lemma mirror_applyChild_bringUp (d₁ d₂ : Dir)
-    (t : BinaryTree α) :
+    (t : Tree α) :
     (applyChild d₁ d₂.bringUp t).mirror =
       applyChild d₁.flip d₂.flip.bringUp t.mirror := by
   rcases t with _ | ⟨l, k, r⟩
@@ -97,13 +97,13 @@ def Frame.flip (f : Frame α) : Frame α :=
 /-- Descend from `t` toward `q`, returning the subtree reached (either the
 matching node or `.empty` if `q` is absent) and the path above it. The head
 of the returned list is the deepest frame (parent of the returned subtree). -/
-def descend [LinearOrder α] (t : BinaryTree α) (q : α) : BinaryTree α × List (Frame α) :=
+def descend [LinearOrder α] (t : Tree α) (q : α) : Tree α × List (Frame α) :=
   go t []
 where
-  go : BinaryTree α → List (Frame α) → BinaryTree α × List (Frame α)
-  | .empty, acc => (.empty, acc)
-  | .node l k r, acc =>
-    if q = k then (.node l k r, acc)
+  go : Tree α → List (Frame α) → Tree α × List (Frame α)
+  | .nil, acc => (.nil, acc)
+  | .node k l r, acc =>
+    if q = k then (.node k l r, acc)
     else if q < k then go l ({ dir := .L, key := k, sibling := r } :: acc)
     else go r ({ dir := .R, key := k, sibling := l } :: acc)
 
@@ -115,7 +115,7 @@ up. Each double step (parent `f1`, grandparent `f2`) is:
   `f2.dir`-child (in direction `f1.dir`), then one outer rotation (in
   direction `f2.dir`).
 A leftover single frame is a plain zig/zag. -/
-def splayUp : BinaryTree α → List (Frame α) → BinaryTree α
+def splayUp : Tree α → List (Frame α) → Tree α
   | c, [] => c
   | c, [f] => f.dir.bringUp (f.attach c)
   | c, f1 :: f2 :: rest =>
@@ -129,25 +129,25 @@ def splayUp : BinaryTree α → List (Frame α) → BinaryTree α
 
 /-- Bottom-up splay: the "textbook" splay analysed by Tarjan, Sundar, and
 Elmasry. If `q` is absent the last visited ancestor is splayed to the root. -/
-def splay [LinearOrder α] (t : BinaryTree α) (q : α) : BinaryTree α :=
+def splay [LinearOrder α] (t : Tree α) (q : α) : Tree α :=
   match descend t q with
-  | (.empty, []) => .empty
-  | (.empty, f :: rest) => splayUp (f.attach .empty) rest
+  | (.nil, []) => .nil
+  | (.nil, f :: rest) => splayUp (f.attach .nil) rest
   | (x@(.node _ _ _), path) => splayUp x path
 
 /-- Reassemble a subtree `c` with its ancestral path `path` (deepest frame
 first) back into the original tree. -/
-def reassemble (c : BinaryTree α) (path : List (Frame α)) : BinaryTree α :=
+def reassemble (c : Tree α) (path : List (Frame α)) : Tree α :=
   path.foldl (fun c' f => f.attach c') c
 
-@[simp] lemma reassemble_nil (c : BinaryTree α) : reassemble c [] = c := rfl
+@[simp] lemma reassemble_nil (c : Tree α) : reassemble c [] = c := rfl
 
-@[simp] lemma reassemble_cons (c : BinaryTree α) (f : Frame α) (rest : List (Frame α)) :
+@[simp] lemma reassemble_cons (c : Tree α) (f : Frame α) (rest : List (Frame α)) :
     reassemble c (f :: rest) = reassemble (f.attach c) rest := rfl
 
 /-- Number of nodes a single frame contributes when re-attached: the
 ancestor itself plus its sibling subtree. -/
-def Frame.nodes (f : Frame α) : ℕ := 1 + f.sibling.num_nodes
+def Frame.nodes (f : Frame α) : ℕ := 1 + f.sibling.numNodes
 
 /-- Total number of nodes contributed by a path above a subtree. -/
 def pathNodes : List (Frame α) → ℕ
@@ -160,12 +160,12 @@ end Definitions
 /-! ### Unfolding and Induction Lemmas for `splayUp` -/
 section SplayUpInduction
 
-@[simp] theorem splayUp_nil (c : BinaryTree α) : splayUp c [] = c := rfl
+@[simp] theorem splayUp_nil (c : Tree α) : splayUp c [] = c := rfl
 
-@[simp] theorem splayUp_singleton (c : BinaryTree α) (f : Frame α) :
+@[simp] theorem splayUp_singleton (c : Tree α) (f : Frame α) :
     splayUp c [f] = f.dir.bringUp (f.attach c) := rfl
 
-theorem splayUp_cons_cons (c : BinaryTree α) (f1 f2 : Frame α) (rest : List (Frame α)) :
+theorem splayUp_cons_cons (c : Tree α) (f1 f2 : Frame α) (rest : List (Frame α)) :
     splayUp c (f1 :: f2 :: rest) =
       splayUp
         (if f1.dir = f2.dir then
@@ -175,13 +175,13 @@ theorem splayUp_cons_cons (c : BinaryTree α) (f1 f2 : Frame α) (rest : List (F
             (f2.attach (f1.attach c))))
         rest := rfl
 
-theorem splayUp_cons_cons_same (c : BinaryTree α) (f1 f2 : Frame α)
+theorem splayUp_cons_cons_same (c : Tree α) (f1 f2 : Frame α)
     (rest : List (Frame α)) (h : f1.dir = f2.dir) :
     splayUp c (f1 :: f2 :: rest) =
       splayUp (f2.dir.bringUp (f2.dir.bringUp (f2.attach (f1.attach c)))) rest := by
   rw [splayUp_cons_cons]; simp [h]
 
-theorem splayUp_cons_cons_opp (c : BinaryTree α) (f1 f2 : Frame α)
+theorem splayUp_cons_cons_opp (c : Tree α) (f1 f2 : Frame α)
     (rest : List (Frame α)) (h : f1.dir ≠ f2.dir) :
     splayUp c (f1 :: f2 :: rest) =
       splayUp (f2.dir.bringUp
@@ -192,12 +192,12 @@ theorem splayUp_cons_cons_opp (c : BinaryTree α) (f1 f2 : Frame α)
 singleton frame, and the general pair-cons step. The tree `c` is
 generalised automatically. -/
 theorem splayUp_induction
-    {motive : BinaryTree α → List (Frame α) → Prop}
+    {motive : Tree α → List (Frame α) → Prop}
     (nil : ∀ c, motive c [])
     (single : ∀ c f, motive c [f])
     (step : ∀ c f1 f2 rest,
       (∀ c', motive c' rest) → motive c (f1 :: f2 :: rest))
-    (c : BinaryTree α) (path : List (Frame α)) : motive c path := by
+    (c : Tree α) (path : List (Frame α)) : motive c path := by
   induction path using List.twoStepInduction generalizing c with
   | nil => exact nil c
   | singleton f => exact single c f
@@ -215,19 +215,19 @@ section NodeCount
     pathNodes (f :: rest) = f.nodes + pathNodes rest := rfl
 
 @[simp]
-theorem num_nodes_Frame_attach (c : BinaryTree α) (f : Frame α) :
+theorem num_nodes_Frame_attach (c : Tree α) (f : Frame α) :
     (f.attach c).num_nodes = c.num_nodes + f.nodes := by
   unfold Frame.attach Frame.nodes
   cases f.dir <;> simp <;> omega
 
 @[simp]
-theorem num_nodes_bringUp (d : Dir) (t : BinaryTree α) :
+theorem num_nodes_bringUp (d : Dir) (t : Tree α) :
     (d.bringUp t).num_nodes = t.num_nodes := by
   cases d <;> simp [Dir.bringUp]
 
 @[simp]
-theorem num_nodes_applyChild (d : Dir) (op : BinaryTree α → BinaryTree α)
-    (hop : ∀ s, (op s).num_nodes = s.num_nodes) (t : BinaryTree α) :
+theorem num_nodes_applyChild (d : Dir) (op : Tree α → Tree α)
+    (hop : ∀ s, (op s).num_nodes = s.num_nodes) (t : Tree α) :
     (applyChild d op t).num_nodes = t.num_nodes := by
   cases t with
   | empty => rfl
@@ -235,12 +235,12 @@ theorem num_nodes_applyChild (d : Dir) (op : BinaryTree α → BinaryTree α)
     cases d <;> simp [applyChild, hop]
 
 @[simp]
-theorem num_nodes_applyChild_bringUp (d₁ d₂ : Dir) (t : BinaryTree α) :
+theorem num_nodes_applyChild_bringUp (d₁ d₂ : Dir) (t : Tree α) :
     (applyChild d₁ d₂.bringUp t).num_nodes = t.num_nodes :=
   num_nodes_applyChild _ _ (num_nodes_bringUp _) _
 
 @[simp]
-theorem num_nodes_splayUp (c : BinaryTree α) (path : List (Frame α)) :
+theorem num_nodes_splayUp (c : Tree α) (path : List (Frame α)) :
     (splayUp c path).num_nodes = c.num_nodes + pathNodes path := by
   induction path using List.twoStepInduction generalizing c with
   | nil => simp [splayUp]
@@ -251,7 +251,7 @@ theorem num_nodes_splayUp (c : BinaryTree α) (path : List (Frame α)) :
     · rw [ih]; simp [Frame.nodes, pathNodes_cons]; omega
     · rw [ih]; simp [Frame.nodes, pathNodes_cons]; omega
 
-theorem num_nodes_descend_go [LinearOrder α] (t : BinaryTree α) (q : α) (acc : List (Frame α)) :
+theorem num_nodes_descend_go [LinearOrder α] (t : Tree α) (q : α) (acc : List (Frame α)) :
     let r := descend.go q t acc
     r.1.num_nodes + pathNodes r.2 = t.num_nodes + pathNodes acc := by
   induction t generalizing acc with
@@ -265,13 +265,13 @@ theorem num_nodes_descend_go [LinearOrder α] (t : BinaryTree α) (q : α) (acc
     · have := ihr (acc := ⟨.R, k, l⟩ :: acc)
       simp [Frame.nodes] at this ⊢; omega
 
-theorem num_nodes_descend [LinearOrder α] (t : BinaryTree α) (q : α) :
+theorem num_nodes_descend [LinearOrder α] (t : Tree α) (q : α) :
     (descend t q).1.num_nodes + pathNodes (descend t q).2 = t.num_nodes := by
   have := num_nodes_descend_go t q []
   simpa [descend] using this
 
 @[simp]
-theorem num_nodes_splay [LinearOrder α] (t : BinaryTree α) (q : α) :
+theorem num_nodes_splay [LinearOrder α] (t : Tree α) (q : α) :
     (splay t q).num_nodes = t.num_nodes := by
   unfold splay
   have hd := num_nodes_descend t q
@@ -298,7 +298,7 @@ section DescendLemmas
 
 @[simp] lemma descend_empty [LinearOrder α] (q : α) : descend .empty q = (.empty, []) := rfl
 
-lemma descend_go_append [LinearOrder α] (q : α) (t : BinaryTree α) (acc : List (Frame α)) :
+lemma descend_go_append [LinearOrder α] (q : α) (t : Tree α) (acc : List (Frame α)) :
     descend.go q t acc =
       ((descend.go q t []).1, (descend.go q t []).2 ++ acc) := by
   induction t generalizing acc with
@@ -312,15 +312,15 @@ lemma descend_go_append [LinearOrder α] (q : α) (t : BinaryTree α) (acc : Lis
     · rw [ihr (acc := ⟨.R, k, l⟩ :: acc),
         ihr (acc := [⟨.R, k, l⟩])]; simp
 
-lemma descend_node_eq [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) :
+lemma descend_node_eq [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) :
     descend (.node l k r) k = (.node l k r, []) := by
   simp [descend, descend.go]
 
-lemma descend_eq_descend_go [LinearOrder α] (t : BinaryTree α) (q : α) :
+lemma descend_eq_descend_go [LinearOrder α] (t : Tree α) (q : α) :
     descend t q = descend.go q t [] := rfl
 
-lemma descend_node_lt [LinearOrder α] {l : BinaryTree α} {k : α}
-    {r : BinaryTree α} {q : α} (h : q < k) :
+lemma descend_node_lt [LinearOrder α] {l : Tree α} {k : α}
+    {r : Tree α} {q : α} (h : q < k) :
     descend (.node l k r) q =
       ((descend l q).1,
        (descend l q).2 ++ [⟨.L, k, r⟩]) := by
@@ -329,8 +329,8 @@ lemma descend_node_lt [LinearOrder α] {l : BinaryTree α} {k : α}
   unfold descend.go
   rw [if_neg hne, if_pos h, descend_go_append q l [⟨.L, k, r⟩]]; rfl
 
-lemma descend_node_gt [LinearOrder α] {l : BinaryTree α} {k : α}
-    {r : BinaryTree α} {q : α} (h : k < q) :
+lemma descend_node_gt [LinearOrder α] {l : Tree α} {k : α}
+    {r : Tree α} {q : α} (h : k < q) :
     descend (.node l k r) q =
       ((descend r q).1,
        (descend r q).2 ++ [⟨.R, k, l⟩]) := by
@@ -340,11 +340,11 @@ lemma descend_node_gt [LinearOrder α] {l : BinaryTree α} {k : α}
   rw [if_neg hne, if_neg (not_lt.mpr h.le),
       descend_go_append q r [⟨.R, k, l⟩]]; rfl
 
-lemma reassemble_append (c : BinaryTree α) (p1 p2 : List (Frame α)) :
+lemma reassemble_append (c : Tree α) (p1 p2 : List (Frame α)) :
     reassemble c (p1 ++ p2) = reassemble (reassemble c p1) p2 := by
   simp [reassemble, List.foldl_append]
 
-theorem descend_go_preserves_tree [LinearOrder α] (t : BinaryTree α)
+theorem descend_go_preserves_tree [LinearOrder α] (t : Tree α)
   (q : α) (acc : List (Frame α)) :
     reassemble (descend.go q t acc).1 (descend.go q t acc).2 =
       reassemble t acc := by
@@ -357,12 +357,12 @@ theorem descend_go_preserves_tree [LinearOrder α] (t : BinaryTree α)
     · exact ihl (acc := ⟨.L, k, r⟩ :: acc)
     · exact ihr (acc := ⟨.R, k, l⟩ :: acc)
 
-theorem descend_preserves_tree [LinearOrder α] (t : BinaryTree α) (q : α) :
+theorem descend_preserves_tree [LinearOrder α] (t : Tree α) (q : α) :
     reassemble (descend t q).1 (descend t q).2 = t := by
   have := descend_go_preserves_tree t q []
   simpa [descend] using this
 
-lemma descend_go_length_le [LinearOrder α] (q : α) (t : BinaryTree α) (acc : List (Frame α)) :
+lemma descend_go_length_le [LinearOrder α] (q : α) (t : Tree α) (acc : List (Frame α)) :
     acc.length ≤ (descend.go q t acc).2.length := by
   induction t generalizing acc with
   | empty => simp [descend.go]