Lean4
/-- **Internal use only**
O(1). Rebalance a tree which was previously balanced but has had its right
side grow by 1, or its left side shrink by 1. -/
def balanceR (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α :=
by
rcases id l with _ | ls
· rcases id r with _ | ⟨rs, rl, rx, rr⟩
· exact ι x
· rcases id rr with _ | rrs
· rcases rl with _ | ⟨_, _, rlx⟩
· exact node 2 nil x r
· exact node 3 (ι x) rlx ι rx
· rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
· exact node 3 (ι x) rx rr
·
exact
if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
else node (rs + 1) (node (size rll + 1) nil x rll) rlx (node (size rlr + rrs + 1) rlr rx rr)
· rcases id r with _ | ⟨rs, rl, rx, rr⟩
· exact node (ls + 1) l x nil
· refine if rs > delta * ls then ?_ else node (ls + rs + 1) l x r
rcases id rr with _ | rrs
· exact nil
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
· exact nil
exact
if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
else node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx (node (size rlr + rrs + 1) rlr rx rr)
