Additional lemmas for Red-black trees

@[simp]

theorem RBTree.RBNode.min?_reverse {α : Type u_1} (t : RBNode α) : t.reverse.min? = t.max?

@[simp]

theorem RBTree.RBNode.max?_reverse {α : Type u_1} (t : RBNode α) : t.reverse.max? = t.min?

@[simp]

theorem RBTree.RBNode.mem_nil {α : Type u_1} {x : α} : ¬x ∈ nil

@[simp]

theorem RBTree.RBNode.mem_node {α : Type u_1} {y : α} {c : RBColor} {a : RBNode α} {x : α} {b : RBNode α} : y ∈ node c a x b ↔ y = x ∨ y ∈ a ∨ y ∈ b

theorem RBTree.RBNode.All_def {α : Type u_1} {p : α → Prop} {t : RBNode α} : All p t ↔ ∀ (x : α), x ∈ t → p x

theorem RBTree.RBNode.Any_def {α : Type u_1} {p : α → Prop} {t : RBNode α} : Any p t ↔ ∃ (x : α), x ∈ t ∧ p x

theorem RBTree.RBNode.memP_def {α✝ : Type u_1} {cut : α✝ → Ordering} {t : RBNode α✝} : MemP cut t ↔ ∃ (x : α✝), x ∈ t ∧ cut x = Ordering.eq

theorem RBTree.RBNode.mem_def {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {x : α✝} {t : RBNode α✝} : Mem cmp x t ↔ ∃ (y : α✝), y ∈ t ∧ cmp x y = Ordering.eq

theorem RBTree.RBNode.mem_congr {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBNode α} (h : cmp x y = Ordering.eq) : Mem cmp x t ↔ Mem cmp y t

theorem RBTree.RBNode.isOrdered_iff' {α : Type u_1} {cmp : α → α → Ordering} {L R : Option α} [Std.TransCmp cmp] {t : RBNode α} : isOrdered cmp t L R = true ↔ (∀ (a : α), a ∈ L → All (fun (x : α) => cmpLT cmp a x) t) ∧ (∀ (a : α), a ∈ R → All (fun (x : α) => cmpLT cmp x a) t) ∧ (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → cmpLT cmp a b) ∧ Ordered cmp t

theorem RBTree.RBNode.isOrdered_iff {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t : RBNode α} : isOrdered cmp t = true ↔ Ordered cmp t

@[implicit_reducible]

instance RBTree.RBNode.instDecidableOrderedOfTransCmp {α : Type u_1} (cmp : α → α → Ordering) [Std.TransCmp cmp] (t : RBNode α) : Decidable (Ordered cmp t)

Equations

• RBTree.RBNode.instDecidableOrderedOfTransCmp cmp t = decidable_of_iff (RBTree.RBNode.isOrdered cmp t = true) ⋯

class RBTree.RBNode.IsCut {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) : Prop

A cut is like a homomorphism of orderings: it is a monotonic predicate with respect to cmp, but it can make things that are distinguished by cmp equal. This is sufficient for find? to locate an element on which cut returns .eq, but there may be other elements, not returned by find?, on which cut also returns .eq.

• le_lt_trans {x y : α} [Std.TransCmp cmp] : cmp x y ≠ Ordering.gt → cut x = Ordering.lt → cut y = Ordering.lt

  The set {x | cut x = .lt} is downward-closed.

• le_gt_trans {x y : α} [Std.TransCmp cmp] : cmp x y ≠ Ordering.gt → cut y = Ordering.gt → cut x = Ordering.gt

  The set {x | cut x = .gt} is upward-closed.

theorem RBTree.RBNode.IsCut.lt_trans {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {cut : α✝ → Ordering} {x y : α✝} [IsCut cmp cut] [Std.TransCmp cmp] (H : cmp x y = Ordering.lt) : cut x = Ordering.lt → cut y = Ordering.lt

theorem RBTree.RBNode.IsCut.gt_trans {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {cut : α✝ → Ordering} {x y : α✝} [IsCut cmp cut] [Std.TransCmp cmp] (H : cmp x y = Ordering.lt) : cut y = Ordering.gt → cut x = Ordering.gt

theorem RBTree.RBNode.IsCut.congr {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {cut : α✝ → Ordering} {x y : α✝} [IsCut cmp cut] [Std.TransCmp cmp] (H : cmp x y = Ordering.eq) : cut x = cut y

instance RBTree.RBNode.instIsCutFlipOrderingSwap {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) [IsCut cmp cut] : IsCut (flip cmp) fun (x : α) => (cut x).swap

class RBTree.RBNode.IsStrictCut {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) extends RBTree.RBNode.IsCut cmp cut : Prop

IsStrictCut upgrades the IsCut property to ensure that at most one element of the tree can match the cut, and hence find? will return the unique such element if one exists.

• le_lt_trans {x y : α} [Std.TransCmp cmp] : cmp x y ≠ Ordering.gt → cut x = Ordering.lt → cut y = Ordering.lt
• le_gt_trans {x y : α} [Std.TransCmp cmp] : cmp x y ≠ Ordering.gt → cut y = Ordering.gt → cut x = Ordering.gt
• exact {x y : α} [Std.TransCmp cmp] : cut x = Ordering.eq → cmp x y = cut y

  If cut = x, then cut and x have compare the same with respect to other elements.

instance RBTree.RBNode.instIsStrictCut {α : Type u_1} (cmp : α → α → Ordering) (a : α) : IsStrictCut cmp (cmp a)

A "representable cut" is one generated by cmp a for some a. This is always a valid cut.

instance RBTree.RBNode.instIsStrictCutFlipOrderingSwap {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) [IsStrictCut cmp cut] : IsStrictCut (flip cmp) fun (x : α) => (cut x).swap

theorem RBTree.RBNode.foldr_cons {α : Type u_1} (t : RBNode α) (l : List α) : foldr (fun (x1 : α) (x2 : List α) => x1 :: x2) t l = t.toList ++ l

@[simp]

theorem RBTree.RBNode.toList_nil {α : Type u_1} : nil.toList = []

@[simp]

theorem RBTree.RBNode.toList_node {α : Type u_1} {c : RBColor} {a : RBNode α} {x : α} {b : RBNode α} : (node c a x b).toList = a.toList ++ x :: b.toList

@[simp]

theorem RBTree.RBNode.toList_reverse {α : Type u_1} (t : RBNode α) : t.reverse.toList = t.toList.reverse

@[simp]

theorem RBTree.RBNode.mem_toList {α : Type u_1} {x : α} {t : RBNode α} : x ∈ t.toList ↔ x ∈ t

@[simp]

theorem RBTree.RBNode.mem_reverse {α : Type u_1} {a : α} {t : RBNode α} : a ∈ t.reverse ↔ a ∈ t

theorem RBTree.RBNode.min?_eq_toList_head? {α : Type u_1} {t : RBNode α} : t.min? = t.toList.head?

theorem RBTree.RBNode.max?_eq_toList_getLast? {α : Type u_1} {t : RBNode α} : t.max? = t.toList.getLast?

theorem RBTree.RBNode.foldr_eq_foldr_toList {α : Type u_1} {α✝ : Type u_2} {f : α → α✝ → α✝} {init : α✝} {t : RBNode α} : foldr f t init = List.foldr f init t.toList

theorem RBTree.RBNode.foldl_eq_foldl_toList {α : Type u_1} {α✝ : Type u_2} {f : α✝ → α → α✝} {init : α✝} {t : RBNode α} : foldl f init t = List.foldl f init t.toList

theorem RBTree.RBNode.foldl_reverse {α : Type u_1} {β : Type u_2} {t : RBNode α} {f : β → α → β} {init : β} : foldl f init t.reverse = foldr (flip f) t init

theorem RBTree.RBNode.foldr_reverse {α : Type u_1} {β : Type u_2} {t : RBNode α} {f : α → β → β} {init : β} : foldr f t.reverse init = foldl (flip f) init t

theorem RBTree.RBNode.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {f : α → m PUnit} [Monad m] [LawfulMonad m] {t : RBNode α} : forM f t = t.toList.forM f

theorem RBTree.RBNode.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {a✝ : Type u_1} {f : a✝ → α → m a✝} {init : a✝} [Monad m] [LawfulMonad m] {t : RBNode α} : foldlM f init t = List.foldlM f init t.toList

theorem RBTree.RBNode.forIn_visit_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {α✝ : Type u_1} {f : α → α✝ → m (ForInStep α✝)} {init : α✝} [Monad m] [LawfulMonad m] {t : RBNode α} : forIn.visit f t init = ForInStep.bindList f t.toList (ForInStep.yield init)

theorem RBTree.RBNode.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {α✝ : Type u_1} {init : α✝} {f : α → α✝ → m (ForInStep α✝)} [Monad m] [LawfulMonad m] {t : RBNode α} : forIn t init f = forIn t.toList init f

theorem RBTree.RBNode.Stream.foldr_cons {α : Type u_1} (t : RBNode.Stream α) (l : List α) : foldr (fun (x1 : α) (x2 : List α) => x1 :: x2) t l = t.toList ++ l

@[simp]

theorem RBTree.RBNode.Stream.toList_nil {α : Type u_1} : nil.toList = []

@[simp]

theorem RBTree.RBNode.Stream.toList_cons {α : Type u_1} {x : α} {r : RBNode α} {s : RBNode.Stream α} : (cons x r s).toList = x :: r.toList ++ s.toList

theorem RBTree.RBNode.Stream.foldr_eq_foldr_toList {α : Type u_1} {α✝ : Type u_2} {f : α → α✝ → α✝} {init : α✝} {s : RBNode.Stream α} : foldr f s init = List.foldr f init s.toList

theorem RBTree.RBNode.Stream.foldl_eq_foldl_toList {α : Type u_1} {α✝ : Type u_2} {f : α✝ → α → α✝} {init : α✝} {t : RBNode.Stream α} : foldl f init t = List.foldl f init t.toList

theorem RBTree.RBNode.Stream.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {α✝ : Type u_1} {init : α✝} {f : α → α✝ → m (ForInStep α✝)} [Monad m] [LawfulMonad m] {t : RBNode α} : forIn t init f = forIn t.toList init f

theorem RBTree.RBNode.toStream_toList' {α : Type u_1} {t : RBNode α} {s : RBNode.Stream α} : (t.toStream s).toList = t.toList ++ s.toList

@[simp]

theorem RBTree.RBNode.toStream_toList {α : Type u_1} {t : RBNode α} : t.toStream.toList = t.toList

theorem RBTree.RBNode.Stream.next?_toList {α : Type u_1} {s : RBNode.Stream α} : Option.map (fun (x : α × RBNode.Stream α) => match x with | (a, b) => (a, b.toList)) s.next? = s.toList.next?

theorem RBTree.RBNode.ordered_iff {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} : Ordered cmp t ↔ List.Pairwise (cmpLT cmp) t.toList

theorem RBTree.RBNode.Ordered.toList_sorted {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} : Ordered cmp t → List.Pairwise (cmpLT cmp) t.toList

theorem RBTree.RBNode.min?_mem {α : Type u_1} {a : α} {t : RBNode α} (h : t.min? = some a) : a ∈ t

theorem RBTree.RBNode.Ordered.min?_le {α : Type u_1} {cmp : α → α → Ordering} {a : α} {t : RBNode α} [Std.TransCmp cmp] (ht : Ordered cmp t) (h : t.min? = some a) (x : α) (hx : x ∈ t) : cmp a x ≠ Ordering.gt

theorem RBTree.RBNode.max?_mem {α : Type u_1} {a : α} {t : RBNode α} (h : t.max? = some a) : a ∈ t

theorem RBTree.RBNode.Ordered.le_max? {α : Type u_1} {cmp : α → α → Ordering} {a : α} {t : RBNode α} [Std.TransCmp cmp] (ht : Ordered cmp t) (h : t.max? = some a) (x : α) (hx : x ∈ t) : cmp x a ≠ Ordering.gt

@[simp]

theorem RBTree.RBNode.setBlack_toList {α : Type u_1} {t : RBNode α} : t.setBlack.toList = t.toList

@[simp]

theorem RBTree.RBNode.setRed_toList {α : Type u_1} {t : RBNode α} : t.setRed.toList = t.toList

@[simp]

theorem RBTree.RBNode.balance1_toList {α : Type u_1} {l : RBNode α} {v : α} {r : RBNode α} : (l.balance1 v r).toList = l.toList ++ v :: r.toList

@[simp]

theorem RBTree.RBNode.balance2_toList {α : Type u_1} {l : RBNode α} {v : α} {r : RBNode α} : (l.balance2 v r).toList = l.toList ++ v :: r.toList

@[simp]

theorem RBTree.RBNode.balLeft_toList {α : Type u_1} {l : RBNode α} {v : α} {r : RBNode α} : (l.balLeft v r).toList = l.toList ++ v :: r.toList

@[simp]

theorem RBTree.RBNode.balRight_toList {α : Type u_1} {l : RBNode α} {v : α} {r : RBNode α} : (l.balRight v r).toList = l.toList ++ v :: r.toList

theorem RBTree.RBNode.size_eq {α : Type u_1} {t : RBNode α} : t.size = t.toList.length

@[simp]

theorem RBTree.RBNode.reverse_size {α : Type u_1} (t : RBNode α) : t.reverse.size = t.size

@[simp]

theorem RBTree.RBNode.Any_reverse {α : Type u_1} {p : α → Prop} {t : RBNode α} : Any p t.reverse ↔ Any p t

@[simp]

theorem RBTree.RBNode.memP_reverse {α : Type u_1} {cut : α → Ordering} {t : RBNode α} : MemP cut t.reverse ↔ MemP (fun (x : α) => (cut x).swap) t

theorem RBTree.RBNode.Mem_reverse {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBNode α} : Mem cmp x t.reverse ↔ Mem (flip cmp) x t

theorem RBTree.RBNode.find?_some_eq_eq {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} : x ∈ find? cut t → cut x = Ordering.eq

theorem RBTree.RBNode.find?_some_mem {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} : x ∈ find? cut t → x ∈ t

theorem RBTree.RBNode.find?_some_memP {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} (h : x ∈ find? cut t) : MemP cut t

theorem RBTree.RBNode.Ordered.memP_iff_find? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} [Std.TransCmp cmp] [IsCut cmp cut] (ht : Ordered cmp t) : MemP cut t ↔ ∃ (x : α), find? cut t = some x

theorem RBTree.RBNode.Ordered.unique {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} {x y : α} [Std.TransCmp cmp] (ht : Ordered cmp t) (hx : x ∈ t) (hy : y ∈ t) (e : cmp x y = Ordering.eq) : x = y

theorem RBTree.RBNode.Ordered.find?_some {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {x : α} [Std.TransCmp cmp] [IsStrictCut cmp cut] (ht : Ordered cmp t) : find? cut t = some x ↔ x ∈ t ∧ cut x = Ordering.eq

@[simp]

theorem RBTree.RBNode.find?_reverse {α : Type u_1} (t : RBNode α) (cut : α → Ordering) : find? cut t.reverse = find? (fun (x : α) => (cut x).swap) t

def RBTree.RBNode.setRoot {α : Type u_1} (v : α) : RBNode α → RBNode α

Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

Equations

• RBTree.RBNode.setRoot v RBTree.RBNode.nil = RBTree.RBNode.node RBTree.RBColor.red RBTree.RBNode.nil v RBTree.RBNode.nil
• RBTree.RBNode.setRoot v (RBTree.RBNode.node c a v_1 b) = RBTree.RBNode.node c a v b

def RBTree.RBNode.delRoot {α : Type u_1} : RBNode α → RBNode α

Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

Equations

• RBTree.RBNode.nil.delRoot = RBTree.RBNode.nil
• (RBTree.RBNode.node c a v b).delRoot = a.append b

@[simp]

theorem RBTree.RBNode.upperBound?_reverse {α : Type u_1} (t : RBNode α) (cut : α → Ordering) (ub : Option α) : upperBound? cut t.reverse ub = lowerBound? (fun (x : α) => (cut x).swap) t ub

@[simp]

theorem RBTree.RBNode.lowerBound?_reverse {α : Type u_1} (t : RBNode α) (cut : α → Ordering) (lb : Option α) : lowerBound? cut t.reverse lb = upperBound? (fun (x : α) => (cut x).swap) t lb

theorem RBTree.RBNode.upperBound?_eq_find? {α : Type u_1} {x : α} {t : RBNode α} {cut : α → Ordering} (ub : Option α) (H : find? cut t = some x) : upperBound? cut t ub = some x

theorem RBTree.RBNode.lowerBound?_eq_find? {α : Type u_1} {x : α} {t : RBNode α} {cut : α → Ordering} (lb : Option α) (H : find? cut t = some x) : lowerBound? cut t lb = some x

theorem RBTree.RBNode.upperBound?_ge' {α : Type u_1} {ub : Option α} {cut : α → Ordering} {x : α} {t : RBNode α} (H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) : upperBound? cut t ub = some x → cut x ≠ Ordering.gt

The value x returned by upperBound? is greater or equal to the cut.

theorem RBTree.RBNode.upperBound?_ge {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} : upperBound? cut t = some x → cut x ≠ Ordering.gt

The value x returned by upperBound? is greater or equal to the cut.

theorem RBTree.RBNode.lowerBound?_le' {α : Type u_1} {lb : Option α} {cut : α → Ordering} {x : α} {t : RBNode α} (H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) : lowerBound? cut t lb = some x → cut x ≠ Ordering.lt

The value x returned by lowerBound? is less or equal to the cut.

theorem RBTree.RBNode.lowerBound?_le {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} : lowerBound? cut t = some x → cut x ≠ Ordering.lt

The value x returned by lowerBound? is less or equal to the cut.

theorem RBTree.RBNode.All.upperBound?_ub {α : Type u_1} {p : α → Prop} {ub : Option α} {cut : α → Ordering} {x : α} {t : RBNode α} (hp : All p t) (H : ∀ {x : α}, ub = some x → p x) : RBNode.upperBound? cut t ub = some x → p x

theorem RBTree.RBNode.All.upperBound? {α : Type u_1} {p : α → Prop} {cut : α → Ordering} {x : α} {t : RBNode α} (hp : All p t) : RBNode.upperBound? cut t = some x → p x

theorem RBTree.RBNode.All.lowerBound?_lb {α : Type u_1} {p : α → Prop} {lb : Option α} {cut : α → Ordering} {x : α} {t : RBNode α} (hp : All p t) (H : ∀ {x : α}, lb = some x → p x) : RBNode.lowerBound? cut t lb = some x → p x

theorem RBTree.RBNode.All.lowerBound? {α : Type u_1} {p : α → Prop} {cut : α → Ordering} {x : α} {t : RBNode α} (hp : All p t) : RBNode.lowerBound? cut t = some x → p x

theorem RBTree.RBNode.upperBound?_mem_ub {α : Type u_1} {cut : α → Ordering} {ub : Option α} {x : α} {t : RBNode α} (h : upperBound? cut t ub = some x) : x ∈ t ∨ ub = some x

theorem RBTree.RBNode.upperBound?_mem {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} (h : upperBound? cut t = some x) : x ∈ t

theorem RBTree.RBNode.lowerBound?_mem_lb {α : Type u_1} {cut : α → Ordering} {lb : Option α} {x : α} {t : RBNode α} (h : lowerBound? cut t lb = some x) : x ∈ t ∨ lb = some x

theorem RBTree.RBNode.lowerBound?_mem {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBNode α} (h : lowerBound? cut t = some x) : x ∈ t

theorem RBTree.RBNode.upperBound?_of_some {α : Type u_1} {cut : α → Ordering} {y : α} {t : RBNode α} : ∃ (x : α), upperBound? cut t (some y) = some x

theorem RBTree.RBNode.lowerBound?_of_some {α : Type u_1} {cut : α → Ordering} {y : α} {t : RBNode α} : ∃ (x : α), lowerBound? cut t (some y) = some x

theorem RBTree.RBNode.Ordered.upperBound?_exists {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} [Std.TransCmp cmp] [IsCut cmp cut] (h : Ordered cmp t) : (∃ (x : α), upperBound? cut t = some x) ↔ ∃ (x : α), x ∈ t ∧ cut x ≠ Ordering.gt

theorem RBTree.RBNode.Ordered.lowerBound?_exists {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} [Std.TransCmp cmp] [IsCut cmp cut] (h : Ordered cmp t) : (∃ (x : α), lowerBound? cut t = some x) ↔ ∃ (x : α), x ∈ t ∧ cut x ≠ Ordering.lt

theorem RBTree.RBNode.Ordered.upperBound?_least_ub {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {ub : Option α} {x y : α} [Std.TransCmp cmp] [IsCut cmp cut] (h : Ordered cmp t) (hub : ∀ {x : α}, ub = some x → All (fun (x_1 : α) => cmpLT cmp x_1 x) t) : upperBound? cut t ub = some x → y ∈ t → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt

theorem RBTree.RBNode.Ordered.lowerBound?_greatest_lb {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {lb : Option α} {x y : α} [Std.TransCmp cmp] [IsCut cmp cut] (h : Ordered cmp t) (hlb : ∀ {x : α}, lb = some x → All (fun (x_1 : α) => cmpLT cmp x x_1) t) : lowerBound? cut t lb = some x → y ∈ t → cut x = Ordering.gt → cmp x y = Ordering.lt → cut y = Ordering.lt

theorem RBTree.RBNode.Ordered.upperBound?_least {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {x y : α} [Std.TransCmp cmp] [IsCut cmp cut] (ht : Ordered cmp t) (H : upperBound? cut t = some x) (hy : y ∈ t) (xy : cmp y x = Ordering.lt) (hx : cut x = Ordering.lt) : cut y = Ordering.gt

A statement of the least-ness of the result of upperBound?. If x is the return value of upperBound? and it is strictly greater than the cut, then any other y < x in the tree is in fact strictly less than the cut (so there is no exact match, and nothing closer to the cut).

theorem RBTree.RBNode.Ordered.lowerBound?_greatest {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {x y : α} [Std.TransCmp cmp] [IsCut cmp cut] (ht : Ordered cmp t) (H : lowerBound? cut t = some x) (hy : y ∈ t) (xy : cmp x y = Ordering.lt) (hx : cut x = Ordering.gt) : cut y = Ordering.lt

A statement of the greatest-ness of the result of lowerBound?. If x is the return value of lowerBound? and it is strictly less than the cut, then any other y > x in the tree is in fact strictly greater than the cut (so there is no exact match, and nothing closer to the cut).

theorem RBTree.RBNode.Ordered.memP_iff_upperBound? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} [Std.TransCmp cmp] [IsCut cmp cut] (ht : Ordered cmp t) : MemP cut t ↔ ∃ (x : α), upperBound? cut t = some x ∧ cut x = Ordering.eq

theorem RBTree.RBNode.Ordered.memP_iff_lowerBound? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} [Std.TransCmp cmp] [IsCut cmp cut] (ht : Ordered cmp t) : MemP cut t ↔ ∃ (x : α), lowerBound? cut t = some x ∧ cut x = Ordering.eq

theorem RBTree.RBNode.Ordered.lowerBound?_lt {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {x y : α} [Std.TransCmp cmp] [IsStrictCut cmp cut] (ht : Ordered cmp t) (H : lowerBound? cut t = some x) (hy : y ∈ t) : cmp x y = Ordering.lt ↔ cut y = Ordering.lt

A stronger version of lowerBound?_greatest that holds when the cut is strict.

theorem RBTree.RBNode.Ordered.lt_upperBound? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBNode α} {x y : α} [Std.TransCmp cmp] [IsStrictCut cmp cut] (ht : Ordered cmp t) (H : upperBound? cut t = some x) (hy : y ∈ t) : cmp y x = Ordering.lt ↔ cut y = Ordering.gt

A stronger version of upperBound?_least that holds when the cut is strict.

def RBTree.RBNode.Path.listL {α : Type u_1} : Path α → List α

The list of elements to the left of the hole. (This function is intended for specification purposes only.)

Equations

• RBTree.RBNode.Path.root.listL = []
• (RBTree.RBNode.Path.left c parent v r).listL = parent.listL
• (RBTree.RBNode.Path.right c l v parent).listL = parent.listL ++ (l.toList ++ [v])

def RBTree.RBNode.Path.listR {α : Type u_1} : Path α → List α

The list of elements to the right of the hole. (This function is intended for specification purposes only.)

Equations

• RBTree.RBNode.Path.root.listR = []
• (RBTree.RBNode.Path.left c parent v r).listR = v :: r.toList ++ parent.listR
• (RBTree.RBNode.Path.right c l v parent).listR = parent.listR

@[reducible, inline]

abbrev RBTree.RBNode.Path.withList {α : Type u_1} (p : Path α) (l : List α) : List α

Wraps a list of elements with the left and right elements of the path.

Equations

• p.withList l = p.listL ++ l ++ p.listR

theorem RBTree.RBNode.Path.rootOrdered_iff {α : Type u_1} {cmp : α → α → Ordering} {v : α} {p : Path α} (hp : Ordered cmp p) : RootOrdered cmp p v ↔ (∀ (a : α), a ∈ p.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ p.listR → cmpLT cmp v a

theorem RBTree.RBNode.Path.ordered_iff {α : Type u_1} {cmp : α → α → Ordering} {p : Path α} : Ordered cmp p ↔ List.Pairwise (cmpLT cmp) p.listL ∧ List.Pairwise (cmpLT cmp) p.listR ∧ ∀ (x : α), x ∈ p.listL → ∀ (y : α), y ∈ p.listR → cmpLT cmp x y

theorem RBTree.RBNode.Path.zoom_zoomed₁ {α✝ : Type u_1} {cut : α✝ → Ordering} {t : RBNode α✝} {path : Path α✝} {t' : RBNode α✝} {path' : Path α✝} (e : zoom cut t path = (t', path')) : OnRoot (fun (x : α✝) => cut x = Ordering.eq) t'

@[simp]

theorem RBTree.RBNode.Path.fill_toList {α : Type u_1} {t : RBNode α} {p : Path α} : (p.fill t).toList = p.withList t.toList

theorem RBTree.RBNode.zoom_toList {α : Type u_1} {cut : α → Ordering} {t' : RBNode α} {p' : Path α} {t : RBNode α} (eq : zoom cut t = (t', p')) : p'.withList t'.toList = t.toList

@[simp]

theorem RBTree.RBNode.Path.ins_toList {α : Type u_1} {t : RBNode α} {p : Path α} : (p.ins t).toList = p.withList t.toList

@[simp]

theorem RBTree.RBNode.Path.insertNew_toList {α : Type u_1} {v : α} {p : Path α} : (p.insertNew v).toList = p.withList [v]

theorem RBTree.RBNode.Path.insert_toList {α : Type u_1} {t : RBNode α} {v : α} {p : Path α} : (p.insert t v).toList = p.withList (setRoot v t).toList

theorem RBTree.RBNode.Path.Balanced.insert {α : Type u_1} {c₀ : RBColor} {n₀ : Nat} {c : RBColor} {n : Nat} {t : RBNode α} {v : α} {path : Path α} (hp : Path.Balanced c₀ n₀ path c n) : t.Balanced c n → ∃ (c : RBColor), ∃ (n : Nat), (path.insert t v).Balanced c n

theorem RBTree.RBNode.Path.Ordered.insert {α : Type u_1} {cmp : α → α → Ordering} {v : α} {path : Path α} {t : RBNode α} : Ordered cmp path → RBNode.Ordered cmp t → All (RootOrdered cmp path) t → RootOrdered cmp path v → OnRoot (cmpEq cmp v) t → RBNode.Ordered cmp (path.insert t v)

theorem RBTree.RBNode.Path.Ordered.erase {α : Type u_1} {cmp : α → α → Ordering} {path : Path α} {t : RBNode α} : Ordered cmp path → RBNode.Ordered cmp t → All (RootOrdered cmp path) t → RBNode.Ordered cmp (path.erase t)

theorem RBTree.RBNode.Path.zoom_ins {α : Type u_1} {v : α} {path : Path α} {t' : RBNode α} {path' : Path α} {t : RBNode α} {cmp : α → α → Ordering} : zoom (cmp v) t path = (t', path') → path.ins (RBNode.ins cmp v t) = path'.ins (setRoot v t')

theorem RBTree.RBNode.Path.insertNew_eq_insert {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {t : RBNode α✝} {path : Path α✝} {v : α✝} (h : zoom (cmp v) t = (nil, path)) : path.insertNew v = (RBNode.insert cmp t v).setBlack

theorem RBTree.RBNode.Path.ins_eq_fill {α : Type u_1} {c₀ : RBColor} {n₀ : Nat} {c : RBColor} {n : Nat} {path : Path α} {t : RBNode α} : Path.Balanced c₀ n₀ path c n → t.Balanced c n → path.ins t = (path.fill t).setBlack

theorem RBTree.RBNode.Path.zoom_insert {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {t' : RBNode α} {v : α} {path : Path α} {t : RBNode α} (ht : t.Balanced c n) (H : zoom (cmp v) t = (t', path)) : (path.insert t' v).setBlack = (RBNode.insert cmp t v).setBlack

theorem RBTree.RBNode.Path.zoom_del {α : Type u_1} {cut : α → Ordering} {path : Path α} {t' : RBNode α} {path' : Path α} {t : RBNode α} : zoom cut t path = (t', path') → path.del (RBNode.del cut t) (match t with | node c l v r => c | x => RBColor.red) = path'.del t'.delRoot (match t' with | node c l v r => c | x => RBColor.red)

def RBTree.RBNode.Path.AllL {α : Type u_1} (p : α → Prop) : Path α → Prop

Asserts that p holds on all elements to the left of the hole.

Equations

• RBTree.RBNode.Path.AllL p RBTree.RBNode.Path.root = True
• RBTree.RBNode.Path.AllL p (RBTree.RBNode.Path.left c parent v r) = RBTree.RBNode.Path.AllL p parent
• RBTree.RBNode.Path.AllL p (RBTree.RBNode.Path.right c l v parent) = (RBTree.RBNode.All p l ∧ p v ∧ RBTree.RBNode.Path.AllL p parent)

def RBTree.RBNode.Path.AllR {α : Type u_1} (p : α → Prop) : Path α → Prop

Asserts that p holds on all elements to the right of the hole.

Equations

• RBTree.RBNode.Path.AllR p RBTree.RBNode.Path.root = True
• RBTree.RBNode.Path.AllR p (RBTree.RBNode.Path.left c parent v r) = (RBTree.RBNode.Path.AllR p parent ∧ p v ∧ RBTree.RBNode.All p r)
• RBTree.RBNode.Path.AllR p (RBTree.RBNode.Path.right c l v parent) = RBTree.RBNode.Path.AllR p parent

theorem RBTree.RBNode.insert_toList_zoom {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {t' : RBNode α} {p : Path α} {v : α} {t : RBNode α} (ht : t.Balanced c n) (e : zoom (cmp v) t = (t', p)) : (insert cmp t v).toList = p.withList (setRoot v t').toList

theorem RBTree.RBNode.insert_toList_zoom_nil {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {p : Path α} {v : α} {t : RBNode α} (ht : t.Balanced c n) (e : zoom (cmp v) t = (nil, p)) : (insert cmp t v).toList = p.withList [v]

theorem RBTree.RBNode.exists_insert_toList_zoom_nil {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {p : Path α} {v : α} {t : RBNode α} (ht : t.Balanced c n) (e : zoom (cmp v) t = (nil, p)) : ∃ (L : List α), ∃ (R : List α), t.toList = L ++ R ∧ (insert cmp t v).toList = L ++ v :: R

theorem RBTree.RBNode.insert_toList_zoom_node {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {c' : RBColor} {l : RBNode α} {v' : α} {r : RBNode α} {p : Path α} {v : α} {t : RBNode α} (ht : t.Balanced c n) (e : zoom (cmp v) t = (node c' l v' r, p)) : (insert cmp t v).toList = p.withList (node c l v r).toList

theorem RBTree.RBNode.exists_insert_toList_zoom_node {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {c' : RBColor} {l : RBNode α} {v' : α} {r : RBNode α} {p : Path α} {v : α} {t : RBNode α} (ht : t.Balanced c n) (e : zoom (cmp v) t = (node c' l v' r, p)) : ∃ (L : List α), ∃ (R : List α), t.toList = L ++ v' :: R ∧ (insert cmp t v).toList = L ++ v :: R

theorem RBTree.RBNode.mem_insert_self {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {v : α} {t : RBNode α} (ht : t.Balanced c n) : v ∈ insert cmp t v

theorem RBTree.RBNode.mem_insert_of_mem {α : Type u_1} {c : RBColor} {n : Nat} {v' : α} {cmp : α → α → Ordering} {v : α} {t : RBNode α} (ht : t.Balanced c n) (h : v' ∈ t) : v' ∈ insert cmp t v ∨ cmp v v' = Ordering.eq

theorem RBTree.RBNode.exists_find?_insert_self {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {c : RBColor} {n : Nat} {v : α} [Std.TransCmp cmp] [IsCut cmp cut] {t : RBNode α} (ht : t.Balanced c n) (ht₂ : Ordered cmp t) (hv : cut v = Ordering.eq) : ∃ (x : α), find? cut (insert cmp t v) = some x

theorem RBTree.RBNode.find?_insert_self {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {c : RBColor} {n : Nat} {v : α} [Std.TransCmp cmp] [IsStrictCut cmp cut] {t : RBNode α} (ht : t.Balanced c n) (ht₂ : Ordered cmp t) (hv : cut v = Ordering.eq) : find? cut (insert cmp t v) = some v

theorem RBTree.RBNode.mem_insert {α : Type u_1} {cmp : α → α → Ordering} {c : RBColor} {n : Nat} {v v' : α} [Std.TransCmp cmp] {t : RBNode α} (ht : t.Balanced c n) (ht₂ : Ordered cmp t) : v' ∈ insert cmp t v ↔ v' ∈ t ∧ find? (cmp v) t ≠ some v' ∨ v' = v

@[simp]

theorem RBTree.RBSet.val_toList {α : Type u_1} {cmp : α → α → Ordering} {t : RBSet α cmp} : t.val.toList = t.toList

@[simp]

theorem RBTree.RBSet.mkRBSet_eq {α : Type u_1} {cmp : α → α → Ordering} : mkRBSet α cmp = ∅

@[simp]

theorem RBTree.RBSet.empty_eq {α : Type u_1} {cmp : α → α → Ordering} : empty = ∅

@[simp]

theorem RBTree.RBSet.default_eq {α : Type u_1} {cmp : α → α → Ordering} : default = ∅

@[simp]

theorem RBTree.RBSet.empty_toList {α : Type u_1} {cmp : α → α → Ordering} : ∅.toList = []

@[simp]

theorem RBTree.RBSet.single_toList {α : Type u_1} {cmp : α → α → Ordering} {a : α} : (single a).toList = [a]

theorem RBTree.RBSet.mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} : x ∈ t.toList ↔ x ∈ t.val

theorem RBTree.RBSet.mem_congr {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBSet α cmp} (h : cmp x y = Ordering.eq) : x ∈ t ↔ y ∈ t

theorem RBTree.RBSet.mem_iff_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} : x ∈ t ↔ ∃ (y : α), y ∈ t.toList ∧ cmp x y = Ordering.eq

theorem RBTree.RBSet.mem_of_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBSet α cmp} (h : x ∈ t.toList) : x ∈ t

theorem RBTree.RBSet.foldl_eq_foldl_toList {α : Type u_1} {cmp : α → α → Ordering} {α✝ : Type u_2} {f : α✝ → α → α✝} {init : α✝} {t : RBSet α cmp} : foldl f init t = List.foldl f init t.toList

theorem RBTree.RBSet.foldr_eq_foldr_toList {α : Type u_1} {cmp : α → α → Ordering} {α✝ : Type u_2} {f : α → α✝ → α✝} {init : α✝} {t : RBSet α cmp} : foldr f init t = List.foldr f init t.toList

theorem RBTree.RBSet.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} {a✝ : Type u_1} {f : a✝ → α → m a✝} {init : a✝} [Monad m] [LawfulMonad m] {t : RBSet α cmp} : foldlM f init t = List.foldlM f init t.toList

theorem RBTree.RBSet.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} {f : α → m PUnit} [Monad m] [LawfulMonad m] {t : RBSet α cmp} : forM f t = t.toList.forM f

theorem RBTree.RBSet.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} {α✝ : Type u_1} {init : α✝} {f : α → α✝ → m (ForInStep α✝)} [Monad m] [LawfulMonad m] {t : RBSet α cmp} : forIn t init f = forIn t.toList init f

theorem RBTree.RBSet.toStream_eq {α : Type u_1} {cmp : α → α → Ordering} {t : RBSet α cmp} : Std.toStream t = t.val.toStream

@[simp]

theorem RBTree.RBSet.toStream_toList {α : Type u_1} {cmp : α → α → Ordering} {t : RBSet α cmp} : (Std.toStream t).toList = t.toList

theorem RBTree.RBSet.isEmpty_iff_toList_eq_nil {α : Type u_1} {cmp : α → α → Ordering} {t : RBSet α cmp} : t.isEmpty = true ↔ t.toList = []

theorem RBTree.RBSet.toList_sorted {α : Type u_1} {cmp : α → α → Ordering} {t : RBSet α cmp} : List.Pairwise (RBNode.cmpLT cmp) t.toList

theorem RBTree.RBSet.findP?_some_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} {t : RBSet α cmp} : t.findP? cut = some y → cut y = Ordering.eq

theorem RBTree.RBSet.find?_some_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} : t.find? x = some y → cmp x y = Ordering.eq

theorem RBTree.RBSet.findP?_some_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} {t : RBSet α cmp} (h : t.findP? cut = some y) : y ∈ t.toList

theorem RBTree.RBSet.find?_some_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} (h : t.find? x = some y) : y ∈ t.toList

theorem RBTree.RBSet.findP?_some_memP {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} {t : RBSet α cmp} (h : t.findP? cut = some y) : MemP cut t

theorem RBTree.RBSet.find?_some_mem {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} (h : t.find? x = some y) : x ∈ t

theorem RBTree.RBSet.mem_toList_unique {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBSet α cmp} (hx : x ∈ t.toList) (hy : y ∈ t.toList) (e : cmp x y = Ordering.eq) : x = y

theorem RBTree.RBSet.findP?_some {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {y : α} [Std.TransCmp cmp] [RBNode.IsStrictCut cmp cut] {t : RBSet α cmp} : t.findP? cut = some y ↔ y ∈ t.toList ∧ cut y = Ordering.eq

theorem RBTree.RBSet.find?_some {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBSet α cmp} : t.find? x = some y ↔ y ∈ t.toList ∧ cmp x y = Ordering.eq

theorem RBTree.RBSet.memP_iff_findP? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] {t : RBSet α cmp} : MemP cut t ↔ ∃ (y : α), t.findP? cut = some y

theorem RBTree.RBSet.mem_iff_find? {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : RBSet α cmp} : x ∈ t ↔ ∃ (y : α), t.find? x = some y

@[simp]

theorem RBTree.RBSet.contains_iff {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : RBSet α cmp} : t.contains x = true ↔ x ∈ t

@[implicit_reducible]

instance RBTree.RBSet.instDecidableMemOfTransCmp {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : RBSet α cmp} : Decidable (x ∈ t)

Equations

• RBTree.RBSet.instDecidableMemOfTransCmp = decidable_of_iff (t.contains x = true) ⋯

theorem RBTree.RBSet.size_eq {α : Type u_1} {cmp : α → α → Ordering} (t : RBSet α cmp) : t.size = t.toList.length

theorem RBTree.RBSet.mem_toList_insert_self {α : Type u_1} {cmp : α → α → Ordering} (v : α) (t : RBSet α cmp) : v ∈ (t.insert v).toList

theorem RBTree.RBSet.mem_insert_self {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] (v : α) (t : RBSet α cmp) : v ∈ t.insert v

theorem RBTree.RBSet.mem_insert_of_eq {α : Type u_1} {cmp : α → α → Ordering} {v v' : α} [Std.TransCmp cmp] (t : RBSet α cmp) (h : cmp v v' = Ordering.eq) : v' ∈ t.insert v

theorem RBTree.RBSet.mem_toList_insert_of_mem {α : Type u_1} {cmp : α → α → Ordering} {v' : α} (v : α) {t : RBSet α cmp} (h : v' ∈ t.toList) : v' ∈ (t.insert v).toList ∨ cmp v v' = Ordering.eq

theorem RBTree.RBSet.mem_insert_of_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {v' : α} [Std.OrientedCmp cmp] (v : α) {t : RBSet α cmp} (h : v' ∈ t.toList) : v' ∈ t.insert v

theorem RBTree.RBSet.mem_insert_of_mem {α : Type u_1} {cmp : α → α → Ordering} {v' : α} [Std.TransCmp cmp] (v : α) {t : RBSet α cmp} (h : v' ∈ t) : v' ∈ t.insert v

theorem RBTree.RBSet.mem_toList_insert {α : Type u_1} {cmp : α → α → Ordering} {v v' : α} [Std.TransCmp cmp] {t : RBSet α cmp} : v' ∈ (t.insert v).toList ↔ v' ∈ t.toList ∧ t.find? v ≠ some v' ∨ v' = v

theorem RBTree.RBSet.mem_insert {α : Type u_1} {cmp : α → α → Ordering} {v v' : α} [Std.TransCmp cmp] {t : RBSet α cmp} : v' ∈ t.insert v ↔ v' ∈ t ∨ cmp v v' = Ordering.eq

theorem RBTree.RBSet.find?_congr {α : Type u_1} {cmp : α → α → Ordering} {v₁ v₂ : α} [Std.TransCmp cmp] (t : RBSet α cmp) (h : cmp v₁ v₂ = Ordering.eq) : t.find? v₁ = t.find? v₂

theorem RBTree.RBSet.findP?_insert_of_eq {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {v : α} [Std.TransCmp cmp] [RBNode.IsStrictCut cmp cut] (t : RBSet α cmp) (h : cut v = Ordering.eq) : (t.insert v).findP? cut = some v

theorem RBTree.RBSet.find?_insert_of_eq {α : Type u_1} {cmp : α → α → Ordering} {v' v : α} [Std.TransCmp cmp] (t : RBSet α cmp) (h : cmp v' v = Ordering.eq) : (t.insert v).find? v' = some v

theorem RBTree.RBSet.findP?_insert_of_ne {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {v : α} [Std.TransCmp cmp] [RBNode.IsStrictCut cmp cut] (t : RBSet α cmp) (h : cut v ≠ Ordering.eq) : (t.insert v).findP? cut = t.findP? cut

theorem RBTree.RBSet.find?_insert_of_ne {α : Type u_1} {cmp : α → α → Ordering} {v' v : α} [Std.TransCmp cmp] (t : RBSet α cmp) (h : cmp v' v ≠ Ordering.eq) : (t.insert v).find? v' = t.find? v'

theorem RBTree.RBSet.findP?_insert {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : RBSet α cmp) (v : α) (cut : α → Ordering) [RBNode.IsStrictCut cmp cut] : (t.insert v).findP? cut = if cut v = Ordering.eq then some v else t.findP? cut

theorem RBTree.RBSet.find?_insert {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : RBSet α cmp) (v v' : α) : (t.insert v).find? v' = if cmp v' v = Ordering.eq then some v else t.find? v'

theorem RBTree.RBSet.upperBoundP?_eq_findP? {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} {cut : α → Ordering} (H : t.findP? cut = some x) : t.upperBoundP? cut = some x

theorem RBTree.RBSet.lowerBoundP?_eq_findP? {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} {cut : α → Ordering} (H : t.findP? cut = some x) : t.lowerBoundP? cut = some x

theorem RBTree.RBSet.upperBound?_eq_find? {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} (H : t.find? x = some y) : t.upperBound? x = some y

theorem RBTree.RBSet.lowerBound?_eq_find? {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} (H : t.find? x = some y) : t.lowerBound? x = some y

theorem RBTree.RBSet.upperBoundP?_ge {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBSet α cmp} : t.upperBoundP? cut = some x → cut x ≠ Ordering.gt

The value x returned by upperBoundP? is greater or equal to the cut.

theorem RBTree.RBSet.upperBound?_ge {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} : t.upperBound? x = some y → cmp x y ≠ Ordering.gt

The value y returned by upperBound? x is greater or equal to x.

theorem RBTree.RBSet.lowerBoundP?_le {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBSet α cmp} : t.lowerBoundP? cut = some x → cut x ≠ Ordering.lt

The value x returned by lowerBoundP? is less or equal to the cut.

theorem RBTree.RBSet.lowerBound?_le {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} : t.lowerBound? x = some y → cmp x y ≠ Ordering.lt

The value y returned by lowerBound? x is less or equal to x.

theorem RBTree.RBSet.upperBoundP?_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBSet α cmp} (h : t.upperBoundP? cut = some x) : x ∈ t.toList

theorem RBTree.RBSet.upperBound?_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} (h : t.upperBound? x = some y) : y ∈ t.toList

theorem RBTree.RBSet.lowerBoundP?_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBSet α cmp} (h : t.lowerBoundP? cut = some x) : x ∈ t.toList

theorem RBTree.RBSet.lowerBound?_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBSet α cmp} (h : t.lowerBound? x = some y) : y ∈ t.toList

theorem RBTree.RBSet.upperBoundP?_mem {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBSet α cmp} (h : t.upperBoundP? cut = some x) : x ∈ t

theorem RBTree.RBSet.lowerBoundP?_mem {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBSet α cmp} (h : t.lowerBoundP? cut = some x) : x ∈ t

theorem RBTree.RBSet.upperBound?_mem {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.OrientedCmp cmp] {t : RBSet α cmp} (h : t.upperBound? x = some y) : y ∈ t

theorem RBTree.RBSet.lowerBound?_mem {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.OrientedCmp cmp] {t : RBSet α cmp} (h : t.lowerBound? x = some y) : y ∈ t

theorem RBTree.RBSet.upperBoundP?_exists {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] : (∃ (x : α), t.upperBoundP? cut = some x) ↔ ∃ (x : α), x ∈ t ∧ cut x ≠ Ordering.gt

theorem RBTree.RBSet.lowerBoundP?_exists {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] : (∃ (x : α), t.lowerBoundP? cut = some x) ↔ ∃ (x : α), x ∈ t ∧ cut x ≠ Ordering.lt

theorem RBTree.RBSet.upperBound?_exists {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} [Std.TransCmp cmp] : (∃ (y : α), t.upperBound? x = some y) ↔ ∃ (y : α), y ∈ t ∧ cmp x y ≠ Ordering.gt

theorem RBTree.RBSet.lowerBound?_exists {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} [Std.TransCmp cmp] : (∃ (y : α), t.lowerBound? x = some y) ↔ ∃ (y : α), y ∈ t ∧ cmp x y ≠ Ordering.lt

theorem RBTree.RBSet.upperBoundP?_least {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] (H : t.upperBoundP? cut = some x) (hy : y ∈ t) (xy : cmp y x = Ordering.lt) (hx : cut x = Ordering.lt) : cut y = Ordering.gt

A statement of the least-ness of the result of upperBoundP?. If x is the return value of upperBoundP? and it is strictly greater than the cut, then any other y < x in the tree is in fact strictly less than the cut (so there is no exact match, and nothing closer to the cut).

theorem RBTree.RBSet.lowerBoundP?_greatest {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] (H : t.lowerBoundP? cut = some x) (hy : y ∈ t) (xy : cmp x y = Ordering.lt) (hx : cut x = Ordering.gt) : cut y = Ordering.lt

A statement of the greatest-ness of the result of lowerBoundP?. If x is the return value of lowerBoundP? and it is strictly less than the cut, then any other y > x in the tree is in fact strictly greater than the cut (so there is no exact match, and nothing closer to the cut).

theorem RBTree.RBSet.memP_iff_upperBoundP? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] : MemP cut t ↔ ∃ (x : α), t.upperBoundP? cut = some x ∧ cut x = Ordering.eq

theorem RBTree.RBSet.memP_iff_lowerBoundP? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsCut cmp cut] : MemP cut t ↔ ∃ (x : α), t.lowerBoundP? cut = some x ∧ cut x = Ordering.eq

theorem RBTree.RBSet.mem_iff_upperBound? {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} [Std.TransCmp cmp] : x ∈ t ↔ ∃ (y : α), t.upperBound? x = some y ∧ cmp x y = Ordering.eq

theorem RBTree.RBSet.mem_iff_lowerBound? {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBSet α cmp} [Std.TransCmp cmp] : x ∈ t ↔ ∃ (y : α), t.lowerBound? x = some y ∧ cmp x y = Ordering.eq

theorem RBTree.RBSet.lt_upperBoundP? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsStrictCut cmp cut] (H : t.upperBoundP? cut = some x) (hy : y ∈ t) : cmp y x = Ordering.lt ↔ cut y = Ordering.gt

A stronger version of upperBoundP?_least that holds when the cut is strict.

theorem RBTree.RBSet.lowerBoundP?_lt {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBSet α cmp} [Std.TransCmp cmp] [RBNode.IsStrictCut cmp cut] (H : t.lowerBoundP? cut = some x) (hy : y ∈ t) : cmp x y = Ordering.lt ↔ cut y = Ordering.lt

A stronger version of lowerBoundP?_greatest that holds when the cut is strict.

theorem RBTree.RBSet.lt_upperBound? {α : Type u_1} {cmp : α → α → Ordering} {x y z : α} {t : RBSet α cmp} [Std.TransCmp cmp] (H : t.upperBound? x = some y) (hz : z ∈ t) : cmp z y = Ordering.lt ↔ cmp z x = Ordering.lt

theorem RBTree.RBSet.lowerBound?_lt {α : Type u_1} {cmp : α → α → Ordering} {x y z : α} {t : RBSet α cmp} [Std.TransCmp cmp] (H : t.lowerBound? x = some y) (hz : z ∈ t) : cmp y z = Ordering.lt ↔ cmp x z = Ordering.lt

theorem RBTree.RBMap.val_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBMap α β cmp} : t.val.toList = t.toList

@[simp]

theorem RBTree.RBMap.mkRBSet_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : mkRBMap α β cmp = ∅

@[simp]

theorem RBTree.RBMap.empty_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : empty = ∅

@[simp]

theorem RBTree.RBMap.default_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : default = ∅

@[simp]

theorem RBTree.RBMap.empty_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : ∅.toList = []

@[simp]

theorem RBTree.RBMap.single_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {a : α} {b : β} : (single a b).toList = [(a, b)]

theorem RBTree.RBMap.mem_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α × β} {t : RBMap α β cmp} : x ∈ t.toList ↔ x ∈ t.val

theorem RBTree.RBMap.foldl_eq_foldl_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {α✝ : Type u_3} {f : α✝ → α → β → α✝} {init : α✝} {t : RBMap α β cmp} : foldl f init t = List.foldl (fun (r : α✝) (p : α × β) => f r p.fst p.snd) init t.toList

theorem RBTree.RBMap.foldr_eq_foldr_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {α✝ : Type u_3} {f : α → β → α✝ → α✝} {init : α✝} {t : RBMap α β cmp} : foldr f init t = List.foldr (fun (p : α × β) (r : α✝) => f p.fst p.snd r) init t.toList

theorem RBTree.RBMap.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {a✝ : Type u_1} {f : a✝ → α → β → m a✝} {init : a✝} [Monad m] [LawfulMonad m] {t : RBMap α β cmp} : foldlM f init t = List.foldlM (fun (r : a✝) (p : α × β) => f r p.fst p.snd) init t.toList

theorem RBTree.RBMap.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {f : α → β → m PUnit} [Monad m] [LawfulMonad m] {t : RBMap α β cmp} : forM f t = t.toList.forM fun (p : α × β) => f p.fst p.snd

theorem RBTree.RBMap.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {α✝ : Type u_1} {init : α✝} {f : α × β → α✝ → m (ForInStep α✝)} [Monad m] [LawfulMonad m] {t : RBMap α β cmp} : forIn t init f = forIn t.toList init f

theorem RBTree.RBMap.toStream_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBMap α β cmp} : Std.toStream t = t.val.toStream

@[simp]

theorem RBTree.RBMap.toStream_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBMap α β cmp} : (Std.toStream t).toList = t.toList

theorem RBTree.RBMap.toList_sorted {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBMap α β cmp} : List.Pairwise (RBNode.cmpLT fun (x1 x2 : α × β) => cmp x1.fst x2.fst) t.toList

theorem RBTree.RBMap.findEntry?_some_eq_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x y : α} {v : β} {t : RBMap α β cmp} : t.findEntry? x = some (y, v) → cmp x y = Ordering.eq

theorem RBTree.RBMap.findEntry?_some_mem_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {y : α × β} {t : RBMap α β cmp} (h : t.findEntry? x = some y) : y ∈ t.toList

theorem RBTree.RBMap.find?_some_mem_toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {v : β} {t : RBMap α β cmp} (h : t.find? x = some v) : ∃ (y : α), (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

theorem RBTree.RBMap.mem_toList_unique {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {x y : α × β} [Std.TransCmp cmp] {t : RBMap α β cmp} (hx : x ∈ t.toList) (hy : y ∈ t.toList) (e : cmp x.fst y.fst = Ordering.eq) : x = y

instance RBTree.RBMap.instIsStrictCut {α : Type u_1} (cmp : α → α → Ordering) (a : α) : RBNode.IsStrictCut cmp (cmp a)

A "representable cut" is one generated by cmp a for some a. This is always a valid cut.

instance RBTree.RBMap.instIsStrictCutByKeyOfTransCmp {α : Type u_1} {β : Type u_2} (f : α → β) (cmp : β → β → Ordering) [Std.TransCmp cmp] (x : β) : RBNode.IsStrictCut (Ordering.byKey f cmp) fun (y : α) => cmp x (f y)

theorem RBTree.RBMap.findEntry?_some {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {x : α} {y : α × β} [Std.TransCmp cmp] {t : RBMap α β cmp} : t.findEntry? x = some y ↔ y ∈ t.toList ∧ cmp x y.fst = Ordering.eq

theorem RBTree.RBMap.find?_some {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {x : α} {v : β} [Std.TransCmp cmp] {t : RBMap α β cmp} : t.find? x = some v ↔ ∃ (y : α), (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

theorem RBTree.RBMap.contains_iff_findEntry? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {t : RBMap α β cmp} : t.contains x = true ↔ ∃ (v : α × β), t.findEntry? x = some v

theorem RBTree.RBMap.contains_iff_find? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {t : RBMap α β cmp} : t.contains x = true ↔ ∃ (v : β), t.find? x = some v

theorem RBTree.RBMap.size_eq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBMap α β cmp) : t.size = t.toList.length

theorem RBTree.RBMap.mem_toList_insert_self {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {k : α} (v : β) (t : RBMap α β cmp) : (k, v) ∈ (t.insert k v).toList

theorem RBTree.RBMap.mem_toList_insert_of_mem {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {y : α × β} {k : α} (v : β) {t : RBMap α β cmp} (h : y ∈ t.toList) : y ∈ (t.insert k v).toList ∨ cmp k y.fst = Ordering.eq

theorem RBTree.RBMap.mem_toList_insert {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k : α} {v : β} {y : α × β} [Std.TransCmp cmp] {t : RBMap α β cmp} : y ∈ (t.insert k v).toList ↔ y ∈ t.toList ∧ t.findEntry? k ≠ some y ∨ y = (k, v)

theorem RBTree.RBMap.findEntry?_congr {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k₁ k₂ : α} [Std.TransCmp cmp] (t : RBMap α β cmp) (h : cmp k₁ k₂ = Ordering.eq) : t.findEntry? k₁ = t.findEntry? k₂

theorem RBTree.RBMap.find?_congr {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k₁ k₂ : α} [Std.TransCmp cmp] (t : RBMap α β cmp) (h : cmp k₁ k₂ = Ordering.eq) : t.find? k₁ = t.find? k₂

theorem RBTree.RBMap.findEntry?_insert_of_eq {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp] (t : RBMap α β cmp) (h : cmp k' k = Ordering.eq) : (t.insert k v).findEntry? k' = some (k, v)

theorem RBTree.RBMap.find?_insert_of_eq {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp] (t : RBMap α β cmp) (h : cmp k' k = Ordering.eq) : (t.insert k v).find? k' = some v

theorem RBTree.RBMap.findEntry?_insert_of_ne {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp] (t : RBMap α β cmp) (h : cmp k' k ≠ Ordering.eq) : (t.insert k v).findEntry? k' = t.findEntry? k'

theorem RBTree.RBMap.find?_insert_of_ne {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp] (t : RBMap α β cmp) (h : cmp k' k ≠ Ordering.eq) : (t.insert k v).find? k' = t.find? k'

theorem RBTree.RBMap.findEntry?_insert {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} [Std.TransCmp cmp] (t : RBMap α β cmp) (k : α) (v : β) (k' : α) : (t.insert k v).findEntry? k' = if cmp k' k = Ordering.eq then some (k, v) else t.findEntry? k'

theorem RBTree.RBMap.find?_insert {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} [Std.TransCmp cmp] (t : RBMap α β cmp) (k : α) (v : β) (k' : α) : (t.insert k v).find? k' = if cmp k' k = Ordering.eq then some v else t.find? k'