Invariants for the verification of Ordnode
#
An Ordnode
, defined in Mathlib.Data.Ordmap.Ordnode
, is an inductive type which describes a
tree which stores the size
at internal nodes.
In this file we define the correctness invariant of an Ordnode
, comprising:
Ordnode.Sized t
: All internalsize
fields 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 r
andsize r ≤ δ * size l
, whereδ := 3
is 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 ifa
is in the left subtree andb
is the root, thena ≤ b
and¬(b ≤ a)
. We enforce this usingOrdnode.Bounded
which includes also a global upper and lower bound.
This whole file is in the Ordnode
namespace, because we first have to prove the correctness of
all the operations (and defining what correctness means here is somewhat subtle).
The actual Ordset
operations are in Mathlib.Data.Ordmap.Ordset
.
TODO #
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 #
singleton
#
size
and empty
#
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
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
- Ordnode.BalancedSz l r = (l + r ≤ 1 ∨ l ≤ Ordnode.delta * r ∧ r ≤ Ordnode.delta * l)
Instances For
Equations
- Ordnode.BalancedSz.dec x✝¹ x✝ = inferInstanceAs (Decidable (x✝¹ + x✝ ≤ 1 ∨ x✝¹ ≤ Ordnode.delta * x✝ ∧ x✝ ≤ Ordnode.delta * x✝¹))
The Balanced t
asserts that the tree t
satisfies the balance invariants
(at every level).
Equations
- Ordnode.nil.Balanced = True
- (Ordnode.node size l x_1 r).Balanced = (Ordnode.BalancedSz l.size r.size ∧ l.Balanced ∧ r.Balanced)
Instances For
Equations
- Ordnode.Balanced.dec Ordnode.nil = ⋯.mpr inferInstance
- Ordnode.Balanced.dec (Ordnode.node size l x_1 r) = ⋯.mpr inferInstance
rotate
and balance
#
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
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
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
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
A left balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.
Equations
Instances For
A right balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.
Equations
Instances For
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
All
, Any
, Emem
, Amem
#
toList
#
mem
#
(find/erase/split)(Min/Max)
#
glue
#
merge
#
insert
#
balance
properties #
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.