Documentation

Mathlib.Data.Ordmap.Ordset

Verification of Ordnode #

This file uses the invariants defined in Mathlib.Data.Ordmap.Invariants 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 #

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 α) :

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).

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

    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
    Instances For
      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₂) :
      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 α] :
      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.Validt.dual.Valid
      theorem Ordnode.Valid.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} :
      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) :
      theorem Ordnode.Valid.right {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (H : (node s l x 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 : α} :
      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 = 0r.size 1) (H₂ : 1 l.size1 r.sizer.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 = 0l.size 1) (H₂ : 1 r.size1 l.sizel.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 α} :
      theorem Ordnode.eraseMax.valid {α : Type u_1} [Preorder α] {t : Ordnode α} (h : t.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.sizeValid' 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 xx f y f y x) {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
      Valid' o₁ t o₂nil.Bounded o₁ xnil.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 xx f y f y x) {t : Ordnode α} (h : 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) :
      theorem Ordnode.insert'_eq_insertWith {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (t : Ordnode α) :
      theorem Ordnode.insert'.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableLE α] (x : α) {t : Ordnode α} (h : 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
      Instances For
        def Ordset.nil {α : Type u_1} [Preorder α] :

        O(1). The empty set.

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

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

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

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

            Equations
            Instances For
              Equations
              instance Ordset.instInhabited {α : Type u_1} [Preorder α] :
              Equations
              instance Ordset.instSingleton {α : Type u_1} [Preorder α] :
              Equations
              def Ordset.Empty {α : Type u_1} [Preorder α] (s : Ordset α) :

              O(1). Is the set empty?

              Equations
              Instances For
                theorem Ordset.empty_iff {α : Type u_1} [Preorder α] {s : Ordset α} :
                s = (↑s).empty = true
                def Ordset.insert {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableLE α] (x : α) (s : 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
                Instances For
                  instance Ordset.instInsert {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableLE α] :
                  Insert α (Ordset α)
                  Equations
                  def Ordset.insert' {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableLE α] (x : α) (s : 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
                  Instances For
                    def Ordset.mem {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) :

                    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
                    Instances For
                      def Ordset.find {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) :

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

                      Equations
                      Instances For
                        instance Ordset.instMembership {α : Type u_1} [Preorder α] [DecidableLE α] :
                        Equations
                        instance Ordset.mem.decidable {α : Type u_1} [Preorder α] [DecidableLE α] (x : α) (s : Ordset α) :
                        Equations
                        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 α) :

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

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

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

                          Equations
                          Instances For