Verification of Ordnode
#
This file uses the invariants defined in Mathlib.Data.Ordmap.Invariants
to construct Ordset α
,
a wrapper around Ordnode α
which includes the correctness invariant of the type. It exposes
parallel operations like insert
as functions on Ordset
that do the same thing but bundle the
correctness proofs.
The advantage is that it is possible to, for example, prove that the result of find
on insert
will actually find the element, while Ordnode
cannot guarantee this if the input tree did not
satisfy the type invariants.
Main definitions #
Ordnode.Valid
: The validity predicate for anOrdnode
subtree.Ordset α
: A well formed set of values of typeα
.
Implementation notes #
Because the Ordnode
file was ported from Haskell, the correctness invariants of some
of the functions have not been spelled out, and some theorems like
Ordnode.Valid'.balanceL_aux
show very intricate assumptions on the sizes,
which may need to be revised if it turns out some operations violate these assumptions,
because there is a decent amount of slop in the actual data structure invariants, so the
theorem will go through with multiple choices of assumption.
The validity predicate for an Ordnode
subtree. This asserts that the size
fields are
correct, the tree is balanced, and the elements of the tree are organized according to the
ordering. This version of Valid
also puts all elements in the tree in the interval (lo, hi)
.
Instances For
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
O(1). Construct a singleton set containing value a
.
Equations
- Ordset.singleton a = ⟨{a}, ⋯⟩
Instances For
Equations
- Ordset.instEmptyCollection = { emptyCollection := Ordset.nil }
Equations
- Ordset.instInhabited = { default := Ordset.nil }
Equations
- Ordset.instSingleton = { singleton := Ordset.singleton }
Equations
- Ordset.Empty.instDecidablePred x✝ = decidable_of_iff' ((↑x✝).empty = true) ⋯
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, ⋯⟩
Instances For
Equations
- Ordset.instInsert = { insert := Ordset.insert }
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, ⋯⟩
Instances For
O(log n). Does the set contain the element x
? That is,
is there an element that is equivalent to x
in the order?
Equations
- Ordset.mem x s = decide (x ∈ ↑s)
Instances For
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
Instances For
Equations
- Ordset.instMembership = { mem := fun (s : Ordset α) (x : α) => Ordset.mem x s = true }
Equations
- Ordset.mem.decidable x s = instDecidableEqBool (Ordset.mem x s) true
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, ⋯⟩
Instances For
O(n). Map a function across a tree, without changing the structure.
Equations
- Ordset.map f f_strict_mono s = ⟨Ordnode.map f ↑s, ⋯⟩