Verification of Ordnode

This file uses the invariants defined in Mathlib/Data/Ordmap/Invariants.lean to construct Ordset α, a wrapper around Ordnode α which includes the correctness invariant of the type. It exposes parallel operations like insert as functions on Ordset that do the same thing but bundle the correctness proofs.

The advantage is that it is possible to, for example, prove that the result of find on insert will actually find the element, while Ordnode cannot guarantee this if the input tree did not satisfy the type invariants.

Main definitions

• Ordnode.Valid: The validity predicate for an Ordnode subtree.
• Ordset α: A well formed set of values of type α.

Implementation notes

Because the Ordnode file was ported from Haskell, the correctness invariants of some of the functions have not been spelled out, and some theorems like Ordnode.Valid'.balanceL_aux show very intricate assumptions on the sizes, which may need to be revised if it turns out some operations violate these assumptions, because there is a decent amount of slop in the actual data structure invariants, so the theorem will go through with multiple choices of assumption.

structure Ordnode.Valid' {α : Type u_1} [Preorder α] (lo : WithBot α) (t : Ordnode α) (hi : WithTop α) : Prop

The validity predicate for an Ordnode subtree. This asserts that the size fields are correct, the tree is balanced, and the elements of the tree are organized according to the ordering. This version of Valid also puts all elements in the tree in the interval (lo, hi).

• ord : t.Bounded lo hi
• sz : t.Sized
• bal : t.Balanced

def Ordnode.Valid {α : Type u_1} [Preorder α] (t : Ordnode α) : Prop

The validity predicate for an Ordnode subtree. This asserts that the size fields are correct, the tree is balanced, and the elements of the tree are organized according to the ordering.

Equations

• t.Valid = Ordnode.Valid' ⊥ t ⊤

theorem Ordnode.Valid'.mono_left {α : Type u_1} [Preorder α] {x y : α} (xy : x ≤ y) {t : Ordnode α} {o : WithTop α} (h : Valid' (↑y) t o) : Valid' (↑x) t o

theorem Ordnode.Valid'.mono_right {α : Type u_1} [Preorder α] {x y : α} (xy : x ≤ y) {t : Ordnode α} {o : WithBot α} (h : Valid' o t ↑x) : Valid' o t ↑y

theorem Ordnode.Valid'.trans_left {α : Type u_1} [Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (h : t₁.Bounded o₁ ↑x) (H : Valid' (↑x) t₂ o₂) : Valid' o₁ t₂ o₂

theorem Ordnode.Valid'.trans_right {α : Type u_1} [Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ t₁ ↑x) (h : t₂.Bounded (↑x) o₂) : Valid' o₁ t₁ o₂

theorem Ordnode.Valid'.of_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ t o₂) (h₁ : nil.Bounded o₁ ↑x) (h₂ : All (fun (x_1 : α) => x_1 < x) t) : Valid' o₁ t ↑x

theorem Ordnode.Valid'.of_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ t o₂) (h₁ : nil.Bounded (↑x) o₂) (h₂ : All (fun (x_1 : α) => x_1 > x) t) : Valid' (↑x) t o₂

theorem Ordnode.Valid'.valid {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (h : Valid' o₁ t o₂) : t.Valid

theorem Ordnode.valid'_nil {α : Type u_1} [Preorder α] {o₁ : WithBot α} {o₂ : WithTop α} (h : nil.Bounded o₁ o₂) : Valid' o₁ nil o₂

theorem Ordnode.valid_nil {α : Type u_1} [Preorder α] : nil.Valid

theorem Ordnode.Valid'.node {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H : BalancedSz l.size r.size) (hs : s = l.size + r.size + 1) : Valid' o₁ (Ordnode.node s l x r) o₂

theorem Ordnode.Valid'.dual {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Valid' o₁ t o₂ → Valid' o₂ t.dual o₁

theorem Ordnode.Valid'.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Valid' o₁ t o₂ ↔ Valid' o₂ t.dual o₁

theorem Ordnode.Valid.dual {α : Type u_1} [Preorder α] {t : Ordnode α} : t.Valid → t.dual.Valid

theorem Ordnode.Valid.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} : t.Valid ↔ t.dual.Valid

theorem Ordnode.Valid'.left {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ (Ordnode.node s l x r) o₂) : Valid' o₁ l ↑x

theorem Ordnode.Valid'.right {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ (Ordnode.node s l x r) o₂) : Valid' (↑x) r o₂

theorem Ordnode.Valid.left {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : (node s l x r).Valid) : l.Valid

theorem Ordnode.Valid.right {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : (node s l x r).Valid) : r.Valid

theorem Ordnode.Valid.size_eq {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : (node s l x r).Valid) : (node s l x r).size = l.size + r.size + 1

theorem Ordnode.Valid'.node' {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H : BalancedSz l.size r.size) : Valid' o₁ (l.node' x r) o₂

theorem Ordnode.valid'_singleton {α : Type u_1} [Preorder α] {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (h₁ : nil.Bounded o₁ ↑x) (h₂ : nil.Bounded (↑x) o₂) : Valid' o₁ {x} o₂

theorem Ordnode.valid_singleton {α : Type u_1} [Preorder α] {x : α} : {x}.Valid

theorem Ordnode.Valid'.node3L {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hm : Valid' (↑x) m ↑y) (hr : Valid' (↑y) r o₂) (H1 : BalancedSz l.size m.size) (H2 : BalancedSz (l.size + m.size + 1) r.size) : Valid' o₁ (l.node3L x m y r) o₂

theorem Ordnode.Valid'.node3R {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hm : Valid' (↑x) m ↑y) (hr : Valid' (↑y) r o₂) (H1 : BalancedSz l.size (m.size + r.size + 1)) (H2 : BalancedSz m.size r.size) : Valid' o₁ (l.node3R x m y r) o₂

theorem Ordnode.Valid'.node4L_lemma₁ {a b c d : ℕ} (lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9) (mr₂ : b + c + 1 ≤ 3 * d) (mm₁ : b ≤ 3 * c) : b < 3 * a + 1

theorem Ordnode.Valid'.node4L_lemma₂ {b c d : ℕ} (mr₂ : b + c + 1 ≤ 3 * d) : c ≤ 3 * d

theorem Ordnode.Valid'.node4L_lemma₃ {b c d : ℕ} (mr₁ : 2 * d ≤ b + c + 1) (mm₁ : b ≤ 3 * c) : d ≤ 3 * c

theorem Ordnode.Valid'.node4L_lemma₄ {a b c d : ℕ} (lr₁ : 3 * a ≤ b + c + 1 + d) (mr₂ : b + c + 1 ≤ 3 * d) (mm₁ : b ≤ 3 * c) : a + b + 1 ≤ 3 * (c + d + 1)

theorem Ordnode.Valid'.node4L_lemma₅ {a b c d : ℕ} (lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9) (mr₁ : 2 * d ≤ b + c + 1) (mm₂ : c ≤ 3 * b) : c + d + 1 ≤ 3 * (a + b + 1)

theorem Ordnode.Valid'.node4L {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hm : Valid' (↑x) m ↑y) (hr : Valid' (↑y) r o₂) (Hm : 0 < m.size) (H : l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨ 0 < l.size ∧ ratio * r.size ≤ m.size ∧ delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ delta * r.size) : Valid' o₁ (l.node4L x m y r) o₂

theorem Ordnode.Valid'.rotateL_lemma₁ {a b c : ℕ} (H2 : 3 * a ≤ b + c) (hb₂ : c ≤ 3 * b) : a ≤ 3 * b

theorem Ordnode.Valid'.rotateL_lemma₂ {a b c : ℕ} (H3 : 2 * (b + c) ≤ 9 * a + 3) (h : b < 2 * c) : b < 3 * a + 1

theorem Ordnode.Valid'.rotateL_lemma₃ {a b c : ℕ} (H2 : 3 * a ≤ b + c) (h : b < 2 * c) : a + b < 3 * c

theorem Ordnode.Valid'.rotateL_lemma₄ {a b : ℕ} (H3 : 2 * b ≤ 9 * a + 3) : 3 * b ≤ 16 * a + 9

theorem Ordnode.Valid'.rotateL {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H1 : ¬l.size + r.size ≤ 1) (H2 : delta * l.size < r.size) (H3 : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3) : Valid' o₁ (l.rotateL x r) o₂

theorem Ordnode.Valid'.rotateR {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H1 : ¬l.size + r.size ≤ 1) (H2 : delta * r.size < l.size) (H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3) : Valid' o₁ (l.rotateR x r) o₂

theorem Ordnode.Valid'.balance'_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3) (H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3) : Valid' o₁ (l.balance' x r) o₂

theorem Ordnode.Valid'.balance'_lemma {α : Type u_2} {l : Ordnode α} {l' : ℕ} {r : Ordnode α} {r' : ℕ} (H1 : BalancedSz l' r') (H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l') : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

theorem Ordnode.Valid'.balance' {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H : ∃ (l' : ℕ) (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')) : Valid' o₁ (l.balance' x r) o₂

theorem Ordnode.Valid'.balance {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H : ∃ (l' : ℕ) (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')) : Valid' o₁ (l.balance x r) o₂

theorem Ordnode.Valid'.balanceL_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H₁ : l.size = 0 → r.size ≤ 1) (H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size) (H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3) : Valid' o₁ (l.balanceL x r) o₂

theorem Ordnode.Valid'.balanceL {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r') : Valid' o₁ (l.balanceL x r) o₂

theorem Ordnode.Valid'.balanceR_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H₁ : r.size = 0 → l.size ≤ 1) (H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size) (H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3) : Valid' o₁ (l.balanceR x r) o₂

theorem Ordnode.Valid'.balanceR {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) (H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r') : Valid' o₁ (l.balanceR x r) o₂

theorem Ordnode.Valid'.eraseMax_aux {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ (Ordnode.node s l x r) o₂) : Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1

theorem Ordnode.Valid'.eraseMin_aux {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Valid' o₁ (Ordnode.node s l x r) o₂) : Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

theorem Ordnode.eraseMin.valid {α : Type u_1} [Preorder α] {t : Ordnode α} : t.Valid → t.eraseMin.Valid

theorem Ordnode.eraseMax.valid {α : Type u_1} [Preorder α] {t : Ordnode α} (h : t.Valid) : t.eraseMax.Valid

theorem Ordnode.Valid'.glue_aux {α : Type u_1} [Preorder α] {l r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l o₂) (hr : Valid' o₁ r o₂) (sep : All (fun (x : α) => All (fun (y : α) => x < y) r) l) (bal : BalancedSz l.size r.size) : Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size

theorem Ordnode.Valid'.glue {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l ↑x) (hr : Valid' (↑x) r o₂) : BalancedSz l.size r.size → Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size

theorem Ordnode.Valid'.merge_lemma {a b c : ℕ} (h₁ : 3 * a < b + c + 1) (h₂ : b ≤ 3 * c) : 2 * (a + b) ≤ 9 * c + 5

theorem Ordnode.Valid'.merge_aux₁ {α : Type u_1} [Preorder α] {o₁ : WithBot α} {o₂ : WithTop α} {ls : ℕ} {ll : Ordnode α} {lx : α} {lr : Ordnode α} {rs : ℕ} {rl : Ordnode α} {rx : α} {rr t : Ordnode α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂) (h : delta * ls < rs) (v : Valid' o₁ t ↑rx) (e : t.size = ls + rl.size) : Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

theorem Ordnode.Valid'.merge_aux {α : Type u_1} [Preorder α] {l r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ l o₂) (hr : Valid' o₁ r o₂) (sep : All (fun (x : α) => All (fun (y : α) => x < y) r) l) : Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size

theorem Ordnode.Valid.merge {α : Type u_1} [Preorder α] {l r : Ordnode α} (hl : l.Valid) (hr : r.Valid) (sep : All (fun (x : α) => All (fun (y : α) => x < y) r) l) : (l.merge r).Valid

theorem Ordnode.insertWith.valid_aux {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (f : α → α) (x : α) (hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Valid' o₁ t o₂ → nil.Bounded o₁ ↑x → nil.Bounded (↑x) o₂ → Valid' o₁ (insertWith f x t) o₂ ∧ Raised t.size (insertWith f x t).size

theorem Ordnode.insertWith.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (f : α → α) (x : α) (hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) {t : Ordnode α} (h : t.Valid) : (insertWith f x t).Valid

theorem Ordnode.insert_eq_insertWith {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (t : Ordnode α) : Ordnode.insert x t = insertWith (fun (x_1 : α) => x) x t

theorem Ordnode.insert.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (x : α) {t : Ordnode α} (h : t.Valid) : (Ordnode.insert x t).Valid

theorem Ordnode.insert'_eq_insertWith {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (t : Ordnode α) : insert' x t = insertWith id x t

theorem Ordnode.insert'.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (x : α) {t : Ordnode α} (h : t.Valid) : (insert' x t).Valid

theorem Ordnode.Valid'.map_aux {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {f : α → β} (f_strict_mono : StrictMono f) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t a₂) : Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.size

theorem Ordnode.map.valid {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {f : α → β} (f_strict_mono : StrictMono f) {t : Ordnode α} (h : t.Valid) : (map f t).Valid

theorem Ordnode.Valid'.erase_aux {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t a₂) : Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size

theorem Ordnode.erase.valid {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) {t : Ordnode α} (h : t.Valid) : (erase x t).Valid

theorem Ordnode.size_erase_of_mem {α : Type u_1} [Preorder α] [DecidableLE α] {x : α} {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t a₂) (h_mem : x ∈ t) : (erase x t).size = t.size - 1

def Ordset (α : Type u_2) [Preorder α] : Type u_2

An Ordset α is a finite set of values, represented as a tree. The operations on this type maintain that the tree is balanced and correctly stores subtree sizes at each level. The correctness property of the tree is baked into the type, so all operations on this type are correct by construction.

Equations

• Ordset α = { t : Ordnode α // t.Valid }

def Ordset.nil {α : Type u_1} [Preorder α] : Ordset α

O(1). The empty set.

Equations

• Ordset.nil = ⟨Ordnode.nil, ⋯⟩

def Ordset.size {α : Type u_1} [Preorder α] (s : Ordset α) : ℕ

O(1). Get the size of the set.

Equations

• s.size = (↑s).size

def Ordset.singleton {α : Type u_1} [Preorder α] (a : α) : Ordset α

O(1). Construct a singleton set containing value a.

Equations

• Ordset.singleton a = ⟨{a}, ⋯⟩

instance Ordset.instEmptyCollection {α : Type u_1} [Preorder α] : EmptyCollection (Ordset α)

Equations

• Ordset.instEmptyCollection = { emptyCollection := Ordset.nil }

instance Ordset.instInhabited {α : Type u_1} [Preorder α] : Inhabited (Ordset α)

Equations

• Ordset.instInhabited = { default := Ordset.nil }

instance Ordset.instSingleton {α : Type u_1} [Preorder α] : Singleton α (Ordset α)

Equations

• Ordset.instSingleton = { singleton := Ordset.singleton }

def Ordset.Empty {α : Type u_1} [Preorder α] (s : Ordset α) : Prop

O(1). Is the set empty?

Equations

• s.Empty = (s = ∅)

theorem Ordset.empty_iff {α : Type u_1} [Preorder α] {s : Ordset α} : s = ∅ ↔ (↑s).empty = true

instance Ordset.Empty.instDecidablePred {α : Type u_1} [Preorder α] : DecidablePred Empty

Equations

• Ordset.Empty.instDecidablePred x✝ = decidable_of_iff' ((↑x✝).empty = true) ⋯

def Ordset.insert {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (x : α) (s : Ordset α) : Ordset α

O(log n). Insert an element into the set, preserving balance and the BST property. If an equivalent element is already in the set, this replaces it.

Equations

• Ordset.insert x s = ⟨Ordnode.insert x ↑s, ⋯⟩

instance Ordset.instInsert {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] : Insert α (Ordset α)

Equations

• Ordset.instInsert = { insert := Ordset.insert }

def Ordset.insert' {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (x : α) (s : Ordset α) : Ordset α

O(log n). Insert an element into the set, preserving balance and the BST property. If an equivalent element is already in the set, the set is returned as is.

Equations

• Ordset.insert' x s = ⟨Ordnode.insert' x ↑s, ⋯⟩

def Ordset.mem {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) : Bool

O(log n). Does the set contain the element x? That is, is there an element that is equivalent to x in the order?

Equations

• Ordset.mem x s = decide (x ∈ ↑s)

def Ordset.find {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) : Option α

O(log n). Retrieve an element in the set that is equivalent to x in the order, if it exists.

Equations

• Ordset.find x s = Ordnode.find x ↑s

instance Ordset.instMembership {α : Type u_1} [Preorder α] [DecidableLE α] : Membership α (Ordset α)

Equations

• Ordset.instMembership = { mem := fun (s : Ordset α) (x : α) => Ordset.mem x s = true }

instance Ordset.mem.decidable {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) : Decidable (x ∈ s)

Equations

• Ordset.mem.decidable x s = instDecidableEqBool (Ordset.mem x s) true

theorem Ordset.pos_size_of_mem {α : Type u_1} [Preorder α] [DecidableLE α] {x : α} {t : Ordset α} (h_mem : x ∈ t) : 0 < t.size

def Ordset.erase {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) : Ordset α

O(log n). Remove an element from the set equivalent to x. Does nothing if there is no such element.

Equations

• Ordset.erase x s = ⟨Ordnode.erase x ↑s, ⋯⟩

def Ordset.map {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] (f : α → β) (f_strict_mono : StrictMono f) (s : Ordset α) : Ordset β

O(n). Map a function across a tree, without changing the structure.

Equations

• Ordset.map f f_strict_mono s = ⟨Ordnode.map f ↑s, ⋯⟩