Red-black trees

This module implements a type RBMap α β cmp which is a functional data structure for storing a key-value store in a binary search tree.

It is built on the simpler RBSet α cmp type, which stores a set of values of type α using the function cmp : α → α → Ordering for determining the ordering relation. The tree will never store two elements that compare .eq under the cmp function, but the function does not have to satisfy cmp x y = .eq → x = y, and in the map case α is a key-value pair and the cmp function only compares the keys.

inductive Std.RBColor : Type

In a red-black tree, every node has a color which is either "red" or "black" (this particular choice of colors is conventional). A nil node is considered black.

• red: Std.RBColor

  A red node is required to have black children.

• black: Std.RBColor

  Every path from the root to a leaf must pass through the same number of black nodes.

instance Std.instReprRBColor : Repr Std.RBColor

Equations

• Std.instReprRBColor = { reprPrec := Std.reprRBColor✝ }

inductive Std.RBNode (α : Type u) : Type u

A red-black tree. (This is an internal implementation detail of the RBSet type, which includes the invariants of the tree.) This is a binary search tree augmented with a "color" field which is either red or black for each node and used to implement the re-balancing operations. See: Red–black tree

• nil: {α : Type u} → Std.RBNode α

  An empty tree.

• node: {α : Type u} → Std.RBColor → Std.RBNode α → α → Std.RBNode α → Std.RBNode α

  A node consists of a value v, a subtree l of smaller items, and a subtree r of larger items. The color c is either red or black and participates in the red-black balance invariant (see Balanced).

instance Std.instReprRBNode : {α : Type u_1} → [inst : Repr α] → Repr (Std.RBNode α)

Equations

• Std.instReprRBNode = { reprPrec := Std.reprRBNode✝ }

instance Std.RBNode.instEmptyCollectionRBNode {α : Type u_1} : EmptyCollection (Std.RBNode α)

Equations

• Std.RBNode.instEmptyCollectionRBNode = { emptyCollection := Std.RBNode.nil }

def Std.RBNode.min {α : Type u_1} : Std.RBNode α → Option α

The minimum element of a tree is the left-most value.

Equations

• Std.RBNode.min Std.RBNode.nil = none
• Std.RBNode.min (Std.RBNode.node c Std.RBNode.nil v r) = some v
• Std.RBNode.min (Std.RBNode.node c l v r) = Std.RBNode.min l

def Std.RBNode.max {α : Type u_1} : Std.RBNode α → Option α

The maximum element of a tree is the right-most value.

Equations

• Std.RBNode.max Std.RBNode.nil = none
• Std.RBNode.max (Std.RBNode.node c l v Std.RBNode.nil) = some v
• Std.RBNode.max (Std.RBNode.node c l v r) = Std.RBNode.max r

@[specialize #[]]

def Std.RBNode.fold {σ : Sort u_1} {α : Type u_2} (v₀ : σ) (f : σ → α → σ → σ) : Std.RBNode α → σ

Fold a function in tree order along the nodes. v₀ is used at nil nodes and f is used to combine results at branching nodes.

Equations

• Std.RBNode.fold v₀ f Std.RBNode.nil = v₀
• Std.RBNode.fold v₀ f (Std.RBNode.node a a_1 a_2 a_3) = f (Std.RBNode.fold v₀ f a_1) a_2 (Std.RBNode.fold v₀ f a_3)

@[specialize #[]]

def Std.RBNode.foldl {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (init : σ) : Std.RBNode α → σ

Fold a function on the values from left to right (in increasing order).

Equations

• Std.RBNode.foldl f x Std.RBNode.nil = x
• Std.RBNode.foldl f x (Std.RBNode.node c l v r) = Std.RBNode.foldl f (f (Std.RBNode.foldl f x l) v) r

@[specialize #[]]

def Std.RBNode.foldr {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) : Std.RBNode α → σ → σ

Fold a function on the values from right to left (in decreasing order).

Equations

• Std.RBNode.foldr f Std.RBNode.nil x = x
• Std.RBNode.foldr f (Std.RBNode.node c l v r) x = Std.RBNode.foldr f l (f v (Std.RBNode.foldr f r x))

def Std.RBNode.toList {α : Type u_1} (t : Std.RBNode α) : List α

O(n). Convert the tree to a list in ascending order.

Equations

• Std.RBNode.toList t = Std.RBNode.foldr (fun (x : α) (x_1 : List α) => x :: x_1) t []

@[specialize #[]]

def Std.RBNode.forM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → m PUnit) : Std.RBNode α → m PUnit

Run monadic function f on each element of the tree (in increasing order).

Equations

• Std.RBNode.forM f Std.RBNode.nil = pure PUnit.unit
• Std.RBNode.forM f (Std.RBNode.node a a_1 a_2 a_3) = do Std.RBNode.forM f a_1 f a_2 Std.RBNode.forM f a_3

@[specialize #[]]

def Std.RBNode.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} [Monad m] (f : σ → α → m σ) (init : σ) : Std.RBNode α → m σ

Fold a monadic function on the values from left to right (in increasing order).

Equations

• Std.RBNode.foldlM f x Std.RBNode.nil = pure x
• Std.RBNode.foldlM f x (Std.RBNode.node c l v r) = do let __do_lift ← Std.RBNode.foldlM f x l let __do_lift ← f __do_lift v Std.RBNode.foldlM f __do_lift r

@[inline]

def Std.RBNode.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [Monad m] (as : Std.RBNode α) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ

Implementation of for x in t loops over a RBNode (in increasing order).

Equations

• Std.RBNode.forIn as init f = ForInStep.run <$> Std.RBNode.forIn.visit f as init

@[specialize #[]]

def Std.RBNode.forIn.visit {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [Monad m] (f : α → σ → m (ForInStep σ)) : Std.RBNode α → σ → m (ForInStep σ)

Inner loop of forIn.

Equations

• Std.RBNode.forIn.visit f Std.RBNode.nil x = pure (ForInStep.yield x)
• Std.RBNode.forIn.visit f (Std.RBNode.node c l v r) x = ForInStep.bindM (Std.RBNode.forIn.visit f l x) fun (b : σ) => ForInStep.bindM (f v b) fun (x : σ) => Std.RBNode.forIn.visit f r x

instance Std.RBNode.instForInRBNode {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn m (Std.RBNode α) α

Equations

• Std.RBNode.instForInRBNode = { forIn := fun {β : Type u_1} [Monad m] => Std.RBNode.forIn }

inductive Std.RBNode.Stream (α : Type u_1) : Type u_1

An auxiliary data structure (an iterator) over an RBNode which lazily pulls elements from the left.

• nil: {α : Type u_1} → Std.RBNode.Stream α

  The stream is empty.

• cons: {α : Type u_1} → α → Std.RBNode α → Std.RBNode.Stream α → Std.RBNode.Stream α

  We are ready to deliver element v with right child r, and where tail represents all the subtrees we have yet to destructure.

def Std.RBNode.toStream {α : Type u_1} : Std.RBNode α → optParam (Std.RBNode.Stream α) Std.RBNode.Stream.nil → Std.RBNode.Stream α

O(log n). Turn a node into a stream, by descending along the left spine.

Equations

• Std.RBNode.toStream Std.RBNode.nil x = x
• Std.RBNode.toStream (Std.RBNode.node c l v r) x = Std.RBNode.toStream l (Std.RBNode.Stream.cons v r x)

def Std.RBNode.Stream.next? {α : Type u_1} : Std.RBNode.Stream α → Option (α × Std.RBNode.Stream α)

O(1) amortized, O(log n) worst case: Get the next element from the stream.

Equations

• Std.RBNode.Stream.next? x = match x with | Std.RBNode.Stream.nil => none | Std.RBNode.Stream.cons v r tail => some (v, Std.RBNode.toStream r tail)

@[specialize #[]]

def Std.RBNode.Stream.foldl {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (init : σ) : Std.RBNode.Stream α → σ

Fold a function on the values from left to right (in increasing order).

Equations

• Std.RBNode.Stream.foldl f x Std.RBNode.Stream.nil = x
• Std.RBNode.Stream.foldl f x (Std.RBNode.Stream.cons v r tail) = Std.RBNode.Stream.foldl f (Std.RBNode.foldl f (f x v) r) tail

@[specialize #[]]

def Std.RBNode.Stream.foldr {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) : Std.RBNode.Stream α → σ → σ

Fold a function on the values from right to left (in decreasing order).

Equations

• Std.RBNode.Stream.foldr f Std.RBNode.Stream.nil x = x
• Std.RBNode.Stream.foldr f (Std.RBNode.Stream.cons v r tail) x = f v (Std.RBNode.foldr f r (Std.RBNode.Stream.foldr f tail x))

def Std.RBNode.Stream.toList {α : Type u_1} (t : Std.RBNode.Stream α) : List α

O(n). Convert the stream to a list in ascending order.

Equations

• Std.RBNode.Stream.toList t = Std.RBNode.Stream.foldr (fun (x : α) (x_1 : List α) => x :: x_1) t []

instance Std.RBNode.instToStreamRBNodeStream {α : Type u_1} : ToStream (Std.RBNode α) (Std.RBNode.Stream α)

Equations

• Std.RBNode.instToStreamRBNodeStream = { toStream := fun (x : Std.RBNode α) => Std.RBNode.toStream x }

instance Std.RBNode.instStreamStream {α : Type u_1} : Stream (Std.RBNode.Stream α) α

Equations

• Std.RBNode.instStreamStream = { next? := Std.RBNode.Stream.next? }

@[specialize #[]]

def Std.RBNode.all {α : Type u_1} (p : α → Bool) : Std.RBNode α → Bool

Returns true iff every element of the tree satisfies p.

Equations

• Std.RBNode.all p Std.RBNode.nil = true
• Std.RBNode.all p (Std.RBNode.node a a_1 a_2 a_3) = (p a_2 && Std.RBNode.all p a_1 && Std.RBNode.all p a_3)

@[specialize #[]]

def Std.RBNode.any {α : Type u_1} (p : α → Bool) : Std.RBNode α → Bool

Returns true iff any element of the tree satisfies p.

Equations

• Std.RBNode.any p Std.RBNode.nil = false
• Std.RBNode.any p (Std.RBNode.node a a_1 a_2 a_3) = (p a_2 || Std.RBNode.any p a_1 || Std.RBNode.any p a_3)

def Std.RBNode.All {α : Type u_1} (p : α → Prop) : Std.RBNode α → Prop

Asserts that p holds on every element of the tree.

Equations

• Std.RBNode.All p Std.RBNode.nil = True
• Std.RBNode.All p (Std.RBNode.node a a_1 a_2 a_3) = (p a_2 ∧ Std.RBNode.All p a_1 ∧ Std.RBNode.All p a_3)

theorem Std.RBNode.All.imp {α : Type u_1} {p : α → Prop} {q : α → Prop} (H : ∀ {x : α}, p x → q x) {t : Std.RBNode α} : Std.RBNode.All p t → Std.RBNode.All q t

theorem Std.RBNode.all_iff {α : Type u_1} {p : α → Bool} {t : Std.RBNode α} : Std.RBNode.all p t = true ↔ Std.RBNode.All (fun (x : α) => p x = true) t

instance Std.RBNode.instDecidableAll {α : Type u_1} {p : α → Prop} {t : Std.RBNode α} [DecidablePred p] : Decidable (Std.RBNode.All p t)

Equations

• Std.RBNode.instDecidableAll = decidable_of_iff (Std.RBNode.all (fun (b : α) => decide (p b)) t = true) (_ : Std.RBNode.all (fun (b : α) => decide (p b)) t = true ↔ Std.RBNode.All p t)

def Std.RBNode.Any {α : Type u_1} (p : α → Prop) : Std.RBNode α → Prop

Asserts that p holds on some element of the tree.

Equations

• Std.RBNode.Any p Std.RBNode.nil = False
• Std.RBNode.Any p (Std.RBNode.node a a_1 a_2 a_3) = (p a_2 ∨ Std.RBNode.Any p a_1 ∨ Std.RBNode.Any p a_3)

theorem Std.RBNode.any_iff {α : Type u_1} {p : α → Bool} {t : Std.RBNode α} : Std.RBNode.any p t = true ↔ Std.RBNode.Any (fun (x : α) => p x = true) t

instance Std.RBNode.instDecidableAny {α : Type u_1} {p : α → Prop} {t : Std.RBNode α} [DecidablePred p] : Decidable (Std.RBNode.Any p t)

Equations

• Std.RBNode.instDecidableAny = decidable_of_iff (Std.RBNode.any (fun (b : α) => decide (p b)) t = true) (_ : Std.RBNode.any (fun (b : α) => decide (p b)) t = true ↔ Std.RBNode.Any p t)

def Std.RBNode.EMem {α : Type u_1} (x : α) (t : Std.RBNode α) : Prop

True if x is an element of t "exactly", i.e. up to equality, not the cmp relation.

Equations

• Std.RBNode.EMem x t = Std.RBNode.Any (fun (x_1 : α) => x = x_1) t

instance Std.RBNode.instMembershipRBNode {α : Type u_1} : Membership α (Std.RBNode α)

Equations

• Std.RBNode.instMembershipRBNode = { mem := Std.RBNode.EMem }

def Std.RBNode.MemP {α : Type u_1} (cut : α → Ordering) (t : Std.RBNode α) : Prop

True if the specified cut matches at least one element of of t.

Equations

• Std.RBNode.MemP cut t = Std.RBNode.Any (fun (x : α) => cut x = Ordering.eq) t

@[reducible]

def Std.RBNode.Mem {α : Type u_1} (cmp : α → α → Ordering) (x : α) (t : Std.RBNode α) : Prop

True if x is equivalent to an element of t.

Equations

• Std.RBNode.Mem cmp x t = Std.RBNode.MemP (cmp x) t

def Std.RBNode.Slow.instDecidableEMem {α : Type u_1} {x : α} [DecidableEq α] {t : Std.RBNode α} : Decidable (Std.RBNode.EMem x t)

Equations

• Std.RBNode.Slow.instDecidableEMem = inferInstanceAs (Decidable (Std.RBNode.Any (fun (x_1 : α) => x = x_1) t))

def Std.RBNode.Slow.instDecidableMemP {α : Type u_1} {cut : α → Ordering} {t : Std.RBNode α} : Decidable (Std.RBNode.MemP cut t)

Equations

• Std.RBNode.Slow.instDecidableMemP = inferInstanceAs (Decidable (Std.RBNode.Any (fun (x : α) => cut x = Ordering.eq) t))

def Std.RBNode.Slow.instDecidableMem {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : Std.RBNode α} : Decidable (Std.RBNode.Mem cmp x t)

Equations

• Std.RBNode.Slow.instDecidableMem = inferInstanceAs (Decidable (Std.RBNode.Any (fun (x_1 : α) => cmp x x_1 = Ordering.eq) t))

@[specialize #[]]

def Std.RBNode.all₂ {α : Type u_1} {β : Type u_2} (R : α → β → Bool) (t₁ : Std.RBNode α) (t₂ : Std.RBNode β) : Bool

Asserts that t₁ and t₂ have the same number of elements in the same order, and R holds pairwise between them. The tree structure is ignored.

Equations

• One or more equations did not get rendered due to their size.

instance Std.RBNode.instBEqRBNode {α : Type u_1} [BEq α] : BEq (Std.RBNode α)

Equations

• Std.RBNode.instBEqRBNode = { beq := fun (a b : Std.RBNode α) => Std.RBNode.all₂ (fun (x x_1 : α) => x == x_1) a b }

def Std.RBNode.cmpLT {α : Sort u_1} (cmp : α → α → Ordering) (x : α) (y : α) : Prop

We say that x < y under the comparator cmp if cmp x y = .lt.

• In order to avoid assuming the comparator is always lawful, we use a local ∀ [TransCmp cmp] binder in the relation so that the ordering properties of the tree only need to hold if the comparator is lawful.
• The Nonempty wrapper is a no-op because this is already a proposition, but it prevents the [TransCmp cmp] binder from being introduced when we don't want it.

Equations

• Std.RBNode.cmpLT cmp x y = Nonempty (∀ [inst : Std.TransCmp cmp], cmp x y = Ordering.lt)

theorem Std.RBNode.cmpLT_iff : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Std.TransCmp cmp], Std.RBNode.cmpLT cmp x y ↔ cmp x y = Ordering.lt

instance Std.RBNode.instDecidableCmpLT : {α : Sort u_1} → {x y : α} → (cmp : α → α → Ordering) → [inst : Std.TransCmp cmp] → Decidable (Std.RBNode.cmpLT cmp x y)

Equations

• Std.RBNode.instDecidableCmpLT cmp = decidable_of_iff' (cmp x y = Ordering.lt) (_ : Std.RBNode.cmpLT cmp x y ↔ cmp x y = Ordering.lt)

def Std.RBNode.cmpEq {α : Sort u_1} (cmp : α → α → Ordering) (x : α) (y : α) : Prop

We say that x ≈ y under the comparator cmp if cmp x y = .eq. See also cmpLT.

Equations

• Std.RBNode.cmpEq cmp x y = Nonempty (∀ [inst : Std.TransCmp cmp], cmp x y = Ordering.eq)

theorem Std.RBNode.cmpEq_iff : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Std.TransCmp cmp], Std.RBNode.cmpEq cmp x y ↔ cmp x y = Ordering.eq

instance Std.RBNode.instDecidableCmpEq : {α : Sort u_1} → {x y : α} → (cmp : α → α → Ordering) → [inst : Std.TransCmp cmp] → Decidable (Std.RBNode.cmpEq cmp x y)

Equations

• Std.RBNode.instDecidableCmpEq cmp = decidable_of_iff' (cmp x y = Ordering.eq) (_ : Std.RBNode.cmpEq cmp x y ↔ cmp x y = Ordering.eq)

def Std.RBNode.isOrdered {α : Type u_1} (cmp : α → α → Ordering) (t : Std.RBNode α) (l : optParam (Option α) none) (r : optParam (Option α) none) : Bool

O(n). Verifies an ordering relation on the nodes of the tree.

Equations

• Std.RBNode.isOrdered cmp Std.RBNode.nil l r = match l, r with | some l, some r => decide (cmp l r = Ordering.lt) | x, x_1 => true
• Std.RBNode.isOrdered cmp (Std.RBNode.node a a_1 a_2 a_3) l r = (Std.RBNode.isOrdered cmp a_1 l (some a_2) && Std.RBNode.isOrdered cmp a_3 (some a_2) r)

@[inline]

def Std.RBNode.balance1 {α : Type u_1} : Std.RBNode α → α → Std.RBNode α → Std.RBNode α

The first half of Okasaki's balance, concerning red-red sequences in the left child.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.RBNode.balance2 {α : Type u_1} : Std.RBNode α → α → Std.RBNode α → Std.RBNode α

The second half of Okasaki's balance, concerning red-red sequences in the right child.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.RBNode.isRed {α : Type u_1} : Std.RBNode α → Std.RBColor

Returns red if the node is red, otherwise black. (Nil nodes are treated as black.)

Equations

• Std.RBNode.isRed x = match x with | Std.RBNode.node c l v r => c | x => Std.RBColor.black

@[inline]

def Std.RBNode.isBlack {α : Type u_1} : Std.RBNode α → Std.RBColor

Returns black if the node is black, otherwise red. (Nil nodes are treated as red, which is not the usual convention but useful for deletion.)

Equations

• Std.RBNode.isBlack x = match x with | Std.RBNode.node c l v r => c | x => Std.RBColor.red

def Std.RBNode.setBlack {α : Type u_1} : Std.RBNode α → Std.RBNode α

Change the color of the root to black.

Equations

• Std.RBNode.setBlack x = match x with | Std.RBNode.nil => Std.RBNode.nil | Std.RBNode.node c l v r => Std.RBNode.node Std.RBColor.black l v r

@[specialize #[]]

def Std.RBNode.ins {α : Type u_1} (cmp : α → α → Ordering) (x : α) : Std.RBNode α → Std.RBNode α

The core of the insert function. This adds an element x to a balanced red-black tree. Importantly, the result of calling ins is not a proper red-black tree, because it has a broken balance invariant. (See Balanced.ins for the balance invariant of ins.) The insert function does the final fixup needed to restore the invariant.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.ins cmp x Std.RBNode.nil = Std.RBNode.node Std.RBColor.red Std.RBNode.nil x Std.RBNode.nil

@[specialize #[]]

def Std.RBNode.insert {α : Type u_1} (cmp : α → α → Ordering) (t : Std.RBNode α) (v : α) : Std.RBNode α

insert cmp t v inserts element v into the tree, using the provided comparator cmp to put it in the right place and automatically rebalancing the tree as necessary.

Equations

• Std.RBNode.insert cmp t v = match Std.RBNode.isRed t with | Std.RBColor.red => Std.RBNode.setBlack (Std.RBNode.ins cmp v t) | Std.RBColor.black => Std.RBNode.ins cmp v t

def Std.RBNode.setRed {α : Type u_1} : Std.RBNode α → Std.RBNode α

Recolor the root of the tree to red if possible.

Equations

• Std.RBNode.setRed x = match x with | Std.RBNode.node c a v b => Std.RBNode.node Std.RBColor.red a v b | Std.RBNode.nil => Std.RBNode.nil

def Std.RBNode.balLeft {α : Type u_1} (l : Std.RBNode α) (v : α) (r : Std.RBNode α) : Std.RBNode α

Rebalancing a tree which has shrunk on the left.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBNode.balRight {α : Type u_1} (l : Std.RBNode α) (v : α) (r : Std.RBNode α) : Std.RBNode α

Rebalancing a tree which has shrunk on the right.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBNode.size {α : Type u_1} : Std.RBNode α → Nat

The number of nodes in the tree.

Equations

• Std.RBNode.size Std.RBNode.nil = 0
• Std.RBNode.size (Std.RBNode.node a a_1 a_2 a_3) = Std.RBNode.size a_1 + Std.RBNode.size a_3 + 1

def Std.RBNode.append {α : Type u_1} : Std.RBNode α → Std.RBNode α → Std.RBNode α

Concatenate two trees with the same black-height.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.append Std.RBNode.nil x = x
• Std.RBNode.append x Std.RBNode.nil = x

erase

@[specialize #[]]

def Std.RBNode.del {α : Type u_1} (cut : α → Ordering) : Std.RBNode α → Std.RBNode α

The core of the erase function. The tree returned from this function has a broken invariant, which is restored in erase.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.del cut Std.RBNode.nil = Std.RBNode.nil

@[specialize #[]]

def Std.RBNode.erase {α : Type u_1} (cut : α → Ordering) (t : Std.RBNode α) : Std.RBNode α

The erase cut t function removes an element from the tree t. The cut function is used to locate an element in the tree: it returns .gt if we go too high and .lt if we go too low; if it returns .eq we will remove the element. (The function cmp k for some key k is a valid cut function, but we can also use cuts that are not of this form as long as they are suitably monotonic.)

Equations

• Std.RBNode.erase cut t = Std.RBNode.setBlack (Std.RBNode.del cut t)

@[specialize #[]]

def Std.RBNode.find? {α : Type u_1} (cut : α → Ordering) : Std.RBNode α → Option α

Finds an element in the tree satisfying the cut function.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.find? cut Std.RBNode.nil = none

@[specialize #[]]

def Std.RBNode.lowerBound? {α : Type u_1} (cut : α → Ordering) : Std.RBNode α → Option α → Option α

lowerBound? cut retrieves the largest entry smaller than or equal to cut, if it exists.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.lowerBound? cut Std.RBNode.nil x = x

def Std.RBNode.root? {α : Type u_1} : Std.RBNode α → Option α

Returns the root of the tree, if any.

Equations

• Std.RBNode.root? x = match x with | Std.RBNode.nil => none | Std.RBNode.node c l v r => some v

@[specialize #[]]

def Std.RBNode.map {α : Type u_1} {β : Type u_2} (f : α → β) : Std.RBNode α → Std.RBNode β

O(n). Map a function on every value in the tree. This requires IsMonotone on the function in order to preserve the order invariant.

Equations

• Std.RBNode.map f Std.RBNode.nil = Std.RBNode.nil
• Std.RBNode.map f (Std.RBNode.node a a_1 a_2 a_3) = Std.RBNode.node a (Std.RBNode.map f a_1) (f a_2) (Std.RBNode.map f a_3)

def Std.RBNode.toArray {α : Type u_1} (n : Std.RBNode α) : Array α

Converts the tree into an array in increasing sorted order.

Equations

• Std.RBNode.toArray n = Std.RBNode.foldl (fun (x : Array α) (x_1 : α) => Array.push x x_1) #[] n

inductive Std.RBNode.Path (α : Type u) : Type u

A RBNode.Path α is a "cursor" into an RBNode which represents the path from the root to a subtree. Note that the path goes from the target subtree up to the root, which is reversed from the normal way data is stored in the tree. See Zipper for more information.

• root: {α : Type u} → Std.RBNode.Path α

  The root of the tree, which is the end of the path of parents.

• left: {α : Type u} → Std.RBColor → Std.RBNode.Path α → α → Std.RBNode α → Std.RBNode.Path α

  A path that goes down the left subtree.

• right: {α : Type u} → Std.RBColor → Std.RBNode α → α → Std.RBNode.Path α → Std.RBNode.Path α

  A path that goes down the right subtree.

def Std.RBNode.Path.fill {α : Type u_1} : Std.RBNode.Path α → Std.RBNode α → Std.RBNode α

Fills the Path with a subtree.

Equations

• Std.RBNode.Path.fill Std.RBNode.Path.root x = x
• Std.RBNode.Path.fill (Std.RBNode.Path.left c parent y b) x = Std.RBNode.Path.fill parent (Std.RBNode.node c x y b)
• Std.RBNode.Path.fill (Std.RBNode.Path.right c a y parent) x = Std.RBNode.Path.fill parent (Std.RBNode.node c a y x)

@[specialize #[]]

def Std.RBNode.zoom {α : Type u_1} (cut : α → Ordering) : Std.RBNode α → optParam (Std.RBNode.Path α) Std.RBNode.Path.root → Std.RBNode α × Std.RBNode.Path α

Like find?, but instead of just returning the element, it returns the entire subtree at the element and a path back to the root for reconstructing the tree.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.zoom cut Std.RBNode.nil x = (Std.RBNode.nil, x)

def Std.RBNode.Path.ins {α : Type u_1} : Std.RBNode.Path α → Std.RBNode α → Std.RBNode α

This function does the second part of RBNode.ins, which unwinds the stack and rebuilds the tree.

Equations

• Std.RBNode.Path.ins Std.RBNode.Path.root x = Std.RBNode.setBlack x
• Std.RBNode.Path.ins (Std.RBNode.Path.left Std.RBColor.red parent y b) x = Std.RBNode.Path.ins parent (Std.RBNode.node Std.RBColor.red x y b)
• Std.RBNode.Path.ins (Std.RBNode.Path.right Std.RBColor.red a y parent) x = Std.RBNode.Path.ins parent (Std.RBNode.node Std.RBColor.red a y x)
• Std.RBNode.Path.ins (Std.RBNode.Path.left Std.RBColor.black parent y b) x = Std.RBNode.Path.ins parent (Std.RBNode.balance1 x y b)
• Std.RBNode.Path.ins (Std.RBNode.Path.right Std.RBColor.black a y parent) x = Std.RBNode.Path.ins parent (Std.RBNode.balance2 a y x)

@[inline]

def Std.RBNode.Path.insertNew {α : Type u_1} (path : Std.RBNode.Path α) (v : α) : Std.RBNode α

path.insertNew v inserts element v into the tree, assuming that path is zoomed in on a nil node such that inserting a new element at this position is valid.

Equations

• Std.RBNode.Path.insertNew path v = Std.RBNode.Path.ins path (Std.RBNode.node Std.RBColor.red Std.RBNode.nil v Std.RBNode.nil)

def Std.RBNode.Path.insert {α : Type u_1} (path : Std.RBNode.Path α) (t : Std.RBNode α) (v : α) : Std.RBNode α

path.insert t v inserts element v into the tree, assuming that (t, path) was the result of a previous zoom operation (so either the root of t is equivalent to v or it is empty).

Equations

• Std.RBNode.Path.insert path t v = match t with | Std.RBNode.nil => Std.RBNode.Path.insertNew path v | Std.RBNode.node c a v_1 b => Std.RBNode.Path.fill path (Std.RBNode.node c a v b)

def Std.RBNode.Path.del {α : Type u_1} : Std.RBNode.Path α → Std.RBNode α → Std.RBColor → Std.RBNode α

path.del t c does the second part of RBNode.del, which unwinds the stack and rebuilds the tree. The c argument is the color of the node before the deletion (we used t₀.isBlack for this in RBNode.del but the original tree is no longer available in this formulation).

Equations

• Std.RBNode.Path.del Std.RBNode.Path.root x✝ x = Std.RBNode.setBlack x✝
• Std.RBNode.Path.del (Std.RBNode.Path.left c parent y b) x Std.RBColor.red = Std.RBNode.Path.del parent (Std.RBNode.node Std.RBColor.red x y b) c
• Std.RBNode.Path.del (Std.RBNode.Path.right c a y parent) x Std.RBColor.red = Std.RBNode.Path.del parent (Std.RBNode.node Std.RBColor.red a y x) c
• Std.RBNode.Path.del (Std.RBNode.Path.left c parent y b) x Std.RBColor.black = Std.RBNode.Path.del parent (Std.RBNode.balLeft x y b) c
• Std.RBNode.Path.del (Std.RBNode.Path.right c a y parent) x Std.RBColor.black = Std.RBNode.Path.del parent (Std.RBNode.balRight a y x) c

def Std.RBNode.Path.erase {α : Type u_1} (path : Std.RBNode.Path α) (t : Std.RBNode α) : Std.RBNode α

path.erase t v removes the root element of t from the tree, assuming that (t, path) was the result of a previous zoom operation.

Equations

• Std.RBNode.Path.erase path t = match t with | Std.RBNode.nil => Std.RBNode.Path.fill path Std.RBNode.nil | Std.RBNode.node c a v b => Std.RBNode.Path.del path (Std.RBNode.append a b) c

@[specialize #[]]

def Std.RBNode.modify {α : Type u_1} (cut : α → Ordering) (f : α → α) (t : Std.RBNode α) : Std.RBNode α

modify cut f t uses cut to find an element, then modifies the element using f and reinserts it into the tree.

Because the tree structure is not modified, f must not modify the ordering properties of the element.

The element in t is used linearly if t is unshared.

Equations

• Std.RBNode.modify cut f t = match Std.RBNode.zoom cut t with | (Std.RBNode.nil, snd) => t | (Std.RBNode.node c a x b, path) => Std.RBNode.Path.fill path (Std.RBNode.node c a (f x) b)

@[specialize #[]]

def Std.RBNode.alter {α : Type u_1} (cut : α → Ordering) (f : Option α → Option α) (t : Std.RBNode α) : Std.RBNode α

alter cut f t simultaneously handles inserting, erasing and replacing an element using a function f : Option α → Option α. It is passed the result of t.find? cut and can either return none to remove the element or some a to replace/insert the element with a (which must have the same ordering properties as the original element).

The element is used linearly if t is unshared.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBNode.Ordered {α : Type u_1} (cmp : α → α → Ordering) : Std.RBNode α → Prop

The ordering invariant of a red-black tree, which is a binary search tree. This says that every element of a left subtree is less than the root, and every element in the right subtree is greater than the root, where the less than relation x < y is understood to mean cmp x y = .lt.

Because we do not assume that cmp is lawful when stating this property, we write it in such a way that if cmp is not lawful then the condition holds trivially. That way we can prove the ordering invariants without assuming cmp is lawful.

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.Ordered cmp Std.RBNode.nil = True

def Std.RBNode.Slow.instDecidableOrdered {α : Type u_1} (cmp : α → α → Ordering) [Std.TransCmp cmp] (t : Std.RBNode α) : Decidable (Std.RBNode.Ordered cmp t)

Equations

• One or more equations did not get rendered due to their size.
• Std.RBNode.Slow.instDecidableOrdered cmp Std.RBNode.nil = inferInstanceAs (Decidable True)

inductive Std.RBNode.Balanced {α : Type u_1} : Std.RBNode α → Std.RBColor → Nat → Prop

The red-black balance invariant. Balanced t c n says that the color of the root node is c, and the black-height (the number of black nodes on any path from the root) of the tree is n. Additionally, every red node must have black children.

• nil: ∀ {α : Type u_1}, Std.RBNode.Balanced Std.RBNode.nil Std.RBColor.black 0

  A nil node is balanced with black-height 0, and it is considered black.

• red: ∀ {α : Type u_1} {x : Std.RBNode α} {n : Nat} {y : Std.RBNode α} {v : α}, Std.RBNode.Balanced x Std.RBColor.black n → Std.RBNode.Balanced y Std.RBColor.black n → Std.RBNode.Balanced (Std.RBNode.node Std.RBColor.red x v y) Std.RBColor.red n

  A red node is balanced with black-height n if its children are both black with with black-height n.

• black: ∀ {α : Type u_1} {x : Std.RBNode α} {c₁ : Std.RBColor} {n : Nat} {y : Std.RBNode α} {c₂ : Std.RBColor} {v : α}, Std.RBNode.Balanced x c₁ n → Std.RBNode.Balanced y c₂ n → Std.RBNode.Balanced (Std.RBNode.node Std.RBColor.black x v y) Std.RBColor.black (n + 1)

  A black node is balanced with black-height n + 1 if its children both have black-height n.

inductive Std.RBNode.WF {α : Type u_1} (cmp : α → α → Ordering) : Std.RBNode α → Prop

The well-formedness invariant for a red-black tree. The first constructor is the real invariant, and the others allow us to "cheat" in this file and define insert and erase, which have more complex proofs that are delayed to Std.Data.RBMap.Lemmas.

• mk: ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} {c : Std.RBColor} {n : Nat}, Std.RBNode.Ordered cmp t → Std.RBNode.Balanced t c n → Std.RBNode.WF cmp t

  The actual well-formedness invariant: a red-black tree has the ordering and balance invariants.

• insert: ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} {a : α}, Std.RBNode.WF cmp t → Std.RBNode.WF cmp (Std.RBNode.insert cmp t a)

  Inserting into a well-formed tree yields another well-formed tree. (See Ordered.insert and Balanced.insert for the actual proofs.)

• erase: ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} {cut : α → Ordering}, Std.RBNode.WF cmp t → Std.RBNode.WF cmp (Std.RBNode.erase cut t)

  Erasing from a well-formed tree yields another well-formed tree. (See Ordered.erase and Balanced.erase for the actual proofs.)

def Std.RBSet (α : Type u) (cmp : α → α → Ordering) : Type u

An RBSet is a self-balancing binary search tree. The cmp function is the comparator that will be used for performing searches; it should satisfy the requirements of TransCmp for it to have sensible behavior.

Equations

• Std.RBSet α cmp = { t : Std.RBNode α // Std.RBNode.WF cmp t }

@[inline]

def Std.mkRBSet (α : Type u) (cmp : α → α → Ordering) : Std.RBSet α cmp

O(1). Construct a new empty tree.

Equations

• Std.mkRBSet α cmp = { val := Std.RBNode.nil, property := (_ : Std.RBNode.WF cmp Std.RBNode.nil) }

@[inline]

def Std.RBSet.empty {α : Type u_1} {cmp : α → α → Ordering} : Std.RBSet α cmp

O(1). Construct a new empty tree.

Equations

• Std.RBSet.empty = Std.mkRBSet α cmp

instance Std.RBSet.instEmptyCollectionRBSet (α : Type u) (cmp : α → α → Ordering) : EmptyCollection (Std.RBSet α cmp)

Equations

• Std.RBSet.instEmptyCollectionRBSet α cmp = { emptyCollection := Std.RBSet.empty }

instance Std.RBSet.instInhabitedRBSet (α : Type u) (cmp : α → α → Ordering) : Inhabited (Std.RBSet α cmp)

Equations

• Std.RBSet.instInhabitedRBSet α cmp = { default := ∅ }

@[inline]

def Std.RBSet.single {α : Type u_1} {cmp : α → α → Ordering} (v : α) : Std.RBSet α cmp

O(1). Construct a new tree with one element v.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.RBSet.foldl {σ : Sort u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : σ → α → σ) (init : σ) (t : Std.RBSet α cmp) : σ

O(n). Fold a function on the values from left to right (in increasing order).

Equations

• Std.RBSet.foldl f init t = Std.RBNode.foldl f init t.val

@[inline]

def Std.RBSet.foldr {α : Type u_1} {σ : Sort u_2} {cmp : α → α → Ordering} (f : α → σ → σ) (init : σ) (t : Std.RBSet α cmp) : σ

O(n). Fold a function on the values from right to left (in decreasing order).

Equations

• Std.RBSet.foldr f init t = Std.RBNode.foldr f t.val init

@[inline]

def Std.RBSet.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} {cmp : α → α → Ordering} [Monad m] (f : σ → α → m σ) (init : σ) (t : Std.RBSet α cmp) : m σ

O(n). Fold a monadic function on the values from left to right (in increasing order).

Equations

• Std.RBSet.foldlM f init t = Std.RBNode.foldlM f init t.val

@[inline]

def Std.RBSet.forM {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} [Monad m] (f : α → m PUnit) (t : Std.RBSet α cmp) : m PUnit

O(n). Run monadic function f on each element of the tree (in increasing order).

Equations

• Std.RBSet.forM f t = Std.RBNode.forM f t.val

instance Std.RBSet.instForInRBSet {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} : ForIn m (Std.RBSet α cmp) α

Equations

• Std.RBSet.instForInRBSet = { forIn := fun {β : Type u_1} [Monad m] (t : Std.RBSet α cmp) => Std.RBNode.forIn t.val }

instance Std.RBSet.instToStreamRBSetStream {α : Type u_1} {cmp : α → α → Ordering} : ToStream (Std.RBSet α cmp) (Std.RBNode.Stream α)

Equations

• Std.RBSet.instToStreamRBSetStream = { toStream := fun (x : Std.RBSet α cmp) => Std.RBNode.toStream x.val }

@[inline]

def Std.RBSet.isEmpty {α : Type u_1} {cmp : α → α → Ordering} : Std.RBSet α cmp → Bool

O(1). Is the tree empty?

Equations

• Std.RBSet.isEmpty x = match x with | { val := Std.RBNode.nil, property := property } => true | x => false

@[inline]

def Std.RBSet.toList {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) : List α

O(n). Convert the tree to a list in ascending order.

Equations

• Std.RBSet.toList t = Std.RBNode.toList t.val

@[inline]

def Std.RBSet.min {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) : Option α

O(log n). Returns the entry a such that a ≤ k for all keys in the RBSet.

Equations

• Std.RBSet.min t = Std.RBNode.min t.val

@[inline]

def Std.RBSet.max {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) : Option α

O(log n). Returns the entry a such that a ≥ k for all keys in the RBSet.

Equations

• Std.RBSet.max t = Std.RBNode.max t.val

instance Std.RBSet.instReprRBSet {α : Type u_1} {cmp : α → α → Ordering} [Repr α] : Repr (Std.RBSet α cmp)

Equations

• Std.RBSet.instReprRBSet = { reprPrec := fun (m : Std.RBSet α cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "RBSet.ofList " ++ repr (Std.RBSet.toList m)) prec }

@[inline]

def Std.RBSet.insert {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (v : α) : Std.RBSet α cmp

O(log n). Insert element v into the tree.

Equations

• Std.RBSet.insert t v = { val := Std.RBNode.insert cmp t.val v, property := (_ : Std.RBNode.WF cmp (Std.RBNode.insert cmp t.val v)) }

@[inline]

def Std.RBSet.erase {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) : Std.RBSet α cmp

O(log n). Remove an element from the tree using a cut function. The cut function is used to locate an element in the tree: it returns .gt if we go too high and .lt if we go too low; if it returns .eq we will remove the element. (The function cmp k for some key k is a valid cut function, but we can also use cuts that are not of this form as long as they are suitably monotonic.)

Equations

• Std.RBSet.erase t cut = { val := Std.RBNode.erase cut t.val, property := (_ : Std.RBNode.WF cmp (Std.RBNode.erase cut t.val)) }

@[inline]

def Std.RBSet.findP? {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) : Option α

O(log n). Find an element in the tree using a cut function.

Equations

• Std.RBSet.findP? t cut = Std.RBNode.find? cut t.val

@[inline]

def Std.RBSet.find? {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (x : α) : Option α

O(log n). Returns an element in the tree equivalent to x if one exists.

Equations

• Std.RBSet.find? t x = Std.RBNode.find? (cmp x) t.val

@[inline]

def Std.RBSet.findPD {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) (v₀ : α) : α

O(log n). Find an element in the tree, or return a default value v₀.

Equations

• Std.RBSet.findPD t cut v₀ = Option.getD (Std.RBSet.findP? t cut) v₀

@[inline]

def Std.RBSet.lowerBoundP? {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) : Option α

O(log n). lowerBoundP cut retrieves the largest entry comparing lt or eq under cut, if it exists.

Equations

• Std.RBSet.lowerBoundP? t cut = Std.RBNode.lowerBound? cut t.val none

@[inline]

def Std.RBSet.lowerBound? {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (k : α) : Option α

O(log n). lowerBound? k retrieves the largest entry smaller than or equal to k, if it exists.

Equations

• Std.RBSet.lowerBound? t k = Std.RBNode.lowerBound? (cmp k) t.val none

@[inline]

def Std.RBSet.containsP {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) : Bool

O(log n). Returns true if the given cut returns eq for something in the RBSet.

Equations

• Std.RBSet.containsP t cut = Option.isSome (Std.RBSet.findP? t cut)

@[inline]

def Std.RBSet.contains {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (a : α) : Bool

O(log n). Returns true if the given key a is in the RBSet.

Equations

• Std.RBSet.contains t a = Option.isSome (Std.RBSet.find? t a)

@[inline]

def Std.RBSet.ofList {α : Type u_1} (l : List α) (cmp : α → α → Ordering) : Std.RBSet α cmp

O(n log n). Build a tree from an unsorted list by inserting them one at a time.

Equations

• Std.RBSet.ofList l cmp = List.foldl (fun (r : Std.RBSet α cmp) (p : α) => Std.RBSet.insert r p) (Std.mkRBSet α cmp) l

@[inline]

def Std.RBSet.ofArray {α : Type u_1} (l : Array α) (cmp : α → α → Ordering) : Std.RBSet α cmp

O(n log n). Build a tree from an unsorted array by inserting them one at a time.

Equations

• Std.RBSet.ofArray l cmp = Array.foldl (fun (r : Std.RBSet α cmp) (p : α) => Std.RBSet.insert r p) (Std.mkRBSet α cmp) l 0

@[inline]

def Std.RBSet.all {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (p : α → Bool) : Bool

O(n). Returns true if the given predicate is true for all items in the RBSet.

Equations

• Std.RBSet.all t p = Std.RBNode.all p t.val

@[inline]

def Std.RBSet.any {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (p : α → Bool) : Bool

O(n). Returns true if the given predicate is true for any item in the RBSet.

Equations

• Std.RBSet.any t p = Std.RBNode.any p t.val

@[inline]

def Std.RBSet.all₂ {α : Type u_1} {β : Type u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} (R : α → β → Bool) (t₁ : Std.RBSet α cmpα) (t₂ : Std.RBSet β cmpβ) : Bool

Asserts that t₁ and t₂ have the same number of elements in the same order, and R holds pairwise between them. The tree structure is ignored.

Equations

• Std.RBSet.all₂ R t₁ t₂ = Std.RBNode.all₂ R t₁.val t₂.val

def Std.RBSet.EMem {α : Type u_1} {cmp : α → α → Ordering} (x : α) (t : Std.RBSet α cmp) : Prop

True if x is an element of t "exactly", i.e. up to equality, not the cmp relation.

Equations

• Std.RBSet.EMem x t = Std.RBNode.EMem x t.val

def Std.RBSet.MemP {α : Type u_1} {cmp : α → α → Ordering} (cut : α → Ordering) (t : Std.RBSet α cmp) : Prop

True if the specified cut matches at least one element of of t.

Equations

• Std.RBSet.MemP cut t = Std.RBNode.MemP cut t.val

def Std.RBSet.Mem {α : Type u_1} {cmp : α → α → Ordering} (x : α) (t : Std.RBSet α cmp) : Prop

True if x is equivalent to an element of t.

Equations

• Std.RBSet.Mem x t = Std.RBSet.MemP (cmp x) t

instance Std.RBSet.instMembershipRBSet {α : Type u_1} {cmp : α → α → Ordering} : Membership α (Std.RBSet α cmp)

Equations

• Std.RBSet.instMembershipRBSet = { mem := Std.RBSet.Mem }

def Std.RBSet.Slow.instDecidableEMem {α : Type u_1} {cmp : α → α → Ordering} {x : α} [DecidableEq α] {t : Std.RBSet α cmp} : Decidable (Std.RBSet.EMem x t)

Equations

• Std.RBSet.Slow.instDecidableEMem = inferInstanceAs (Decidable (Std.RBNode.Any (fun (x_1 : α) => x = x_1) t.val))

def Std.RBSet.Slow.instDecidableMemP {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBSet α cmp} : Decidable (Std.RBSet.MemP cut t)

Equations

• Std.RBSet.Slow.instDecidableMemP = inferInstanceAs (Decidable (Std.RBNode.Any (fun (x : α) => cut x = Ordering.eq) t.val))

def Std.RBSet.Slow.instDecidableMem {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : Std.RBSet α cmp} : Decidable (Std.RBSet.Mem x t)

Equations

• Std.RBSet.Slow.instDecidableMem = inferInstanceAs (Decidable (Std.RBNode.Any (fun (x_1 : α) => cmp x x_1 = Ordering.eq) t.val))

instance Std.RBSet.instBEqRBSet {α : Type u_1} {cmp : α → α → Ordering} [BEq α] : BEq (Std.RBSet α cmp)

Returns true if t₁ and t₂ are equal as sets (assuming cmp and == are compatible), ignoring the internal tree structure.

Equations

• Std.RBSet.instBEqRBSet = { beq := fun (a b : Std.RBSet α cmp) => Std.RBSet.all₂ (fun (x x_1 : α) => x == x_1) a b }

def Std.RBSet.size {α : Type u_1} {cmp : α → α → Ordering} (m : Std.RBSet α cmp) : Nat

O(n). The number of items in the RBSet.

Equations

• Std.RBSet.size m = Std.RBNode.size m.val

@[inline]

def Std.RBSet.min! {α : Type u_1} {cmp : α → α → Ordering} [Inhabited α] (t : Std.RBSet α cmp) : α

O(log n). Returns the minimum element of the tree, or panics if the tree is empty.

Equations

• Std.RBSet.min! t = Option.getD (Std.RBSet.min t) (panicWithPosWithDecl "Std.Data.RBMap.Basic" "Std.RBSet.min!" 755 70 "tree is empty")

@[inline]

def Std.RBSet.max! {α : Type u_1} {cmp : α → α → Ordering} [Inhabited α] (t : Std.RBSet α cmp) : α

O(log n). Returns the maximum element of the tree, or panics if the tree is empty.

Equations

• Std.RBSet.max! t = Option.getD (Std.RBSet.max t) (panicWithPosWithDecl "Std.Data.RBMap.Basic" "Std.RBSet.max!" 758 70 "tree is empty")

@[inline]

def Std.RBSet.findP! {α : Type u_1} {cmp : α → α → Ordering} [Inhabited α] (t : Std.RBSet α cmp) (cut : α → Ordering) : α

O(log n). Attempts to find the value with key k : α in t and panics if there is no such key.

Equations

• Std.RBSet.findP! t cut = Option.getD (Std.RBSet.findP? t cut) (panicWithPosWithDecl "Std.Data.RBMap.Basic" "Std.RBSet.findP!" 764 23 "key is not in the tree")

@[inline]

def Std.RBSet.find! {α : Type u_1} {cmp : α → α → Ordering} [Inhabited α] (t : Std.RBSet α cmp) (k : α) : α

O(log n). Attempts to find the value with key k : α in t and panics if there is no such key.

Equations

• Std.RBSet.find! t k = Option.getD (Std.RBSet.find? t k) (panicWithPosWithDecl "Std.Data.RBMap.Basic" "Std.RBSet.find!" 770 20 "key is not in the tree")

class Std.RBSet.ModifyWF {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) (f : α → α) : Prop

The predicate asserting that the result of modifyP is safe to construct.

• wf : Std.RBNode.WF cmp (Std.RBNode.modify cut f t.val)

  The resulting tree is well formed.

def Std.RBSet.modifyP {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) (f : α → α) [wf : Std.RBSet.ModifyWF t cut f] : Std.RBSet α cmp

O(log n). In-place replace an element found by cut. This takes the element out of the tree while f runs, so it uses the element linearly if t is unshared.

The ModifyWF assumption is required because f may change the ordering properties of the element, which would break the invariants.

Equations

• Std.RBSet.modifyP t cut f = { val := Std.RBNode.modify cut f t.val, property := (_ : Std.RBNode.WF cmp (Std.RBNode.modify cut f t.val)) }

class Std.RBSet.AlterWF {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) (f : Option α → Option α) : Prop

The predicate asserting that the result of alterP is safe to construct.

• wf : Std.RBNode.WF cmp (Std.RBNode.alter cut f t.val)

  The resulting tree is well formed.

def Std.RBSet.alterP {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (cut : α → Ordering) (f : Option α → Option α) [wf : Std.RBSet.AlterWF t cut f] : Std.RBSet α cmp

O(log n). alterP cut f t simultaneously handles inserting, erasing and replacing an element using a function f : Option α → Option α. It is passed the result of t.findP? cut and can either return none to remove the element or some a to replace/insert the element with a (which must have the same ordering properties as the original element).

The element is used linearly if t is unshared.

The AlterWF assumption is required because f may change the ordering properties of the element, which would break the invariants.

Equations

• Std.RBSet.alterP t cut f = { val := Std.RBNode.alter cut f t.val, property := (_ : Std.RBNode.WF cmp (Std.RBNode.alter cut f t.val)) }

def Std.RBSet.union {α : Type u_1} {cmp : α → α → Ordering} (t₁ : Std.RBSet α cmp) (t₂ : Std.RBSet α cmp) : Std.RBSet α cmp

O(n₂ * log (n₁ + n₂)). Merges the maps t₁ and t₂. If equal keys exist in both, the key from t₂ is preferred.

Equations

• Std.RBSet.union t₁ t₂ = Std.RBSet.foldl Std.RBSet.insert t₁ t₂

def Std.RBSet.mergeWith {α : Type u_1} {cmp : α → α → Ordering} (mergeFn : α → α → α) (t₁ : Std.RBSet α cmp) (t₂ : Std.RBSet α cmp) : Std.RBSet α cmp

O(n₂ * log (n₁ + n₂)). Merges the maps t₁ and t₂. If equal keys exist in both, then use mergeFn a₁ a₂ to produce the new merged value.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBSet.intersectWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} {cmpγ : γ → γ → Ordering} (cmp : α → β → Ordering) (mergeFn : α → β → γ) (t₁ : Std.RBSet α cmpα) (t₂ : Std.RBSet β cmpβ) : Std.RBSet γ cmpγ

O(n₁ * log (n₁ + n₂)). Intersects the maps t₁ and t₂ using mergeFn a b to produce the new value.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBSet.filter {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) (p : α → Bool) : Std.RBSet α cmp

O(n * log n). Constructs the set of all elements satisfying p.

Equations

• Std.RBSet.filter t p = Std.RBSet.foldl (fun (acc : Std.RBSet α cmp) (a : α) => bif p a then Std.RBSet.insert acc a else acc) ∅ t

def Std.RBSet.map {α : Type u_1} {cmpα : α → α → Ordering} {β : Type u_2} {cmpβ : β → β → Ordering} (t : Std.RBSet α cmpα) (f : α → β) : Std.RBSet β cmpβ

O(n * log n). Map a function on every value in the set. If the function is monotone, consider using the more efficient RBSet.mapMonotone instead.

Equations

• Std.RBSet.map t f = Std.RBSet.foldl (fun (acc : Std.RBSet β cmpβ) (a : α) => Std.RBSet.insert acc (f a)) ∅ t

def Std.RBSet.sdiff {α : Type u_1} {cmp : α → α → Ordering} (t₁ : Std.RBSet α cmp) (t₂ : Std.RBSet α cmp) : Std.RBSet α cmp

O(n₁ * (log n₁ + log n₂)). Constructs the set of all elements of t₁ that are not in t₂.

Equations

• Std.RBSet.sdiff t₁ t₂ = Std.RBSet.filter t₁ fun (x : α) => !Std.RBSet.contains t₂ x

def Std.RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v)

An RBMap is a self-balancing binary search tree, used to store a key-value map. The cmp function is the comparator that will be used for performing searches; it should satisfy the requirements of TransCmp for it to have sensible behavior.

Equations

• Std.RBMap α β cmp = Std.RBSet (α × β) (Ordering.byKey Prod.fst cmp)

@[inline]

def Std.mkRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Std.RBMap α β cmp

O(1). Construct a new empty map.

Equations

• Std.mkRBMap α β cmp = Std.mkRBSet (α × β) (Ordering.byKey Prod.fst cmp)

@[inline]

def Std.RBMap.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.RBMap α β cmp

O(1). Construct a new empty map.

Equations

• Std.RBMap.empty = Std.mkRBMap α β cmp

instance Std.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : EmptyCollection (Std.RBMap α β cmp)

Equations

• Std.instEmptyCollectionRBMap α β cmp = { emptyCollection := Std.RBMap.empty }

instance Std.instInhabitedRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Inhabited (Std.RBMap α β cmp)

Equations

• Std.instInhabitedRBMap α β cmp = { default := ∅ }

@[inline]

def Std.RBMap.single {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v : β) : Std.RBMap α β cmp

O(1). Construct a new tree with one key-value pair k, v.

Equations

• Std.RBMap.single k v = Std.RBSet.single (k, v)

@[inline]

def Std.RBMap.foldl {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) : Std.RBMap α β cmp → σ

O(n). Fold a function on the values from left to right (in increasing order).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.RBMap.foldr {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} (f : α → β → σ → σ) (init : σ) : Std.RBMap α β cmp → σ

O(n). Fold a function on the values from right to left (in decreasing order).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.RBMap.foldlM {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering} {m : Type w → Type u_1} [Monad m] (f : σ → α → β → m σ) (init : σ) : Std.RBMap α β cmp → m σ

O(n). Fold a monadic function on the values from left to right (in increasing order).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.RBMap.forM {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} [Monad m] (f : α → β → m PUnit) (t : Std.RBMap α β cmp) : m PUnit

O(n). Run monadic function f on each element of the tree (in increasing order).

Equations

• Std.RBMap.forM f t = Std.RBMap.foldlM (fun (x : PUnit) (k : α) (v : β) => f k v) PUnit.unit t

instance Std.RBMap.instForInRBMapProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForIn m (Std.RBMap α β cmp) (α × β)

Equations

• Std.RBMap.instForInRBMapProd = inferInstanceAs (ForIn m (Std.RBSet (α × β) (Ordering.byKey Prod.fst cmp)) (α × β))

instance Std.RBMap.instToStreamRBMapStreamProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ToStream (Std.RBMap α β cmp) (Std.RBNode.Stream (α × β))

Equations

• Std.RBMap.instToStreamRBMapStreamProd = inferInstanceAs (ToStream (Std.RBSet (α × β) (Ordering.byKey Prod.fst cmp)) (Std.RBNode.Stream (α × β)))

@[inline]

def Std.RBMap.keysArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : Array α

O(n). Constructs the array of keys of the map.

Equations

• Std.RBMap.keysArray t = Std.RBNode.foldl (fun (x : Array α) (x_1 : α × β) => Array.push x x_1.fst) #[] t.val

@[inline]

def Std.RBMap.keysList {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : List α

O(n). Constructs the list of keys of the map.

Equations

• Std.RBMap.keysList t = Std.RBNode.foldr (fun (x : α × β) (x_1 : List α) => x.fst :: x_1) t.val []

def Std.RBMap.Keys (α : Type u_1) (β : Type u_2) (cmp : α → α → Ordering) : Type (max u_1 u_2)

An "iterator" over the keys of the map. This is a trivial wrapper over the underlying map, but it comes with a small API to use it in a for loop or convert it to an array or list.

Equations

• Std.RBMap.Keys α β cmp = Std.RBMap α β cmp

@[inline]

def Std.RBMap.keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : Std.RBMap.Keys α β cmp

The keys of the map. This is an O(1) wrapper operation, which can be used in for loops or converted to an array or list.

Equations

• Std.RBMap.keys t = t

@[inline]

def Std.RBMap.Keys.toArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : Array α

O(n). Constructs the array of keys of the map.

Equations

• @Std.RBMap.Keys.toArray = @Std.RBMap.keysArray

@[inline]

def Std.RBMap.Keys.toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : List α

O(n). Constructs the list of keys of the map.

Equations

• @Std.RBMap.Keys.toList = @Std.RBMap.keysList

instance Std.RBMap.instCoeHeadKeysArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} : CoeHead (Std.RBMap.Keys α β cmp) (Array α)

Equations

• Std.RBMap.instCoeHeadKeysArray = { coe := Std.RBMap.keysArray }

instance Std.RBMap.instCoeHeadKeysList {α : Type u} {β : Type v} {cmp : α → α → Ordering} : CoeHead (Std.RBMap.Keys α β cmp) (List α)

Equations

• Std.RBMap.instCoeHeadKeysList = { coe := Std.RBMap.keysList }

instance Std.RBMap.instForInKeys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForIn m (Std.RBMap.Keys α β cmp) α

Equations

• One or more equations did not get rendered due to their size.

instance Std.RBMap.instForMKeys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForM m (Std.RBMap.Keys α β cmp) α

Equations

• Std.RBMap.instForMKeys = { forM := fun [Monad m] (t : Std.RBMap.Keys α β cmp) (f : α → m PUnit) => Std.RBNode.forM (fun (x : α × β) => f x.fst) t.val }

def Std.RBMap.Keys.Stream (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

The result of toStream on a Keys.

Equations

• Std.RBMap.Keys.Stream α β = Std.RBNode.Stream (α × β)

def Std.RBMap.Keys.toStream {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap.Keys α β cmp) : Std.RBMap.Keys.Stream α β

A stream over the iterator.

Equations

• Std.RBMap.Keys.toStream t = Std.RBNode.toStream t.val

def Std.RBMap.Keys.Stream.next? {α : Type u} {β : Type v} (t : Std.RBMap.Keys.Stream α β) : Option (α × Std.RBMap.Keys.Stream α β)

O(1) amortized, O(log n) worst case: Get the next element from the stream.

Equations

• Std.RBMap.Keys.Stream.next? t = match inline (Std.RBNode.Stream.next? t) with | none => none | some ((a, snd), t) => some (a, t)

instance Std.RBMap.instToStreamKeysStream {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ToStream (Std.RBMap.Keys α β cmp) (Std.RBMap.Keys.Stream α β)

Equations

• Std.RBMap.instToStreamKeysStream = { toStream := Std.RBMap.Keys.toStream }

instance Std.RBMap.instStreamStream {α : Type u} {β : Type v} : Stream (Std.RBMap.Keys.Stream α β) α

Equations

• Std.RBMap.instStreamStream = { next? := Std.RBMap.Keys.Stream.next? }

@[inline]

def Std.RBMap.valuesArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : Array β

O(n). Constructs the array of values of the map.

Equations

• Std.RBMap.valuesArray t = Std.RBNode.foldl (fun (x : Array β) (x_1 : α × β) => Array.push x x_1.snd) #[] t.val

@[inline]

def Std.RBMap.valuesList {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : List β

O(n). Constructs the list of values of the map.

Equations

• Std.RBMap.valuesList t = Std.RBNode.foldr (fun (x : α × β) (x_1 : List β) => x.snd :: x_1) t.val []

def Std.RBMap.Values (α : Type u_1) (β : Type u_2) (cmp : α → α → Ordering) : Type (max u_1 u_2)

An "iterator" over the values of the map. This is a trivial wrapper over the underlying map, but it comes with a small API to use it in a for loop or convert it to an array or list.

Equations

• Std.RBMap.Values α β cmp = Std.RBMap α β cmp

@[inline]

def Std.RBMap.values {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : Std.RBMap.Values α β cmp

The "keys" of the map. This is an O(1) wrapper operation, which can be used in for loops or converted to an array or list.

Equations

• Std.RBMap.values t = t

@[inline]

def Std.RBMap.Values.toArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : Array β

O(n). Constructs the array of values of the map.

Equations

• @Std.RBMap.Values.toArray = @Std.RBMap.valuesArray

@[inline]

def Std.RBMap.Values.toList {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) : List β

O(n). Constructs the list of values of the map.

Equations

• @Std.RBMap.Values.toList = @Std.RBMap.valuesList

instance Std.RBMap.instCoeHeadValuesArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} : CoeHead (Std.RBMap.Values α β cmp) (Array β)

Equations

• Std.RBMap.instCoeHeadValuesArray = { coe := Std.RBMap.valuesArray }

instance Std.RBMap.instCoeHeadValuesList {α : Type u} {β : Type v} {cmp : α → α → Ordering} : CoeHead (Std.RBMap.Values α β cmp) (List β)

Equations

• Std.RBMap.instCoeHeadValuesList = { coe := Std.RBMap.valuesList }

instance Std.RBMap.instForInValues {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForIn m (Std.RBMap.Values α β cmp) β

Equations

• One or more equations did not get rendered due to their size.

instance Std.RBMap.instForMValues {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} : ForM m (Std.RBMap.Values α β cmp) β

Equations

• Std.RBMap.instForMValues = { forM := fun [Monad m] (t : Std.RBMap.Values α β cmp) (f : β → m PUnit) => Std.RBNode.forM (fun (x : α × β) => f x.snd) t.val }

def Std.RBMap.Values.Stream (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

The result of toStream on a Values.

Equations

• Std.RBMap.Values.Stream α β = Std.RBNode.Stream (α × β)

def Std.RBMap.Values.toStream {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap.Values α β cmp) : Std.RBMap.Values.Stream α β

A stream over the iterator.

Equations

• Std.RBMap.Values.toStream t = Std.RBNode.toStream t.val

def Std.RBMap.Values.Stream.next? {α : Type u} {β : Type v} (t : Std.RBMap.Values.Stream α β) : Option (β × Std.RBMap.Values.Stream α β)

O(1) amortized, O(log n) worst case: Get the next element from the stream.

Equations

• Std.RBMap.Values.Stream.next? t = match inline (Std.RBNode.Stream.next? t) with | none => none | some ((fst, b), t) => some (b, t)

instance Std.RBMap.instToStreamValuesStream {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ToStream (Std.RBMap.Values α β cmp) (Std.RBMap.Values.Stream α β)

Equations

• Std.RBMap.instToStreamValuesStream = { toStream := Std.RBMap.Values.toStream }

instance Std.RBMap.instStreamStream_1 {α : Type u} {β : Type v} : Stream (Std.RBMap.Values.Stream α β) β

Equations

• Std.RBMap.instStreamStream_1 = { next? := Std.RBMap.Values.Stream.next? }

@[inline]

def Std.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.RBMap α β cmp → Bool

O(1). Is the tree empty?

Equations

• Std.RBMap.isEmpty = Std.RBSet.isEmpty

@[inline]

def Std.RBMap.toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.RBMap α β cmp → List (α × β)

O(n). Convert the tree to a list in ascending order.

Equations

• Std.RBMap.toList = Std.RBSet.toList

@[inline]

def Std.RBMap.min {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.RBMap α β cmp → Option (α × β)

O(log n). Returns the key-value pair (a, b) such that a ≤ k for all keys in the RBMap.

Equations

• Std.RBMap.min = Std.RBSet.min

@[inline]

def Std.RBMap.max {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.RBMap α β cmp → Option (α × β)

O(log n). Returns the key-value pair (a, b) such that a ≥ k for all keys in the RBMap.

Equations

• Std.RBMap.max = Std.RBSet.max

instance Std.RBMap.instReprRBMap {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Repr α] [Repr β] : Repr (Std.RBMap α β cmp)

Equations

• Std.RBMap.instReprRBMap = { reprPrec := fun (m : Std.RBMap α β cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "RBMap.ofList " ++ repr (Std.RBMap.toList m)) prec }

@[inline]

def Std.RBMap.insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) (v : β) : Std.RBMap α β cmp

O(log n). Insert key-value pair (k, v) into the tree.

Equations

• Std.RBMap.insert t k v = Std.RBSet.insert t (k, v)

@[inline]

def Std.RBMap.erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) : Std.RBMap α β cmp

O(log n). Remove an element k from the map.

Equations

• Std.RBMap.erase t k = Std.RBSet.erase t fun (x : α × β) => cmp k x.fst

@[inline]

def Std.RBMap.ofList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : Std.RBMap α β cmp

O(n log n). Build a tree from an unsorted list by inserting them one at a time.

Equations

• Std.RBMap.ofList l cmp = Std.RBSet.ofList l (Ordering.byKey Prod.fst cmp)

@[inline]

def Std.RBMap.ofArray {α : Type u} {β : Type v} (l : Array (α × β)) (cmp : α → α → Ordering) : Std.RBMap α β cmp

O(n log n). Build a tree from an unsorted array by inserting them one at a time.

Equations

• Std.RBMap.ofArray l cmp = Std.RBSet.ofArray l (Ordering.byKey Prod.fst cmp)

@[inline]

def Std.RBMap.findEntry? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) : Option (α × β)

O(log n). Find an entry in the tree with key equal to k.

Equations

• Std.RBMap.findEntry? t k = Std.RBSet.findP? t fun (x : α × β) => cmp k x.fst

@[inline]

def Std.RBMap.find? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) : Option β

O(log n). Find the value corresponding to key k.

Equations

• Std.RBMap.find? t k = Option.map (fun (x : α × β) => x.snd) (Std.RBMap.findEntry? t k)

@[inline]

def Std.RBMap.findD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) (v₀ : β) : β

O(log n). Find the value corresponding to key k, or return v₀ if it is not in the map.

Equations

• Std.RBMap.findD t k v₀ = Option.getD (Std.RBMap.find? t k) v₀

@[inline]

def Std.RBMap.lowerBound? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (k : α) : Option (α × β)

O(log n). lowerBound? k retrieves the key-value pair of the largest key smaller than or equal to k, if it exists.

Equations

• Std.RBMap.lowerBound? t k = Std.RBSet.lowerBoundP? t fun (x : α × β) => cmp k x.fst

@[inline]

def Std.RBMap.contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (a : α) : Bool

O(log n). Returns true if the given key a is in the RBMap.

Equations

• Std.RBMap.contains t a = Option.isSome (Std.RBMap.findEntry? t a)

@[inline]

def Std.RBMap.all {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (p : α → β → Bool) : Bool

O(n). Returns true if the given predicate is true for all items in the RBMap.

Equations

• Std.RBMap.all t p = Std.RBSet.all t fun (x : α × β) => match x with | (a, b) => p a b

@[inline]

def Std.RBMap.any {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (p : α → β → Bool) : Bool

O(n). Returns true if the given predicate is true for any item in the RBMap.

Equations

• Std.RBMap.any t p = Std.RBSet.any t fun (x : α × β) => match x with | (a, b) => p a b

@[inline]

def Std.RBMap.all₂ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {cmpα : α → α → Ordering} {cmpγ : γ → γ → Ordering} (R : α × β → γ × δ → Bool) (t₁ : Std.RBMap α β cmpα) (t₂ : Std.RBMap γ δ cmpγ) : Bool

Asserts that t₁ and t₂ have the same number of elements in the same order, and R holds pairwise between them. The tree structure is ignored.

Equations

• Std.RBMap.all₂ R t₁ t₂ = Std.RBSet.all₂ R t₁ t₂

@[inline]

def Std.RBMap.eqKeys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {γ : Type u_1} (t₁ : Std.RBMap α β cmp) (t₂ : Std.RBMap α γ cmp) : Bool

Asserts that t₁ and t₂ have the same set of keys (up to equality).

Equations

• Std.RBMap.eqKeys t₁ t₂ = Std.RBMap.all₂ (fun (x : α × β) (x_1 : α × γ) => decide (cmp x.fst x_1.fst = Ordering.eq)) t₁ t₂

instance Std.RBMap.instBEqRBMap {α : Type u} {β : Type v} {cmp : α → α → Ordering} [BEq α] [BEq β] : BEq (Std.RBMap α β cmp)

Returns true if t₁ and t₂ have the same keys and values (assuming cmp and == are compatible), ignoring the internal tree structure.

Equations

• Std.RBMap.instBEqRBMap = inferInstanceAs (BEq (Std.RBSet (α × β) (Ordering.byKey Prod.fst cmp)))

def Std.RBMap.size {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.RBMap α β cmp → Nat

O(n). The number of items in the RBMap.

Equations

• Std.RBMap.size = Std.RBSet.size

@[inline]

def Std.RBMap.min! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] [Inhabited β] : Std.RBMap α β cmp → α × β

O(log n). Returns the minimum element of the map, or panics if the map is empty.

Equations

• Std.RBMap.min! = Std.RBSet.min!

@[inline]

def Std.RBMap.max! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] [Inhabited β] : Std.RBMap α β cmp → α × β

O(log n). Returns the maximum element of the map, or panics if the map is empty.

Equations

• Std.RBMap.max! = Std.RBSet.max!

@[inline]

def Std.RBMap.find! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited β] (t : Std.RBMap α β cmp) (k : α) : β

Attempts to find the value with key k : α in t and panics if there is no such key.

Equations

• Std.RBMap.find! t k = Option.getD (Std.RBMap.find? t k) (panicWithPosWithDecl "Std.Data.RBMap.Basic" "Std.RBMap.find!" 1081 20 "key is not in the map")

def Std.RBMap.mergeWith {α : Type u} {β : Type v} {cmp : α → α → Ordering} (mergeFn : α → β → β → β) (t₁ : Std.RBMap α β cmp) (t₂ : Std.RBMap α β cmp) : Std.RBMap α β cmp

O(n₂ * log (n₁ + n₂)). Merges the maps t₁ and t₂, if a key a : α exists in both, then use mergeFn a b₁ b₂ to produce the new merged value.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBMap.intersectWith {α : Type u} {β : Type v} {cmp : α → α → Ordering} {γ : Type u_1} {δ : Type u_2} (mergeFn : α → β → γ → δ) (t₁ : Std.RBMap α β cmp) (t₂ : Std.RBMap α γ cmp) : Std.RBMap α δ cmp

O(n₁ * log (n₁ + n₂)). Intersects the maps t₁ and t₂ using mergeFn a b to produce the new value.

Equations

• One or more equations did not get rendered due to their size.

def Std.RBMap.filter {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.RBMap α β cmp) (p : α → β → Bool) : Std.RBMap α β cmp

O(n * log n). Constructs the set of all elements satisfying p.

Equations

• Std.RBMap.filter t p = Std.RBSet.filter t fun (x : α × β) => match x with | (a, b) => p a b

def Std.RBMap.sdiff {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t₁ : Std.RBMap α β cmp) (t₂ : Std.RBMap α β cmp) : Std.RBMap α β cmp

O(n₁ * (log n₁ + log n₂)). Constructs the set of all elements of t₁ that are not in t₂.

Equations

• Std.RBMap.sdiff t₁ t₂ = Std.RBMap.filter t₁ fun (a : α) (x : β) => !Std.RBMap.contains t₂ a

@[inline, reducible]

abbrev List.toRBMap {α : Type u_1} {β : Type u_2} (l : List (α × β)) (cmp : α → α → Ordering) : Std.RBMap α β cmp

O(n log n). Build a tree from an unsorted list by inserting them one at a time.

Equations

• List.toRBMap l cmp = Std.RBMap.ofList l cmp