Lean4
/-- **Internal use only**
O(1). Rebalance a tree which was previously balanced but has had its left
side grow by 1, or its right side shrink by 1. -/
def balanceL (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α :=
by
rcases id r with _ | rs
· rcases id l with _ | ⟨ls, ll, lx, lr⟩
· exact ι x
· rcases id ll with _ | lls
· rcases lr with _ | ⟨_, _, lrx⟩
· exact node 2 l x nil
· exact node 3 (ι lx) lrx ι x
· rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
· exact node 3 ll lx ι x
·
exact
if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
else node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx (node (size lrr + 1) lrr x nil)
· rcases id l with _ | ⟨ls, ll, lx, lr⟩
· exact node (rs + 1) nil x r
· refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r
rcases id ll with _ | lls
· exact nil
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
· exact nil
exact
if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x r)
else node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx (node (size lrr + rs + 1) lrr x r)
