import data.ordmap.ordnode

import algebra.order.ring.defs

import data.nat.dist

import tactic.linarith

variable {α : Type*}

namespace ordnode

theorem not_le_delta {s} (H : 1 ≤ s) : ¬ s ≤ delta * 0 :=

not_le_of_gt H

theorem delta_lt_false {a b : ℕ}

(h₁ : delta * a < b) (h₂ : delta * b < a) : false :=

not_le_of_lt (lt_trans ((mul_lt_mul_left dec_trivial).2 h₁) h₂) $

by simpa [mul_assoc] using nat.mul_le_mul_right a (dec_trivial : 1 ≤ delta * delta)

def real_size : ordnode α → ℕ

| nil := 0

| (node _ l _ r) := real_size l + real_size r + 1

def sized : ordnode α → Prop

| nil := true

| (node s l _ r) := s = size l + size r + 1 ∧ sized l ∧ sized r

theorem sized.node' {l x r} (hl : @sized α l) (hr : sized r) : sized (node' l x r) :=

⟨rfl, hl, hr⟩

theorem sized.eq_node' {s l x r} (h : @sized α (node s l x r)) : node s l x r = node' l x r :=

by rw h.1; refl

theorem sized.size_eq {s l x r} (H : sized (@node α s l x r)) :

size (@node α s l x r) = size l + size r + 1 := H.1

@[elab_as_eliminator] theorem sized.induction {t} (hl : @sized α t)

{C : ordnode α → Prop} (H0 : C nil)

(H1 : ∀ l x r, C l → C r → C (node' l x r)) : C t :=

induction t, {exact H0},

rw hl.eq_node',

exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

theorem size_eq_real_size : ∀ {t : ordnode α}, sized t → size t = real_size t

| nil _ := rfl

| (node s l x r) ⟨h₁, h₂, h₃⟩ :=

by rw [size, h₁, size_eq_real_size h₂, size_eq_real_size h₃]; refl

@[simp] theorem sized.size_eq_zero {t : ordnode α} (ht : sized t) : size t = 0 ↔ t = nil :=

by cases t; [simp, simp [ht.1]]

theorem sized.pos {s l x r} (h : sized (@node α s l x r)) : 0 < s :=

by rw h.1; apply nat.le_add_left

theorem dual_dual : ∀ (t : ordnode α), dual (dual t) = t

| nil := rfl

| (node s l x r) := by rw [dual, dual, dual_dual, dual_dual]

@[simp] theorem size_dual (t : ordnode α) : size (dual t) = size t :=

by cases t; refl

def balanced_sz (l r : ℕ) : Prop :=

l + r ≤ 1 ∨ (l ≤ delta * r ∧ r ≤ delta * l)

instance balanced_sz.dec : decidable_rel balanced_sz := λ l r, or.decidable

def balanced : ordnode α → Prop

| nil := true

| (node _ l _ r) := balanced_sz (size l) (size r) ∧ balanced l ∧ balanced r

instance balanced.dec : decidable_pred (@balanced α) | t :=

by induction t; unfold balanced; resetI; apply_instance

theorem balanced_sz.symm {l r : ℕ} : balanced_sz l r → balanced_sz r l :=

or.imp (by rw add_comm; exact id) and.symm

theorem balanced_sz_zero {l : ℕ} : balanced_sz l 0 ↔ l ≤ 1 :=

by simp [balanced_sz] { contextual := tt }

theorem balanced_sz_up {l r₁ r₂ : ℕ} (h₁ : r₁ ≤ r₂)

(h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l)

(H : balanced_sz l r₁) : balanced_sz l r₂ :=

refine or_iff_not_imp_left.2 (λ h, _),

refine ⟨_, h₂.resolve_left h⟩,

cases H,

{ cases r₂,

{ cases h (le_trans (nat.add_le_add_left (nat.zero_le _) _) H) },

{ exact le_trans (le_trans (nat.le_add_right _ _) H) (nat.le_add_left 1 _) } },

{ exact le_trans H.1 (nat.mul_le_mul_left _ h₁) }

theorem balanced_sz_down {l r₁ r₂ : ℕ} (h₁ : r₁ ≤ r₂)

(h₂ : l + r₂ ≤ 1 ∨ l ≤ delta * r₁)

(H : balanced_sz l r₂) : balanced_sz l r₁ :=

have l + r₂ ≤ 1 → balanced_sz l r₁, from

λ H, or.inl (le_trans (nat.add_le_add_left h₁ _) H),

or.cases_on H this (λ H, or.cases_on h₂ this (λ h₂,

or.inr ⟨h₂, le_trans h₁ H.2⟩))

theorem balanced.dual : ∀ {t : ordnode α}, balanced t → balanced (dual t)

| nil h := ⟨⟩

| (node s l x r) ⟨b, bl, br⟩ :=

⟨by rw [size_dual, size_dual]; exact b.symm, br.dual, bl.dual⟩

def node3_l (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) : ordnode α :=

node' (node' l x m) y r

def node3_r (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) : ordnode α :=

node' l x (node' m y r)

def node4_l : ordnode α → α → ordnode α → α → ordnode α → ordnode α

| l x (node _ ml y mr) z r := node' (node' l x ml) y (node' mr z r)

| l x nil z r := node3_l l x nil z r -- should not happen

def node4_r : ordnode α → α → ordnode α → α → ordnode α → ordnode α

| l x (node _ ml y mr) z r := node' (node' l x ml) y (node' mr z r)

| l x nil z r := node3_r l x nil z r -- should not happen

def rotate_l : ordnode α → α → ordnode α → ordnode α

| l x (node _ m y r) :=

if size m < ratio * size r then node3_l l x m y r else node4_l l x m y r

| l x nil := node' l x nil -- should not happen

def rotate_r : ordnode α → α → ordnode α → ordnode α

| (node _ l x m) y r :=

if size m < ratio * size l then node3_r l x m y r else node4_r l x m y r

| nil y r := node' nil y r -- should not happen

def balance_l' (l : ordnode α) (x : α) (r : ordnode α) : ordnode α :=

if size l + size r ≤ 1 then node' l x r else

if size l > delta * size r then rotate_r l x r else

node' l x r

def balance_r' (l : ordnode α) (x : α) (r : ordnode α) : ordnode α :=

if size l + size r ≤ 1 then node' l x r else

if size r > delta * size l then rotate_l l x r else

node' l x r

def balance' (l : ordnode α) (x : α) (r : ordnode α) : ordnode α :=

if size l + size r ≤ 1 then node' l x r else

if size r > delta * size l then rotate_l l x r else

if size l > delta * size r then rotate_r l x r else

node' l x r

theorem dual_node' (l : ordnode α) (x : α) (r : ordnode α) :

dual (node' l x r) = node' (dual r) x (dual l) := by simp [node', add_comm]

theorem dual_node3_l (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :

dual (node3_l l x m y r) = node3_r (dual r) y (dual m) x (dual l) :=

by simp [node3_l, node3_r, dual_node']

theorem dual_node3_r (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :

dual (node3_r l x m y r) = node3_l (dual r) y (dual m) x (dual l) :=

by simp [node3_l, node3_r, dual_node']

theorem dual_node4_l (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :

dual (node4_l l x m y r) = node4_r (dual r) y (dual m) x (dual l) :=

by cases m; simp [node4_l, node4_r, dual_node3_l, dual_node']

theorem dual_node4_r (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :

dual (node4_r l x m y r) = node4_l (dual r) y (dual m) x (dual l) :=

by cases m; simp [node4_l, node4_r, dual_node3_r, dual_node']

theorem dual_rotate_l (l : ordnode α) (x : α) (r : ordnode α) :

dual (rotate_l l x r) = rotate_r (dual r) x (dual l) :=

by cases r; simp [rotate_l, rotate_r, dual_node'];

split_ifs; simp [dual_node3_l, dual_node4_l]

theorem dual_rotate_r (l : ordnode α) (x : α) (r : ordnode α) :

dual (rotate_r l x r) = rotate_l (dual r) x (dual l) :=

by rw [← dual_dual (rotate_l _ _ _), dual_rotate_l, dual_dual, dual_dual]

theorem dual_balance' (l : ordnode α) (x : α) (r : ordnode α) :

dual (balance' l x r) = balance' (dual r) x (dual l) :=

simp [balance', add_comm], split_ifs; simp [dual_node', dual_rotate_l, dual_rotate_r],

cases delta_lt_false h_1 h_2

theorem dual_balance_l (l : ordnode α) (x : α) (r : ordnode α) :

dual (balance_l l x r) = balance_r (dual r) x (dual l) :=

unfold balance_l balance_r,

cases r with rs rl rx rr,

{ cases l with ls ll lx lr, {refl},

cases ll with lls lll llx llr; cases lr with lrs lrl lrx lrr;

dsimp only [dual]; try {refl},

split_ifs; repeat {simp [h, add_comm]} },

{ cases l with ls ll lx lr, {refl},

dsimp only [dual],

split_ifs, swap, {simp [add_comm]},

cases ll with lls lll llx llr; cases lr with lrs lrl lrx lrr; try {refl},

dsimp only [dual],

split_ifs; simp [h, add_comm] },

theorem dual_balance_r (l : ordnode α) (x : α) (r : ordnode α) :

dual (balance_r l x r) = balance_l (dual r) x (dual l) :=

by rw [← dual_dual (balance_l _ _ _), dual_balance_l, dual_dual, dual_dual]

theorem sized.node3_l {l x m y r}

(hl : @sized α l) (hm : sized m) (hr : sized r) : sized (node3_l l x m y r) :=

(hl.node' hm).node' hr

theorem sized.node3_r {l x m y r}

(hl : @sized α l) (hm : sized m) (hr : sized r) : sized (node3_r l x m y r) :=

hl.node' (hm.node' hr)

theorem sized.node4_l {l x m y r}

(hl : @sized α l) (hm : sized m) (hr : sized r) : sized (node4_l l x m y r) :=

by cases m; [exact (hl.node' hm).node' hr,

exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]

theorem node3_l_size {l x m y r} :

size (@node3_l α l x m y r) = size l + size m + size r + 2 :=

by dsimp [node3_l, node', size]; rw add_right_comm _ 1

theorem node3_r_size {l x m y r} :

size (@node3_r α l x m y r) = size l + size m + size r + 2 :=

by dsimp [node3_r, node', size]; rw [← add_assoc, ← add_assoc]

theorem node4_l_size {l x m y r} (hm : sized m) :

size (@node4_l α l x m y r) = size l + size m + size r + 2 :=

by cases m; simp [node4_l, node3_l, node', add_comm, add_left_comm]; [skip, simp [size, hm.1]];

rw [← add_assoc, ← bit0]; simp [add_comm, add_left_comm]

theorem sized.dual : ∀ {t : ordnode α} (h : sized t), sized (dual t)

| nil h := ⟨⟩

| (node s l x r) ⟨rfl, sl, sr⟩ := ⟨by simp [size_dual, add_comm], sized.dual sr, sized.dual sl⟩

theorem sized.dual_iff {t : ordnode α} : sized (dual t) ↔ sized t :=

⟨λ h, by rw ← dual_dual t; exact h.dual, sized.dual⟩

theorem sized.rotate_l {l x r} (hl : @sized α l) (hr : sized r) : sized (rotate_l l x r) :=

cases r, {exact hl.node' hr},

rw rotate_l, split_ifs,

{ exact hl.node3_l hr.2.1 hr.2.2 },

{ exact hl.node4_l hr.2.1 hr.2.2 }

theorem sized.rotate_r {l x r} (hl : @sized α l) (hr : sized r) : sized (rotate_r l x r) :=

sized.dual_iff.1 $ by rw dual_rotate_r; exact hr.dual.rotate_l hl.dual

theorem sized.rotate_l_size {l x r} (hm : sized r) :

size (@rotate_l α l x r) = size l + size r + 1 :=

cases r; simp [rotate_l],

simp [size, hm.1, add_comm, add_left_comm], rw [← add_assoc, ← bit0], simp,

split_ifs; simp [node3_l_size, node4_l_size hm.2.1, add_comm, add_left_comm]

theorem sized.rotate_r_size {l x r} (hl : sized l) :

size (@rotate_r α l x r) = size l + size r + 1 :=

by rw [← size_dual, dual_rotate_r, hl.dual.rotate_l_size,

size_dual, size_dual, add_comm (size l)]

theorem sized.balance' {l x r} (hl : @sized α l) (hr : sized r) : sized (balance' l x r) :=

unfold balance', split_ifs,

{ exact hl.node' hr },

{ exact hl.rotate_l hr },

{ exact hl.rotate_r hr },

{ exact hl.node' hr }

theorem size_balance' {l x r} (hl : @sized α l) (hr : sized r) :

size (@balance' α l x r) = size l + size r + 1 :=

unfold balance', split_ifs,

{ refl },

{ exact hr.rotate_l_size },

{ exact hl.rotate_r_size },

{ refl }

theorem all.imp {P Q : α → Prop} (H : ∀ a, P a → Q a) : ∀ {t}, all P t → all Q t

| nil h := ⟨⟩

| (node _ l x r) ⟨h₁, h₂, h₃⟩ := ⟨h₁.imp, H _ h₂, h₃.imp⟩

theorem any.imp {P Q : α → Prop} (H : ∀ a, P a → Q a) : ∀ {t}, any P t → any Q t

| nil := id

| (node _ l x r) := or.imp any.imp $ or.imp (H _) any.imp

theorem all_singleton {P : α → Prop} {x : α} : all P (singleton x) ↔ P x :=

⟨λ h, h.2.1, λ h, ⟨⟨⟩, h, ⟨⟩⟩⟩

theorem any_singleton {P : α → Prop} {x : α} : any P (singleton x) ↔ P x :=

⟨by rintro (⟨⟨⟩⟩ | h | ⟨⟨⟩⟩); exact h, λ h, or.inr (or.inl h)⟩

theorem all_dual {P : α → Prop} : ∀ {t : ordnode α},

all P (dual t) ↔ all P t

| nil := iff.rfl

| (node s l x r) :=

⟨λ ⟨hr, hx, hl⟩, ⟨all_dual.1 hl, hx, all_dual.1 hr⟩,

λ ⟨hl, hx, hr⟩, ⟨all_dual.2 hr, hx, all_dual.2 hl⟩⟩

theorem all_iff_forall {P : α → Prop} : ∀ {t}, all P t ↔ ∀ x, emem x t → P x

| nil := (iff_true_intro $ by rintro _ ⟨⟩).symm

| (node _ l x r) :=

by simp [all, emem, all_iff_forall, any, or_imp_distrib, forall_and_distrib]

theorem any_iff_exists {P : α → Prop} : ∀ {t}, any P t ↔ ∃ x, emem x t ∧ P x

| nil := ⟨by rintro ⟨⟩, by rintro ⟨_, ⟨⟩, _⟩⟩

| (node _ l x r) :=

by simp [any, emem, any_iff_exists, or_and_distrib_right, exists_or_distrib]

theorem emem_iff_all {x : α} {t} : emem x t ↔ ∀ P, all P t → P x :=

⟨λ h P al, all_iff_forall.1 al _ h,

λ H, H _ $ all_iff_forall.2 $ λ _, id⟩

theorem all_node' {P l x r} :

@all α P (node' l x r) ↔ all P l ∧ P x ∧ all P r := iff.rfl

theorem all_node3_l {P l x m y r} :

@all α P (node3_l l x m y r) ↔ all P l ∧ P x ∧ all P m ∧ P y ∧ all P r :=

by simp [node3_l, all_node', and_assoc]

theorem all_node3_r {P l x m y r} :

@all α P (node3_r l x m y r) ↔ all P l ∧ P x ∧ all P m ∧ P y ∧ all P r := iff.rfl

theorem all_node4_l {P l x m y r} :

@all α P (node4_l l x m y r) ↔ all P l ∧ P x ∧ all P m ∧ P y ∧ all P r :=

by cases m; simp [node4_l, all_node', all, all_node3_l, and_assoc]

theorem all_node4_r {P l x m y r} :

@all α P (node4_r l x m y r) ↔ all P l ∧ P x ∧ all P m ∧ P y ∧ all P r :=

by cases m; simp [node4_r, all_node', all, all_node3_r, and_assoc]

theorem all_rotate_l {P l x r} :

@all α P (rotate_l l x r) ↔ all P l ∧ P x ∧ all P r :=

by cases r; simp [rotate_l, all_node'];

split_ifs; simp [all_node3_l, all_node4_l, all]

theorem all_rotate_r {P l x r} :

@all α P (rotate_r l x r) ↔ all P l ∧ P x ∧ all P r :=

by rw [← all_dual, dual_rotate_r, all_rotate_l];

simp [all_dual, and_comm, and.left_comm]

theorem all_balance' {P l x r} :

@all α P (balance' l x r) ↔ all P l ∧ P x ∧ all P r :=

by rw balance'; split_ifs; simp [all_node', all_rotate_l, all_rotate_r]

theorem foldr_cons_eq_to_list : ∀ (t : ordnode α) (r : list α),

t.foldr list.cons r = to_list t ++ r

| nil r := rfl

| (node _ l x r) r' := by rw [foldr, foldr_cons_eq_to_list, foldr_cons_eq_to_list,

← list.cons_append, ← list.append_assoc, ← foldr_cons_eq_to_list]; refl

@[simp] theorem to_list_nil : to_list (@nil α) = [] := rfl

@[simp] theorem to_list_node (s l x r) : to_list (@node α s l x r) = to_list l ++ x :: to_list r :=

by rw [to_list, foldr, foldr_cons_eq_to_list]; refl

theorem emem_iff_mem_to_list {x : α} {t} : emem x t ↔ x ∈ to_list t :=

by unfold emem; induction t; simp [any, *, or_assoc]

theorem length_to_list' : ∀ t : ordnode α, (to_list t).length = t.real_size

| nil := rfl

| (node _ l _ r) := by rw [to_list_node, list.length_append, list.length_cons,

length_to_list', length_to_list']; refl

theorem length_to_list {t : ordnode α} (h : sized t) : (to_list t).length = t.size :=

by rw [length_to_list', size_eq_real_size h]

theorem equiv_iff {t₁ t₂ : ordnode α} (h₁ : sized t₁) (h₂ : sized t₂) :

equiv t₁ t₂ ↔ to_list t₁ = to_list t₂ :=

and_iff_right_of_imp $ λ h, by rw [← length_to_list h₁, h, length_to_list h₂]

theorem pos_size_of_mem [has_le α] [@decidable_rel α (≤)]

{x : α} {t : ordnode α} (h : sized t) (h_mem : x ∈ t) : 0 < size t :=

by { cases t, { contradiction }, { simp [h.1] } }

theorem find_min'_dual : ∀ t (x : α), find_min' (dual t) x = find_max' x t

| nil x := rfl

| (node _ l x r) _ := find_min'_dual r x

theorem find_max'_dual (t) (x : α) : find_max' x (dual t) = find_min' t x :=

by rw [← find_min'_dual, dual_dual]

theorem find_min_dual : ∀ t : ordnode α, find_min (dual t) = find_max t

| nil := rfl

| (node _ l x r) := congr_arg some $ find_min'_dual _ _

theorem find_max_dual (t : ordnode α) : find_max (dual t) = find_min t :=

by rw [← find_min_dual, dual_dual]

theorem dual_erase_min : ∀ t : ordnode α, dual (erase_min t) = erase_max (dual t)

| nil := rfl

| (node _ nil x r) := rfl

| (node _ l@(node _ _ _ _) x r) :=

by rw [erase_min, dual_balance_r, dual_erase_min, dual, dual, dual, erase_max]

theorem dual_erase_max (t : ordnode α) : dual (erase_max t) = erase_min (dual t) :=

by rw [← dual_dual (erase_min _), dual_erase_min, dual_dual]

theorem split_min_eq : ∀ s l (x : α) r,

split_min' l x r = (find_min' l x, erase_min (node s l x r))

| _ nil x r := rfl

| _ (node ls ll lx lr) x r :=

by rw [split_min', split_min_eq, split_min', find_min', erase_min]

theorem split_max_eq : ∀ s l (x : α) r,

split_max' l x r = (erase_max (node s l x r), find_max' x r)

| _ l x nil := rfl

| _ l x (node ls ll lx lr) :=

by rw [split_max', split_max_eq, split_max', find_max', erase_max]

theorem find_min'_all {P : α → Prop} : ∀ t (x : α), all P t → P x → P (find_min' t x)

| nil x h hx := hx

| (node _ ll lx lr) x ⟨h₁, h₂, h₃⟩ hx := find_min'_all _ _ h₁ h₂

theorem find_max'_all {P : α → Prop} : ∀ (x : α) t, P x → all P t → P (find_max' x t)

| x nil hx h := hx

| x (node _ ll lx lr) hx ⟨h₁, h₂, h₃⟩ := find_max'_all _ _ h₂ h₃

@[simp] theorem merge_nil_left (t : ordnode α) : merge t nil = t := by cases t; refl

@[simp] theorem merge_nil_right (t : ordnode α) : merge nil t = t := rfl

@[simp] theorem merge_node {ls ll lx lr rs rl rx rr} :

merge (@node α ls ll lx lr) (node rs rl rx rr) =

if delta * ls < rs then

balance_l (merge (node ls ll lx lr) rl) rx rr

else if delta * rs < ls then

balance_r ll lx (merge lr (node rs rl rx rr))

else glue (node ls ll lx lr) (node rs rl rx rr) := rfl

theorem dual_insert [preorder α] [is_total α (≤)] [@decidable_rel α (≤)] (x : α) :

∀ t : ordnode α, dual (ordnode.insert x t) = @ordnode.insert αᵒᵈ _ _ x (dual t)

| nil := rfl

| (node _ l y r) := begin

have : @cmp_le αᵒᵈ _ _ x y = cmp_le y x := rfl,

rw [ordnode.insert, dual, ordnode.insert, this, ← cmp_le_swap x y],

cases cmp_le x y;

simp [ordering.swap, ordnode.insert, dual_balance_l, dual_balance_r, dual_insert]

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 :=

cases l with ls ll lx lr,

{ cases r with rs rl rx rr,

{ refl },

{ rw sr.eq_node' at hr ⊢,

cases rl with rls rll rlx rlr; cases rr with rrs rrl rrx rrr;

dsimp [balance, balance'],

{ refl },

{ have : size rrl = 0 ∧ size rrr = 0,

{ have := balanced_sz_zero.1 hr.1.symm,

rwa [size, sr.2.2.1, nat.succ_le_succ_iff,

le_zero_iff, add_eq_zero_iff] 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, rotate_l, if_pos], {refl},

all_goals {exact dec_trivial} },

{ have : size rll = 0 ∧ size rlr = 0,

{ have := balanced_sz_zero.1 hr.1,

rwa [size, sr.2.1.1, nat.succ_le_succ_iff,

le_zero_iff, add_eq_zero_iff] 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, rotate_l, if_neg], {refl},

all_goals {exact dec_trivial} },

{ symmetry, rw [zero_add, if_neg, if_pos, rotate_l],

{ split_ifs,

{ simp [node3_l, node', add_comm, add_left_comm] },

{ simp [node4_l, node', sr.2.1.1, add_comm, add_left_comm] } },

{ exact dec_trivial },

{ exact not_le_of_gt (nat.succ_lt_succ

(add_pos sr.2.1.pos sr.2.2.pos)) } } } },

{ cases r with rs rl rx rr,

{ rw sl.eq_node' at hl ⊢,

cases ll with lls lll llx llr; cases lr with lrs lrl lrx lrr;

dsimp [balance, balance'],

{ refl },

{ have : size lrl = 0 ∧ size lrr = 0,

{ have := balanced_sz_zero.1 hl.1.symm,

rwa [size, sl.2.2.1, nat.succ_le_succ_iff,

le_zero_iff, add_eq_zero_iff] 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_neg, if_pos, rotate_r, if_neg], {refl},

all_goals {exact dec_trivial} },

{ have : size lll = 0 ∧ size llr = 0,

{ have := balanced_sz_zero.1 hl.1,

rwa [size, sl.2.1.1, nat.succ_le_succ_iff,

le_zero_iff, add_eq_zero_iff] 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_neg, if_pos, rotate_r, if_pos], {refl},

all_goals {exact dec_trivial} },

{ symmetry, rw [if_neg, if_neg, if_pos, rotate_r],

{ split_ifs,

{ simp [node3_r, node', add_comm, add_left_comm] },

{ simp [node4_r, node', sl.2.2.1, add_comm, add_left_comm] } },

{ exact dec_trivial },

{ exact dec_trivial },

{ exact not_le_of_gt (nat.succ_lt_succ

(add_pos sl.2.1.pos sl.2.2.pos)) } } },

{ simp [balance, balance'],

symmetry, rw [if_neg],

{ split_ifs,

{ have rd : delta ≤ size rl + size rr,

{ have := lt_of_le_of_lt (nat.mul_le_mul_left _ sl.pos) h,

rwa [sr.1, nat.lt_succ_iff] at this },

cases rl with rls rll rlx rlr,

{ rw [size, zero_add] at rd,

exact absurd (le_trans rd (balanced_sz_zero.1 hr.1.symm)) dec_trivial },

cases rr with rrs rrl rrx rrr,

{ exact absurd (le_trans rd (balanced_sz_zero.1 hr.1)) dec_trivial },

dsimp [rotate_l], split_ifs,

{ simp [node3_l, node', sr.1, add_comm, add_left_comm] },

{ simp [node4_l, node', sr.1, sr.2.1.1, add_comm, add_left_comm] } },

{ have ld : delta ≤ size ll + size lr,

{ have := lt_of_le_of_lt (nat.mul_le_mul_left _ sr.pos) h_1,

rwa [sl.1, nat.lt_succ_iff] at this },

cases ll with lls lll llx llr,

{ rw [size, zero_add] at ld,

exact absurd (le_trans ld (balanced_sz_zero.1 hl.1.symm)) dec_trivial },

cases lr with lrs lrl lrx lrr,

{ exact absurd (le_trans ld (balanced_sz_zero.1 hl.1)) dec_trivial },

dsimp [rotate_r], split_ifs,

{ simp [node3_r, node', sl.1, add_comm, add_left_comm] },

{ simp [node4_r, node', sl.1, sl.2.2.1, add_comm, add_left_comm] } },

{ simp [node'] } },

{ exact not_le_of_gt (add_le_add sl.pos sr.pos : 2 ≤ ls + rs) } } }

theorem balance_l_eq_balance {l x r}

(sl : sized l) (sr : sized r)

(H1 : size l = 0 → size r ≤ 1)

(H2 : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l) :

@balance_l α l x r = balance l x r :=

cases r with rs rl rx rr,

{ refl },

{ cases l with ls ll lx lr,

{ have : size rl = 0 ∧ size rr = 0,

{ have := H1 rfl,

rwa [size, sr.1, nat.succ_le_succ_iff,

le_zero_iff, add_eq_zero_iff] at this },

cases sr.2.1.size_eq_zero.1 this.1,

cases sr.2.2.size_eq_zero.1 this.2,

rw sr.eq_node', refl },

{ replace H2 : ¬ rs > delta * ls := not_lt_of_le (H2 sl.pos sr.pos),

simp [balance_l, balance, H2]; split_ifs; simp [add_comm] } }

def raised (n m : ℕ) : Prop := m = n ∨ m = n + 1

theorem raised_iff {n m} : raised n m ↔ n ≤ m ∧ m ≤ n + 1 :=

split, rintro (rfl | rfl),

{ exact ⟨le_rfl, nat.le_succ _⟩ },

{ exact ⟨nat.le_succ _, le_rfl⟩ },

{ rintro ⟨h₁, h₂⟩,

rcases eq_or_lt_of_le h₁ with rfl | h₁,

{ exact or.inl rfl },

{ exact or.inr (le_antisymm h₂ h₁) } }

theorem raised.dist_le {n m} (H : raised n m) : nat.dist n m ≤ 1 :=

by cases raised_iff.1 H with H1 H2;

rwa [nat.dist_eq_sub_of_le H1, tsub_le_iff_left]

theorem raised.dist_le' {n m} (H : raised n m) : nat.dist m n ≤ 1 :=

by rw nat.dist_comm; exact H.dist_le

theorem raised.add_left (k) {n m} (H : raised n m) : raised (k + n) (k + m) :=

rcases H with rfl | rfl,

{ exact or.inl rfl },

{ exact or.inr rfl }

theorem raised.add_right (k) {n m} (H : raised n m) : raised (n + k) (m + k) :=

by rw [add_comm, add_comm m]; exact H.add_left _

theorem raised.right {l x₁ x₂ r₁ r₂} (H : raised (size r₁) (size r₂)) :

raised (size (@node' α l x₁ r₁)) (size (@node' α l x₂ r₂)) :=

dsimp [node', size], generalize_hyp : size r₂ = m at H ⊢,

rcases H with rfl | rfl,

{ exact or.inl rfl },

{ exact or.inr rfl }

theorem balance_l_eq_balance' {l x r}

(hl : balanced l) (hr : balanced r)

(sl : sized l) (sr : sized r)

(H : (∃ l', raised l' (size l) ∧ balanced_sz l' (size r)) ∨

(∃ r', raised (size r) r' ∧ balanced_sz (size l) r')) :

@balance_l α l x r = balance' l x r :=

rw [← balance_eq_balance' hl hr sl sr, balance_l_eq_balance sl sr],

{ intro l0, rw l0 at H,

rcases H with ⟨_, ⟨⟨⟩⟩|⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩,

{ exact balanced_sz_zero.1 H.symm },

exact le_trans (raised_iff.1 e).1 (balanced_sz_zero.1 H.symm) },

{ intros l1 r1,

rcases H with ⟨l', e, H | ⟨H₁, H₂⟩⟩ | ⟨r', e, H | ⟨H₁, H₂⟩⟩,

{ exact le_trans (le_trans (nat.le_add_left _ _) H)

(mul_pos dec_trivial l1 : (0:ℕ)<_) },

{ exact le_trans H₂ (nat.mul_le_mul_left _ (raised_iff.1 e).1) },

{ cases raised_iff.1 e, unfold delta, linarith },

{ exact le_trans (raised_iff.1 e).1 H₂ } }

theorem balance_sz_dual {l r}

(H : (∃ l', raised (@size α l) l' ∧ balanced_sz l' (@size α r)) ∨

∃ r', raised r' (size r) ∧ balanced_sz (size l) r') :

(∃ l', raised l' (size (dual r)) ∧ balanced_sz l' (size (dual l))) ∨

∃ r', raised (size (dual l)) r' ∧ balanced_sz (size (dual r)) r' :=

rw [size_dual, size_dual],

exact H.symm.imp

(Exists.imp $ λ _, and.imp_right balanced_sz.symm)

(Exists.imp $ λ _, and.imp_right balanced_sz.symm)

theorem size_balance_l {l x r}

(hl : balanced l) (hr : balanced r)

(sl : sized l) (sr : sized r)

(H : (∃ l', raised l' (size l) ∧ balanced_sz l' (size r)) ∨

(∃ r', raised (size r) r' ∧ balanced_sz (size l) r')) :

size (@balance_l α l x r) = size l + size r + 1 :=

by rw [balance_l_eq_balance' hl hr sl sr H, size_balance' sl sr]

theorem all_balance_l {P l x r}

(hl : balanced l) (hr : balanced r)

(sl : sized l) (sr : sized r)

(H : (∃ l', raised l' (size l) ∧ balanced_sz l' (size r)) ∨

(∃ r', raised (size r) r' ∧ balanced_sz (size l) r')) :

all P (@balance_l α l x r) ↔ all P l ∧ P x ∧ all P r :=

by rw [balance_l_eq_balance' hl hr sl sr H, all_balance']

theorem balance_r_eq_balance' {l x r}

(hl : balanced l) (hr : balanced r)

(sl : sized l) (sr : sized r)

(H : (∃ l', raised (size l) l' ∧ balanced_sz l' (size r)) ∨

(∃ r', raised r' (size r) ∧ balanced_sz (size l) r')) :

@balance_r α l x r = balance' l x r :=

by rw [← dual_dual (balance_r l x r), dual_balance_r,

balance_l_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H),

← dual_balance', dual_dual]

theorem size_balance_r {l x r}

(hl : balanced l) (hr : balanced r)

(sl : sized l) (sr : sized r)

(H : (∃ l', raised (size l) l' ∧ balanced_sz l' (size r)) ∨

(∃ r', raised r' (size r) ∧ balanced_sz (size l) r')) :

size (@balance_r α l x r) = size l + size r + 1 :=

by rw [balance_r_eq_balance' hl hr sl sr H, size_balance' sl sr]

theorem all_balance_r {P l x r}

(hl : balanced l) (hr : balanced r)

(sl : sized l) (sr : sized r)

(H : (∃ l', raised (size l) l' ∧ balanced_sz l' (size r)) ∨

(∃ r', raised r' (size r) ∧ balanced_sz (size l) r')) :

all P (@balance_r α l x r) ↔ all P l ∧ P x ∧ all P r :=

by rw [balance_r_eq_balance' hl hr sl sr H, all_balance']

variable [preorder α]

def bounded : ordnode α → with_bot α → with_top α → Prop

| nil (some a) (some b) := a < b

| nil _ _ := true

| (node _ l x r) o₁ o₂ := bounded l o₁ ↑x ∧ bounded r ↑x o₂

theorem bounded.dual : ∀ {t : ordnode α} {o₁ o₂} (h : bounded t o₁ o₂),

@bounded αᵒᵈ _ (dual t) o₂ o₁

| nil o₁ o₂ h := by cases o₁; cases o₂; try {trivial}; exact h

| (node s l x r) _ _ ⟨ol, or⟩ := ⟨or.dual, ol.dual⟩

theorem bounded.dual_iff {t : ordnode α} {o₁ o₂} :

bounded t o₁ o₂ ↔ @bounded αᵒᵈ _ (dual t) o₂ o₁ :=

⟨bounded.dual, λ h, by have := bounded.dual h;

rwa [dual_dual, order_dual.preorder.dual_dual] at this⟩

theorem bounded.weak_left : ∀ {t : ordnode α} {o₁ o₂}, bounded t o₁ o₂ → bounded t ⊥ o₂

| nil o₁ o₂ h := by cases o₂; try {trivial}; exact h

| (node s l x r) _ _ ⟨ol, or⟩ := ⟨ol.weak_left, or⟩

theorem bounded.weak_right : ∀ {t : ordnode α} {o₁ o₂}, bounded t o₁ o₂ → bounded t o₁ ⊤

| nil o₁ o₂ h := by cases o₁; try {trivial}; exact h

| (node s l x r) _ _ ⟨ol, or⟩ := ⟨ol, or.weak_right⟩

theorem bounded.weak {t : ordnode α} {o₁ o₂} (h : bounded t o₁ o₂) : bounded t ⊥ ⊤ :=

h.weak_left.weak_right

theorem bounded.mono_left {x y : α} (xy : x ≤ y) :

∀ {t : ordnode α} {o}, bounded t ↑y o → bounded t ↑x o

| nil none h := ⟨⟩

| nil (some z) h := lt_of_le_of_lt xy h

| (node s l z r) o ⟨ol, or⟩ := ⟨ol.mono_left, or⟩

theorem bounded.mono_right {x y : α} (xy : x ≤ y) :

∀ {t : ordnode α} {o}, bounded t o ↑x → bounded t o ↑y

| nil none h := ⟨⟩

| nil (some z) h := lt_of_lt_of_le h xy

| (node s l z r) o ⟨ol, or⟩ := ⟨ol, or.mono_right⟩

theorem bounded.to_lt : ∀ {t : ordnode α} {x y : α}, bounded t x y → x < y

| nil x y h := h

| (node _ l y r) x z ⟨h₁, h₂⟩ := lt_trans h₁.to_lt h₂.to_lt

theorem bounded.to_nil {t : ordnode α} : ∀ {o₁ o₂}, bounded t o₁ o₂ → bounded nil o₁ o₂

| none _ h := ⟨⟩

| (some _) none h := ⟨⟩

| (some x) (some y) h := h.to_lt

theorem bounded.trans_left {t₁ t₂ : ordnode α} {x : α} :

∀ {o₁ o₂}, bounded t₁ o₁ ↑x → bounded t₂ ↑x o₂ → bounded t₂ o₁ o₂

| none o₂ h₁ h₂ := h₂.weak_left

| (some y) o₂ h₁ h₂ := h₂.mono_left (le_of_lt h₁.to_lt)

theorem bounded.trans_right {t₁ t₂ : ordnode α} {x : α} :

∀ {o₁ o₂}, bounded t₁ o₁ ↑x → bounded t₂ ↑x o₂ → bounded t₁ o₁ o₂

| o₁ none h₁ h₂ := h₁.weak_right

| o₁ (some y) h₁ h₂ := h₁.mono_right (le_of_lt h₂.to_lt)

theorem bounded.mem_lt : ∀ {t o} {x : α}, bounded t o ↑x → all (< x) t

| nil o x _ := ⟨⟩

| (node _ l y r) o x ⟨h₁, h₂⟩ :=

⟨h₁.mem_lt.imp (λ z h, lt_trans h h₂.to_lt), h₂.to_lt, h₂.mem_lt⟩

theorem bounded.mem_gt : ∀ {t o} {x : α}, bounded t ↑x o → all (> x) t

| nil o x _ := ⟨⟩

| (node _ l y r) o x ⟨h₁, h₂⟩ :=

⟨h₁.mem_gt, h₁.to_lt, h₂.mem_gt.imp (λ z, lt_trans h₁.to_lt)⟩

theorem bounded.of_lt : ∀ {t o₁ o₂} {x : α},

bounded t o₁ o₂ → bounded nil o₁ ↑x → all (< x) t → bounded t o₁ ↑x

| nil o₁ o₂ x _ hn _ := hn

| (node _ l y r) o₁ o₂ x ⟨h₁, h₂⟩ hn ⟨al₁, al₂, al₃⟩ := ⟨h₁, h₂.of_lt al₂ al₃⟩

theorem bounded.of_gt : ∀ {t o₁ o₂} {x : α},

bounded t o₁ o₂ → bounded nil ↑x o₂ → all (> x) t → bounded t ↑x o₂

| nil o₁ o₂ x _ hn _ := hn

| (node _ l y r) o₁ o₂ x ⟨h₁, h₂⟩ hn ⟨al₁, al₂, al₃⟩ := ⟨h₁.of_gt al₂ al₁, h₂⟩

theorem bounded.to_sep {t₁ t₂ o₁ o₂} {x : α}

(h₁ : bounded t₁ o₁ ↑x) (h₂ : bounded t₂ ↑x o₂) : t₁.all (λ y, t₂.all (λ z : α, y < z)) :=

h₁.mem_lt.imp $ λ y yx, h₂.mem_gt.imp $ λ z xz, lt_trans yx xz

variable [preorder α]

structure valid' (lo : with_bot α) (t : ordnode α) (hi : with_top α) : Prop :=

(ord : t.bounded lo hi)

(sz : t.sized)

(bal : t.balanced)

def valid (t : ordnode α) : Prop := valid' ⊥ t ⊤

theorem valid'.mono_left {x y : α} (xy : x ≤ y)

{t : ordnode α} {o} (h : valid' ↑y t o) : valid' ↑x t o :=

⟨h.1.mono_left xy, h.2, h.3⟩

theorem valid'.mono_right {x y : α} (xy : x ≤ y)

{t : ordnode α} {o} (h : valid' o t ↑x) : valid' o t ↑y :=

⟨h.1.mono_right xy, h.2, h.3⟩

theorem valid'.trans_left {t₁ t₂ : ordnode α} {x : α} {o₁ o₂}

(h : bounded t₁ o₁ ↑x) (H : valid' ↑x t₂ o₂) : valid' o₁ t₂ o₂ :=

⟨h.trans_left H.1, H.2, H.3⟩

theorem valid'.trans_right {t₁ t₂ : ordnode α} {x : α} {o₁ o₂}

(H : valid' o₁ t₁ ↑x) (h : bounded t₂ ↑x o₂) : valid' o₁ t₁ o₂ :=

⟨H.1.trans_right h, H.2, H.3⟩

theorem valid'.of_lt {t : ordnode α} {x : α} {o₁ o₂}

(H : valid' o₁ t o₂) (h₁ : bounded nil o₁ ↑x) (h₂ : all (< x) t) : valid' o₁ t ↑x :=

⟨H.1.of_lt h₁ h₂, H.2, H.3⟩

theorem valid'.of_gt {t : ordnode α} {x : α} {o₁ o₂}

(H : valid' o₁ t o₂) (h₁ : bounded nil ↑x o₂) (h₂ : all (> x) t) : valid' ↑x t o₂ :=

⟨H.1.of_gt h₁ h₂, H.2, H.3⟩

theorem valid'.valid {t o₁ o₂} (h : @valid' α _ o₁ t o₂) : valid t := ⟨h.1.weak, h.2, h.3⟩

theorem valid'_nil {o₁ o₂} (h : bounded nil o₁ o₂) : valid' o₁ (@nil α) o₂ := ⟨h, ⟨⟩, ⟨⟩⟩

theorem valid_nil : valid (@nil α) := valid'_nil ⟨⟩

theorem valid'.node {s l x r o₁ o₂}

(hl : valid' o₁ l ↑x) (hr : valid' ↑x r o₂)

(H : balanced_sz (size l) (size r)) (hs : s = size l + size r + 1) :

valid' o₁ (@node α s l x r) o₂ :=

⟨⟨hl.1, hr.1⟩, ⟨hs, hl.2, hr.2⟩, ⟨H, hl.3, hr.3⟩⟩

theorem valid'.dual : ∀ {t : ordnode α} {o₁ o₂} (h : valid' o₁ t o₂), @valid' αᵒᵈ _ o₂ (dual t) o₁

| nil o₁ o₂ h := valid'_nil h.1.dual

| (node s l x r) o₁ o₂ ⟨⟨ol, or⟩, ⟨rfl, sl, sr⟩, ⟨b, bl, br⟩⟩ :=

let ⟨ol', sl', bl'⟩ := valid'.dual ⟨ol, sl, bl⟩,

⟨or', sr', br'⟩ := valid'.dual ⟨or, sr, br⟩ in

⟨⟨or', ol'⟩,

⟨by simp [size_dual, add_comm], sr', sl'⟩,

⟨by rw [size_dual, size_dual]; exact b.symm, br', bl'⟩⟩

theorem valid'.dual_iff {t : ordnode α} {o₁ o₂} : valid' o₁ t o₂ ↔ @valid' αᵒᵈ _ o₂ (dual t) o₁ :=

⟨valid'.dual, λ h, by have := valid'.dual h;

rwa [dual_dual, order_dual.preorder.dual_dual] at this⟩

theorem valid.dual {t : ordnode α} : valid t → @valid αᵒᵈ _ (dual t) := valid'.dual

theorem valid.dual_iff {t : ordnode α} : valid t ↔ @valid αᵒᵈ _ (dual t) := valid'.dual_iff

theorem valid'.left {s l x r o₁ o₂} (H : valid' o₁ (@node α s l x r) o₂) : valid' o₁ l x :=

⟨H.1.1, H.2.2.1, H.3.2.1⟩

theorem valid'.right {s l x r o₁ o₂} (H : valid' o₁ (@node α s l x r) o₂) : valid' ↑x r o₂ :=

⟨H.1.2, H.2.2.2, H.3.2.2⟩

theorem valid.left {s l x r} (H : valid (@node α s l x r)) : valid l := H.left.valid

theorem valid.right {s l x r} (H : valid (@node α s l x r)) : valid r := H.right.valid

theorem valid.size_eq {s l x r} (H : valid (@node α s l x r)) :

size (@node α s l x r) = size l + size r + 1 := H.2.1

theorem valid'.node' {l x r o₁ o₂} (hl : valid' o₁ l ↑x) (hr : valid' ↑x r o₂)

(H : balanced_sz (size l) (size r)) : valid' o₁ (@node' α l x r) o₂ :=

hl.node hr H rfl

theorem valid'_singleton {x : α} {o₁ o₂}

(h₁ : bounded nil o₁ ↑x) (h₂ : bounded nil ↑x o₂) : valid' o₁ (singleton x : ordnode α) o₂ :=

(valid'_nil h₁).node (valid'_nil h₂) (or.inl zero_le_one) rfl

theorem valid_singleton {x : α} : valid (singleton x : ordnode α) := valid'_singleton ⟨⟩ ⟨⟩

theorem valid'.node3_l {l x m y r o₁ o₂}

(hl : valid' o₁ l ↑x) (hm : valid' ↑x m ↑y) (hr : valid' ↑y r o₂)

(H1 : balanced_sz (size l) (size m))

(H2 : balanced_sz (size l + size m + 1) (size r)) :

valid' o₁ (@node3_l α l x m y r) o₂ :=

(hl.node' hm H1).node' hr H2

theorem valid'.node3_r {l x m y r o₁ o₂}

(hl : valid' o₁ l ↑x) (hm : valid' ↑x m ↑y) (hr : valid' ↑y r o₂)

(H1 : balanced_sz (size l) (size m + size r + 1))

(H2 : balanced_sz (size m) (size r)) :

valid' o₁ (@node3_r α l x m y r) o₂ :=

hl.node' (hm.node' hr H2) H1

theorem valid'.node4_l_lemma₁ {a b c d : ℕ}

(lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9)

(mr₂ : b + c + 1 ≤ 3 * d)

(mm₁ : b ≤ 3 * c) : b < 3 * a + 1 := by linarith

theorem valid'.node4_l_lemma₂ {b c d : ℕ} (mr₂ : b + c + 1 ≤ 3 * d) : c ≤ 3 * d := by linarith

theorem valid'.node4_l_lemma₃ {b c d : ℕ}

(mr₁ : 2 * d ≤ b + c + 1)

(mm₁ : b ≤ 3 * c) : d ≤ 3 * c := by linarith

theorem valid'.node4_l_lemma₄ {a b c d : ℕ}

(lr₁ : 3 * a ≤ b + c + 1 + d)