English
Erasing an element x from a valid tree yields a valid tree and the size strictly decreases.
Русский
Стирание элемента x из валидного дерева даёт валидное дерево и размер строго уменьшается.
LaTeX
$$$\\forall x,\\ t, a_1, a_2,\\ h:\\mathrm{Valid}' a_1 t a_2\\Rightarrow \\mathrm{Valid}' a_1(\\mathrm{erase}\\ x\\ t) a_2 \\land \\mathrm{Raised}(\\mathrm{erase}\\ x\\ t).size\\ t.size$$$
Lean4
theorem erase_aux [DecidableLE α] (x : α) {t a₁ a₂} (h : Valid' a₁ t a₂) :
Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size := by
induction t generalizing a₁ a₂ with
| nil => simpa [erase, Raised]
| node _ t_l t_x t_r t_ih_l t_ih_r =>
simp only [erase, size_node]
have t_ih_l' := t_ih_l h.left
have t_ih_r' := t_ih_r h.right
clear t_ih_l t_ih_r
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
cases cmpLE x t_x <;> rw [h.sz.1]
· suffices h_balanceable : _ by
constructor
· exact Valid'.balanceR t_l_valid h.right h_balanceable
· rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
repeat apply Raised.add_right
exact t_l_size
left; exists t_l.size; exact And.intro t_l_size h.bal.1
· have h_glue := Valid'.glue h.left h.right h.bal.1
obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
constructor
· exact h_glue_valid
· right; rw [h_glue_sized]
· suffices h_balanceable : _ by
constructor
· exact Valid'.balanceL h.left t_r_valid h_balanceable
· rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
apply Raised.add_right
apply Raised.add_left
exact t_r_size
right; exists t_r.size; exact And.intro t_r_size h.bal.1
