English
If two valid trees can be glued together under a separator and balanced sizes, then the glued tree is valid and its size equals the sum of the sizes of the parts.
Русский
Если два допустимых дерева можно соединить (glue) через разделитель и сбалансировать размеры, то полученное дерево валидно и его размер равен сумме размеров частей.
LaTeX
$$$\\forall l r o_1 o_2\\; (hl: Valid' o_1 l o_2) (hr: Valid' o_1 r o_2) (sep: l.All (\\lambda x. r.All (\\lambda y. x < y))) (bal: BalancedSz (size l) (size r)) :\\n Valid' o_1 (l.glue r) o_2 \\land size (l.glue r) = size l + size r$$$
Lean4
theorem glue_aux {l r o₁ o₂} (hl : Valid' o₁ l o₂) (hr : Valid' o₁ r o₂) (sep : l.All fun x => r.All fun y => x < y)
(bal : BalancedSz (size l) (size r)) : Valid' o₁ (@glue α l r) o₂ ∧ size (glue l r) = size l + size r :=
by
obtain - | ⟨ls, ll, lx, lr⟩ := l; · exact ⟨hr, (zero_add _).symm⟩
obtain - | ⟨rs, rl, rx, rr⟩ := r; · exact ⟨hl, rfl⟩
dsimp [glue]; split_ifs
· rw [splitMax_eq]
· obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl
suffices H : _ by
refine ⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩
· refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂) lx lr hl.1.2.to_nil (sep.2.2.imp ?_)
exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)
· exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2
· rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.2.1]; rfl
refine Or.inl ⟨_, Or.inr e, ?_⟩
rwa [hl.2.eq_node'] at bal
· rw [splitMin_eq]
· obtain ⟨v, e⟩ := Valid'.eraseMin_aux hr
suffices H : _ by
refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩
· refine
@findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α)) _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil
exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)
·
exact
@findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
(all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx) (sep.imp fun y hy => hy.2.1)
· rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl
refine Or.inr ⟨_, Or.inr e, ?_⟩
rwa [hr.2.eq_node'] at bal
