Verification of the ordnode α datatype #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
ordset α: A well formed set of values of typeα
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:
ordnode.sized t: All internalsizefields must match the actual measured size of the tree. (This is not hard to satisfy.)ordnode.balanced t: Unless the tree has the form()or((a) b)or(a (b))(that is, nil or a single singleton subtree), the two subtrees must satisfysize l ≤ δ * size randsize r ≤ δ * size l, whereδ := 3is a global parameter of the data structure (and this property must hold recursively at subtrees). This is why we say this is a "size balanced tree" data structure.ordnode.bounded lo hi t: The members of the tree must be in strictly increasing order, meaning that ifais in the left subtree andbis the root, thena ≤ band¬ (b ≤ a). We enforce this usingordnode.boundedwhich includes also a global upper and lower bound.
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'.balance_l_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.delta_lt_false
{a b : ℕ}
(h₁ : ordnode.delta * a < b)
(h₂ : ordnode.delta * b < a) :
singleton #
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) :
@[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
The balanced_sz 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
- ordnode.balanced_sz l r = (l + r ≤ 1 ∨ l ≤ ordnode.delta * r ∧ r ≤ ordnode.delta * l)
Instances for ordnode.balanced_sz
@[protected, instance]
Equations
- ordnode.balanced_sz.dec = λ (l r : ℕ), or.decidable
The balanced t asserts that the tree t satisfies the balance invariants
(at every level).
Equations
- (ordnode.node _x l _x_1 r).balanced = (ordnode.balanced_sz l.size r.size ∧ l.balanced ∧ r.balanced)
- ordnode.nil.balanced = true
Instances for ordnode.balanced
@[protected, instance]
Equations
- ordnode.balanced.dec t = ordnode.rec (ordnode.balanced.dec._main._proof_1.mpr decidable.true) (λ (t_size : ℕ) (t_l : ordnode α) (t_x : α) (t_r : ordnode α) (t_ih_l : decidable t_l.balanced) (t_ih_r : decidable t_r.balanced), _.mpr and.decidable) t
theorem
ordnode.balanced_sz_up
{l r₁ r₂ : ℕ}
(h₁ : r₁ ≤ r₂)
(h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ ordnode.delta * l)
(H : ordnode.balanced_sz l r₁) :
ordnode.balanced_sz l r₂
theorem
ordnode.balanced_sz_down
{l r₁ r₂ : ℕ}
(h₁ : r₁ ≤ r₂)
(h₂ : l + r₂ ≤ 1 ∨ l ≤ ordnode.delta * r₁)
(H : ordnode.balanced_sz l r₂) :
ordnode.balanced_sz l r₁
rotate and balance #
Build a tree from three nodes, with a () b -> (a ()) b and a (b c) d -> ((a b) (c d)).
Equations
- l.node4_l x (ordnode.node _x ml y mr) z r = (l.node' x ml).node' y (mr.node' z r)
- l.node4_l x ordnode.nil z r = l.node3_l x ordnode.nil z r
Build a tree from three nodes, with a () b -> a (() b) and a (b c) d -> ((a b) (c d)).
Equations
- l.node4_r x (ordnode.node _x ml y mr) z r = (l.node' x ml).node' y (mr.node' z r)
- l.node4_r x ordnode.nil z r = l.node3_r x ordnode.nil z r
Concatenate two nodes, performing a left rotation x (y z) -> ((x y) z)
if balance is upset.
Equations
- l.rotate_l x (ordnode.node _x m y r) = ite (m.size < ordnode.ratio * r.size) (l.node3_l x m y r) (l.node4_l x m y r)
- l.rotate_l x ordnode.nil = l.node' x ordnode.nil
Concatenate two nodes, performing a right rotation (x y) z -> (x (y z))
if balance is upset.
Equations
- (ordnode.node _x l x m).rotate_r y r = ite (m.size < ordnode.ratio * l.size) (l.node3_r x m y r) (l.node4_r x m y r)
- ordnode.nil.rotate_r y r = ordnode.nil.node' y r
A left balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.
A right balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.
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.
all, any, emem, amem #
theorem
ordnode.all.imp
{α : Type u_1}
{P Q : α → Prop}
(H : ∀ (a : α), P a → Q a)
{t : ordnode α} :
ordnode.all P t → ordnode.all Q t
theorem
ordnode.any.imp
{α : Type u_1}
{P Q : α → Prop}
(H : ∀ (a : α), P a → Q a)
{t : ordnode α} :
ordnode.any P t → ordnode.any Q t
theorem
ordnode.all_dual
{α : Type u_1}
{P : α → Prop}
{t : ordnode α} :
ordnode.all P t.dual ↔ ordnode.all P t
theorem
ordnode.all_iff_forall
{α : Type u_1}
{P : α → Prop}
{t : ordnode α} :
ordnode.all P t ↔ ∀ (x : α), ordnode.emem x t → P 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 t → P 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_node3_l
{α : Type u_1}
{P : α → Prop}
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α} :
ordnode.all P (l.node3_l x m y r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P m ∧ P y ∧ ordnode.all P r
theorem
ordnode.all_node3_r
{α : Type u_1}
{P : α → Prop}
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α} :
ordnode.all P (l.node3_r x m y r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P m ∧ P y ∧ ordnode.all P r
theorem
ordnode.all_node4_l
{α : Type u_1}
{P : α → Prop}
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α} :
ordnode.all P (l.node4_l x m y r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P m ∧ P y ∧ ordnode.all P r
theorem
ordnode.all_node4_r
{α : Type u_1}
{P : α → Prop}
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α} :
ordnode.all P (l.node4_r x m y r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P m ∧ P y ∧ ordnode.all P r
theorem
ordnode.all_rotate_l
{α : Type u_1}
{P : α → Prop}
{l : ordnode α}
{x : α}
{r : ordnode α} :
ordnode.all P (l.rotate_l x r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P r
theorem
ordnode.all_rotate_r
{α : Type u_1}
{P : α → Prop}
{l : ordnode α}
{x : α}
{r : ordnode α} :
ordnode.all P (l.rotate_r 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
to_list #
theorem
ordnode.foldr_cons_eq_to_list
{α : Type u_1}
(t : ordnode α)
(r : list α) :
ordnode.foldr list.cons t r = t.to_list ++ r
theorem
ordnode.emem_iff_mem_to_list
{α : Type u_1}
{x : α}
{t : ordnode α} :
ordnode.emem x t ↔ x ∈ t.to_list
mem #
(find/erase/split)_(min/max) #
theorem
ordnode.find_min'_dual
{α : Type u_1}
(t : ordnode α)
(x : α) :
t.dual.find_min' x = ordnode.find_max' x t
theorem
ordnode.find_max'_dual
{α : Type u_1}
(t : ordnode α)
(x : α) :
ordnode.find_max' x t.dual = t.find_min' x
theorem
ordnode.split_min_eq
{α : Type u_1}
(s : ℕ)
(l : ordnode α)
(x : α)
(r : ordnode α) :
l.split_min' x r = (l.find_min' x, (ordnode.node s l x r).erase_min)
theorem
ordnode.split_max_eq
{α : Type u_1}
(s : ℕ)
(l : ordnode α)
(x : α)
(r : ordnode α) :
l.split_max' x r = ((ordnode.node s l x r).erase_max, ordnode.find_max' x r)
theorem
ordnode.find_min'_all
{α : Type u_1}
{P : α → Prop}
(t : ordnode α)
(x : α) :
ordnode.all P t → P x → P (t.find_min' x)
theorem
ordnode.find_max'_all
{α : Type u_1}
{P : α → Prop}
(x : α)
(t : ordnode α) :
P x → ordnode.all P t → P (ordnode.find_max' x t)
glue #
merge #
@[simp]
@[simp]
@[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) = ite (ordnode.delta * ls < rs) (((ordnode.node ls ll lx lr).merge rl).balance_l rx rr) (ite (ordnode.delta * rs < ls) (ll.balance_r lx (lr.merge (ordnode.node rs rl rx rr))) ((ordnode.node ls ll lx lr).glue (ordnode.node rs rl rx rr)))
insert #
theorem
ordnode.dual_insert
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le]
(x : α)
(t : ordnode α) :
(ordnode.insert x t).dual = ordnode.insert x t.dual
balance properties #
raised n m means m is either equal or one up from n.
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₁ r₂ : ordnode α}
(H : ordnode.raised r₁.size r₂.size) :
ordnode.raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
theorem
ordnode.balance_l_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.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r.size r' ∧ ordnode.balanced_sz l.size r') :
theorem
ordnode.balance_sz_dual
{α : Type u_1}
{l r : ordnode α}
(H : (∃ (l' : ℕ), ordnode.raised l.size l' ∧ ordnode.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r' r.size ∧ ordnode.balanced_sz l.size r') :
theorem
ordnode.size_balance_l
{α : 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.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r.size r' ∧ ordnode.balanced_sz l.size r') :
theorem
ordnode.all_balance_l
{α : 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.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r.size r' ∧ ordnode.balanced_sz l.size r') :
ordnode.all P (l.balance_l x r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P r
theorem
ordnode.balance_r_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.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r' r.size ∧ ordnode.balanced_sz l.size r') :
theorem
ordnode.size_balance_r
{α : 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.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r' r.size ∧ ordnode.balanced_sz l.size r') :
theorem
ordnode.all_balance_r
{α : 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.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r' r.size ∧ ordnode.balanced_sz l.size r') :
ordnode.all P (l.balance_r x r) ↔ ordnode.all P l ∧ P x ∧ ordnode.all P r
bounded #
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.node _x l x r).bounded o₁ o₂ = (l.bounded o₁ ↑x ∧ r.bounded ↑x o₂)
- ordnode.nil.bounded (option.some a) (option.some b) = (a < b)
- ordnode.nil.bounded (option.some val) option.none = true
- ordnode.nil.bounded option.none _x = true
theorem
ordnode.bounded.to_sep
{α : Type u_1}
[preorder α]
{t₁ t₂ : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
{x : α}
(h₁ : t₁.bounded o₁ ↑x)
(h₂ : t₂.bounded ↑x o₂) :
ordnode.all (λ (y : α), ordnode.all (λ (z : α), y < z) t₂) t₁
valid #
structure
ordnode.valid'
{α : Type u_1}
[preorder α]
(lo : with_bot α)
(t : ordnode α)
(hi : with_top α) :
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).
theorem
ordnode.valid'.mono_left
{α : Type u_1}
[preorder α]
{x y : α}
(xy : x ≤ y)
{t : ordnode α}
{o : with_top α}
(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 : with_bot α}
(h : ordnode.valid' o t ↑x) :
ordnode.valid' o t ↑y
theorem
ordnode.valid'.trans_left
{α : Type u_1}
[preorder α]
{t₁ t₂ : ordnode α}
{x : α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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₁ t₂ : ordnode α}
{x : α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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₁ : with_bot α}
{o₂ : with_top α}
(H : ordnode.valid' o₁ t o₂)
(h₁ : ordnode.nil.bounded o₁ ↑x)
(h₂ : ordnode.all (λ (_x : α), _x < x) t) :
ordnode.valid' o₁ t ↑x
theorem
ordnode.valid'.of_gt
{α : Type u_1}
[preorder α]
{t : ordnode α}
{x : α}
{o₁ : with_bot α}
{o₂ : with_top α}
(H : ordnode.valid' o₁ t o₂)
(h₁ : ordnode.nil.bounded ↑x o₂)
(h₂ : ordnode.all (λ (_x : α), _x > x) t) :
ordnode.valid' ↑x t o₂
theorem
ordnode.valid'.valid
{α : Type u_1}
[preorder α]
{t : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(h : ordnode.valid' o₁ t o₂) :
t.valid
theorem
ordnode.valid'_nil
{α : Type u_1}
[preorder α]
{o₁ : with_bot α}
{o₂ : with_top α}
(h : ordnode.nil.bounded o₁ o₂) :
ordnode.valid' o₁ ordnode.nil o₂
theorem
ordnode.valid'.node
{α : Type u_1}
[preorder α]
{s : ℕ}
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H : ordnode.balanced_sz 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₁ : with_bot α}
{o₂ : with_top α}
(h : ordnode.valid' o₁ t o₂) :
ordnode.valid' o₂ t.dual o₁
theorem
ordnode.valid'.dual_iff
{α : Type u_1}
[preorder α]
{t : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α} :
ordnode.valid' o₁ t o₂ ↔ ordnode.valid' o₂ t.dual o₁
theorem
ordnode.valid'.left
{α : Type u_1}
[preorder α]
{s : ℕ}
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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₁ : with_bot α}
{o₂ : with_top α}
(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'.node'
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H : ordnode.balanced_sz l.size r.size) :
ordnode.valid' o₁ (l.node' x r) o₂
theorem
ordnode.valid'_singleton
{α : Type u_1}
[preorder α]
{x : α}
{o₁ : with_bot α}
{o₂ : with_top α}
(h₁ : ordnode.nil.bounded o₁ ↑x)
(h₂ : ordnode.nil.bounded ↑x o₂) :
ordnode.valid' o₁ {x} o₂
theorem
ordnode.valid'.node3_l
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hm : ordnode.valid' ↑x m ↑y)
(hr : ordnode.valid' ↑y r o₂)
(H1 : ordnode.balanced_sz l.size m.size)
(H2 : ordnode.balanced_sz (l.size + m.size + 1) r.size) :
ordnode.valid' o₁ (l.node3_l x m y r) o₂
theorem
ordnode.valid'.node3_r
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hm : ordnode.valid' ↑x m ↑y)
(hr : ordnode.valid' ↑y r o₂)
(H1 : ordnode.balanced_sz l.size (m.size + r.size + 1))
(H2 : ordnode.balanced_sz m.size r.size) :
ordnode.valid' o₁ (l.node3_r x m y r) o₂
theorem
ordnode.valid'.node4_l
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{m : ordnode α}
{y : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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.node4_l x m y r) o₂
theorem
ordnode.valid'.rotate_l
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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.rotate_l x r) o₂
theorem
ordnode.valid'.rotate_r
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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.rotate_r x r) o₂
theorem
ordnode.valid'.balance'_aux
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(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'
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H : ∃ (l' r' : ℕ), ordnode.balanced_sz 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₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H : ∃ (l' r' : ℕ), ordnode.balanced_sz 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_l_aux
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H₁ : l.size = 0 → r.size ≤ 1)
(H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ ordnode.delta * l.size)
(H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3) :
ordnode.valid' o₁ (l.balance_l x r) o₂
theorem
ordnode.valid'.balance_l
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H : (∃ (l' : ℕ), ordnode.raised l' l.size ∧ ordnode.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r.size r' ∧ ordnode.balanced_sz l.size r') :
ordnode.valid' o₁ (l.balance_l x r) o₂
theorem
ordnode.valid'.balance_r_aux
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H₁ : r.size = 0 → l.size ≤ 1)
(H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ ordnode.delta * r.size)
(H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3) :
ordnode.valid' o₁ (l.balance_r x r) o₂
theorem
ordnode.valid'.balance_r
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂)
(H : (∃ (l' : ℕ), ordnode.raised l.size l' ∧ ordnode.balanced_sz l' r.size) ∨ ∃ (r' : ℕ), ordnode.raised r' r.size ∧ ordnode.balanced_sz l.size r') :
ordnode.valid' o₁ (l.balance_r x r) o₂
theorem
ordnode.valid'.erase_max_aux
{α : Type u_1}
[preorder α]
{s : ℕ}
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(H : ordnode.valid' o₁ (ordnode.node s l x r) o₂) :
theorem
ordnode.valid'.erase_min_aux
{α : Type u_1}
[preorder α]
{s : ℕ}
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(H : ordnode.valid' o₁ (ordnode.node s l x r) o₂) :
theorem
ordnode.valid'.glue_aux
{α : Type u_1}
[preorder α]
{l r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l o₂)
(hr : ordnode.valid' o₁ r o₂)
(sep : ordnode.all (λ (x : α), ordnode.all (λ (y : α), x < y) r) l)
(bal : ordnode.balanced_sz l.size r.size) :
theorem
ordnode.valid'.glue
{α : Type u_1}
[preorder α]
{l : ordnode α}
{x : α}
{r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l ↑x)
(hr : ordnode.valid' ↑x r o₂) :
theorem
ordnode.valid'.merge_aux₁
{α : Type u_1}
[preorder α]
{o₁ : with_bot α}
{o₂ : with_top α}
{ls : ℕ}
{ll : ordnode α}
{lx : α}
{lr : ordnode α}
{rs : ℕ}
{rl : ordnode α}
{rx : α}
{rr 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) :
theorem
ordnode.valid'.merge_aux
{α : Type u_1}
[preorder α]
{l r : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α}
(hl : ordnode.valid' o₁ l o₂)
(hr : ordnode.valid' o₁ r o₂)
(sep : ordnode.all (λ (x : α), ordnode.all (λ (y : α), x < y) r) l) :
theorem
ordnode.valid.merge
{α : Type u_1}
[preorder α]
{l r : ordnode α}
(hl : l.valid)
(hr : r.valid)
(sep : ordnode.all (λ (x : α), ordnode.all (λ (y : α), x < y) r) l) :
theorem
ordnode.insert_with.valid_aux
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le]
(f : α → α)
(x : α)
(hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x)
{t : ordnode α}
{o₁ : with_bot α}
{o₂ : with_top α} :
ordnode.valid' o₁ t o₂ → ordnode.nil.bounded o₁ ↑x → ordnode.nil.bounded ↑x o₂ → ordnode.valid' o₁ (ordnode.insert_with f x t) o₂ ∧ ordnode.raised t.size (ordnode.insert_with f x t).size
theorem
ordnode.insert_eq_insert_with
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
(x : α)
(t : ordnode α) :
ordnode.insert x t = ordnode.insert_with (λ (_x : α), x) x t
theorem
ordnode.insert.valid
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le]
(x : α)
{t : ordnode α}
(h : t.valid) :
(ordnode.insert x t).valid
theorem
ordnode.insert'_eq_insert_with
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
(x : α)
(t : ordnode α) :
ordnode.insert' x t = ordnode.insert_with id x t
theorem
ordnode.insert'.valid
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le]
(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 : strict_mono f)
{t : ordnode α}
{a₁ : with_bot α}
{a₂ : with_top α}
(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 : strict_mono f)
{t : ordnode α}
(h : t.valid) :
(ordnode.map f t).valid
theorem
ordnode.valid'.erase_aux
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
(x : α)
{t : ordnode α}
{a₁ : with_bot α}
{a₂ : with_top α}
(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 α]
[decidable_rel has_le.le]
(x : α)
{t : ordnode α}
(h : t.valid) :
(ordnode.erase x t).valid
theorem
ordnode.size_erase_of_mem
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
{x : α}
{t : ordnode α}
{a₁ : with_bot α}
{a₂ : with_top α}
(h : ordnode.valid' a₁ t a₂)
(h_mem : x ∈ t) :
(ordnode.erase x t).size = t.size - 1
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.
Instances for ordset
O(1). The empty set.
Equations
- ordset.nil = ⟨ordnode.nil α, _⟩
@[protected]
O(1). Construct a singleton set containing value a.
Equations
- ordset.singleton a = ⟨{a}, _⟩
@[protected, instance]
Equations
- ordset.has_emptyc = {emptyc := ordset.nil _inst_1}
@[protected, instance]
Equations
- ordset.inhabited = {default := ordset.nil _inst_1}
@[protected, instance]
Equations
- ordset.has_singleton = {singleton := ordset.singleton _inst_1}
O(1). Is the set empty?
Instances for ordset.empty
@[protected, instance]
Equations
- ordset.empty.decidable_pred = λ (s : ordset α), decidable_of_iff' ↥(s.val.empty) ordset.empty_iff
@[protected]
def
ordset.insert
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le]
(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.val, _⟩
@[protected, instance]
def
ordset.has_insert
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le] :
has_insert α (ordset α)
Equations
- ordset.has_insert = {insert := ordset.insert (λ (a b : α), _inst_3 a b)}
def
ordset.insert'
{α : Type u_1}
[preorder α]
[is_total α has_le.le]
[decidable_rel has_le.le]
(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.val, _⟩
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 = decidable.to_bool (x ∈ s.val)
def
ordset.find
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
(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.val
@[protected, instance]
Equations
- ordset.has_mem = {mem := λ (x : α) (s : ordset α), ↥(ordset.mem x s)}
@[protected, instance]
def
ordset.mem.decidable
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
(x : α)
(s : ordset α) :
Equations
- ordset.mem.decidable x s = bool.decidable_eq (ordset.mem x s) bool.tt
theorem
ordset.pos_size_of_mem
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
{x : α}
{t : ordset α}
(h_mem : x ∈ t) :
def
ordset.erase
{α : Type u_1}
[preorder α]
[decidable_rel has_le.le]
(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.val, _⟩
def
ordset.map
{α : Type u_1}
[preorder α]
{β : Type u_2}
[preorder β]
(f : α → β)
(f_strict_mono : strict_mono 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.val, _⟩