mathlib3 documentation

data.rbtree.init

inductive rbnode (α : Type u) :

leaf : Π {α : Type u}, rbnode α
red_node : Π {α : Type u}, rbnode α → α → rbnode α → rbnode α
black_node : Π {α : Type u}, rbnode α → α → rbnode α → rbnode α

Instances for rbnode

rbnode.has_sizeof_inst
rbnode.inhabited

inductive rbnode.color :

red : rbnode.color
black : rbnode.color

Instances for rbnode.color

rbnode.color.has_sizeof_inst
rbnode.color.inhabited

@[protected, instance]

def rbnode.color.decidable_eq :

decidable_eq rbnode.color

Equations

rbnode.color.decidable_eq = λ (a b : rbnode.color), a.cases_on (b.cases_on (decidable.is_true rfl) (decidable.is_false rbnode.color.decidable_eq._proof_1)) (b.cases_on (decidable.is_false rbnode.color.decidable_eq._proof_2) (decidable.is_true rfl))

def rbnode.depth {α : Type u} (f : ℕ → ℕ → ℕ) :

rbnode α → ℕ

Equations

rbnode.depth f (l.black_node _x r) = (f (rbnode.depth f l) (rbnode.depth f r)).succ
rbnode.depth f (l.red_node _x r) = (f (rbnode.depth f l) (rbnode.depth f r)).succ
rbnode.depth f rbnode.leaf = 0

@[protected]

def rbnode.min {α : Type u} :

rbnode α → option α

Equations

((lchild.black_node val rchild).black_node v _x).min = (lchild.black_node val rchild).min
((lchild.red_node val rchild).black_node v _x).min = (lchild.red_node val rchild).min
(rbnode.leaf.black_node v _x).min = option.some v
((lchild.black_node val rchild).red_node v _x).min = (lchild.black_node val rchild).min
((lchild.red_node val rchild).red_node v _x).min = (lchild.red_node val rchild).min
(rbnode.leaf.red_node v _x).min = option.some v
rbnode.leaf.min = option.none

@[protected]

def rbnode.max {α : Type u} :

rbnode α → option α

Equations

(_x.black_node v (lchild.black_node val rchild)).max = (lchild.black_node val rchild).max
(_x.black_node v (lchild.red_node val rchild)).max = (lchild.red_node val rchild).max
(_x.black_node v rbnode.leaf).max = option.some v
(_x.red_node v (lchild.black_node val rchild)).max = (lchild.black_node val rchild).max
(_x.red_node v (lchild.red_node val rchild)).max = (lchild.red_node val rchild).max
(_x.red_node v rbnode.leaf).max = option.some v
rbnode.leaf.max = option.none

def rbnode.fold {α : Type u} {β : Type v} (f : α → β → β) :

rbnode α → β → β

Equations

rbnode.fold f (l.black_node v r) b = rbnode.fold f r (f v (rbnode.fold f l b))
rbnode.fold f (l.red_node v r) b = rbnode.fold f r (f v (rbnode.fold f l b))
rbnode.fold f rbnode.leaf b = b

def rbnode.rev_fold {α : Type u} {β : Type v} (f : α → β → β) :

rbnode α → β → β

Equations

rbnode.rev_fold f (l.black_node v r) b = rbnode.rev_fold f l (f v (rbnode.rev_fold f r b))
rbnode.rev_fold f (l.red_node v r) b = rbnode.rev_fold f l (f v (rbnode.rev_fold f r b))
rbnode.rev_fold f rbnode.leaf b = b

def rbnode.balance1 {α : Type u} :

rbnode α → α → rbnode α → α → rbnode α → rbnode α

Equations

(lchild.black_node val rchild).balance1 y (lchild_1.black_node val_1 rchild_1) v t = ((lchild.black_node val rchild).red_node y (lchild_1.black_node val_1 rchild_1)).black_node v t
(lchild.black_node val rchild).balance1 y (l₂.red_node x r) v t = ((lchild.black_node val rchild).black_node y l₂).red_node x (r.black_node v t)
(lchild.black_node val rchild).balance1 y rbnode.leaf v t = ((lchild.black_node val rchild).red_node y rbnode.leaf).black_node v t
(l.red_node x r₁).balance1 y (lchild.black_node val rchild) v t = (l.black_node x r₁).red_node y ((lchild.black_node val rchild).black_node v t)
(l.red_node x r₁).balance1 y (lchild.red_node val rchild) v t = (l.black_node x r₁).red_node y ((lchild.red_node val rchild).black_node v t)
(l.red_node x r₁).balance1 y rbnode.leaf v t = (l.black_node x r₁).red_node y (rbnode.leaf.black_node v t)
rbnode.leaf.balance1 y (lchild.black_node val rchild) v t = (rbnode.leaf.red_node y (lchild.black_node val rchild)).black_node v t
rbnode.leaf.balance1 y (l₂.red_node x r) v t = (rbnode.leaf.black_node y l₂).red_node x (r.black_node v t)
rbnode.leaf.balance1 y rbnode.leaf v t = (rbnode.leaf.red_node y rbnode.leaf).black_node v t

def rbnode.balance1_node {α : Type u} :

rbnode α → α → rbnode α → rbnode α

Equations

(l.black_node x r).balance1_node v t = l.balance1 x r v t
(l.red_node x r).balance1_node v t = l.balance1 x r v t
rbnode.leaf.balance1_node v t = t

def rbnode.balance2 {α : Type u} :

rbnode α → α → rbnode α → α → rbnode α → rbnode α

Equations

(lchild.black_node val rchild).balance2 y (lchild_1.black_node val_1 rchild_1) v t = t.black_node v ((lchild.black_node val rchild).red_node y (lchild_1.black_node val_1 rchild_1))
(lchild.black_node val rchild).balance2 y (l₂.red_node x₂ r₂) v t = (t.black_node v (lchild.black_node val rchild)).red_node y (l₂.black_node x₂ r₂)
(lchild.black_node val rchild).balance2 y rbnode.leaf v t = t.black_node v ((lchild.black_node val rchild).red_node y rbnode.leaf)
(l.red_node x₁ r₁).balance2 y (lchild.black_node val rchild) v t = (t.black_node v l).red_node x₁ (r₁.black_node y (lchild.black_node val rchild))
(l.red_node x₁ r₁).balance2 y (lchild.red_node val rchild) v t = (t.black_node v l).red_node x₁ (r₁.black_node y (lchild.red_node val rchild))
(l.red_node x₁ r₁).balance2 y rbnode.leaf v t = (t.black_node v l).red_node x₁ (r₁.black_node y rbnode.leaf)
rbnode.leaf.balance2 y (lchild.black_node val rchild) v t = t.black_node v (rbnode.leaf.red_node y (lchild.black_node val rchild))
rbnode.leaf.balance2 y (l₂.red_node x₂ r₂) v t = (t.black_node v rbnode.leaf).red_node y (l₂.black_node x₂ r₂)
rbnode.leaf.balance2 y rbnode.leaf v t = t.black_node v (rbnode.leaf.red_node y rbnode.leaf)

def rbnode.balance2_node {α : Type u} :

rbnode α → α → rbnode α → rbnode α

Equations

(l.black_node x r).balance2_node v t = l.balance2 x r v t
(l.red_node x r).balance2_node v t = l.balance2 x r v t
rbnode.leaf.balance2_node v t = t

def rbnode.get_color {α : Type u} :

rbnode α → rbnode.color

Equations

(lchild.black_node val rchild).get_color = rbnode.color.black
(_x.red_node _x_1 _x_2).get_color = rbnode.color.red
rbnode.leaf.get_color = rbnode.color.black

def rbnode.ins {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :

rbnode α → α → rbnode α

Equations

rbnode.ins lt (a.black_node y b) x = rbnode.ins._match_2 a y b x (rbnode.ins lt a x) (rbnode.ins lt b x) (cmp_using lt x y)
rbnode.ins lt (a.red_node y b) x = rbnode.ins._match_1 a y b x (rbnode.ins lt a x) (rbnode.ins lt b x) (cmp_using lt x y)
rbnode.ins lt rbnode.leaf x = rbnode.leaf.red_node x rbnode.leaf
rbnode.ins._match_2 a y b x _f_1 _f_2 ordering.gt = ite (b.get_color = rbnode.color.red) (_f_2.balance2_node y a) (a.black_node y _f_2)
rbnode.ins._match_2 a y b x _f_1 _f_2 ordering.eq = a.black_node x b
rbnode.ins._match_2 a y b x _f_1 _f_2 ordering.lt = ite (a.get_color = rbnode.color.red) (_f_1.balance1_node y b) (_f_1.black_node y b)
rbnode.ins._match_1 a y b x _f_1 _f_2 ordering.gt = a.red_node y _f_2
rbnode.ins._match_1 a y b x _f_1 _f_2 ordering.eq = a.red_node x b
rbnode.ins._match_1 a y b x _f_1 _f_2 ordering.lt = _f_1.red_node y b

def rbnode.mk_insert_result {α : Type u} :

rbnode.color → rbnode α → rbnode α

Equations

rbnode.mk_insert_result rbnode.color.black t = t
rbnode.mk_insert_result rbnode.color.red (lchild.black_node val rchild) = lchild.black_node val rchild
rbnode.mk_insert_result rbnode.color.red (l.red_node v r) = l.black_node v r
rbnode.mk_insert_result rbnode.color.red rbnode.leaf = rbnode.leaf

def rbnode.insert {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (t : rbnode α) (x : α) :

Equations

rbnode.insert lt t x = rbnode.mk_insert_result t.get_color (rbnode.ins lt t x)

def rbnode.mem {α : Type u} (lt : α → α → Prop) :

α → rbnode α → Prop

Equations

rbnode.mem lt a (l.black_node v r) = (rbnode.mem lt a l ∨ ¬lt a v ∧ ¬lt v a ∨ rbnode.mem lt a r)
rbnode.mem lt a (l.red_node v r) = (rbnode.mem lt a l ∨ ¬lt a v ∧ ¬lt v a ∨ rbnode.mem lt a r)
rbnode.mem lt a rbnode.leaf = false

def rbnode.mem_exact {α : Type u} :

α → rbnode α → Prop

Equations

rbnode.mem_exact a (l.black_node v r) = (rbnode.mem_exact a l ∨ a = v ∨ rbnode.mem_exact a r)
rbnode.mem_exact a (l.red_node v r) = (rbnode.mem_exact a l ∨ a = v ∨ rbnode.mem_exact a r)
rbnode.mem_exact a rbnode.leaf = false

def rbnode.find {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :

rbnode α → α → option α

Equations

rbnode.find lt (a.black_node y b) x = rbnode.find._match_2 y (rbnode.find lt a x) (rbnode.find lt b x) (cmp_using lt x y)
rbnode.find lt (a.red_node y b) x = rbnode.find._match_1 y (rbnode.find lt a x) (rbnode.find lt b x) (cmp_using lt x y)
rbnode.find lt rbnode.leaf x = option.none
rbnode.find._match_2 y _f_1 _f_2 ordering.gt = _f_2
rbnode.find._match_2 y _f_1 _f_2 ordering.eq = option.some y
rbnode.find._match_2 y _f_1 _f_2 ordering.lt = _f_1
rbnode.find._match_1 y _f_1 _f_2 ordering.gt = _f_2
rbnode.find._match_1 y _f_1 _f_2 ordering.eq = option.some y
rbnode.find._match_1 y _f_1 _f_2 ordering.lt = _f_1

inductive rbnode.well_formed {α : Type u} (lt : α → α → Prop) :

rbnode α → Prop

leaf_wff : ∀ {α : Type u} {lt : α → α → Prop}, rbnode.well_formed lt rbnode.leaf
insert_wff : ∀ {α : Type u} {lt : α → α → Prop} {n n' : rbnode α} {x : α} [_inst_1 : decidable_rel lt], rbnode.well_formed lt n → n' = rbnode.insert lt n x → rbnode.well_formed lt n'

def rbtree (α : Type u) (lt : α → α → Prop . "default_lt") :

Equations

rbtree α lt = {t // rbnode.well_formed lt t}

Instances for rbtree

def mk_rbtree (α : Type u) (lt : α → α → Prop . "default_lt") :

rbtree α lt

Equations

mk_rbtree α lt = ⟨rbnode.leaf α, _⟩

@[protected]

def rbtree.mem {α : Type u} {lt : α → α → Prop} (a : α) (t : rbtree α lt) :

Prop

Equations

rbtree.mem a t = rbnode.mem lt a t.val

@[protected, instance]

def rbtree.has_mem {α : Type u} {lt : α → α → Prop} :

has_mem α (rbtree α lt)

Equations

rbtree.has_mem = {mem := rbtree.mem lt}

def rbtree.mem_exact {α : Type u} {lt : α → α → Prop} (a : α) (t : rbtree α lt) :

Prop

Equations

rbtree.mem_exact a t = rbnode.mem_exact a t.val

def rbtree.depth {α : Type u} {lt : α → α → Prop} (f : ℕ → ℕ → ℕ) (t : rbtree α lt) :

Equations

rbtree.depth f t = rbnode.depth f t.val

def rbtree.fold {α : Type u} {β : Type v} {lt : α → α → Prop} (f : α → β → β) :

rbtree α lt → β → β

Equations

rbtree.fold f ⟨t, _x⟩ b = rbnode.fold f t b

def rbtree.rev_fold {α : Type u} {β : Type v} {lt : α → α → Prop} (f : α → β → β) :

rbtree α lt → β → β

Equations

rbtree.rev_fold f ⟨t, _x⟩ b = rbnode.rev_fold f t b

def rbtree.empty {α : Type u} {lt : α → α → Prop} :

rbtree α lt → bool

Equations

rbtree.empty ⟨lchild.black_node val rchild, property⟩ = bool.ff
rbtree.empty ⟨lchild.red_node val rchild, property⟩ = bool.ff
rbtree.empty ⟨rbnode.leaf α, _x⟩ = bool.tt

def rbtree.to_list {α : Type u} {lt : α → α → Prop} :

rbtree α lt → list α

Equations

rbtree.to_list ⟨t, _x⟩ = rbnode.rev_fold (λ (_x : α) (_y : list α), _x :: _y) t list.nil

@[protected]

def rbtree.min {α : Type u} {lt : α → α → Prop} :

rbtree α lt → option α

Equations

rbtree.min ⟨t, _x⟩ = t.min

@[protected]

def rbtree.max {α : Type u} {lt : α → α → Prop} :

rbtree α lt → option α

Equations

rbtree.max ⟨t, _x⟩ = t.max

@[protected, instance]

def rbtree.has_repr {α : Type u} {lt : α → α → Prop} [has_repr α] :

has_repr (rbtree α lt)

Equations

rbtree.has_repr = {repr := λ (t : rbtree α lt), "rbtree_of " ++ repr t.to_list}

def rbtree.insert {α : Type u} {lt : α → α → Prop} [decidable_rel lt] :

rbtree α lt → α → rbtree α lt

Equations

rbtree.insert ⟨t, w⟩ x = ⟨rbnode.insert lt t x, _⟩

def rbtree.find {α : Type u} {lt : α → α → Prop} [decidable_rel lt] :

rbtree α lt → α → option α

Equations

rbtree.find ⟨t, _x⟩ x = rbnode.find lt t x

def rbtree.contains {α : Type u} {lt : α → α → Prop} [decidable_rel lt] (t : rbtree α lt) (a : α) :

Equations

t.contains a = (t.find a).is_some

def rbtree.from_list {α : Type u} (l : list α) (lt : α → α → Prop . "default_lt") [decidable_rel lt] :

rbtree α lt

Equations

rbtree.from_list l lt = list.foldl rbtree.insert (mk_rbtree α lt) l

def rbtree_of {α : Type u} (l : list α) (lt : α → α → Prop . "default_lt") [decidable_rel lt] :

rbtree α lt

Equations

rbtree_of l lt = rbtree.from_list l lt