Additional lemmas for Red-black trees #

source

def Std.RBNode.depth {α : Type u_1} :

Std.RBNode α → Nat

O(n). depth t is the maximum number of nodes on any path to a leaf. It is an upper bound on most tree operations.

Equations

Std.RBNode.depth Std.RBNode.nil = 0
Std.RBNode.depth (Std.RBNode.node c a v b) = max (Std.RBNode.depth a) (Std.RBNode.depth b) + 1

Instances For

source

theorem Std.RBNode.size_lt_depth {α : Type u_1} (t : Std.RBNode α) :

Std.RBNode.size t < 2 ^ Std.RBNode.depth t

source

def Std.RBNode.depthLB :

Std.RBColor → Nat → Nat

depthLB c n is the best upper bound on the depth of any balanced red-black tree with root colored c and black-height n.

Equations

Std.RBNode.depthLB x✝ x = match x✝, x with | Std.RBColor.red, n => n + 1 | Std.RBColor.black, n => n

Instances For

source

theorem Std.RBNode.depthLB_le (c : Std.RBColor) (n : Nat) :

n ≤ Std.RBNode.depthLB c n

source

def Std.RBNode.depthUB :

Std.RBColor → Nat → Nat

depthUB c n is the best upper bound on the depth of any balanced red-black tree with root colored c and black-height n.

Equations

Std.RBNode.depthUB x✝ x = match x✝, x with | Std.RBColor.red, n => 2 * n + 1 | Std.RBColor.black, n => 2 * n

Instances For

source

theorem Std.RBNode.depthUB_le (c : Std.RBColor) (n : Nat) :

Std.RBNode.depthUB c n ≤ 2 * n + 1

source

theorem Std.RBNode.depthUB_le_two_depthLB (c : Std.RBColor) (n : Nat) :

Std.RBNode.depthUB c n ≤ 2 * Std.RBNode.depthLB c n

source

theorem Std.RBNode.Balanced.depth_le {α : Type u_1} {t : Std.RBNode α} {c : Std.RBColor} {n : Nat} :

Std.RBNode.Balanced t c n → Std.RBNode.depth t ≤ Std.RBNode.depthUB c n

source

theorem Std.RBNode.Balanced.le_size {α : Type u_1} {t : Std.RBNode α} {c : Std.RBColor} {n : Nat} :

Std.RBNode.Balanced t c n → 2 ^ Std.RBNode.depthLB c n ≤ Std.RBNode.size t + 1

source

theorem Std.RBNode.Balanced.depth_bound {α : Type u_1} {t : Std.RBNode α} {c : Std.RBColor} {n : Nat} (h : Std.RBNode.Balanced t c n) :

Std.RBNode.depth t ≤ 2 * Nat.log2 (Std.RBNode.size t + 1)

source

theorem Std.RBNode.WF.depth_bound {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} (h : Std.RBNode.WF cmp t) :

Std.RBNode.depth t ≤ 2 * Nat.log2 (Std.RBNode.size t + 1)

A well formed tree has t.depth ∈ O(log t.size), that is, it is well balanced. This justifies the O(log n) bounds on most searching operations of RBSet.

source

@[simp]

theorem Std.RBNode.mem_nil {α : Type u_1} {x : α} :

¬x ∈ Std.RBNode.nil

source

@[simp]

theorem Std.RBNode.mem_node {α : Type u_1} {y : α} {c : Std.RBColor} {a : Std.RBNode α} {x : α} {b : Std.RBNode α} :

y ∈ Std.RBNode.node c a x b ↔ y = x ∨ y ∈ a ∨ y ∈ b

source

theorem Std.RBNode.All_def {α : Type u_1} {p : α → Prop} {t : Std.RBNode α} :

Std.RBNode.All p t ↔ ∀ (x : α), x ∈ t → p x

source

theorem Std.RBNode.Any_def {α : Type u_1} {p : α → Prop} {t : Std.RBNode α} :

Std.RBNode.Any p t ↔ ∃ (x : α), x ∈ t ∧ p x

source

theorem Std.RBNode.memP_def :

∀ {α : Type u_1} {cut : α → Ordering} {t : Std.RBNode α}, Std.RBNode.MemP cut t ↔ ∃ (x : α), x ∈ t ∧ cut x = Ordering.eq

source

theorem Std.RBNode.mem_def :

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

source

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

Std.RBNode.Mem cmp x t ↔ Std.RBNode.Mem cmp y t

source

theorem Std.RBNode.isOrdered_iff' {α : Type u_1} {cmp : α → α → Ordering} {L : Option α} {R : Option α} [Std.TransCmp cmp] {t : Std.RBNode α} :

Std.RBNode.isOrdered cmp t L R = true ↔ (∀ (a : α), a ∈ L → Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp a x) t) ∧ (∀ (a : α), a ∈ R → Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp x a) t) ∧ (∀ (a : α), a ∈ L → ∀ (b : α), b ∈ R → Std.RBNode.cmpLT cmp a b) ∧ Std.RBNode.Ordered cmp t

source

theorem Std.RBNode.isOrdered_iff {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t : Std.RBNode α} :

Std.RBNode.isOrdered cmp t none none = true ↔ Std.RBNode.Ordered cmp t

source

instance Std.RBNode.instDecidableOrdered {α : Type u_1} (cmp : α → α → Ordering) [Std.TransCmp cmp] (t : Std.RBNode α) :

Decidable (Std.RBNode.Ordered cmp t)

Equations

Std.RBNode.instDecidableOrdered cmp t = decidable_of_iff (Std.RBNode.isOrdered cmp t none none = true) (_ : Std.RBNode.isOrdered cmp t none none = true ↔ Std.RBNode.Ordered cmp t)

source

class Std.RBNode.IsCut {α : Sort 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 : α} [inst : 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 : α} [inst : 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.

Instances

source

theorem Std.RBNode.IsCut.lt_trans :

∀ {α : Sort u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} [inst : Std.RBNode.IsCut cmp cut] [inst : Std.TransCmp cmp], cmp x y = Ordering.lt → cut x = Ordering.lt → cut y = Ordering.lt

source

theorem Std.RBNode.IsCut.gt_trans :

∀ {α : Sort u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} [inst : Std.RBNode.IsCut cmp cut] [inst : Std.TransCmp cmp], cmp x y = Ordering.lt → cut y = Ordering.gt → cut x = Ordering.gt

source

theorem Std.RBNode.IsCut.congr :

∀ {α : Sort u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} [inst : Std.RBNode.IsCut cmp cut] [inst : Std.TransCmp cmp], cmp x y = Ordering.eq → cut x = cut y

source

class Std.RBNode.IsStrictCut {α : Sort u_1} (cmp : α → α → Ordering) (cut : α → Ordering) extends Std.RBNode.IsCut :

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 : α} [inst : Std.TransCmp cmp], cmp x y ≠ Ordering.gt → cut x = Ordering.lt → cut y = Ordering.lt
le_gt_trans : ∀ {x y : α} [inst : Std.TransCmp cmp], cmp x y ≠ Ordering.gt → cut y = Ordering.gt → cut x = Ordering.gt
exact : ∀ {x y : α} [inst : 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.

Instances

source

instance Std.RBNode.instIsStrictCut {α : Sort u_1} (cmp : α → α → Ordering) (a : α) :

Std.RBNode.IsStrictCut cmp (cmp a)

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

Equations

(_ : Std.RBNode.IsStrictCut cmp (cmp a)) = (_ : Std.RBNode.IsStrictCut cmp (cmp a))

source

theorem Std.RBNode.find?_some_eq_eq {α : Type u_1} {x : α} {cut : α → Ordering} {t : Std.RBNode α} :

x ∈ Std.RBNode.find? cut t → cut x = Ordering.eq

source

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

x ∈ Std.RBNode.find? cut t → x ∈ t

source

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

Std.RBNode.MemP cut t

source

theorem Std.RBNode.Ordered.memP_iff_find? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBNode α} [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (ht : Std.RBNode.Ordered cmp t) :

Std.RBNode.MemP cut t ↔ ∃ (x : α), Std.RBNode.find? cut t = some x

source

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

x = y

source

theorem Std.RBNode.Ordered.find?_some {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBNode α} {x : α} [Std.TransCmp cmp] [Std.RBNode.IsStrictCut cmp cut] (ht : Std.RBNode.Ordered cmp t) :

Std.RBNode.find? cut t = some x ↔ x ∈ t ∧ cut x = Ordering.eq

source

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

Std.RBNode.lowerBound? cut t lb = some x → cut x ≠ Ordering.lt

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

source

theorem Std.RBNode.lowerBound?_le {α : Type u_1} {cut : α → Ordering} {x : α} {t : Std.RBNode α} :

Std.RBNode.lowerBound? cut t none = some x → cut x ≠ Ordering.lt

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

source

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

Std.RBNode.lowerBound? cut t lb = some x → p x

source

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

Std.RBNode.lowerBound? cut t none = some x → p x

source

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

x ∈ t ∨ x ∈ lb

source

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

x ∈ t

source

theorem Std.RBNode.lowerBound?_of_some {α : Type u_1} {cut : α → Ordering} {y : α} {t : Std.RBNode α} :

∃ (x : α), Std.RBNode.lowerBound? cut t (some y) = some x

source

theorem Std.RBNode.Ordered.lowerBound?_exists {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBNode α} [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (h : Std.RBNode.Ordered cmp t) :

(∃ (x : α), Std.RBNode.lowerBound? cut t none = some x) ↔ ∃ (x : α), x ∈ t ∧ cut x ≠ Ordering.lt

source

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

Std.RBNode.lowerBound? cut t lb = some x → y ∈ t → cut x = Ordering.gt → cmp x y = Ordering.lt → cut y = Ordering.lt

source

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

cut y = Ordering.lt

A statement of the least-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).

source

theorem Std.RBNode.Ordered.memP_iff_lowerBound? {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBNode α} [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (ht : Std.RBNode.Ordered cmp t) :

Std.RBNode.MemP cut t ↔ ∃ (x : α), Std.RBNode.lowerBound? cut t none = some x ∧ cut x = Ordering.eq

source

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

cmp x y = Ordering.lt ↔ cut y = Ordering.lt

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

source

theorem Std.RBNode.foldr_cons {α : Type u_1} (t : Std.RBNode α) (l : List α) :

Std.RBNode.foldr (fun (x : α) (x_1 : List α) => x :: x_1) t l = Std.RBNode.toList t ++ l

source

@[simp]

theorem Std.RBNode.toList_nil {α : Type u_1} :

Std.RBNode.toList Std.RBNode.nil = []

source

@[simp]

theorem Std.RBNode.toList_node {α : Type u_1} {c : Std.RBColor} {a : Std.RBNode α} {x : α} {b : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.node c a x b) = Std.RBNode.toList a ++ x :: Std.RBNode.toList b

source

@[simp]

theorem Std.RBNode.mem_toList {α : Type u_1} {x : α} {t : Std.RBNode α} :

x ∈ Std.RBNode.toList t ↔ x ∈ t

source

theorem Std.RBNode.foldr_eq_foldr_toList {α : Type u_1} :

∀ {α_1 : Type u_2} {f : α → α_1 → α_1} {init : α_1} {t : Std.RBNode α}, Std.RBNode.foldr f t init = List.foldr f init (Std.RBNode.toList t)

source

theorem Std.RBNode.foldl_eq_foldl_toList {α : Type u_1} :

∀ {α_1 : Type u_2} {f : α_1 → α → α_1} {init : α_1} {t : Std.RBNode α}, Std.RBNode.foldl f init t = List.foldl f init (Std.RBNode.toList t)

source

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

Std.RBNode.forM f t = List.forM (Std.RBNode.toList t) f

source

theorem Std.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} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Std.RBNode α}, Std.RBNode.foldlM f init t = List.foldlM f init (Std.RBNode.toList t)

source

theorem Std.RBNode.forIn_visit_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} :

∀ {α_1 : Type u_1} {f : α → α_1 → m (ForInStep α_1)} {init : α_1} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Std.RBNode α}, Std.RBNode.forIn.visit f t init = ForInStep.bindList f (Std.RBNode.toList t) (ForInStep.yield init)

source

theorem Std.RBNode.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} :

∀ {α_1 : Type u_1} {init : α_1} {f : α → α_1 → m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Std.RBNode α}, forIn t init f = forIn (Std.RBNode.toList t) init f

source

theorem Std.RBNode.Stream.foldr_cons {α : Type u_1} (t : Std.RBNode.Stream α) (l : List α) :

Std.RBNode.Stream.foldr (fun (x : α) (x_1 : List α) => x :: x_1) t l = Std.RBNode.Stream.toList t ++ l

source

@[simp]

theorem Std.RBNode.Stream.toList_nil {α : Type u_1} :

Std.RBNode.Stream.toList Std.RBNode.Stream.nil = []

source

@[simp]

theorem Std.RBNode.Stream.toList_cons {α : Type u_1} {x : α} {r : Std.RBNode α} {s : Std.RBNode.Stream α} :

Std.RBNode.Stream.toList (Std.RBNode.Stream.cons x r s) = x :: Std.RBNode.toList r ++ Std.RBNode.Stream.toList s

source

theorem Std.RBNode.Stream.foldr_eq_foldr_toList {α : Type u_1} :

∀ {α_1 : Type u_2} {f : α → α_1 → α_1} {init : α_1} {s : Std.RBNode.Stream α}, Std.RBNode.Stream.foldr f s init = List.foldr f init (Std.RBNode.Stream.toList s)

source

theorem Std.RBNode.Stream.foldl_eq_foldl_toList {α : Type u_1} :

∀ {α_1 : Type u_2} {f : α_1 → α → α_1} {init : α_1} {t : Std.RBNode.Stream α}, Std.RBNode.Stream.foldl f init t = List.foldl f init (Std.RBNode.Stream.toList t)

source

theorem Std.RBNode.Stream.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} :

∀ {α_1 : Type u_1} {init : α_1} {f : α → α_1 → m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Std.RBNode α}, forIn t init f = forIn (Std.RBNode.toList t) init f

source

theorem Std.RBNode.toStream_toList' {α : Type u_1} {t : Std.RBNode α} {s : Std.RBNode.Stream α} :

Std.RBNode.Stream.toList (Std.RBNode.toStream t s) = Std.RBNode.toList t ++ Std.RBNode.Stream.toList s

source

@[simp]

theorem Std.RBNode.toStream_toList {α : Type u_1} {t : Std.RBNode α} :

Std.RBNode.Stream.toList (Std.RBNode.toStream t Std.RBNode.Stream.nil) = Std.RBNode.toList t

source

theorem Std.RBNode.Stream.next?_toList {α : Type u_1} {s : Std.RBNode.Stream α} :

Option.map (fun (x : α × Std.RBNode.Stream α) => match x with | (a, b) => (a, Std.RBNode.Stream.toList b)) (Std.RBNode.Stream.next? s) = List.next? (Std.RBNode.Stream.toList s)

source

theorem Std.RBNode.ordered_iff {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} :

Std.RBNode.Ordered cmp t ↔ List.Pairwise (Std.RBNode.cmpLT cmp) (Std.RBNode.toList t)

source

theorem Std.RBNode.Ordered.toList_sorted {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} :

Std.RBNode.Ordered cmp t → List.Pairwise (Std.RBNode.cmpLT cmp) (Std.RBNode.toList t)

source

@[simp]

theorem Std.RBNode.setBlack_toList {α : Type u_1} {t : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.setBlack t) = Std.RBNode.toList t

source

@[simp]

theorem Std.RBNode.setRed_toList {α : Type u_1} {t : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.setRed t) = Std.RBNode.toList t

source

@[simp]

theorem Std.RBNode.balance1_toList {α : Type u_1} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.balance1 l v r) = Std.RBNode.toList l ++ v :: Std.RBNode.toList r

source

@[simp]

theorem Std.RBNode.balance2_toList {α : Type u_1} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.balance2 l v r) = Std.RBNode.toList l ++ v :: Std.RBNode.toList r

source

@[simp]

theorem Std.RBNode.balLeft_toList {α : Type u_1} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.balLeft l v r) = Std.RBNode.toList l ++ v :: Std.RBNode.toList r

source

@[simp]

theorem Std.RBNode.balRight_toList {α : Type u_1} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} :

Std.RBNode.toList (Std.RBNode.balRight l v r) = Std.RBNode.toList l ++ v :: Std.RBNode.toList r

source

theorem Std.RBNode.size_eq {α : Type u_1} {t : Std.RBNode α} :

Std.RBNode.size t = List.length (Std.RBNode.toList t)

source

def Std.RBNode.Path.listL {α : Type u_1} :

Std.RBNode.Path α → List α

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

Equations

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

Instances For

source

def Std.RBNode.Path.listR {α : Type u_1} :

Std.RBNode.Path α → List α

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

Equations

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

Instances For

source

@[inline, reducible]

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

List α

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

Equations

Std.RBNode.Path.withList p l = Std.RBNode.Path.listL p ++ l ++ Std.RBNode.Path.listR p

Instances For

source

theorem Std.RBNode.Path.rootOrdered_iff {α : Type u_1} {cmp : α → α → Ordering} {v : α} {p : Std.RBNode.Path α} (hp : Std.RBNode.Path.Ordered cmp p) :

Std.RBNode.Path.RootOrdered cmp p v ↔ (∀ (a : α), a ∈ Std.RBNode.Path.listL p → Std.RBNode.cmpLT cmp a v) ∧ ∀ (a : α), a ∈ Std.RBNode.Path.listR p → Std.RBNode.cmpLT cmp v a

source

theorem Std.RBNode.Path.ordered_iff {α : Type u_1} {cmp : α → α → Ordering} {p : Std.RBNode.Path α} :

Std.RBNode.Path.Ordered cmp p ↔ List.Pairwise (Std.RBNode.cmpLT cmp) (Std.RBNode.Path.listL p) ∧ List.Pairwise (Std.RBNode.cmpLT cmp) (Std.RBNode.Path.listR p) ∧ ∀ (x : α), x ∈ Std.RBNode.Path.listL p → ∀ (y : α), y ∈ Std.RBNode.Path.listR p → Std.RBNode.cmpLT cmp x y

source

@[simp]

theorem Std.RBNode.Path.fill_toList {α : Type u_1} {t : Std.RBNode α} {p : Std.RBNode.Path α} :

Std.RBNode.toList (Std.RBNode.Path.fill p t) = Std.RBNode.Path.withList p (Std.RBNode.toList t)

source

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

Std.RBNode.Path.withList p' (Std.RBNode.toList t') = Std.RBNode.toList t

source

@[simp]

theorem Std.RBNode.Path.ins_toList {α : Type u_1} {t : Std.RBNode α} {p : Std.RBNode.Path α} :

Std.RBNode.toList (Std.RBNode.Path.ins p t) = Std.RBNode.Path.withList p (Std.RBNode.toList t)

source

@[simp]

theorem Std.RBNode.Path.insertNew_toList {α : Type u_1} {v : α} {p : Std.RBNode.Path α} :

Std.RBNode.toList (Std.RBNode.Path.insertNew p v) = Std.RBNode.Path.withList p [v]

source

theorem Std.RBNode.Path.insert_toList {α : Type u_1} {t : Std.RBNode α} {v : α} {p : Std.RBNode.Path α} :

Std.RBNode.toList (Std.RBNode.Path.insert p t v) = Std.RBNode.Path.withList p (Std.RBNode.toList (Std.RBNode.setRoot v t))

source

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

Std.RBNode.toList (Std.RBNode.insert cmp t v) = Std.RBNode.Path.withList p (Std.RBNode.toList (Std.RBNode.setRoot v t'))

source

theorem Std.RBNode.insert_toList_zoom_nil {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : α → α → Ordering} {p : Std.RBNode.Path α} {v : α} {t : Std.RBNode α} (ht : Std.RBNode.Balanced t c n) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.nil, p)) :

Std.RBNode.toList (Std.RBNode.insert cmp t v) = Std.RBNode.Path.withList p [v]

source

theorem Std.RBNode.exists_insert_toList_zoom_nil {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : α → α → Ordering} {p : Std.RBNode.Path α} {v : α} {t : Std.RBNode α} (ht : Std.RBNode.Balanced t c n) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.nil, p)) :

∃ (L : List α), ∃ (R : List α), Std.RBNode.toList t = L ++ R ∧ Std.RBNode.toList (Std.RBNode.insert cmp t v) = L ++ v :: R

source

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

Std.RBNode.toList (Std.RBNode.insert cmp t v) = Std.RBNode.Path.withList p (Std.RBNode.toList (Std.RBNode.node c l v r))

source

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

∃ (L : List α), ∃ (R : List α), Std.RBNode.toList t = L ++ v' :: R ∧ Std.RBNode.toList (Std.RBNode.insert cmp t v) = L ++ v :: R

source

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

v ∈ Std.RBNode.insert cmp t v

source

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

v' ∈ Std.RBNode.insert cmp t v ∨ cmp v v' = Ordering.eq

source

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

∃ (x : α), Std.RBNode.find? cut (Std.RBNode.insert cmp t v) = some x

source

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

Std.RBNode.find? cut (Std.RBNode.insert cmp t v) = some v

source

theorem Std.RBNode.mem_insert {α : Type u_1} {cmp : α → α → Ordering} {c : Std.RBColor} {n : Nat} {v' : α} {v : α} [Std.TransCmp cmp] {t : Std.RBNode α} (ht : Std.RBNode.Balanced t c n) (ht₂ : Std.RBNode.Ordered cmp t) :

v' ∈ Std.RBNode.insert cmp t v ↔ v' ∈ t ∧ Std.RBNode.find? (cmp v) t ≠ some v' ∨ v' = v

source

@[simp]

theorem Std.RBSet.val_toList {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBSet α cmp} :

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

source

@[simp]

theorem Std.RBSet.mkRBSet_eq {α : Type u_1} {cmp : α → α → Ordering} :

Std.mkRBSet α cmp = ∅

source

@[simp]

theorem Std.RBSet.empty_eq {α : Type u_1} {cmp : α → α → Ordering} :

Std.RBSet.empty = ∅

source

@[simp]

theorem Std.RBSet.default_eq {α : Type u_1} {cmp : α → α → Ordering} :

default = ∅

source

@[simp]

theorem Std.RBSet.empty_toList {α : Type u_1} {cmp : α → α → Ordering} :

Std.RBSet.toList ∅ = []

source

@[simp]

theorem Std.RBSet.single_toList {α : Type u_1} {cmp : α → α → Ordering} {a : α} :

Std.RBSet.toList (Std.RBSet.single a) = [a]

source

theorem Std.RBSet.mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : Std.RBSet α cmp} :

x ∈ Std.RBSet.toList t ↔ x ∈ t.val

source

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

x ∈ t ↔ y ∈ t

source

theorem Std.RBSet.mem_iff_mem_toList {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : Std.RBSet α cmp} :

x ∈ t ↔ ∃ (y : α), y ∈ Std.RBSet.toList t ∧ cmp x y = Ordering.eq

source

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

x ∈ t

source

theorem Std.RBSet.foldl_eq_foldl_toList {α : Type u_1} {cmp : α → α → Ordering} :

∀ {α_1 : Type u_2} {f : α_1 → α → α_1} {init : α_1} {t : Std.RBSet α cmp}, Std.RBSet.foldl f init t = List.foldl f init (Std.RBSet.toList t)

source

theorem Std.RBSet.foldr_eq_foldr_toList {α : Type u_1} {cmp : α → α → Ordering} :

∀ {α_1 : Type u_2} {f : α → α_1 → α_1} {init : α_1} {t : Std.RBSet α cmp}, Std.RBSet.foldr f init t = List.foldr f init (Std.RBSet.toList t)

source

theorem Std.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} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Std.RBSet α cmp}, Std.RBSet.foldlM f init t = List.foldlM f init (Std.RBSet.toList t)

source

theorem Std.RBSet.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} :

∀ {α_1 : Type u_1} {init : α_1} {f : α → α_1 → m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Std.RBSet α cmp}, forIn t init f = forIn (Std.RBSet.toList t) init f

source

theorem Std.RBSet.toStream_eq {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBSet α cmp} :

toStream t = Std.RBNode.toStream t.val Std.RBNode.Stream.nil

source

@[simp]

theorem Std.RBSet.toStream_toList {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBSet α cmp} :

Std.RBNode.Stream.toList (toStream t) = Std.RBSet.toList t

source

theorem Std.RBSet.toList_sorted {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBSet α cmp} :

List.Pairwise (Std.RBNode.cmpLT cmp) (Std.RBSet.toList t)

source

theorem Std.RBSet.find?_some_eq_eq {α : Type u_1} {cmp : α → α → Ordering} {x : α} {y : α} {t : Std.RBSet α cmp} :

Std.RBSet.find? t x = some y → cmp x y = Ordering.eq

source

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

y ∈ Std.RBSet.toList t

source

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

x ∈ t

source

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

x = y

source

theorem Std.RBSet.find?_some {α : Type u_1} {cmp : α → α → Ordering} {x : α} {y : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :

Std.RBSet.find? t x = some y ↔ y ∈ Std.RBSet.toList t ∧ cmp x y = Ordering.eq

source

theorem Std.RBSet.mem_iff_find? {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :

x ∈ t ↔ ∃ (y : α), Std.RBSet.find? t x = some y

source

@[simp]

theorem Std.RBSet.contains_iff {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :

Std.RBSet.contains t x = true ↔ x ∈ t

source

instance Std.RBSet.instDecidableMemRBSetInstMembershipRBSet {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :

Decidable (x ∈ t)

Equations

Std.RBSet.instDecidableMemRBSetInstMembershipRBSet = decidable_of_iff (Std.RBSet.contains t x = true) (_ : Std.RBSet.contains t x = true ↔ x ∈ t)

source

theorem Std.RBSet.size_eq {α : Type u_1} {cmp : α → α → Ordering} (t : Std.RBSet α cmp) :

Std.RBSet.size t = List.length (Std.RBSet.toList t)

source

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

v ∈ Std.RBSet.toList (Std.RBSet.insert t v)

source

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

v ∈ Std.RBSet.insert t v

source

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

v' ∈ Std.RBSet.insert t v

source

theorem Std.RBSet.mem_toList_insert_of_mem {α : Type u_1} {cmp : α → α → Ordering} {v' : α} (v : α) {t : Std.RBSet α cmp} (h : v' ∈ Std.RBSet.toList t) :

v' ∈ Std.RBSet.toList (Std.RBSet.insert t v) ∨ cmp v v' = Ordering.eq

source

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

v' ∈ Std.RBSet.insert t v

source

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

v' ∈ Std.RBSet.insert t v

source

theorem Std.RBSet.mem_toList_insert {α : Type u_1} {cmp : α → α → Ordering} {v' : α} {v : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :

v' ∈ Std.RBSet.toList (Std.RBSet.insert t v) ↔ v' ∈ Std.RBSet.toList t ∧ Std.RBSet.find? t v ≠ some v' ∨ v' = v

source

theorem Std.RBSet.mem_insert {α : Type u_1} {cmp : α → α → Ordering} {v' : α} {v : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :

v' ∈ Std.RBSet.insert t v ↔ v' ∈ t ∨ cmp v v' = Ordering.eq

source

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

Std.RBSet.find? t v₁ = Std.RBSet.find? t v₂

source

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

Std.RBSet.find? (Std.RBSet.insert t v) v' = some v

source

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

Std.RBSet.find? (Std.RBSet.insert t v) v' = Std.RBSet.find? t v'

source

theorem Std.RBSet.find?_insert {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.RBSet α cmp) (v : α) (v' : α) :

Std.RBSet.find? (Std.RBSet.insert t v) v' = if cmp v' v = Ordering.eq then some v else Std.RBSet.find? t v'