English
Let l, x, r be subtrees with hl, hr validity and certain nonempty/balance conditions; then the rotated node l.rotateL x r is valid.
Русский
Пусть существуют поддеревья l, x, r с валидностями hl, hr и некоторые условия баланса; тогда повернутое дерево l.rotateL x r является допустимым.
LaTeX
$$$ \forall l, x, r,\ hl, hr,\ H_\mathrm{cond} \Rightarrow \mathrm{Valid}'(o_1, (l.rotateL\ x\ r))\, o_2 $$$
Lean4
theorem rotateL {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂) (H1 : ¬size l + size r ≤ 1)
(H2 : delta * size l < size r) (H3 : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3) : Valid' o₁ (@rotateL α l x r) o₂ :=
by
obtain - | ⟨rs, rl, rx, rr⟩ := r; · cases H2
rw [hr.2.size_eq, Nat.lt_succ_iff] at H2
rw [hr.2.size_eq] at H3
replace H3 : 2 * (size rl + size rr) ≤ 9 * size l + 3 ∨ size rl + size rr ≤ 2 :=
H3.imp (@Nat.le_of_add_le_add_right _ 2 _) Nat.le_of_succ_le_succ
have H3_0 (l0 : size l = 0) : size rl + size rr ≤ 2 := by omega
have H3p : size l > 0 → 2 * (size rl + size rr) ≤ 9 * size l + 3 := fun l0 : 1 ≤ size l =>
(or_iff_left_of_imp <| by cutsat).1 H3
have ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1 := by omega
have hlp : size l > 0 → ¬size rl + size rr ≤ 1 := fun l0 hb =>
absurd (le_trans (le_trans (Nat.mul_le_mul_left _ l0) H2) hb) (by decide)
rw [Ordnode.rotateL_node]; split_ifs with h
· have rr0 : size rr > 0 := (mul_lt_mul_iff_right₀ (by decide)).1 (lt_of_le_of_lt (Nat.zero_le _) h : ratio * 0 < _)
suffices BalancedSz (size l) (size rl) ∧ BalancedSz (size l + size rl + 1) (size rr) by
exact hl.node3L hr.left hr.right this.1 this.2
rcases Nat.eq_zero_or_pos (size l) with l0 | l0
· rw [l0]; replace H3 := H3_0 l0
have := hr.3.1
rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
· rw [rl0] at this ⊢
rw [le_antisymm (balancedSz_zero.1 this.symm) rr0]
decide
have rr1 : size rr = 1 := le_antisymm (ablem rl0 H3) rr0
rw [add_comm] at H3
rw [rr1, show size rl = 1 from le_antisymm (ablem rr0 H3) rl0]
decide
replace H3 := H3p l0
rcases hr.3.1.resolve_left (hlp l0) with ⟨_, hb₂⟩
refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
· exact Valid'.rotateL_lemma₁ H2 hb₂
· exact Nat.le_of_lt_succ (Valid'.rotateL_lemma₂ H3 h)
· exact Valid'.rotateL_lemma₃ H2 h
· exact le_trans hb₂ (Nat.mul_le_mul_left _ <| le_trans (Nat.le_add_left _ _) (Nat.le_add_right _ _))
· rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
· rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h
replace h := h.resolve_left (by decide)
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1
cases H1 (by decide)
refine hl.node4L hr.left hr.right rl0 ?_
rcases Nat.eq_zero_or_pos (size l) with l0 | l0
· replace H3 := H3_0 l0
rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0
· have := hr.3.1
rw [rr0] at this
exact Or.inl ⟨l0, le_antisymm (balancedSz_zero.1 this) rl0, rr0.symm ▸ zero_le_one⟩
exact Or.inl ⟨l0, le_antisymm (ablem rr0 <| by rwa [add_comm]) rl0, ablem rl0 H3⟩
exact Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩
