Lean4
/-- **Internal use only**
O(1). Rebalance a tree which was previously balanced but has had one side change
by at most 1. -/
def balance (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α :=
by
rcases id l with _ | ⟨ls, ll, lx, lr⟩
· rcases id r with _ | ⟨rs, rl, rx, rr⟩
· exact ι x
· rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
· cases id rr
· exact node 2 nil x r
· exact node 3 (ι x) rx rr
· rcases id rr with _ | rrs
· exact node 3 (ι x) rlx ι rx
·
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⟩
· 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)
· refine if delta * ls < rs then ?_ else if delta * rs < ls then ?_ else node (ls + rs + 1) l x r
· rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
· exact nil
rcases id rr with _ | rrs
· 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)
· 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 (lrs + rs + 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)
