mathlib documentation

data.rbtree.insert

@[simp]
theorem rbnode.balance1_eq₁ {α : Type u} (l : rbnode α) (x : α) (r₁ : rbnode α) (y : α) (r₂ : rbnode α) (v : α) (t : rbnode α) :
(l.red_node x r₁).balance1 y r₂ v t = (l.black_node x r₁).red_node y (r₂.black_node v t)
@[simp]
theorem rbnode.balance1_eq₂ {α : Type u} (l₁ : rbnode α) (y : α) (l₂ : rbnode α) (x : α) (r : rbnode α) (v : α) (t : rbnode α) :
l₁.get_color rbnode.color.redl₁.balance1 y (l₂.red_node x r) v t = (l₁.black_node y l₂).red_node x (r.black_node v t)
@[simp]
theorem rbnode.balance1_eq₃ {α : Type u} (l : rbnode α) (y : α) (r : rbnode α) (v : α) (t : rbnode α) :
@[simp]
theorem rbnode.balance2_eq₁ {α : Type u} (l : rbnode α) (x₁ : α) (r₁ : rbnode α) (y : α) (r₂ : rbnode α) (v : α) (t : rbnode α) :
(l.red_node x₁ r₁).balance2 y r₂ v t = (t.black_node v l).red_node x₁ (r₁.black_node y r₂)
@[simp]
theorem rbnode.balance2_eq₂ {α : Type u} (l₁ : rbnode α) (y : α) (l₂ : rbnode α) (x₂ : α) (r₂ : rbnode α) (v : α) (t : rbnode α) :
l₁.get_color rbnode.color.redl₁.balance2 y (l₂.red_node x₂ r₂) v t = (t.black_node v l₁).red_node y (l₂.black_node x₂ r₂)
@[simp]
theorem rbnode.balance2_eq₃ {α : Type u} (l : rbnode α) (y : α) (r : rbnode α) (v : α) (t : rbnode α) :
theorem rbnode.balance.cases {α : Type u} {p : rbnode αα → rbnode α → Prop} (l : rbnode α) (y : α) (r : rbnode α) (red_left : ∀ (l : rbnode α) (x : α) (r₁ : rbnode α) (y : α) (r₂ : rbnode α), p (l.red_node x r₁) y r₂) (red_right : ∀ (l₁ : rbnode α) (y : α) (l₂ : rbnode α) (x : α) (r : rbnode α), l₁.get_color rbnode.color.redp l₁ y (l₂.red_node x r)) (other : ∀ (l : rbnode α) (y : α) (r : rbnode α), l.get_color rbnode.color.redr.get_color rbnode.color.redp l y r) :
p l y r
theorem rbnode.balance1_ne_leaf {α : Type u} (l : rbnode α) (x : α) (r : rbnode α) (v : α) (t : rbnode α) :
theorem rbnode.balance1_node_ne_leaf {α : Type u} {s : rbnode α} (a : α) (t : rbnode α) :
theorem rbnode.balance2_ne_leaf {α : Type u} (l : rbnode α) (x : α) (r : rbnode α) (v : α) (t : rbnode α) :
theorem rbnode.balance2_node_ne_leaf {α : Type u} {s : rbnode α} (a : α) (t : rbnode α) :
theorem rbnode.ins.induction {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {p : rbnode α → Prop} (t : rbnode α) (x : α) (is_leaf : p rbnode.leaf) (is_red_lt : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.ltp ap (a.red_node y b)) (is_red_eq : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.eqp (a.red_node y b)) (is_red_gt : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gtp bp (a.red_node y b)) (is_black_lt_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lta.get_color = rbnode.color.redp ap (a.black_node y b)) (is_black_lt_not_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lta.get_color rbnode.color.redp ap (a.black_node y b)) (is_black_eq : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.eqp (a.black_node y b)) (is_black_gt_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gtb.get_color = rbnode.color.redp bp (a.black_node y b)) (is_black_gt_not_red : ∀ (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gtb.get_color rbnode.color.redp bp (a.black_node y b)) :
p t
theorem rbnode.is_searchable_balance1 {α : Type u} (lt : α → α → Prop) {l : rbnode α} {y : α} {r : rbnode α} {v : α} {t : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt l lo (some y)rbnode.is_searchable lt r (some y) (some v)rbnode.is_searchable lt t (some v) hirbnode.is_searchable lt (l.balance1 y r v t) lo hi
theorem rbnode.is_searchable_balance1_node {α : Type u} (lt : α → α → Prop) {t : rbnode α} [is_trans α lt] {y : α} {s : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt t lo (some y)rbnode.is_searchable lt s (some y) hirbnode.is_searchable lt (t.balance1_node y s) lo hi
theorem rbnode.is_searchable_balance2 {α : Type u} (lt : α → α → Prop) {l : rbnode α} {y : α} {r : rbnode α} {v : α} {t : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt t lo (some v)rbnode.is_searchable lt l (some v) (some y)rbnode.is_searchable lt r (some y) hirbnode.is_searchable lt (l.balance2 y r v t) lo hi
theorem rbnode.is_searchable_balance2_node {α : Type u} (lt : α → α → Prop) {t : rbnode α} [is_trans α lt] {y : α} {s : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt s lo (some y)rbnode.is_searchable lt t (some y) hirbnode.is_searchable lt (t.balance2_node y s) lo hi
theorem rbnode.is_searchable_ins {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {t : rbnode α} {x : α} [is_strict_weak_order α lt] {lo hi : option α} (h : rbnode.is_searchable lt t lo hi) :
rbnode.lift lt lo (some x)rbnode.lift lt (some x) hirbnode.is_searchable lt (rbnode.ins lt t x) lo hi
theorem rbnode.is_searchable_mk_insert_result {α : Type u} (lt : α → α → Prop) {c : rbnode.color} {t : rbnode α} :
theorem rbnode.is_searchable_insert {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {t : rbnode α} {x : α} [is_strict_weak_order α lt] :
theorem rbnode.mem_balance1_node_of_mem_left {α : Type u} (lt : α → α → Prop) {x : α} {s : rbnode α} (v : α) (t : rbnode α) :
rbnode.mem lt x srbnode.mem lt x (s.balance1_node v t)
theorem rbnode.mem_balance2_node_of_mem_left {α : Type u} (lt : α → α → Prop) {x : α} {s : rbnode α} (v : α) (t : rbnode α) :
rbnode.mem lt x srbnode.mem lt x (s.balance2_node v t)
theorem rbnode.mem_balance1_node_of_mem_right {α : Type u} (lt : α → α → Prop) {x : α} {t : rbnode α} (v : α) (s : rbnode α) :
rbnode.mem lt x trbnode.mem lt x (s.balance1_node v t)
theorem rbnode.mem_balance2_node_of_mem_right {α : Type u} (lt : α → α → Prop) {x : α} {t : rbnode α} (v : α) (s : rbnode α) :
rbnode.mem lt x trbnode.mem lt x (s.balance2_node v t)
theorem rbnode.mem_balance1_node_of_incomp {α : Type u} (lt : α → α → Prop) {x v : α} (s t : rbnode α) :
¬lt x v ¬lt v xs rbnode.leafrbnode.mem lt x (s.balance1_node v t)
theorem rbnode.mem_balance2_node_of_incomp {α : Type u} (lt : α → α → Prop) {x v : α} (s t : rbnode α) :
¬lt v x ¬lt x vs rbnode.leafrbnode.mem lt x (s.balance2_node v t)
theorem rbnode.ins_ne_leaf {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (t : rbnode α) (x : α) :
theorem rbnode.insert_ne_leaf {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (t : rbnode α) (x : α) :
theorem rbnode.mem_ins_of_incomp {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (t : rbnode α) {x y : α} (h : ¬lt x y ¬lt y x) :
rbnode.mem lt x (rbnode.ins lt t y)
theorem rbnode.mem_ins_of_mem {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {t : rbnode α} (z : α) {x : α} (h : rbnode.mem lt x t) :
rbnode.mem lt x (rbnode.ins lt t z)
theorem rbnode.mem_mk_insert_result {α : Type u} (lt : α → α → Prop) {a : α} {t : rbnode α} (c : rbnode.color) :
theorem rbnode.mem_of_mem_mk_insert_result {α : Type u} (lt : α → α → Prop) {a : α} {t : rbnode α} {c : rbnode.color} :
theorem rbnode.mem_insert_of_incomp {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (t : rbnode α) {x y : α} (h : ¬lt x y ¬lt y x) :
theorem rbnode.mem_insert_of_mem {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {t : rbnode α} {x : α} (z : α) :
rbnode.mem lt x trbnode.mem lt x (rbnode.insert lt t z)
theorem rbnode.of_mem_balance1_node {α : Type u} (lt : α → α → Prop) {x : α} {s : rbnode α} {v : α} {t : rbnode α} :
rbnode.mem lt x (s.balance1_node v t)rbnode.mem lt x s ¬lt x v ¬lt v x rbnode.mem lt x t
theorem rbnode.of_mem_balance2_node {α : Type u} (lt : α → α → Prop) {x : α} {s : rbnode α} {v : α} {t : rbnode α} :
rbnode.mem lt x (s.balance2_node v t)rbnode.mem lt x s ¬lt x v ¬lt v x rbnode.mem lt x t
theorem rbnode.equiv_or_mem_of_mem_ins {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {t : rbnode α} {x z : α} (h : rbnode.mem lt x (rbnode.ins lt t z)) :
theorem rbnode.equiv_or_mem_of_mem_insert {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {t : rbnode α} {x z : α} (h : rbnode.mem lt x (rbnode.insert lt t z)) :
theorem rbnode.mem_exact_balance1_node_of_mem_exact {α : Type u} {x : α} {s : rbnode α} (v : α) (t : rbnode α) :
theorem rbnode.mem_exact_balance2_node_of_mem_exact {α : Type u} {x : α} {s : rbnode α} (v : α) (t : rbnode α) :
theorem rbnode.find_balance1_node {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {x y z : α} {t s : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt t lo (some z)rbnode.is_searchable lt s (some z) hirbnode.find lt t y = some xstrict_weak_order.equiv y xrbnode.find lt (t.balance1_node z s) y = some x
theorem rbnode.find_balance2_node {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {x y z : α} {s t : rbnode α} [is_trans α lt] {lo hi : option α} :
rbnode.is_searchable lt s lo (some z)rbnode.is_searchable lt t (some z) hirbnode.find lt t y = some xstrict_weak_order.equiv y xrbnode.find lt (t.balance2_node z s) y = some x
theorem rbnode.ite_eq_of_not_lt {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_order α lt] {a b : α} {β : Type v} (t s : β) (h : lt b a) :
ite (lt a b) t s = s
theorem rbnode.find_ins_of_eqv {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (he : strict_weak_order.equiv x y) {lo hi : option α} (hs : rbnode.is_searchable lt t lo hi) (hlt₁ : rbnode.lift lt lo (some x)) (hlt₂ : rbnode.lift lt (some x) hi) :
rbnode.find lt (rbnode.ins lt t x) y = some x
theorem rbnode.find_mk_insert_result {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (c : rbnode.color) (t : rbnode α) (x : α) :
theorem rbnode.find_insert_of_eqv {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (he : strict_weak_order.equiv x y) :
theorem rbnode.weak_trichotomous {α : Type u} (lt : α → α → Prop) (x y : α) {p : Prop} (is_lt : lt x y → p) (is_eqv : ¬lt x y ¬lt y x → p) (is_gt : lt y x → p) :
p
theorem rbnode.find_black_eq_find_red {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {l : rbnode α} {y : α} {r : rbnode α} {x : α} :
rbnode.find lt (l.black_node y r) x = rbnode.find lt (l.red_node y r) x
theorem rbnode.find_red_of_lt {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {l : rbnode α} {y : α} {r : rbnode α} {x : α} (h : lt x y) :
rbnode.find lt (l.red_node y r) x = rbnode.find lt l x
theorem rbnode.find_red_of_gt {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_order α lt] {l : rbnode α} {y : α} {r : rbnode α} {x : α} (h : lt y x) :
rbnode.find lt (l.red_node y r) x = rbnode.find lt r x
theorem rbnode.find_red_of_incomp {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {l : rbnode α} {y : α} {r : rbnode α} {x : α} (h : ¬lt x y ¬lt y x) :
rbnode.find lt (l.red_node y r) x = some y
theorem rbnode.find_balance1_lt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {l r t : rbnode α} {v x y : α} {lo hi : option α} (h : lt x y) (hl : rbnode.is_searchable lt l lo (some v)) (hr : rbnode.is_searchable lt r (some v) (some y)) (ht : rbnode.is_searchable lt t (some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = rbnode.find lt (l.red_node v r) x
theorem rbnode.find_balance1_node_lt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {t s : rbnode α} {x y : α} {lo hi : option α} (hlt : lt y x) (ht : rbnode.is_searchable lt t lo (some x)) (hs : rbnode.is_searchable lt s (some x) hi) (hne : t rbnode.leaf . "ins_ne_leaf_tac") :
theorem rbnode.find_balance1_gt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {l r t : rbnode α} {v x y : α} {lo hi : option α} (h : lt y x) (hl : rbnode.is_searchable lt l lo (some v)) (hr : rbnode.is_searchable lt r (some v) (some y)) (ht : rbnode.is_searchable lt t (some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = rbnode.find lt t x
theorem rbnode.find_balance1_node_gt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {t s : rbnode α} {x y : α} {lo hi : option α} (h : lt x y) (ht : rbnode.is_searchable lt t lo (some x)) (hs : rbnode.is_searchable lt s (some x) hi) (hne : t rbnode.leaf . "ins_ne_leaf_tac") :
theorem rbnode.find_balance1_eqv {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {l r t : rbnode α} {v x y : α} {lo hi : option α} (h : ¬lt x y ¬lt y x) (hl : rbnode.is_searchable lt l lo (some v)) (hr : rbnode.is_searchable lt r (some v) (some y)) (ht : rbnode.is_searchable lt t (some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = some y
theorem rbnode.find_balance1_node_eqv {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {t s : rbnode α} {x y : α} {lo hi : option α} (h : ¬lt x y ¬lt y x) (ht : rbnode.is_searchable lt t lo (some y)) (hs : rbnode.is_searchable lt s (some y) hi) (hne : t rbnode.leaf . "ins_ne_leaf_tac") :
theorem rbnode.find_balance2_lt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {l : rbnode α} {v : α} {r t : rbnode α} {x y : α} {lo hi : option α} (h : lt x y) (hl : rbnode.is_searchable lt l (some y) (some v)) (hr : rbnode.is_searchable lt r (some v) hi) (ht : rbnode.is_searchable lt t lo (some y)) :
rbnode.find lt (l.balance2 v r y t) x = rbnode.find lt t x
theorem rbnode.find_balance2_node_lt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {s t : rbnode α} {x y : α} {lo hi : option α} (h : lt x y) (ht : rbnode.is_searchable lt t (some y) hi) (hs : rbnode.is_searchable lt s lo (some y)) (hne : t rbnode.leaf . "ins_ne_leaf_tac") :
theorem rbnode.find_balance2_gt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {l : rbnode α} {v : α} {r t : rbnode α} {x y : α} {lo hi : option α} (h : lt y x) (hl : rbnode.is_searchable lt l (some y) (some v)) (hr : rbnode.is_searchable lt r (some v) hi) (ht : rbnode.is_searchable lt t lo (some y)) :
rbnode.find lt (l.balance2 v r y t) x = rbnode.find lt (l.red_node v r) x
theorem rbnode.find_balance2_node_gt {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {s t : rbnode α} {x y : α} {lo hi : option α} (h : lt y x) (ht : rbnode.is_searchable lt t (some y) hi) (hs : rbnode.is_searchable lt s lo (some y)) (hne : t rbnode.leaf . "ins_ne_leaf_tac") :
theorem rbnode.find_balance2_eqv {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {l : rbnode α} {v : α} {r t : rbnode α} {x y : α} {lo hi : option α} (h : ¬lt x y ¬lt y x) (hl : rbnode.is_searchable lt l (some y) (some v)) (hr : rbnode.is_searchable lt r (some v) hi) (ht : rbnode.is_searchable lt t lo (some y)) :
rbnode.find lt (l.balance2 v r y t) x = some y
theorem rbnode.find_balance2_node_eqv {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {t s : rbnode α} {x y : α} {lo hi : option α} (h : ¬lt x y ¬lt y x) (ht : rbnode.is_searchable lt t (some y) hi) (hs : rbnode.is_searchable lt s lo (some y)) (hne : t rbnode.leaf . "ins_ne_leaf_tac") :
theorem rbnode.find_ins_of_disj {α : Type u} (lt : α → α → Prop) [is_strict_weak_order α lt] [decidable_rel lt] {x y : α} {t : rbnode α} (hn : lt x y lt y x) {lo hi : option α} (hs : rbnode.is_searchable lt t lo hi) (hlt₁ : rbnode.lift lt lo (some x)) (hlt₂ : rbnode.lift lt (some x) hi) :
rbnode.find lt (rbnode.ins lt t x) y = rbnode.find lt t y
theorem rbnode.find_insert_of_disj {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (hd : lt x y lt y x) :
theorem rbnode.find_insert_of_not_eqv {α : Type u} (lt : α → α → Prop) [decidable_rel lt] [is_strict_weak_order α lt] {x y : α} {t : rbnode α} (hn : ¬strict_weak_order.equiv x y) :
inductive rbnode.is_bad_red_black {α : Type u} :
rbnode α → Prop
theorem rbnode.balance1_rb {α : Type u} {l r t : rbnode α} {y v : α} {c_l c_r c_t : rbnode.color} {n : } :
l.is_red_black c_l nr.is_red_black c_r nt.is_red_black c_t n(∃ (c : rbnode.color), (l.balance1 y r v t).is_red_black c n.succ)
theorem rbnode.balance2_rb {α : Type u} {l r t : rbnode α} {y v : α} {c_l c_r c_t : rbnode.color} {n : } :
l.is_red_black c_l nr.is_red_black c_r nt.is_red_black c_t n(∃ (c : rbnode.color), (l.balance2 y r v t).is_red_black c n.succ)
theorem rbnode.balance1_node_rb {α : Type u} {t s : rbnode α} {y : α} {c : rbnode.color} {n : } :
t.is_bad_red_black ns.is_red_black c n(∃ (c : rbnode.color), (t.balance1_node y s).is_red_black c n.succ)
theorem rbnode.balance2_node_rb {α : Type u} {t s : rbnode α} {y : α} {c : rbnode.color} {n : } :
t.is_bad_red_black ns.is_red_black c n(∃ (c : rbnode.color), (t.balance2_node y s).is_red_black c n.succ)
theorem rbnode.of_get_color_eq_red {α : Type u} {t : rbnode α} {c : rbnode.color} {n : } :
theorem rbnode.of_get_color_ne_red {α : Type u} {t : rbnode α} {c : rbnode.color} {n : } :
theorem rbnode.ins_rb {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {t : rbnode α} (x : α) {c : rbnode.color} {n : } (h : t.is_red_black c n) :
theorem rbnode.insert_rb {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {t : rbnode α} (x : α) {c : rbnode.color} {n : } (h : t.is_red_black c n) :
theorem rbnode.insert_is_red_black {α : Type u} (lt : α → α → Prop) [decidable_rel lt] {t : rbnode α} {c : rbnode.color} {n : } (x : α) :
t.is_red_black c n(∃ (c : rbnode.color) (n : ), (rbnode.insert lt t x).is_red_black c n)