Documentation

Mathlib.Data.Ordmap.Ordset

Verification of the Ordnode α datatype #

This file proves the correctness of the operations in Data.Ordmap.Ordnode. The public facing version is the type Ordset α, which is a wrapper around Ordnode α which includes the correctness invariant of the type, and 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 #

The majority of this file is actually in the Ordnode namespace, because we first have to prove the correctness of all the operations (and defining what correctness means here is actually somewhat subtle). So all the actual Ordset operations are at the very end, once we have all the theorems.

An Ordnode α is an inductive type which describes a tree which stores the size at internal nodes. The correctness invariant of an Ordnode α is:

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.

Note: This file is incomplete, in the sense that the intent is to have verified versions and lemmas about all the definitions in Ordnode.lean, but at the moment only a few operations are verified (the hard part should be out of the way, but still). Contributors are encouraged to pick this up and finish the job, if it appeals to you.

Tags #

ordered map, ordered set, data structure, verified programming

delta and ratio #

theorem Ordnode.not_le_delta {s : } (H : 1 s) :
theorem Ordnode.delta_lt_false {a : } {b : } (h₁ : Ordnode.delta * a < b) (h₂ : Ordnode.delta * b < a) :

singleton #

size and empty #

def Ordnode.realSize {α : Type u_1} :
Ordnode α

O(n). Computes the actual number of elements in the set, ignoring the cached size field.

Equations
  • Ordnode.nil.realSize = 0
  • (Ordnode.node size l x_1 r).realSize = l.realSize + r.realSize + 1
Instances For

    Sized #

    def Ordnode.Sized {α : Type u_1} :
    Ordnode αProp

    The Sized property asserts that all the size fields in nodes match the actual size of the respective subtrees.

    Equations
    Instances For
      theorem Ordnode.Sized.node' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
      (l.node' x r).Sized
      theorem Ordnode.Sized.eq_node' {α : Type u_1} {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (h : (Ordnode.node s l x r).Sized) :
      Ordnode.node s l x r = l.node' x r
      theorem Ordnode.Sized.size_eq {α : Type u_1} {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (H : (Ordnode.node s l x r).Sized) :
      (Ordnode.node s l x r).size = l.size + r.size + 1
      theorem Ordnode.Sized.induction {α : Type u_1} {t : Ordnode α} (hl : t.Sized) {C : Ordnode αProp} (H0 : C Ordnode.nil) (H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C lC rC (l.node' x r)) :
      C t
      theorem Ordnode.size_eq_realSize {α : Type u_1} {t : Ordnode α} :
      t.Sizedt.size = t.realSize
      @[simp]
      theorem Ordnode.Sized.size_eq_zero {α : Type u_1} {t : Ordnode α} (ht : t.Sized) :
      t.size = 0 t = Ordnode.nil
      theorem Ordnode.Sized.pos {α : Type u_1} {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (h : (Ordnode.node s l x r).Sized) :
      0 < s

      dual

      theorem Ordnode.dual_dual {α : Type u_1} (t : Ordnode α) :
      t.dual.dual = t
      @[simp]
      theorem Ordnode.size_dual {α : Type u_1} (t : Ordnode α) :
      t.dual.size = t.size

      Balanced

      def Ordnode.BalancedSz (l : ) (r : ) :

      The BalancedSz l r asserts that a hypothetical tree with children of sizes l and r is balanced: either l ≤ δ * r and r ≤ δ * r, or the tree is trivial with a singleton on one side and nothing on the other.

      Equations
      Instances For
        def Ordnode.Balanced {α : Type u_1} :
        Ordnode αProp

        The Balanced t asserts that the tree t satisfies the balance invariants (at every level).

        Equations
        Instances For
          instance Ordnode.Balanced.dec {α : Type u_1} :
          DecidablePred Ordnode.Balanced
          Equations
          theorem Ordnode.balancedSz_up {l : } {r₁ : } {r₂ : } (h₁ : r₁ r₂) (h₂ : l + r₂ 1 r₂ Ordnode.delta * l) (H : Ordnode.BalancedSz l r₁) :
          theorem Ordnode.balancedSz_down {l : } {r₁ : } {r₂ : } (h₁ : r₁ r₂) (h₂ : l + r₂ 1 l Ordnode.delta * r₁) (H : Ordnode.BalancedSz l r₂) :
          theorem Ordnode.Balanced.dual {α : Type u_1} {t : Ordnode α} :
          t.Balancedt.dual.Balanced

          rotate and balance #

          def Ordnode.node3L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :

          Build a tree from three nodes, left associated (ignores the invariants).

          Equations
          • l.node3L x m y r = (l.node' x m).node' y r
          Instances For
            def Ordnode.node3R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :

            Build a tree from three nodes, right associated (ignores the invariants).

            Equations
            • l.node3R x m y r = l.node' x (m.node' y r)
            Instances For
              def Ordnode.node4L {α : Type u_1} :
              Ordnode ααOrdnode ααOrdnode αOrdnode α

              Build a tree from three nodes, with a () b -> (a ()) b and a (b c) d -> ((a b) (c d)).

              Equations
              • x✝².node4L x✝¹ (Ordnode.node size ml y mr) x✝ x = (x✝².node' x✝¹ ml).node' y (mr.node' x✝ x)
              • x✝².node4L x✝¹ Ordnode.nil x✝ x = x✝².node3L x✝¹ Ordnode.nil x✝ x
              Instances For
                def Ordnode.node4R {α : Type u_1} :
                Ordnode ααOrdnode ααOrdnode αOrdnode α

                Build a tree from three nodes, with a () b -> a (() b) and a (b c) d -> ((a b) (c d)).

                Equations
                • x✝².node4R x✝¹ (Ordnode.node size ml y mr) x✝ x = (x✝².node' x✝¹ ml).node' y (mr.node' x✝ x)
                • x✝².node4R x✝¹ Ordnode.nil x✝ x = x✝².node3R x✝¹ Ordnode.nil x✝ x
                Instances For
                  def Ordnode.rotateL {α : Type u_1} :
                  Ordnode ααOrdnode αOrdnode α

                  Concatenate two nodes, performing a left rotation x (y z) -> ((x y) z) if balance is upset.

                  Equations
                  • x✝.rotateL x (Ordnode.node size m y r) = if m.size < Ordnode.ratio * r.size then x✝.node3L x m y r else x✝.node4L x m y r
                  • x✝.rotateL x Ordnode.nil = x✝.node' x Ordnode.nil
                  Instances For
                    theorem Ordnode.rotateL_node {α : Type u_1} (l : Ordnode α) (x : α) (sz : ) (m : Ordnode α) (y : α) (r : Ordnode α) :
                    l.rotateL x (Ordnode.node sz m y r) = if m.size < Ordnode.ratio * r.size then l.node3L x m y r else l.node4L x m y r
                    theorem Ordnode.rotateL_nil {α : Type u_1} (l : Ordnode α) (x : α) :
                    l.rotateL x Ordnode.nil = l.node' x Ordnode.nil
                    def Ordnode.rotateR {α : Type u_1} :
                    Ordnode ααOrdnode αOrdnode α

                    Concatenate two nodes, performing a right rotation (x y) z -> (x (y z)) if balance is upset.

                    Equations
                    • (Ordnode.node size l x_3 m).rotateR x✝ x = if m.size < Ordnode.ratio * l.size then l.node3R x_3 m x✝ x else l.node4R x_3 m x✝ x
                    • Ordnode.nil.rotateR x✝ x = Ordnode.nil.node' x✝ x
                    Instances For
                      theorem Ordnode.rotateR_node {α : Type u_1} (sz : ) (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                      (Ordnode.node sz l x m).rotateR y r = if m.size < Ordnode.ratio * l.size then l.node3R x m y r else l.node4R x m y r
                      theorem Ordnode.rotateR_nil {α : Type u_1} (y : α) (r : Ordnode α) :
                      Ordnode.nil.rotateR y r = Ordnode.nil.node' y r
                      def Ordnode.balanceL' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :

                      A left balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.

                      Equations
                      • l.balanceL' x r = if l.size + r.size 1 then l.node' x r else if l.size > Ordnode.delta * r.size then l.rotateR x r else l.node' x r
                      Instances For
                        def Ordnode.balanceR' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :

                        A right balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.

                        Equations
                        • l.balanceR' x r = if l.size + r.size 1 then l.node' x r else if r.size > Ordnode.delta * l.size then l.rotateL x r else l.node' x r
                        Instances For
                          def Ordnode.balance' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :

                          The full balance operation. This is the same as balance, but with less manual inlining. It is somewhat easier to work with this version in proofs.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem Ordnode.dual_node' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.node' x r).dual = r.dual.node' x l.dual
                            theorem Ordnode.dual_node3L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual
                            theorem Ordnode.dual_node3R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual
                            theorem Ordnode.dual_node4L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual
                            theorem Ordnode.dual_node4R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
                            (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual
                            theorem Ordnode.dual_rotateL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.rotateL x r).dual = r.dual.rotateR x l.dual
                            theorem Ordnode.dual_rotateR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.rotateR x r).dual = r.dual.rotateL x l.dual
                            theorem Ordnode.dual_balance' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.balance' x r).dual = r.dual.balance' x l.dual
                            theorem Ordnode.dual_balanceL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.balanceL x r).dual = r.dual.balanceR x l.dual
                            theorem Ordnode.dual_balanceR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (l.balanceR x r).dual = r.dual.balanceL x l.dual
                            theorem Ordnode.Sized.node3L {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : l.Sized) (hm : m.Sized) (hr : r.Sized) :
                            (l.node3L x m y r).Sized
                            theorem Ordnode.Sized.node3R {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : l.Sized) (hm : m.Sized) (hr : r.Sized) :
                            (l.node3R x m y r).Sized
                            theorem Ordnode.Sized.node4L {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : l.Sized) (hm : m.Sized) (hr : r.Sized) :
                            (l.node4L x m y r).Sized
                            theorem Ordnode.node3L_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            (l.node3L x m y r).size = l.size + m.size + r.size + 2
                            theorem Ordnode.node3R_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            (l.node3R x m y r).size = l.size + m.size + r.size + 2
                            theorem Ordnode.node4L_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hm : m.Sized) :
                            (l.node4L x m y r).size = l.size + m.size + r.size + 2
                            theorem Ordnode.Sized.dual {α : Type u_1} {t : Ordnode α} :
                            t.Sizedt.dual.Sized
                            theorem Ordnode.Sized.dual_iff {α : Type u_1} {t : Ordnode α} :
                            t.dual.Sized t.Sized
                            theorem Ordnode.Sized.rotateL {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.rotateL x r).Sized
                            theorem Ordnode.Sized.rotateR {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.rotateR x r).Sized
                            theorem Ordnode.Sized.rotateL_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hm : r.Sized) :
                            (l.rotateL x r).size = l.size + r.size + 1
                            theorem Ordnode.Sized.rotateR_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) :
                            (l.rotateR x r).size = l.size + r.size + 1
                            theorem Ordnode.Sized.balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.balance' x r).Sized
                            theorem Ordnode.size_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) (hr : r.Sized) :
                            (l.balance' x r).size = l.size + r.size + 1

                            All, Any, Emem, Amem #

                            theorem Ordnode.All.imp {α : Type u_1} {P : αProp} {Q : αProp} (H : ∀ (a : α), P aQ a) {t : Ordnode α} :
                            theorem Ordnode.Any.imp {α : Type u_1} {P : αProp} {Q : αProp} (H : ∀ (a : α), P aQ a) {t : Ordnode α} :
                            theorem Ordnode.all_singleton {α : Type u_1} {P : αProp} {x : α} :
                            Ordnode.All P {x} P x
                            theorem Ordnode.any_singleton {α : Type u_1} {P : αProp} {x : α} :
                            Ordnode.Any P {x} P x
                            theorem Ordnode.all_dual {α : Type u_1} {P : αProp} {t : Ordnode α} :
                            theorem Ordnode.all_iff_forall {α : Type u_1} {P : αProp} {t : Ordnode α} :
                            Ordnode.All P t ∀ (x : α), Ordnode.Emem x tP x
                            theorem Ordnode.any_iff_exists {α : Type u_1} {P : αProp} {t : Ordnode α} :
                            Ordnode.Any P t ∃ (x : α), Ordnode.Emem x t P x
                            theorem Ordnode.emem_iff_all {α : Type u_1} {x : α} {t : Ordnode α} :
                            Ordnode.Emem x t ∀ (P : αProp), Ordnode.All P tP x
                            theorem Ordnode.all_node' {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            Ordnode.All P (l.node' x r) Ordnode.All P l P x Ordnode.All P r
                            theorem Ordnode.all_node3L {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            Ordnode.All P (l.node3L x m y r) Ordnode.All P l P x Ordnode.All P m P y Ordnode.All P r
                            theorem Ordnode.all_node3R {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            Ordnode.All P (l.node3R x m y r) Ordnode.All P l P x Ordnode.All P m P y Ordnode.All P r
                            theorem Ordnode.all_node4L {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            Ordnode.All P (l.node4L x m y r) Ordnode.All P l P x Ordnode.All P m P y Ordnode.All P r
                            theorem Ordnode.all_node4R {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} :
                            Ordnode.All P (l.node4R x m y r) Ordnode.All P l P x Ordnode.All P m P y Ordnode.All P r
                            theorem Ordnode.all_rotateL {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            Ordnode.All P (l.rotateL x r) Ordnode.All P l P x Ordnode.All P r
                            theorem Ordnode.all_rotateR {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            Ordnode.All P (l.rotateR x r) Ordnode.All P l P x Ordnode.All P r
                            theorem Ordnode.all_balance' {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} :
                            Ordnode.All P (l.balance' x r) Ordnode.All P l P x Ordnode.All P r

                            toList #

                            theorem Ordnode.foldr_cons_eq_toList {α : Type u_1} (t : Ordnode α) (r : List α) :
                            Ordnode.foldr List.cons t r = t.toList ++ r
                            @[simp]
                            theorem Ordnode.toList_nil {α : Type u_1} :
                            Ordnode.nil.toList = []
                            @[simp]
                            theorem Ordnode.toList_node {α : Type u_1} (s : ) (l : Ordnode α) (x : α) (r : Ordnode α) :
                            (Ordnode.node s l x r).toList = l.toList ++ x :: r.toList
                            theorem Ordnode.emem_iff_mem_toList {α : Type u_1} {x : α} {t : Ordnode α} :
                            Ordnode.Emem x t x t.toList
                            theorem Ordnode.length_toList' {α : Type u_1} (t : Ordnode α) :
                            t.toList.length = t.realSize
                            theorem Ordnode.length_toList {α : Type u_1} {t : Ordnode α} (h : t.Sized) :
                            t.toList.length = t.size
                            theorem Ordnode.equiv_iff {α : Type u_1} {t₁ : Ordnode α} {t₂ : Ordnode α} (h₁ : t₁.Sized) (h₂ : t₂.Sized) :
                            t₁.Equiv t₂ t₁.toList = t₂.toList

                            mem #

                            theorem Ordnode.pos_size_of_mem {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] {x : α} {t : Ordnode α} (h : t.Sized) (h_mem : x t) :
                            0 < t.size

                            (find/erase/split)(Min/Max) #

                            theorem Ordnode.findMin'_dual {α : Type u_1} (t : Ordnode α) (x : α) :
                            t.dual.findMin' x = Ordnode.findMax' x t
                            theorem Ordnode.findMax'_dual {α : Type u_1} (t : Ordnode α) (x : α) :
                            Ordnode.findMax' x t.dual = t.findMin' x
                            theorem Ordnode.findMin_dual {α : Type u_1} (t : Ordnode α) :
                            t.dual.findMin = t.findMax
                            theorem Ordnode.findMax_dual {α : Type u_1} (t : Ordnode α) :
                            t.dual.findMax = t.findMin
                            theorem Ordnode.dual_eraseMin {α : Type u_1} (t : Ordnode α) :
                            t.eraseMin.dual = t.dual.eraseMax
                            theorem Ordnode.dual_eraseMax {α : Type u_1} (t : Ordnode α) :
                            t.eraseMax.dual = t.dual.eraseMin
                            theorem Ordnode.splitMin_eq {α : Type u_1} (s : ) (l : Ordnode α) (x : α) (r : Ordnode α) :
                            l.splitMin' x r = (l.findMin' x, (Ordnode.node s l x r).eraseMin)
                            theorem Ordnode.splitMax_eq {α : Type u_1} (s : ) (l : Ordnode α) (x : α) (r : Ordnode α) :
                            l.splitMax' x r = ((Ordnode.node s l x r).eraseMax, Ordnode.findMax' x r)
                            theorem Ordnode.findMin'_all {α : Type u_1} {P : αProp} (t : Ordnode α) (x : α) :
                            Ordnode.All P tP xP (t.findMin' x)
                            theorem Ordnode.findMax'_all {α : Type u_1} {P : αProp} (x : α) (t : Ordnode α) :
                            P xOrdnode.All P tP (Ordnode.findMax' x t)

                            glue #

                            merge #

                            @[simp]
                            theorem Ordnode.merge_nil_left {α : Type u_1} (t : Ordnode α) :
                            t.merge Ordnode.nil = t
                            @[simp]
                            theorem Ordnode.merge_nil_right {α : Type u_1} (t : Ordnode α) :
                            Ordnode.nil.merge t = t
                            @[simp]
                            theorem Ordnode.merge_node {α : Type u_1} {ls : } {ll : Ordnode α} {lx : α} {lr : Ordnode α} {rs : } {rl : Ordnode α} {rx : α} {rr : Ordnode α} :
                            (Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr) = if Ordnode.delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr else if Ordnode.delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr)) else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)

                            insert #

                            theorem Ordnode.dual_insert {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) (t : Ordnode α) :
                            (Ordnode.insert x t).dual = Ordnode.insert x t.dual

                            balance properties #

                            theorem Ordnode.balance_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) :
                            l.balance x r = l.balance' x r
                            theorem Ordnode.balanceL_eq_balance {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (sl : l.Sized) (sr : r.Sized) (H1 : l.size = 0r.size 1) (H2 : 1 l.size1 r.sizer.size Ordnode.delta * l.size) :
                            l.balanceL x r = l.balance x r
                            def Ordnode.Raised (n : ) (m : ) :

                            Raised n m means m is either equal or one up from n.

                            Equations
                            Instances For
                              theorem Ordnode.raised_iff {n : } {m : } :
                              Ordnode.Raised n m n m m n + 1
                              theorem Ordnode.Raised.dist_le {n : } {m : } (H : Ordnode.Raised n m) :
                              n.dist m 1
                              theorem Ordnode.Raised.dist_le' {n : } {m : } (H : Ordnode.Raised n m) :
                              m.dist n 1
                              theorem Ordnode.Raised.add_left (k : ) {n : } {m : } (H : Ordnode.Raised n m) :
                              Ordnode.Raised (k + n) (k + m)
                              theorem Ordnode.Raised.add_right (k : ) {n : } {m : } (H : Ordnode.Raised n m) :
                              Ordnode.Raised (n + k) (m + k)
                              theorem Ordnode.Raised.right {α : Type u_1} {l : Ordnode α} {x₁ : α} {x₂ : α} {r₁ : Ordnode α} {r₂ : Ordnode α} (H : Ordnode.Raised r₁.size r₂.size) :
                              Ordnode.Raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
                              theorem Ordnode.balanceL_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Ordnode.Raised l' l.size Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r.size r' Ordnode.BalancedSz l.size r') :
                              l.balanceL x r = l.balance' x r
                              theorem Ordnode.balance_sz_dual {α : Type u_1} {l : Ordnode α} {r : Ordnode α} (H : (∃ (l' : ), Ordnode.Raised l.size l' Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r' r.size Ordnode.BalancedSz l.size r') :
                              (∃ (l' : ), Ordnode.Raised l' r.dual.size Ordnode.BalancedSz l' l.dual.size) ∃ (r' : ), Ordnode.Raised l.dual.size r' Ordnode.BalancedSz r.dual.size r'
                              theorem Ordnode.size_balanceL {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Ordnode.Raised l' l.size Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r.size r' Ordnode.BalancedSz l.size r') :
                              (l.balanceL x r).size = l.size + r.size + 1
                              theorem Ordnode.all_balanceL {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Ordnode.Raised l' l.size Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r.size r' Ordnode.BalancedSz l.size r') :
                              Ordnode.All P (l.balanceL x r) Ordnode.All P l P x Ordnode.All P r
                              theorem Ordnode.balanceR_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Ordnode.Raised l.size l' Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r' r.size Ordnode.BalancedSz l.size r') :
                              l.balanceR x r = l.balance' x r
                              theorem Ordnode.size_balanceR {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Ordnode.Raised l.size l' Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r' r.size Ordnode.BalancedSz l.size r') :
                              (l.balanceR x r).size = l.size + r.size + 1
                              theorem Ordnode.all_balanceR {α : Type u_1} {P : αProp} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Balanced) (hr : r.Balanced) (sl : l.Sized) (sr : r.Sized) (H : (∃ (l' : ), Ordnode.Raised l.size l' Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r' r.size Ordnode.BalancedSz l.size r') :
                              Ordnode.All P (l.balanceR x r) Ordnode.All P l P x Ordnode.All P r

                              bounded #

                              def Ordnode.Bounded {α : Type u_1} [Preorder α] :
                              Ordnode αWithBot αWithTop αProp

                              Bounded t lo hi says that every element x ∈ t is in the range lo < x < hi, and also this property holds recursively in subtrees, making the full tree a BST. The bounds can be set to lo = ⊥ and hi = ⊤ if we care only about the internal ordering constraints.

                              Equations
                              • Ordnode.nil.Bounded (some a) (some b) = (a < b)
                              • Ordnode.nil.Bounded x✝ x = True
                              • (Ordnode.node size l x_3 r).Bounded x✝ x = (l.Bounded x✝ x_3 r.Bounded (↑x_3) x)
                              Instances For
                                theorem Ordnode.Bounded.dual {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂t.dual.Bounded o₂ o₁
                                theorem Ordnode.Bounded.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂ t.dual.Bounded o₂ o₁
                                theorem Ordnode.Bounded.weak_left {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂t.Bounded o₂
                                theorem Ordnode.Bounded.weak_right {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂t.Bounded o₁
                                theorem Ordnode.Bounded.weak {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (h : t.Bounded o₁ o₂) :
                                t.Bounded
                                theorem Ordnode.Bounded.mono_left {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x y) {t : Ordnode α} {o : WithTop α} :
                                t.Bounded (↑y) ot.Bounded (↑x) o
                                theorem Ordnode.Bounded.mono_right {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x y) {t : Ordnode α} {o : WithBot α} :
                                t.Bounded o xt.Bounded o y
                                theorem Ordnode.Bounded.to_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {y : α} :
                                t.Bounded x yx < y
                                theorem Ordnode.Bounded.to_nil {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t.Bounded o₁ o₂Ordnode.nil.Bounded o₁ o₂
                                theorem Ordnode.Bounded.trans_left {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t₁.Bounded o₁ xt₂.Bounded (↑x) o₂t₂.Bounded o₁ o₂
                                theorem Ordnode.Bounded.trans_right {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                t₁.Bounded o₁ xt₂.Bounded (↑x) o₂t₁.Bounded o₁ o₂
                                theorem Ordnode.Bounded.mem_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {o : WithBot α} {x : α} :
                                t.Bounded o xOrdnode.All (fun (x_1 : α) => x_1 < x) t
                                theorem Ordnode.Bounded.mem_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {o : WithTop α} {x : α} :
                                t.Bounded (↑x) oOrdnode.All (fun (x_1 : α) => x_1 > x) t
                                theorem Ordnode.Bounded.of_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} :
                                t.Bounded o₁ o₂Ordnode.nil.Bounded o₁ xOrdnode.All (fun (x_1 : α) => x_1 < x) tt.Bounded o₁ x
                                theorem Ordnode.Bounded.of_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} :
                                t.Bounded o₁ o₂Ordnode.nil.Bounded (↑x) o₂Ordnode.All (fun (x_1 : α) => x_1 > x) tt.Bounded (↑x) o₂
                                theorem Ordnode.Bounded.to_sep {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} (h₁ : t₁.Bounded o₁ x) (h₂ : t₂.Bounded (↑x) o₂) :
                                Ordnode.All (fun (y : α) => Ordnode.All (fun (z : α) => y < z) t₂) t₁

                                Valid #

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

                                • ord : t.Bounded lo hi
                                • sz : t.Sized
                                • bal : t.Balanced
                                Instances For
                                  theorem Ordnode.Valid'.ord {α : Type u_1} [Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α} (self : Ordnode.Valid' lo t hi) :
                                  t.Bounded lo hi
                                  theorem Ordnode.Valid'.sz {α : Type u_1} [Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α} (self : Ordnode.Valid' lo t hi) :
                                  t.Sized
                                  theorem Ordnode.Valid'.bal {α : Type u_1} [Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α} (self : Ordnode.Valid' lo t hi) :
                                  t.Balanced
                                  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 : Ordnode.Valid' (↑y) t o) :
                                    Ordnode.Valid' (↑x) t o
                                    theorem Ordnode.Valid'.mono_right {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x y) {t : Ordnode α} {o : WithBot α} (h : Ordnode.Valid' o t x) :
                                    theorem Ordnode.Valid'.trans_left {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (h : t₁.Bounded o₁ x) (H : Ordnode.Valid' (↑x) t₂ o₂) :
                                    Ordnode.Valid' o₁ t₂ o₂
                                    theorem Ordnode.Valid'.trans_right {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ t₁ x) (h : t₂.Bounded (↑x) o₂) :
                                    Ordnode.Valid' o₁ t₁ o₂
                                    theorem Ordnode.Valid'.of_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ t o₂) (h₁ : Ordnode.nil.Bounded o₁ x) (h₂ : Ordnode.All (fun (x_1 : α) => x_1 < x) t) :
                                    Ordnode.Valid' o₁ t x
                                    theorem Ordnode.Valid'.of_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ t o₂) (h₁ : Ordnode.nil.Bounded (↑x) o₂) (h₂ : Ordnode.All (fun (x_1 : α) => x_1 > x) t) :
                                    Ordnode.Valid' (↑x) t o₂
                                    theorem Ordnode.Valid'.valid {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (h : Ordnode.Valid' o₁ t o₂) :
                                    t.Valid
                                    theorem Ordnode.valid'_nil {α : Type u_1} [Preorder α] {o₁ : WithBot α} {o₂ : WithTop α} (h : Ordnode.nil.Bounded o₁ o₂) :
                                    Ordnode.Valid' o₁ Ordnode.nil o₂
                                    theorem Ordnode.valid_nil {α : Type u_1} [Preorder α] :
                                    Ordnode.nil.Valid
                                    theorem Ordnode.Valid'.node {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H : Ordnode.BalancedSz l.size r.size) (hs : s = l.size + r.size + 1) :
                                    Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂
                                    theorem Ordnode.Valid'.dual {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                    Ordnode.Valid' o₁ t o₂Ordnode.Valid' o₂ t.dual o₁
                                    theorem Ordnode.Valid'.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                    Ordnode.Valid' o₁ t o₂ Ordnode.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 α} :
                                    t.Valid t.dual.Valid
                                    theorem Ordnode.Valid'.left {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) :
                                    Ordnode.Valid' o₁ l x
                                    theorem Ordnode.Valid'.right {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) :
                                    Ordnode.Valid' (↑x) r o₂
                                    theorem Ordnode.Valid.left {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (H : (Ordnode.node s l x r).Valid) :
                                    l.Valid
                                    theorem Ordnode.Valid.right {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (H : (Ordnode.node s l x r).Valid) :
                                    r.Valid
                                    theorem Ordnode.Valid.size_eq {α : Type u_1} [Preorder α] {s : } {l : Ordnode α} {x : α} {r : Ordnode α} (H : (Ordnode.node s l x r).Valid) :
                                    (Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H : Ordnode.BalancedSz l.size r.size) :
                                    Ordnode.Valid' o₁ (l.node' x r) o₂
                                    theorem Ordnode.valid'_singleton {α : Type u_1} [Preorder α] {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (h₁ : Ordnode.nil.Bounded o₁ x) (h₂ : Ordnode.nil.Bounded (↑x) o₂) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hm : Ordnode.Valid' (↑x) m y) (hr : Ordnode.Valid' (↑y) r o₂) (H1 : Ordnode.BalancedSz l.size m.size) (H2 : Ordnode.BalancedSz (l.size + m.size + 1) r.size) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hm : Ordnode.Valid' (↑x) m y) (hr : Ordnode.Valid' (↑y) r o₂) (H1 : Ordnode.BalancedSz l.size (m.size + r.size + 1)) (H2 : Ordnode.BalancedSz m.size r.size) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hm : Ordnode.Valid' (↑x) m y) (hr : Ordnode.Valid' (↑y) r o₂) (Hm : 0 < m.size) (H : l.size = 0 m.size = 1 r.size 1 0 < l.size Ordnode.ratio * r.size m.size Ordnode.delta * l.size m.size + r.size 3 * (m.size + r.size) 16 * l.size + 9 m.size Ordnode.delta * r.size) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H1 : ¬l.size + r.size 1) (H2 : Ordnode.delta * l.size < r.size) (H3 : 2 * r.size 9 * l.size + 5 r.size 3) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H1 : ¬l.size + r.size 1) (H2 : Ordnode.delta * r.size < l.size) (H3 : 2 * l.size 9 * r.size + 5 l.size 3) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.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) :
                                    Ordnode.Valid' o₁ (l.balance' x r) o₂
                                    theorem Ordnode.Valid'.balance'_lemma {α : Type u_2} {l : Ordnode α} {l' : } {r : Ordnode α} {r' : } (H1 : Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H : ∃ (l' : ) (r' : ), Ordnode.BalancedSz l' r' (l.size.dist l' 1 r.size = r' r.size.dist r' 1 l.size = l')) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H : ∃ (l' : ) (r' : ), Ordnode.BalancedSz l' r' (l.size.dist l' 1 r.size = r' r.size.dist r' 1 l.size = l')) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H₁ : l.size = 0r.size 1) (H₂ : 1 l.size1 r.sizer.size Ordnode.delta * l.size) (H₃ : 2 * l.size 9 * r.size + 5 l.size 3) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H : (∃ (l' : ), Ordnode.Raised l' l.size Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r.size r' Ordnode.BalancedSz l.size r') :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H₁ : r.size = 0l.size 1) (H₂ : 1 r.size1 l.sizel.size Ordnode.delta * r.size) (H₃ : 2 * r.size 9 * l.size + 5 r.size 3) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) (H : (∃ (l' : ), Ordnode.Raised l.size l' Ordnode.BalancedSz l' r.size) ∃ (r' : ), Ordnode.Raised r' r.size Ordnode.BalancedSz l.size r') :
                                    Ordnode.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 : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) :
                                    Ordnode.Valid' o₁ (l.node' x r).eraseMax (Ordnode.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 : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) :
                                    Ordnode.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.Validt.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 : Ordnode α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l o₂) (hr : Ordnode.Valid' o₁ r o₂) (sep : Ordnode.All (fun (x : α) => Ordnode.All (fun (y : α) => x < y) r) l) (bal : Ordnode.BalancedSz l.size r.size) :
                                    Ordnode.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 : Ordnode.Valid' o₁ l x) (hr : Ordnode.Valid' (↑x) r o₂) :
                                    Ordnode.BalancedSz l.size r.sizeOrdnode.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 : Ordnode α} {t : Ordnode α} (hl : Ordnode.Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Ordnode.Valid' o₁ (Ordnode.node rs rl rx rr) o₂) (h : Ordnode.delta * ls < rs) (v : Ordnode.Valid' o₁ t rx) (e : t.size = ls + rl.size) :
                                    Ordnode.Valid' o₁ (t.balanceL rx rr) o₂ (t.balanceL rx rr).size = ls + rs
                                    theorem Ordnode.Valid'.merge_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l o₂) (hr : Ordnode.Valid' o₁ r o₂) (sep : Ordnode.All (fun (x : α) => Ordnode.All (fun (y : α) => x < y) r) l) :
                                    Ordnode.Valid' o₁ (l.merge r) o₂ (l.merge r).size = l.size + r.size
                                    theorem Ordnode.Valid.merge {α : Type u_1} [Preorder α] {l : Ordnode α} {r : Ordnode α} (hl : l.Valid) (hr : r.Valid) (sep : Ordnode.All (fun (x : α) => Ordnode.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] [DecidableRel fun (x1 x2 : α) => x1 x2] (f : αα) (x : α) (hf : ∀ (y : α), x y y xx f y f y x) {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} :
                                    Ordnode.Valid' o₁ t o₂Ordnode.nil.Bounded o₁ xOrdnode.nil.Bounded (↑x) o₂Ordnode.Valid' o₁ (Ordnode.insertWith f x t) o₂ Ordnode.Raised t.size (Ordnode.insertWith f x t).size
                                    theorem Ordnode.insertWith.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] (f : αα) (x : α) (hf : ∀ (y : α), x y y xx f y f y x) {t : Ordnode α} (h : t.Valid) :
                                    (Ordnode.insertWith f x t).Valid
                                    theorem Ordnode.insert_eq_insertWith {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) (t : Ordnode α) :
                                    Ordnode.insert x t = Ordnode.insertWith (fun (x_1 : α) => x) x t
                                    theorem Ordnode.insert.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) {t : Ordnode α} (h : t.Valid) :
                                    (Ordnode.insert x t).Valid
                                    theorem Ordnode.insert'_eq_insertWith {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) (t : Ordnode α) :
                                    theorem Ordnode.insert'.valid {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) {t : Ordnode α} (h : t.Valid) :
                                    (Ordnode.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 : Ordnode.Valid' a₁ t a₂) :
                                    Ordnode.Valid' (Option.map f a₁) (Ordnode.map f t) (Option.map f a₂) (Ordnode.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) :
                                    (Ordnode.map f t).Valid
                                    theorem Ordnode.Valid'.erase_aux {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Ordnode.Valid' a₁ t a₂) :
                                    Ordnode.Valid' a₁ (Ordnode.erase x t) a₂ Ordnode.Raised (Ordnode.erase x t).size t.size
                                    theorem Ordnode.erase.valid {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) {t : Ordnode α} (h : t.Valid) :
                                    (Ordnode.erase x t).Valid
                                    theorem Ordnode.size_erase_of_mem {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] {x : α} {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Ordnode.Valid' a₁ t a₂) (h_mem : x t) :
                                    (Ordnode.erase x t).size = t.size - 1
                                    def Ordset (α : Type u_2) [Preorder α] :
                                    Type (max 0 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
                                      • Ordset.nil = Ordnode.nil,
                                      Instances For
                                        def Ordset.size {α : Type u_1} [Preorder α] (s : Ordset α) :

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

                                        Equations
                                        • s.size = (↑s).size
                                        Instances For
                                          def Ordset.singleton {α : Type u_1} [Preorder α] (a : α) :

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

                                          Equations
                                          Instances For
                                            Equations
                                            • Ordset.instEmptyCollection = { emptyCollection := Ordset.nil }
                                            instance Ordset.instInhabited {α : Type u_1} [Preorder α] :
                                            Equations
                                            • Ordset.instInhabited = { default := Ordset.nil }
                                            instance Ordset.instSingleton {α : Type u_1} [Preorder α] :
                                            Equations
                                            • Ordset.instSingleton = { singleton := Ordset.singleton }
                                            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
                                              instance Ordset.Empty.instDecidablePred {α : Type u_1} [Preorder α] :
                                              DecidablePred Ordset.Empty
                                              Equations
                                              def Ordset.insert {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] (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] [DecidableRel fun (x1 x2 : α) => x1 x2] :
                                                Insert α (Ordset α)
                                                Equations
                                                • Ordset.instInsert = { insert := Ordset.insert }
                                                def Ordset.insert' {α : Type u_1} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] (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 α] [DecidableRel fun (x1 x2 : α) => x1 x2] (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 α] [DecidableRel fun (x1 x2 : α) => x1 x2] (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 α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
                                                      Equations
                                                      instance Ordset.mem.decidable {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] (x : α) (s : Ordset α) :
                                                      Equations
                                                      theorem Ordset.pos_size_of_mem {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] {x : α} {t : Ordset α} (h_mem : x t) :
                                                      0 < t.size
                                                      def Ordset.erase {α : Type u_1} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 x2] (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