merge_aux — Mathlib

English

Let l and r be two ordered trees with a feasibility relation hl and hr, and suppose all elements of l are less than all elements of r (sep). Then l.merge r is a valid tree and its size equals size(l) + size(r).

Русский

Пусть l и r — два упорядоченных дерева; если hl и hr верны и все элементы l меньше всех элементов r, то l.merge r образует корректное дерево и его размер равен размеру l плюс размеру r.

LaTeX

$$$\\forall l,r\\; hl:\\mathrm{Valid}(l)\\; hr:\\mathrm{Valid}(r)\\; sep:\\ l.All(\\lambda x. r.All(\\lambda y. x

Lean4

theorem merge_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) :
    Valid' o₁ (@merge α l r) o₂ ∧ size (merge l r) = size l + size r :=
  by
  induction l generalizing o₁ o₂ r with
  | nil => exact ⟨hr, (zero_add _).symm⟩
  | node ls ll lx lr _ IHlr => ?_
  induction r generalizing o₁ o₂ with
  | nil => exact ⟨hl, rfl⟩
  | node rs rl rx rr IHrl _ => ?_
  rw [merge_node]; split_ifs with h h_1
  · obtain ⟨v, e⟩ := IHrl (hl.of_lt hr.1.1.to_nil <| sep.imp fun x h => h.2.1) hr.left (sep.imp fun x h => h.1)
    exact Valid'.merge_aux₁ hl hr h v e
  · obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2
    have := Valid'.merge_aux₁ hr.dual hl.dual h_1 v.dual
    rw [size_dual, add_comm, size_dual, ← dual_balanceR, ← Valid'.dual_iff, size_dual, add_comm rs] at this
    exact this e
  · refine Valid'.glue_aux hl hr sep (Or.inr ⟨not_lt.1 h_1, not_lt.1 h⟩)

Похожие утверждения