Lean4
theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r) :
@balance α l x r = balance' l x r := by
obtain - | ⟨ls, ll, lx, lr⟩ := l
· obtain - | ⟨rs, rl, rx, rr⟩ := r
· rfl
· rw [sr.eq_node'] at hr ⊢
obtain - | ⟨rls, rll, rlx, rlr⟩ := rl <;> obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr <;> dsimp [balance, balance']
· rfl
· have : size rrl = 0 ∧ size rrr = 0 := by
have := balancedSz_zero.1 hr.1.symm
rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
cases sr.2.2.2.1.size_eq_zero.1 this.1
cases sr.2.2.2.2.size_eq_zero.1 this.2
obtain rfl : rrs = 1 := sr.2.2.1
rw [if_neg, if_pos, rotateL_node, if_pos]; · rfl
all_goals dsimp only [size]; decide
· have : size rll = 0 ∧ size rlr = 0 := by
have := balancedSz_zero.1 hr.1
rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
cases sr.2.1.2.1.size_eq_zero.1 this.1
cases sr.2.1.2.2.size_eq_zero.1 this.2
obtain rfl : rls = 1 := sr.2.1.1
rw [if_neg, if_pos, rotateL_node, if_neg]; · rfl
all_goals dsimp only [size]; decide
· symm; rw [zero_add, if_neg, if_pos, rotateL]
· dsimp only [size_node]; split_ifs
· simp [node3L, node']; abel
· simp [node4L, node', sr.2.1.1]; abel
· apply Nat.zero_lt_succ
· exact not_le_of_gt (Nat.succ_lt_succ (add_pos sr.2.1.pos sr.2.2.pos))
· obtain - | ⟨rs, rl, rx, rr⟩ := r
· rw [sl.eq_node'] at hl ⊢
obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> dsimp [balance, balance']
· rfl
· have : size lrl = 0 ∧ size lrr = 0 := by
have := balancedSz_zero.1 hl.1.symm
rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
cases sl.2.2.2.1.size_eq_zero.1 this.1
cases sl.2.2.2.2.size_eq_zero.1 this.2
obtain rfl : lrs = 1 := sl.2.2.1
rw [if_neg, if_pos, rotateR_node, if_neg]; · rfl
all_goals dsimp only [size]; decide
· have : size lll = 0 ∧ size llr = 0 := by
have := balancedSz_zero.1 hl.1
rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
cases sl.2.1.2.1.size_eq_zero.1 this.1
cases sl.2.1.2.2.size_eq_zero.1 this.2
obtain rfl : lls = 1 := sl.2.1.1
rw [if_neg, if_pos, rotateR_node, if_pos]; · rfl
all_goals dsimp only [size]; decide
· symm; rw [if_neg, if_pos, rotateR]
· dsimp only [size_node]; split_ifs
· simp [node3R, node']; abel
· simp [node4R, node', sl.2.2.1]; abel
· apply Nat.zero_lt_succ
· exact not_le_of_gt (Nat.succ_lt_succ (add_pos sl.2.1.pos sl.2.2.pos))
· simp only [balance, id_eq, balance', size_node, gt_iff_lt]
symm; rw [if_neg]
· split_ifs with h h_1
· have rd : delta ≤ size rl + size rr :=
by
have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
rwa [sr.1, Nat.lt_succ_iff] at this
obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
· rw [size, zero_add] at rd
exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)
obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
· exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)
dsimp [rotateL]; split_ifs
· simp [node3L, node', sr.1]; abel
· simp [node4L, node', sr.1, sr.2.1.1]; abel
· have ld : delta ≤ size ll + size lr :=
by
have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
rwa [sl.1, Nat.lt_succ_iff] at this
obtain - | ⟨lls, lll, llx, llr⟩ := ll
· rw [size, zero_add] at ld
exact absurd (le_trans ld (balancedSz_zero.1 hl.1.symm)) (by decide)
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
· exact absurd (le_trans ld (balancedSz_zero.1 hl.1)) (by decide)
dsimp [rotateR]; split_ifs
· simp [node3R, node', sl.1]; abel
· simp [node4R, node', sl.1, sl.2.2.1]; abel
· simp [node']
· exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))
