@[instance]
Equations
- rbnode.color.decidable_eq = λ (a b : rbnode.color), a.cases_on (b.cases_on (is_true rfl) (is_false rbnode.color.decidable_eq._proof_1)) (b.cases_on (is_false rbnode.color.decidable_eq._proof_2) (is_true rfl))
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
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 = 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 = some v
- rbnode.leaf.min = none
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 = 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 = some v
- rbnode.leaf.max = none
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
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}
(a : rbnode α)
(a_1 : α)
(a_2 : rbnode α)
(a_3 : α)
(a_4 : 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
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}
(a : rbnode α)
(a_1 : α)
(a_2 : rbnode α)
(a_3 : α)
(a_4 : 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)
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
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]
(a : rbnode α)
(a_1 : α) :
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
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 : α) :
rbnode α
Equations
- rbnode.insert lt t x = rbnode.mk_insert_result t.get_color (rbnode.ins lt t x)
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
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]
(a : rbnode α)
(a_1 : α) :
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 = 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 = 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 = some y
- rbnode.find._match_1 y _f_1 _f_2 ordering.lt = _f_1
- 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'
Equations
- rbtree.mem a t = rbnode.mem lt a t.val
@[instance]
Equations
- rbtree.has_mem = {mem := rbtree.mem lt}
Equations
- rbtree.mem_exact a t = rbnode.mem_exact a t.val
Equations
- rbtree.depth f t = rbnode.depth f t.val
def
rbtree.fold
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
(f : α → β → β)
(a : rbtree α lt)
(a_1 : β) :
β
Equations
- rbtree.fold f ⟨t, _x⟩ b = rbnode.fold f t b
def
rbtree.rev_fold
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
(f : α → β → β)
(a : rbtree α lt)
(a_1 : β) :
β
Equations
- rbtree.rev_fold f ⟨t, _x⟩ b = rbnode.rev_fold f t b
Equations
- rbtree.empty ⟨lchild.black_node val rchild, property⟩ = ff
- rbtree.empty ⟨lchild.red_node val rchild, property⟩ = ff
- rbtree.empty ⟨rbnode.leaf α, _x⟩ = tt
Equations
- rbtree.to_list ⟨t, _x⟩ = rbnode.rev_fold (λ (_x : α) (_y : list α), _x :: _y) t list.nil
Equations
- rbtree.min ⟨t, _x⟩ = t.min
Equations
- rbtree.max ⟨t, _x⟩ = t.max
def
rbtree.insert
{α : Type u}
{lt : α → α → Prop}
[decidable_rel lt]
(a : rbtree α lt)
(a_1 : α) :
rbtree α lt
Equations
- rbtree.insert ⟨t, w⟩ x = ⟨rbnode.insert lt t x, _⟩
def
rbtree.find
{α : Type u}
{lt : α → α → Prop}
[decidable_rel lt]
(a : rbtree α lt)
(a_1 : α) :
option α
Equations
- rbtree.find ⟨t, _x⟩ x = rbnode.find lt t x
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