English
Let α be a total preorder with decidable ≤, and f a function satisfying a neighborhood containment condition. Then, for any valid tree t within bounds, inserting with insertWith f x t yields a valid tree and increases the size in the Raised sense.
Русский
Пусть α упорядочено полностью и ≤ разрешимо; если f удовлетворяет условию соседнего окружения, то для любой валидной дерева t вставка через insertWith f x t даёт валидное дерево и размер увеличивается в смысле отношения Raised.
LaTeX
$$$\\forall f,x,\\ hf:\\forall y(x \\le y \\land y \\le x \\rightarrow x \\le f(y) \\land f(y) \\le x)\\; \\forall t\\ o_1\\ o_2,\\ hl:\\mathrm{Valid}' o_1 t o_2 \\rightarrow \\mathrm{Bounded}\\ nil\\ o_1 x \\rightarrow \\mathrm{Bounded}\\ nil x o_2 \\rightarrow \\mathrm{Valid}' o_1 (\\mathrm{insertWith} f x t) o_2 \\land \\mathrm{Raised}(\\mathrm{size}\\ t, \\mathrm{size}(\\mathrm{insertWith} f x t))$$$
Lean4
theorem valid_aux [IsTotal α (· ≤ ·)] [DecidableLE α] (f : α → α) (x : α)
(hf : ∀ y, x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) :
∀ {t o₁ o₂},
Valid' o₁ t o₂ →
Bounded nil o₁ x →
Bounded nil x o₂ → Valid' o₁ (insertWith f x t) o₂ ∧ Raised (size t) (size (insertWith f x t))
| nil, _, _, _, bl, br => ⟨valid'_singleton bl br, Or.inr rfl⟩
| node sz l y r, o₁, o₂, h, bl, br => by
rw [insertWith, cmpLE]
split_ifs with h_1 h_2 <;> dsimp only
· rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩
refine ⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩
· rcases insertWith.valid_aux f x hf h.left bl (lt_of_le_not_ge h_1 h_2) with ⟨vl, e⟩
suffices H : _ by
refine ⟨vl.balanceL h.right H, ?_⟩
rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
exact (e.add_right _).add_right _
exact Or.inl ⟨_, e, h.3.1⟩
· have : y < x := lt_of_le_not_ge ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
suffices H : _ by
refine ⟨h.left.balanceR vr H, ?_⟩
rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
exact (e.add_left _).add_right _
exact Or.inr ⟨_, e, h.3.1⟩
