mathlib3 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.red l₁.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.red l₁.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.red p l₁ y (l₂.red_node x r)) (other : (l : rbnode α) (y : α) (r : rbnode α), l.get_color rbnode.color.red r.get_color rbnode.color.red p 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.lt p a p (a.red_node y b)) (is_red_eq : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.eq p (a.red_node y b)) (is_red_gt : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gt p b p (a.red_node y b)) (is_black_lt_red : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lt a.get_color = rbnode.color.red p a p (a.black_node y b)) (is_black_lt_not_red : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.lt a.get_color rbnode.color.red p a p (a.black_node y b)) (is_black_eq : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.eq p (a.black_node y b)) (is_black_gt_red : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gt b.get_color = rbnode.color.red p b p (a.black_node y b)) (is_black_gt_not_red : (a : rbnode α) (y : α) (b : rbnode α), cmp_using lt x y = ordering.gt b.get_color rbnode.color.red p b p (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 α} :
theorem rbnode.is_searchable_balance1_node {α : Type u} (lt : α α Prop) {t : rbnode α} [is_trans α lt] {y : α} {s : rbnode α} {lo hi : option α} :
theorem rbnode.is_searchable_balance2 {α : Type u} (lt : α α Prop) {l : rbnode α} {y : α} {r : rbnode α} {v : α} {t : rbnode α} {lo hi : option α} :
theorem rbnode.is_searchable_balance2_node {α : Type u} (lt : α α Prop) {t : rbnode α} [is_trans α lt] {y : α} {s : rbnode α} {lo hi : option α} :
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) :
theorem rbnode.mem_balance1_node_of_mem_left {α : Type u} (lt : α α Prop) {x : α} {s : rbnode α} (v : α) (t : rbnode α) :
theorem rbnode.mem_balance2_node_of_mem_left {α : Type u} (lt : α α Prop) {x : α} {s : rbnode α} (v : α) (t : rbnode α) :
theorem rbnode.mem_balance1_node_of_mem_right {α : Type u} (lt : α α Prop) {x : α} {t : rbnode α} (v : α) (s : rbnode α) :
theorem rbnode.mem_balance2_node_of_mem_right {α : Type u} (lt : α α Prop) {x : α} {t : rbnode α} (v : α) (s : rbnode α) :
theorem rbnode.mem_balance1_node_of_incomp {α : Type u} (lt : α α Prop) {x v : α} (s t : rbnode α) :
¬lt x v ¬lt v x s rbnode.leaf rbnode.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 v s rbnode.leaf rbnode.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 t rbnode.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] {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] {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 α} :
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 α} :
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 (option.some x)) (hlt₂ : rbnode.lift lt (option.some x) hi) :
theorem rbnode.find_mk_insert_result {α : Type u} (lt : α α Prop) [decidable_rel lt] (c : rbnode.color) (t : rbnode α) (x : α) :
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) :
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 (option.some v)) (hr : rbnode.is_searchable lt r (option.some v) (option.some y)) (ht : rbnode.is_searchable lt t (option.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 (option.some x)) (hs : rbnode.is_searchable lt s (option.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 (option.some v)) (hr : rbnode.is_searchable lt r (option.some v) (option.some y)) (ht : rbnode.is_searchable lt t (option.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 (option.some x)) (hs : rbnode.is_searchable lt s (option.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 (option.some v)) (hr : rbnode.is_searchable lt r (option.some v) (option.some y)) (ht : rbnode.is_searchable lt t (option.some y) hi) :
rbnode.find lt (l.balance1 v r y t) x = option.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 (option.some y)) (hs : rbnode.is_searchable lt s (option.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 (option.some y) (option.some v)) (hr : rbnode.is_searchable lt r (option.some v) hi) (ht : rbnode.is_searchable lt t lo (option.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 (option.some y) hi) (hs : rbnode.is_searchable lt s lo (option.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 (option.some y) (option.some v)) (hr : rbnode.is_searchable lt r (option.some v) hi) (ht : rbnode.is_searchable lt t lo (option.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 (option.some y) hi) (hs : rbnode.is_searchable lt s lo (option.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 (option.some y) (option.some v)) (hr : rbnode.is_searchable lt r (option.some v) hi) (ht : rbnode.is_searchable lt t lo (option.some y)) :
rbnode.find lt (l.balance2 v r y t) x = option.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 (option.some y) hi) (hs : rbnode.is_searchable lt s lo (option.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 (option.some x)) (hlt₂ : rbnode.lift lt (option.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) :
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 n r.is_red_black c_r n t.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 n r.is_red_black c_r n t.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 : } :
theorem rbnode.balance2_node_rb {α : Type u} {t s : rbnode α} {y : α} {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 : α) :