English
Let l, x, m, y, r be nodes with Valid' structures hl, hm, hr and a nonempty m, and a balance condition H. Then the assembled node4L is a valid node between o1 and o2: Valid'(o1, node4L(l, x, m, y, r)) o2.
Русский
Пусть существуют узлы l, x, m, y, r с валидностями hl, hm, hr и m непусто, а также условие баланса H. Тогда построенный узел node4L является допустным узлом между o1 и o2: Valid'(o1, node4L(l, x, m, y, r)) o2.
LaTeX
$$$ \text{Let } l, x, m, y, r \text{ be nodes with } hl, hm, hr \text{ and } \text{size}(m) > 0 \text{ and balance condition } H. \text{ Then } \text{Valid}'(o_1, (\text{node4L }\alpha\ l\ x\ m\ y\ r))\ o_2.$$$
Lean4
theorem node4L {l} {x : α} {m} {y : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hm : Valid' x m y) (hr : Valid' (↑y) r o₂)
(Hm : 0 < size m)
(H :
size l = 0 ∧ size m = 1 ∧ size r ≤ 1 ∨
0 < size l ∧
ratio * size r ≤ size m ∧
delta * size l ≤ size m + size r ∧ 3 * (size m + size r) ≤ 16 * size l + 9 ∧ size m ≤ delta * size r) :
Valid' o₁ (@node4L α l x m y r) o₂ := by
obtain - | ⟨s, ml, z, mr⟩ := m; · cases Hm
suffices
BalancedSz (size l) (size ml) ∧
BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
from Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2
rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
· rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1
rw [l0, m1.1, m1.2]; revert r0;
rcases size r with (_ | _ | _) <;> [decide; decide; (intro r0; unfold BalancedSz delta; cutsat)]
· rcases Nat.eq_zero_or_pos (size r) with r0 | r0
· rw [r0] at mr₂; cases not_le_of_gt Hm mr₂
rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
by_cases mm : size ml + size mr ≤ 1
· dsimp [delta, ratio] at lr₁ mr₁
have r1 : r.size = 1 := by omega
have l1 : l.size = 1 := by omega
rw [r1, add_assoc] at lr₁
rw [l1, r1]
revert mm; cases size ml <;> cases size mr <;> intro mm
· decide
· rw [zero_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
decide
· rcases mm with (_ | ⟨⟨⟩⟩); decide
· rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩
rcases Nat.eq_zero_or_pos (size ml) with ml0 | ml0
· rw [ml0, mul_zero, Nat.le_zero] at mm₂
rw [ml0, mm₂] at mm; cases mm (by decide)
have : 2 * size l ≤ size ml + size mr + 1 :=
by
have := Nat.mul_le_mul_left ratio lr₁
rw [mul_left_comm, mul_add] at this
have := le_trans this (add_le_add_left mr₁ _)
rw [← Nat.succ_mul] at this
exact (mul_le_mul_iff_right₀ (by decide)).1 this
refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
· refine (mul_le_mul_iff_right₀ (by decide)).1 (le_trans this ?_)
rw [two_mul, Nat.succ_le_iff]
refine add_lt_add_of_lt_of_le ?_ mm₂
simpa using mul_lt_mul_of_pos_right (by decide : 1 < 3) ml0
· exact Nat.le_of_lt_succ (Valid'.node4L_lemma₁ lr₂ mr₂ mm₁)
· exact Valid'.node4L_lemma₂ mr₂
· exact Valid'.node4L_lemma₃ mr₁ mm₁
· exact Valid'.node4L_lemma₄ lr₁ mr₂ mm₁
· exact Valid'.node4L_lemma₅ lr₂ mr₁ mm₂
