Interval tree
Interval Tree
StructureInterval#✓fully proved
An interval is a pair of integers, its low endpoint and its high endpoint, read as the closed interval from the low to the high endpoint. The structure itself imposes no order on the endpoints; the public update operations accept an interval only when its low endpoint is at most its high endpoint.
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqUsed by 47
Interval
DefinitionValid interval#✓fully proved
A closed interval with integer endpoints \(a\) (low) and \(b\) (high) is valid when its low endpoint is at most its high endpoint, \(a \le b\).
def Valid (interval : Interval) : Prop :=
interval.low ≤ interval.highstructure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 1 · Used by 9
DefinitionBoolean interval validity test#✓fully proved
For an interval \([a, b]\) with integer endpoints, the Boolean validity test returns true exactly when \(a \le b\).
def valid (interval : Interval) : Bool :=
letI : Decidable interval.Valid := Int.decLe _ _
decide interval.Validstructure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 2 · Used by 7
DefinitionOverlapping closed intervals#✓fully proved
An interval \(I\) with low endpoint \(a\) and high endpoint \(b\) overlaps an interval \(J\) with low endpoint \(c\) and high endpoint \(d\) when \(a \le d\) and \(c \le b\); in particular, intervals that share only an endpoint overlap.
def Overlaps (left right : Interval) : Prop :=
left.low ≤ right.high ∧ right.low ≤ left.highstructure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 1 · Used by 4
DefinitionOverlap test for closed intervals#✓fully proved
For an interval \(I\) with low endpoint \(a\) and high endpoint \(b\) and an interval \(J\) with low endpoint \(c\) and high endpoint \(d\), the overlap test of \(I\) against \(J\) returns true exactly when \(a \le d\) and \(c \le b\); it compares \(a\) with \(d\) first and returns false without the second comparison when \(a > d\).
def overlaps (left right : Interval) : Bool :=
match Int.decLe left.low right.high with
| .isFalse _ => false
| .isTrue _ =>
match Int.decLe right.low left.high with
| .isFalse _ => false
| .isTrue _ => truestructure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 1 · Used by 6
DefinitionOverlap test with comparison count#✓fully proved
For an interval \(I\) with low endpoint \(a\) and high endpoint \(b\) and an interval \(J\) with low endpoint \(c\) and high endpoint \(d\), the instrumented overlap test of \(I\) against \(J\) returns the pair (false, \(1\)) when \(a > d\), the pair (false, \(2\)) when \(a \le d\) and \(c > b\), and the pair (true, \(2\)) when \(a \le d\) and \(c \le b\); the number is the count of endpoint comparisons evaluated.
def overlapsWithCost (left right : Interval) : Bool × Nat :=
match Int.decLe left.low right.high with
| .isFalse _ => (false, 1)
| .isTrue _ =>
match Int.decLe right.low left.high with
| .isFalse _ => (false, 2)
| .isTrue _ => (true, 2)structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 1 · Used by 7
TheoremThe instrumented overlap test returns the plain result#✓fully proved
For intervals \(I\) and \(J\), the Boolean component of the instrumented overlap test of \(I\) against \(J\) equals the overlap test of \(I\) against \(J\).
@[simp] theorem overlapsWithCost_fst (left right : Interval) :
(left.overlapsWithCost right).1 = left.overlaps rightstructure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 3 · Used by 4
TheoremComparison count of the overlap test#✓fully proved
For intervals \(I\) and \(J\), the instrumented overlap test of \(I\) against \(J\) reports \(2\) endpoint comparisons when the low endpoint of \(I\) is at most the high endpoint of \(J\), and \(1\) comparison otherwise.
theorem overlapsWithCost_snd (left right : Interval) :
(left.overlapsWithCost right).2 = if left.low ≤ right.high then 2 else 1structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 2 · Used by 1
Interval Tree
StructureInterval tree entry#✓fully proved
An entry of the interval tree consists of an identifier, which is a natural number, and an interval with integer low and high endpoints.
Identifiers, rather than endpoints, are meant to be unique among stored entries; this is required by the indexed tree's representation invariant, not by the entry itself.
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqstructure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
Uses 1 · Used by 69
Entry
DefinitionSearch key of an interval entry#✓fully proved
The key of an entry is the pair \((\ell, i) \in \mathbb{Z} \times \mathbb{N}\), where \(\ell\) is the low endpoint of the entry's interval and \(i\) is the entry's identifier.
def key (entry : Entry) : Int × Nat :=
(entry.interval.low, entry.id)structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 2 · Used by 24
Interval Tree
DefinitionLexicographic comparison of keys#✓fully proved
For keys \((a, i)\) and \((b, j)\) in \(\mathbb{Z} \times \mathbb{N}\) (a low endpoint and an occurrence identifier), the comparison returns less-than if \(a < b\), or if \(a = b\) and \(i < j\); greater-than if \(a > b\), or if \(a = b\) and \(i > j\); and equal if \(a = b\) and \(i = j\).
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqUsed by 23
StructureOperation cost counters for interval trees#✓fully proved
A cost record for the interval tree consists of seven natural-number counters, each defaulting to \(0\): node visits, key comparisons, endpoint comparisons, cached-maximum reads, cache writes, rotations, and identifier-index operations.
The cached-maximum counter is deliberately narrow: it counts only the reads made by search pruning, one per visited node where the left subtree's cached maximum decides the descent. Node construction, rebalancing and the rotations read cached heights, sizes and maxima while rebuilding nodes; those reads are not counted separately, and maintenance work is reported through the cache write, rotation and remaining counters instead.
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqUsed by 35
InductiveInterval tree#✓fully proved
An interval tree is either empty or a node consisting of a left subtree, an entry, a right subtree and three cached fields: a height and a size (natural numbers) and a maximum high endpoint (an integer). The type imposes no balance or consistency condition on these fields; it is the carrier on which the AVL interval-tree operations act.
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqstructure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 1 · Used by 69
Tree
DefinitionCached maximum of an interval tree#✓fully proved
The cached maximum of an interval tree is no value when the tree is empty, and when the tree is a node it is the integer stored in the node's cached maximum-high-endpoint field.
It is read in constant time. The tree type itself does not require this field to equal the largest high endpoint of an interval in the subtree.
def cachedMax? : Tree → Option Int
| .empty => none
| .node _ _ maxHigh _ _ _ => some maxHighinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 2 · Used by 7
DefinitionMaximum with an optional value#✓fully proved
For an integer \(a\) and an optional integer \(v\), the value is \(a\) when \(v\) is absent and \(\max(a, v)\) when \(v\) is present. It combines a value with an optional subtree maximum without using a sentinel value.
DefinitionMaximum high endpoint at a node#✓fully proved
For subtrees \(L\) and \(R\) and an entry \(e\), the node maximum is the largest of the high endpoint of the interval of \(e\), the cached maximum high endpoint stored at the root of \(L\), and the one stored at the root of \(R\), where an empty subtree stores no cached maximum and contributes nothing.
def nodeMax (left : Tree) (entry : Entry) (right : Tree) : Int :=
maxWith (maxWith entry.interval.high left.cachedMax?) right.cachedMax?inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
def maxWith (fallback : Int) : Option Int → Int
| none => fallback
| some value => max fallback valueCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:199
Uses 5 · Used by 6
DefinitionNode construction with repaired metadata#✓fully proved
For an interval tree \(T\) write \(h(T)\) and \(|T|\) for its cached height and size, both \(0\) for the empty tree. Given interval trees \(L\) and \(R\) and an entry \(e\), this builds the node with left subtree \(L\), entry \(e\) and right subtree \(R\) whose cached height is \(\max(h(L), h(R)) + 1\), whose cached size is \(|L| + |R| + 1\), and whose cached maximum high endpoint is the largest of the high endpoint of \(e\) and the cached maxima of the nonempty subtrees among \(L\) and \(R\).
It is the sole ordinary node constructor.
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
def nodeMax (left : Tree) (entry : Entry) (right : Tree) : Int :=
maxWith (maxWith entry.interval.high left.cachedMax?) right.cachedMax?CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:204
Uses 3 · Used by 35
DefinitionCache invariant of an interval tree#✓fully proved
An interval tree satisfies the cache invariant when every cached field is exact, recursively. The empty tree satisfies it. A node with stored height \(h\), stored size \(s\), stored maximum \(m\), left subtree \(L\), entry \(e\) and right subtree \(R\) satisfies it when \(L\) and \(R\) satisfy it, \(m\) is at least the high endpoint of every entry of \(L\), of \(e\) and of every entry of \(R\), \(m\) equals the high endpoint of one of these entries, \(h = \max(\operatorname{height} L, \operatorname{height} R) + 1\) and \(s = \operatorname{size} L + \operatorname{size} R + 1\). Here the height and size of a subtree are its stored fields, and the empty tree has height and size \(0\).
def CacheInvariant : Tree → Prop
| .empty => True
| .node storedHeight storedSize maxHigh left entry right =>
left.CacheInvariant ∧ right.CacheInvariant ∧
(∀ stored ∈ left.entries ++ entry :: right.entries,
stored.interval.high ≤ maxHigh) ∧
(∃ stored ∈ left.entries ++ entry :: right.entries,
stored.interval.high = maxHigh) ∧
storedHeight = max left.height right.height + 1 ∧
storedSize = left.size + right.size + 1inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 3 · Used by 17
DefinitionLow-endpoint ordered interval tree#✓fully proved
The empty tree is low-endpoint ordered, and a node is low-endpoint ordered when both of its subtrees are low-endpoint ordered, every interval in the left subtree has low endpoint at most the low endpoint of the node's interval, and the node's low endpoint is at most the low endpoint of every interval in the right subtree.
def LowOrdered : Tree → Prop
| .empty => True
| .node _ _ _ left entry right =>
left.LowOrdered ∧ right.LowOrdered ∧
(∀ stored ∈ left.entries, stored.interval.low ≤ entry.interval.low) ∧
(∀ stored ∈ right.entries, entry.interval.low ≤ stored.interval.low)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
DefinitionValidity invariant of an interval tree#✓fully proved
A tree satisfies the validity invariant when every interval stored in it is valid, that is, its low endpoint is at most its high endpoint. Recursively, the empty tree satisfies it, and a node satisfies it when its left subtree does, the interval of its entry is valid, and its right subtree does.
def ValidInvariant : Tree → Prop
| .empty => True
| .node _ _ _ left entry right =>
left.ValidInvariant ∧ entry.interval.Valid ∧ right.ValidInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 4 · Used by 11
DefinitionRight rotation#✓fully proved
Write \(\langle L, x, R\rangle\) for a node with left subtree \(L\), entry \(x\) and right subtree \(R\). The right rotation sends \(\langle\langle a, x, b\rangle, y, c\rangle\) to \(\langle a, x, \langle b, y, c\rangle\rangle\), where both nodes of the result get freshly recomputed height, size and maximum high endpoint. Every tree not of this shape is returned unchanged.
def rotateRight : Tree → Tree
| .node _ _ _ (.node _ _ _ a x b) y c =>
mkNode a x (mkNode b y c)
| tree => treeinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 3 · Used by 17
DefinitionLeft rotation#✓fully proved
Write \(\langle L, x, R\rangle\) for a node with left subtree \(L\), entry \(x\) and right subtree \(R\). The left rotation sends \(\langle a, x, \langle b, y, c\rangle\rangle\) to \(\langle\langle a, x, b\rangle, y, c\rangle\), where both nodes of the result get freshly recomputed height, size and maximum high endpoint. Every tree not of this shape is returned unchanged.
def rotateLeft : Tree → Tree
| .node _ _ _ a x (.node _ _ _ b y c) =>
mkNode (mkNode a x b) y c
| tree => treeinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 3 · Used by 17
DefinitionLeft-right double rotation#✓fully proved
Write \(\langle L, x, R\rangle\) for a node with left subtree \(L\), entry \(x\) and right subtree \(R\). The left-right rotation sends \(\langle\langle a, x, \langle b, y, c\rangle\rangle, z, d\rangle\) to \(\langle\langle a, x, b\rangle, y, \langle c, z, d\rangle\rangle\), where all three nodes of the result get freshly recomputed height, size and maximum high endpoint. Every tree not of this shape is returned unchanged.
def rotateLeftRight : Tree → Tree
| .node _ _ _ (.node _ _ _ a x (.node _ _ _ b y c)) z d =>
mkNode (mkNode a x b) y (mkNode c z d)
| tree => treeinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 3 · Used by 17
DefinitionRight-left double rotation#✓fully proved
Write \(\langle L, x, R\rangle\) for a node with left subtree \(L\), entry \(x\) and right subtree \(R\). The right-left rotation sends \(\langle a, x, \langle\langle b, y, c\rangle, z, d\rangle\rangle\) to \(\langle\langle a, x, b\rangle, y, \langle c, z, d\rangle\rangle\), where all three nodes of the result get freshly recomputed height, size and maximum high endpoint. Every tree not of this shape is returned unchanged.
def rotateRightLeft : Tree → Tree
| .node _ _ _ a x (.node _ _ _ (.node _ _ _ b y c) z d) =>
mkNode (mkNode a x b) y (mkNode c z d)
| tree => treeinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 3 · Used by 17
DefinitionAVL rebalancing step with cost#✓fully proved
Rebalancing a tree \(T\) returns a tree and a cost, where heights are the stored heights. If \(T\) is empty, or neither subtree of its root is more than one taller than the other, it returns \(T\) unchanged with zero cost. If the left subtree \(L\) is more than one taller than the right subtree, it applies a right rotation, costing \(2\) cache writes and one rotation, when the left child of \(L\) is at least as tall as the right child of \(L\), and otherwise a left-right double rotation, costing \(3\) cache writes and two rotations. If the right subtree \(R\) is more than one taller than the left subtree, it applies a left rotation, costing \(2\) cache writes and one rotation, when the right child of \(R\) is at least as tall as the left child of \(R\), and otherwise a right-left double rotation, costing \(3\) cache writes and two rotations. All other cost counters are zero.
Cslib.Algorithms.Lean.IntervalTree.Tree.rebalanceWithCost · 22 lines
def rebalanceWithCost (tree : Tree) : Tree × Cost :=
match tree with
| .empty => (.empty, {})
| .node _ _ _ left _ right =>
if left.height > right.height + 1 then
match left with
| .empty => (tree, {})
| .node _ _ _ ll _ lr =>
if ll.height ≥ lr.height then
(rotateRight tree, { cacheWrites := 2, rotations := 1 })
else
(rotateLeftRight tree, { cacheWrites := 3, rotations := 2 })
else if right.height > left.height + 1 then
match right with
| .empty => (tree, {})
| .node _ _ _ rl _ rr =>
if rr.height ≥ rl.height then
(rotateLeft tree, { cacheWrites := 2, rotations := 1 })
else
(rotateRightLeft tree, { cacheWrites := 3, rotations := 2 })
else
(tree, {})inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
def rotateRight : Tree → Tree
| .node _ _ _ (.node _ _ _ a x b) y c =>
mkNode a x (mkNode b y c)
| tree => treeCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:254
def rotateLeftRight : Tree → Tree
| .node _ _ _ (.node _ _ _ a x (.node _ _ _ b y c)) z d =>
mkNode (mkNode a x b) y (mkNode c z d)
| tree => treeCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:266
def rotateLeft : Tree → Tree
| .node _ _ _ a x (.node _ _ _ b y c) =>
mkNode (mkNode a x b) y c
| tree => treeCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:260
def rotateRightLeft : Tree → Tree
| .node _ _ _ a x (.node _ _ _ (.node _ _ _ b y c) z d) =>
mkNode (mkNode a x b) y (mkNode c z d)
| tree => treeCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:272
Uses 7 · Used by 24
DefinitionKeyed insertion with cost#✓fully proved
Inserting an entry \(x\) into a tree returns a new tree together with an operation cost; keys (low endpoint, then identifier) are compared lexicographically. Into the empty tree, \(x\) is inserted as a single node, at a cost of one node visit and one cache write. At a node with entry \(y\): if the key of \(x\) equals the key of \(y\), then \(y\) is replaced by \(x\), at a cost of one node visit, one key comparison and one cache write; if the key of \(x\) is smaller (respectively larger), then \(x\) is inserted recursively into the left (respectively right) subtree, the node is rebuilt with recomputed metadata and rebalanced, and the cost is the cost of the recursive insertion, plus one node visit, one key comparison and one cache write, plus the cost of rebalancing.
Cslib.Algorithms.Lean.IntervalTree.Tree.insertKeyWithCost · 20 lines
def insertKeyWithCost (newEntry : Entry) : Tree → Tree × Cost
| .empty =>
(singleton newEntry, { nodeVisits := 1, cacheWrites := 1 })
| .node _ _ _ left entry right =>
match compareKey newEntry.key entry.key with
| .lt =>
let (newLeft, childCost) := insertKeyWithCost newEntry left
let (result, balanceCost) := rebalanceWithCost (mkNode newLeft entry right)
(result,
childCost + { nodeVisits := 1, keyComparisons := 1, cacheWrites := 1 } +
balanceCost)
| .eq =>
(mkNode left newEntry right,
{ nodeVisits := 1, keyComparisons := 1, cacheWrites := 1 })
| .gt =>
let (newRight, childCost) := insertKeyWithCost newEntry right
let (result, balanceCost) := rebalanceWithCost (mkNode left entry newRight)
(result,
childCost + { nodeVisits := 1, keyComparisons := 1, cacheWrites := 1 } +
balanceCost)structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
def singleton (entry : Entry) : Tree :=
mkNode .empty entry .emptyCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:212
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
def rebalanceWithCost (tree : Tree) : Tree × Cost :=
match tree with
| .empty => (.empty, {})
| .node _ _ _ left _ right =>
if left.height > right.height + 1 then
match left with
| .empty => (tree, {})
| .node _ _ _ ll _ lr =>
if ll.height ≥ lr.height then
(rotateRight tree, { cacheWrites := 2, rotations := 1 })
else
(rotateLeftRight tree, { cacheWrites := 3, rotations := 2 })
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:278
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 7 · Used by 7
DefinitionRemoving the leftmost entry, with its cost#✓fully proved
Removing the leftmost entry of an interval tree \(T\) returns nothing when \(T\) is empty. When the root's left subtree is empty, it returns the root entry, the right subtree, and a cost of one node visit. Otherwise it removes the leftmost entry \(m\) of the left subtree recursively (returning nothing if that fails), rebuilds the root node over the new left subtree with recomputed height, size and maximum high endpoint, and rebalances that node; it returns \(m\), the rebalanced tree, and the cost of the recursive call plus one node visit and one cache write plus the cost of rebalancing.
def removeMinWithCost :
Tree → Option (Entry × Tree × Cost)
| .empty => none
| .node _ _ _ .empty entry right =>
some (entry, right, { nodeVisits := 1 })
| .node _ _ _ left entry right =>
match removeMinWithCost left with
| none => none
| some (minimum, newLeft, childCost) =>
let (result, balanceCost) := rebalanceWithCost (mkNode newLeft entry right)
some (minimum, result,
childCost + { nodeVisits := 1, cacheWrites := 1 } + balanceCost)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
def rebalanceWithCost (tree : Tree) : Tree × Cost :=
match tree with
| .empty => (.empty, {})
| .node _ _ _ left _ right =>
if left.height > right.height + 1 then
match left with
| .empty => (tree, {})
| .node _ _ _ ll _ lr =>
if ll.height ≥ lr.height then
(rotateRight tree, { cacheWrites := 2, rotations := 1 })
else
(rotateLeftRight tree, { cacheWrites := 3, rotations := 2 })
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:278
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 5 · Used by 14
DefinitionKeyed erasure with cost#✓fully proved
Erasing a key \(k \in \mathbb{Z} \times \mathbb{N}\) from an interval tree returns a new tree together with its cost; the key of an entry is the pair of its low endpoint and identifier, and keys are compared lexicographically. The empty tree is returned unchanged at a cost of one node visit. At a node with entry \(x\), the key \(k\) is compared with the key of \(x\). If \(k\) is smaller, \(k\) is erased from the left subtree; if it is larger, from the right subtree; in both cases the node is rebuilt with the new subtree and rebalanced, and the cost is the subtree's cost plus one node visit, one key comparison, one cache write and the rebalancing cost. If \(k\) equals the key of \(x\) and the right subtree is empty (so it has no leftmost entry to remove), the result is the left subtree at a cost of one node visit and one key comparison. Otherwise the leftmost entry of the right subtree is removed and takes the place of \(x\), the node is rebuilt and rebalanced, and the cost is the removal's cost plus one node visit, one key comparison, one cache write and the rebalancing cost.
Cslib.Algorithms.Lean.IntervalTree.Tree.eraseKeyWithCost · 26 lines
def eraseKeyWithCost (key : Int × Nat) : Tree → Tree × Cost
| .empty => (.empty, { nodeVisits := 1 })
| .node _ _ _ left entry right =>
match compareKey key entry.key with
| .lt =>
let (newLeft, childCost) := eraseKeyWithCost key left
let (result, balanceCost) := rebalanceWithCost (mkNode newLeft entry right)
(result,
childCost + { nodeVisits := 1, keyComparisons := 1, cacheWrites := 1 } +
balanceCost)
| .gt =>
let (newRight, childCost) := eraseKeyWithCost key right
let (result, balanceCost) := rebalanceWithCost (mkNode left entry newRight)
(result,
childCost + { nodeVisits := 1, keyComparisons := 1, cacheWrites := 1 } +
balanceCost)
| .eq =>
match right.removeMinWithCost with
| none =>
(left, { nodeVisits := 1, keyComparisons := 1 })
| some (successor, newRight, childCost) =>
let (result, balanceCost) := rebalanceWithCost (mkNode left successor newRight)
(result,
childCost +
{ nodeVisits := 1, keyComparisons := 1, cacheWrites := 1 } +
balanceCost)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
def rebalanceWithCost (tree : Tree) : Tree × Cost :=
match tree with
| .empty => (.empty, {})
| .node _ _ _ left _ right =>
if left.height > right.height + 1 then
match left with
| .empty => (tree, {})
| .node _ _ _ ll _ lr =>
if ll.height ≥ lr.height then
(rotateRight tree, { cacheWrites := 2, rotations := 1 })
else
(rotateLeftRight tree, { cacheWrites := 3, rotations := 2 })
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:278
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 8 · Used by 9
DefinitionInstrumented overlap search#✓fully proved
Given a query interval \(q = [c, d]\) and an interval tree \(T\), the instrumented overlap search returns an optional entry together with a cost record, defined by recursion on \(T\). On the empty tree it returns no entry and records one node visit. At a node with left subtree \(L\), entry \(e\) with interval \([a, b]\) and right subtree \(R\), it first tests overlap by evaluating \(a \le d\) and, only if that holds, \(c \le b\); let \(k \in \{1, 2\}\) be the number of relations evaluated. If both hold, it returns \(e\) and records one node visit and \(k\) endpoint comparisons. Otherwise, if \(L\) is empty, it returns the result of searching \(R\), adding one node visit and \(k\) endpoint comparisons to that search's cost. If \(L\) is nonempty with cached maximum high endpoint \(m\), it returns the result of searching \(L\) when \(c \le m\) and of searching \(R\) otherwise, adding one node visit, \(k + 1\) endpoint comparisons and one cached-maximum read to that search's cost. No other counter is ever incremented.
Cslib.Algorithms.Lean.IntervalTree.Tree.searchWithCost · 20 lines
def searchWithCost (query : Interval) : Tree → Option Entry × Cost
| .empty => (none, { nodeVisits := 1 })
| .node _ _ _ left entry right =>
let (overlap, endpointCost) := entry.interval.overlapsWithCost query
if overlap then
(some entry, { nodeVisits := 1, endpointComparisons := endpointCost })
else
match left.cachedMax? with
| none =>
let (answer, childCost) := searchWithCost query right
(answer, childCost + { nodeVisits := 1, endpointComparisons := endpointCost })
| some leftMax =>
if query.low ≤ leftMax then
let (answer, childCost) := searchWithCost query left
(answer, childCost +
{ nodeVisits := 1, endpointComparisons := endpointCost + 1, maxCacheReads := 1 })
else
let (answer, childCost) := searchWithCost query right
(answer, childCost +
{ nodeVisits := 1, endpointComparisons := endpointCost + 1, maxCacheReads := 1 })structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 6 · Used by 7
TheoremInstrumented search in the empty tree#✓fully proved
For every query interval \(q\), the instrumented overlap search of \(q\) in the empty interval tree returns no entry, and its cost record counts one node visit and zero for every other counter (key comparisons, endpoint comparisons, cached-maximum reads, cache writes, rotations and index operations).
@[simp] theorem searchWithCost_empty (query : Interval) :
searchWithCost query .empty = (none, { nodeVisits := 1 })structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
def searchWithCost (query : Interval) : Tree → Option Entry × Cost
| .empty => (none, { nodeVisits := 1 })
| .node _ _ _ left entry right =>
let (overlap, endpointCost) := entry.interval.overlapsWithCost query
if overlap then
(some entry, { nodeVisits := 1, endpointComparisons := endpointCost })
else
match left.cachedMax? with
| none =>
let (answer, childCost) := searchWithCost query right
(answer, childCost + { nodeVisits := 1, endpointComparisons := endpointCost })
| some leftMax =>
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:435
Uses 5
TheoremInstrumented search in a one-entry tree#✓fully proved
Let \(e\) be an entry whose interval is \([a, b]\), let \(q = [c, d]\) be a query interval, and let \(k = 2\) if \(a \le d\) and \(k = 1\) otherwise. Consider the single-node tree built from \(e\) with empty subtrees and exact cached fields. If \([a, b]\) and \([c, d]\) overlap (that is, \(a \le d\) and \(c \le b\)), the instrumented overlap search of \(q\) in this tree returns \(e\) with a cost record of one node visit and \(k\) endpoint comparisons. Otherwise it returns no entry with a cost record of two node visits (the root and its empty right subtree) and \(k\) endpoint comparisons. All other counters are zero in both cases.
theorem searchWithCost_singleton (entry : Entry) (query : Interval) :
searchWithCost query (singleton entry) =
if entry.interval.overlaps query then
(some entry,
{ nodeVisits := 1
endpointComparisons := if entry.interval.low ≤ query.high then 2 else 1 })
else
(none,
{ nodeVisits := 2
endpointComparisons := if entry.interval.low ≤ query.high then 2 else 1 })structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
def searchWithCost (query : Interval) : Tree → Option Entry × Cost
| .empty => (none, { nodeVisits := 1 })
| .node _ _ _ left entry right =>
let (overlap, endpointCost) := entry.interval.overlapsWithCost query
if overlap then
(some entry, { nodeVisits := 1, endpointComparisons := endpointCost })
else
match left.cachedMax? with
| none =>
let (answer, childCost) := searchWithCost query right
(answer, childCost + { nodeVisits := 1, endpointComparisons := endpointCost })
| some leftMax =>
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:435
def singleton (entry : Entry) : Tree :=
mkNode .empty entry .emptyCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:212
DefinitionInterval-tree overlap search#✓fully proved
The overlap search of a query interval \(q\) in an interval tree \(T\) returns the optional entry produced by the instrumented overlap search of \(q\) in \(T\), discarding its cost record.
def search (tree : Tree) (query : Interval) : Option Entry :=
(tree.searchWithCost query).1inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 5 · Used by 4
DefinitionLinear-scan overlap search#✓fully proved
For a tree \(T\) and a query interval \(q\), the oracle search returns the first entry, in the in-order list of entries of \(T\), whose interval overlaps \(q\) as closed intervals, and returns nothing when no entry's interval overlaps \(q\).
It is a separate full-traversal oracle used only by specifications and tests.
def oracleSearch (tree : Tree) (query : Interval) : Option Entry :=
tree.entries.find? fun entry => entry.interval.overlaps queryinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 4
TheoremCompleteness of interval-tree search#✓fully proved
Let \(T\) be an interval tree whose cached height, size and maximum high endpoint are exact at every node, and whose low endpoints respect the search order (at every node, low endpoints in the left subtree are at most the node's, and those in the right subtree at least the node's). If some entry stored in \(T\) has an interval that overlaps the query interval \(Q\) (each interval's low endpoint is at most the other's high endpoint), then searching \(T\) for \(Q\) returns some entry.
theorem search_complete {tree : Tree} {query : Interval} {witness : Entry}
(cache : tree.CacheInvariant) (ordered : tree.LowOrdered)
(member : witness ∈ tree.entries)
(overlap : witness.interval.Overlaps query) :
∃ found, tree.search query = some foundinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 13 · Used by 2
TheoremInterval-tree search fails exactly when nothing overlaps#✓fully proved
Let \(T\) be an interval tree whose cached height, size and maximum high endpoint are exact at every node, and whose low endpoints respect the search order (at every node, low endpoints in the left subtree are at most the node's, and those in the right subtree at least the node's). Then searching \(T\) for a query interval \(Q\) returns nothing if and only if no entry stored in \(T\) has an interval that overlaps \(Q\) (each interval's low endpoint is at most the other's high endpoint).
theorem search_eq_none_iff {tree : Tree} {query : Interval}
(cache : tree.CacheInvariant) (ordered : tree.LowOrdered) :
tree.search query = none ↔
∀ entry ∈ tree.entries, ¬entry.interval.Overlaps queryinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
DefinitionExecutable cache check for interval trees#✓fully proved
The Boolean cache check returns true on the empty tree. On a node with stored height \(h\), stored size \(s\), stored maximum \(m\), left subtree \(L\), entry \(e\) and right subtree \(R\) it returns true exactly when \(h = \max(\operatorname{height} L, \operatorname{height} R) + 1\), \(s = \operatorname{size} L + \operatorname{size} R + 1\), \(m\) is the largest of the high endpoint of \(e\) and the cached maxima of those of \(L\) and \(R\) that are nonempty, and the check returns true on both \(L\) and \(R\). Here the height and size of a subtree are its stored fields, and the empty tree has height and size \(0\).
It is used only by the executable invariant checker.
def cacheOK : Tree → Bool
| .empty => true
| .node storedHeight storedSize storedMax left entry right =>
storedHeight == max left.height right.height + 1 &&
storedSize == left.size + right.size + 1 &&
storedMax == nodeMax left entry right &&
left.cacheOK && right.cacheOKinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def nodeMax (left : Tree) (entry : Entry) (right : Tree) : Int :=
maxWith (maxWith entry.interval.high left.cachedMax?) right.cachedMax?CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:204
Uses 3 · Used by 3
DefinitionKey between optional bounds#✓fully proved
Given an optional lower bound, an optional upper bound and a key \(k\) (a pair of an integer and a natural number), this test returns true exactly when the lower bound is absent or strictly below \(k\), and the upper bound is absent or strictly above \(k\). Keys are compared lexicographically: first by the integer, then by the natural number.
def keyBetween
(lower upper : Option (Int × Nat)) (key : Int × Nat) : Bool :=
lower.all (fun value => compareKey value key == .lt) &&
upper.all (fun value => compareKey key value == .lt)def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
Uses 1 · Used by 3
DefinitionOrdered-and-valid check for interval trees#✓fully proved
Keys of entries are pairs (low endpoint, identifier), ordered lexicographically. Given optional lower and upper key bounds \(\ell\) and \(u\), the check accepts the empty tree, and accepts a node with left subtree \(L\), entry \(e\) and right subtree \(R\) exactly when the key \(k\) of \(e\) is strictly greater than \(\ell\) if \(\ell\) is present and strictly less than \(u\) if \(u\) is present, the interval of \(e\) has low endpoint at most its high endpoint, \(L\) is accepted with bounds \(\ell\) and \(k\), and \(R\) is accepted with bounds \(k\) and \(u\).
def orderedValid :
Option (Int × Nat) → Option (Int × Nat) → Tree → Bool
| _, _, .empty => true
| lower, upper, .node _ _ _ left entry right =>
keyBetween lower upper entry.key && entry.interval.valid &&
orderedValid lower (some entry.key) left &&
orderedValid (some entry.key) upper rightinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def keyBetween
(lower upper : Option (Int × Nat)) (key : Int × Nat) : Bool :=
lower.all (fun value => compareKey value key == .lt) &&
upper.all (fun value => compareKey key value == .lt)CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:615
Uses 6 · Used by 5
DefinitionBoolean AVL balance check for interval trees#✓fully proved
The balance check returns true on the empty tree. On a node whose left and right subtrees have stored heights \(h_L\) and \(h_R\) (the empty tree has height \(0\)), it returns true exactly when the node's stored height equals \(\max(h_L, h_R) + 1\), \(h_L \le h_R + 1\), \(h_R \le h_L + 1\), and the check returns true on both subtrees.
def balanced : Tree → Bool
| .empty => true
| .node storedHeight _ _ left _ right =>
storedHeight == max left.height right.height + 1 &&
left.height ≤ right.height + 1 && right.height ≤ left.height + 1 &&
left.balanced && right.balancedinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 2 · Used by 2
DefinitionAVL balance of an interval tree#✓fully proved
An interval tree is AVL balanced with exact stored heights when it is empty, or when it is a node such that, writing \(h_L\) and \(h_R\) for the stored heights of its left and right subtrees (the empty tree has height \(0\)), the node's stored height equals \(\max(h_L, h_R) + 1\), \(h_L \le h_R + 1\), \(h_R \le h_L + 1\), and both subtrees are again AVL balanced with exact stored heights.
def BalancedProp : Tree → Prop
| .empty => True
| .node storedHeight _ _ left _ right =>
storedHeight = max left.height right.height + 1 ∧
left.height ≤ right.height + 1 ∧ right.height ≤ left.height + 1 ∧
left.BalancedProp ∧ right.BalancedPropinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 2 · Used by 10
DefinitionKey-ordered interval tree#✓fully proved
The empty tree is key-ordered, and a node is key-ordered when both of its subtrees are key-ordered, the key of every entry in the left subtree is strictly less than the key of the node's entry, and the key of the node's entry is strictly less than the key of every entry in the right subtree. Keys are compared lexicographically: low endpoint first, then identifier.
def KeyOrdered : Tree → Prop
| .empty => True
| .node _ _ _ left entry right =>
left.KeyOrdered ∧ right.KeyOrdered ∧
(∀ e ∈ left.entries, compareKey e.key entry.key = .lt) ∧
(∀ e ∈ right.entries, compareKey entry.key e.key = .lt)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
Uses 4 · Used by 14
TheoremThe executable ordering check implies key ordering#✓fully proved
Let \(t\) be an interval tree and let \(\ell\) and \(u\) be optional keys in \(\mathbb{Z} \times \mathbb{N}\). If the executable ordering check of \(t\) with lower bound \(\ell\) and upper bound \(u\) succeeds, then \(t\) is key-ordered, and every entry \(e\) stored in \(t\) satisfies \(\ell < \operatorname{key}(e)\) when \(\ell\) is present and \(\operatorname{key}(e) < u\) when \(u\) is present, where \(<\) is the lexicographic order on keys (low endpoint first, then identifier).
theorem keyOrdered_of_orderedValid {lower upper : Option (Int × Nat)}
{tree : Tree} (h : tree.orderedValid lower upper = true) :
tree.KeyOrdered ∧
∀ e ∈ tree.entries,
(∀ v ∈ lower, compareKey v e.key = .lt) ∧
∀ v ∈ upper, compareKey e.key v = .ltinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
Uses 9 · Used by 2
TheoremThe executable ordering check implies low-endpoint ordering#✓fully proved
Let \(t\) be an interval tree and let \(\ell\) and \(u\) be optional keys in \(\mathbb{Z} \times \mathbb{N}\). If the executable ordering check of \(t\) with lower bound \(\ell\) and upper bound \(u\) succeeds, then \(t\) is low-endpoint ordered, and every entry \(e\) stored in \(t\) satisfies \(\ell < \operatorname{key}(e)\) when \(\ell\) is present and \(\operatorname{key}(e) < u\) when \(u\) is present, where \(<\) is the lexicographic order on keys (low endpoint first, then identifier).
theorem lowOrdered_of_orderedValid {lower upper : Option (Int × Nat)}
{tree : Tree} (h : tree.orderedValid lower upper = true) :
tree.LowOrdered ∧
∀ e ∈ tree.entries,
(∀ v ∈ lower, compareKey v e.key = .lt) ∧
∀ v ∈ upper, compareKey e.key v = .ltinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
TheoremThe ordering check implies interval validity#✓fully proved
Let \(T\) be an interval tree and let \(\ell\) and \(u\) be optional lower and upper key bounds. If the executable check of \(T\) with bounds \(\ell\) and \(u\), which tests that every key lies strictly between its bounds and that every stored interval passes the Boolean validity test, returns true, then every interval stored in \(T\) is valid, that is, its low endpoint is at most its high endpoint.
theorem validInvariant_of_orderedValid {lower upper : Option (Int × Nat)}
{tree : Tree} (h : tree.orderedValid lower upper = true) :
tree.ValidInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 9 · Used by 1
TheoremRemoving the minimum preserves the other entries#✓fully proved
If removing the leftmost entry of a tree \(T\) returns an entry \(m\), a tree \(T'\) and a cost, then the list consisting of \(m\) followed by the in-order entries of \(T'\) is a permutation of the in-order entries of \(T\).
theorem removeMinWithCost_entries_perm {tree : Tree} {minimum : Entry}
{rest : Tree} {cost : Cost}
(h : tree.removeMinWithCost = some (minimum, rest, cost)) :
(minimum :: rest.entries).Perm tree.entriesinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 10 · Used by 1
TheoremEntries after keyed insertion#✓fully proved
Let \(t\) be a tree whose entries are strictly ordered by key, and let \(x\) be an entry. The in-order list of entries of the tree obtained by inserting \(x\) into \(t\) by key is a permutation of the list consisting of \(x\) followed by those entries of \(t\) whose key differs from the key of \(x\).
theorem insertKeyWithCost_entries_perm (newEntry : Entry) {tree : Tree}
(hord : tree.KeyOrdered) :
((tree.insertKeyWithCost newEntry).1.entries).Perm
(newEntry :: tree.entries.filter (fun e => e.key ≠ newEntry.key))structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 13 · Used by 1
TheoremKeyed erasure removes exactly the entries with that key#✓fully proved
The key of an entry is the pair \((\ell, i) \in \mathbb{Z} \times \mathbb{N}\) of its low endpoint \(\ell\) and identifier \(i\); keys are compared lexicographically. Let \(T\) be an interval tree whose keys are strictly ordered (every key in a left subtree is lexicographically below its node's key and every key in a right subtree is above it), and let \(k \in \mathbb{Z} \times \mathbb{N}\) be a key. Then the in-order list of entries of the tree obtained by erasing \(k\) from \(T\) is a permutation of the in-order list of entries of \(T\) with every entry of key \(k\) removed.
theorem eraseKeyWithCost_entries_perm (key : Int × Nat) {tree : Tree}
(hord : tree.KeyOrdered) :
((tree.eraseKeyWithCost key).1.entries).Perm
(tree.entries.filter (fun e => e.key ≠ key))inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 15 · Used by 2
TheoremStrictly key-ordered trees have distinct keys#✓fully proved
If a tree is strictly ordered by key, then the keys of its stored entries are pairwise distinct.
theorem keyNodup_of_keyOrdered {tree : Tree} (hord : tree.KeyOrdered) :
(tree.entries.map Entry.key).Nodupinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
def key (entry : Entry) : Int × Nat :=
(entry.interval.low, entry.id)CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:122
Uses 5 · Used by 3
TheoremThe removed minimum has the least key#✓fully proved
Let \(T\) be a key-ordered interval tree: at every node, the keys in the left subtree are strictly smaller and those in the right subtree strictly larger than the node's key, where the key of an entry is the pair (low endpoint, identifier) compared lexicographically. If removing the leftmost entry of \(T\) returns the entry \(m\) (together with the remaining tree and a cost record), then every entry \(e\) stored in \(T\) is either \(m\) itself or has a key strictly larger than the key of \(m\).
theorem removeMinWithCost_min_le {tree : Tree} {minimum : Entry}
{rest : Tree} {cost : Cost}
(h : tree.removeMinWithCost = some (minimum, rest, cost))
(hord : tree.KeyOrdered) :
∀ e ∈ tree.entries, e = minimum ∨
compareKey minimum.key e.key = .ltinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
def compareKey (left right : Int × Nat) : Ordering :=
if left.1 < right.1 then .lt
else if right.1 < left.1 then .gt
else if left.2 < right.2 then .lt
else if right.2 < left.2 then .gt
else .eqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:128
Uses 9 · Used by 1
TheoremInsertion into an interval tree preserves key ordering#✓fully proved
Let \(t\) be a key-ordered interval tree and let \(e\) be an entry. Then the tree returned by the cost-instrumented keyed insertion of \(e\) into \(t\) (which replaces the entry with the same key, if there is one; the reported cost is discarded) is again key-ordered.
theorem keyOrdered_insertKeyWithCost (newEntry : Entry) {tree : Tree}
(hord : tree.KeyOrdered) :
(tree.insertKeyWithCost newEntry).1.KeyOrderedstructure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 13 · Used by 1
TheoremRemoving the minimum from an interval tree preserves key ordering#✓fully proved
Let \(t\) be a key-ordered interval tree. If the cost-instrumented removal of the leftmost entry of \(t\) succeeds, returning that entry, a remaining tree \(t'\) and a cost, then \(t'\) is key-ordered.
theorem keyOrdered_removeMinWithCost {tree : Tree} {minimum : Entry}
{rest : Tree} {cost : Cost}
(h : tree.removeMinWithCost = some (minimum, rest, cost))
(hord : tree.KeyOrdered) : rest.KeyOrderedinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 13 · Used by 1
TheoremDeletion from an interval tree preserves key ordering#✓fully proved
Let \(t\) be a key-ordered interval tree and let \(k \in \mathbb{Z} \times \mathbb{N}\) be a key. Then the tree returned by the cost-instrumented keyed deletion of \(k\) from \(t\) (the reported cost is discarded) is again key-ordered.
theorem keyOrdered_eraseKeyWithCost (key : Int × Nat) {tree : Tree}
(hord : tree.KeyOrdered) :
(tree.eraseKeyWithCost key).1.KeyOrderedinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 17 · Used by 2
TheoremRebalancing an interval-tree node with exact stored height restores AVL balance#✓fully proved
Let \(L\) and \(R\) be interval trees that are AVL balanced with exact stored heights, with heights \(h_L\) and \(h_R\) satisfying \(h_L \le h_R + 2\) and \(h_R \le h_L + 2\). Let \(N\) be a node with left subtree \(L\), entry \(e\) and right subtree \(R\) whose stored height is \(\max(h_L, h_R) + 1\) (its stored size and stored maximum are arbitrary), and let \(B\) be the tree obtained by rebalancing \(N\) (the tree component of the result; the cost is ignored). Then \(B\) is AVL balanced with exact stored heights, the height of \(B\) is \(\max(h_L, h_R) + 1\) or \(\max(h_L, h_R)\), and it is \(\max(h_L, h_R)\) only if \(h_L = h_R + 2\) or \(h_R = h_L + 2\).
theorem balancedProp_rebalance_node {sh ss : Nat} {mm : Int}
{l : Tree} {e : Entry} {r : Tree}
(hstored : sh = max l.height r.height + 1)
(hl : l.BalancedProp) (hr : r.BalancedProp)
(hbal : l.height ≤ r.height + 2 ∧ r.height ≤ l.height + 2) :
(rebalanceWithCost (.node sh ss mm l e r)).1.BalancedProp ∧
((rebalanceWithCost (.node sh ss mm l e r)).1.height =
max l.height r.height + 1 ∨
(rebalanceWithCost (.node sh ss mm l e r)).1.height + 1 =
max l.height r.height + 1) ∧
((rebalanceWithCost (.node sh ss mm l e r)).1.height + 1 =
max l.height r.height + 1 →
l.height = r.height + 2 ∨ r.height = l.height + 2)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
def rebalanceWithCost (tree : Tree) : Tree × Cost :=
match tree with
| .empty => (.empty, {})
| .node _ _ _ left _ right =>
if left.height > right.height + 1 then
match left with
| .empty => (tree, {})
| .node _ _ _ ll _ lr =>
if ll.height ≥ lr.height then
(rotateRight tree, { cacheWrites := 2, rotations := 1 })
else
(rotateLeftRight tree, { cacheWrites := 3, rotations := 2 })
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:278
Uses 10 · Used by 1
TheoremRebalancing a rebuilt interval-tree node restores AVL balance#✓fully proved
Let \(L\) and \(R\) be interval trees that are AVL balanced with exact stored heights, with heights \(h_L\) and \(h_R\) satisfying \(h_L \le h_R + 2\) and \(h_R \le h_L + 2\), and let \(e\) be an entry. Let \(B\) be the tree obtained by rebalancing the node that the smart constructor builds from \(L\), \(e\) and \(R\) (the tree component of the result; the cost is ignored). Then \(B\) is AVL balanced with exact stored heights, the height of \(B\) is \(\max(h_L, h_R) + 1\) or \(\max(h_L, h_R)\), and it is \(\max(h_L, h_R)\) only if \(h_L = h_R + 2\) or \(h_R = h_L + 2\).
theorem balancedProp_rebalance_mkNode {l : Tree} {e : Entry} {r : Tree}
(hl : l.BalancedProp) (hr : r.BalancedProp)
(hbal : l.height ≤ r.height + 2 ∧ r.height ≤ l.height + 2) :
(rebalanceWithCost (mkNode l e r)).1.BalancedProp ∧
((rebalanceWithCost (mkNode l e r)).1.height =
max l.height r.height + 1 ∨
(rebalanceWithCost (mkNode l e r)).1.height + 1 =
max l.height r.height + 1) ∧
((rebalanceWithCost (mkNode l e r)).1.height + 1 =
max l.height r.height + 1 →
l.height = r.height + 2 ∨ r.height = l.height + 2)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
def rebalanceWithCost (tree : Tree) : Tree × Cost :=
match tree with
| .empty => (.empty, {})
| .node _ _ _ left _ right =>
if left.height > right.height + 1 then
match left with
| .empty => (tree, {})
| .node _ _ _ ll _ lr =>
if ll.height ≥ lr.height then
(rotateRight tree, { cacheWrites := 2, rotations := 1 })
else
(rotateLeftRight tree, { cacheWrites := 3, rotations := 2 })
⋯CSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:278
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 8 · Used by 3
TheoremKeyed insertion preserves AVL balance in an interval tree#✓fully proved
Let \(T\) be an interval tree that is AVL balanced with exact stored heights, and let \(e\) be an entry. The tree \(T'\) returned by keyed insertion of \(e\) into \(T\) (which replaces an entry with the same key, if there is one; we take the tree component of the result and ignore the cost) is again AVL balanced with exact stored heights, and the height of \(T'\) is either the height of \(T\) or one more.
theorem balancedProp_insertKeyWithCost (newEntry : Entry) {tree : Tree}
(hb : tree.BalancedProp) :
(tree.insertKeyWithCost newEntry).1.BalancedProp ∧
((tree.insertKeyWithCost newEntry).1.height = tree.height ∨
(tree.insertKeyWithCost newEntry).1.height = tree.height + 1)structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 10 · Used by 1
TheoremRemoving the minimum preserves AVL balance in an interval tree#✓fully proved
Let \(T\) be an interval tree that is AVL balanced with exact stored heights. If removing the leftmost entry of \(T\) succeeds and returns an entry \(m\), a remaining tree \(R\) and a cost \(c\), then \(R\) is AVL balanced with exact stored heights, and the height of \(R\) is either the height of \(T\) or one less.
theorem balancedProp_removeMinWithCost {tree : Tree} {minimum : Entry}
{rest : Tree} {cost : Cost}
(h : tree.removeMinWithCost = some (minimum, rest, cost))
(hb : tree.BalancedProp) :
rest.BalancedProp ∧
(rest.height = tree.height ∨ rest.height + 1 = tree.height)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 8 · Used by 1
TheoremKeyed deletion preserves AVL balance in an interval tree#✓fully proved
Let \(T\) be an interval tree that is AVL balanced with exact stored heights, and let \(k\) be a key (a pair of an integer low endpoint and a natural-number identifier). The tree \(T'\) returned by keyed deletion of \(k\) from \(T\) (the tree component of the result; the cost is ignored) is again AVL balanced with exact stored heights, and the height of \(T'\) is either the height of \(T\) or one less.
theorem balancedProp_eraseKeyWithCost (key : Int × Nat) {tree : Tree}
(hb : tree.BalancedProp) :
(tree.eraseKeyWithCost key).1.BalancedProp ∧
((tree.eraseKeyWithCost key).1.height = tree.height ∨
(tree.eraseKeyWithCost key).1.height + 1 = tree.height)inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 16 · Used by 2
TheoremNode construction preserves interval validity#✓fully proved
If \(L\) and \(R\) are interval trees satisfying the validity invariant and \(e\) is an entry whose interval \([a, b]\) satisfies \(a \le b\), then the node with left subtree \(L\), entry \(e\) and right subtree \(R\), built by the node constructor that recomputes the cached fields, satisfies the validity invariant.
theorem validInvariant_mkNode {left right : Tree} {entry : Entry}
(hl : left.ValidInvariant) (he : entry.interval.Valid)
(hr : right.ValidInvariant) :
(mkNode left entry right).ValidInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 6 · Used by 3
TheoremStored intervals of a valid tree are valid#✓fully proved
If an interval tree \(T\) satisfies the validity invariant, then every entry stored in \(T\) has an interval \([a, b]\) with \(a \le b\).
theorem validInvariant_mem {tree : Tree} (hv : tree.ValidInvariant)
(e : Entry) (he : e ∈ tree.entries) : e.interval.Validinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 5 · Used by 1
TheoremKeyed insertion preserves interval validity#✓fully proved
Let \(T\) be an interval tree in which every stored interval \([a, b]\) satisfies \(a \le b\), and let \(e\) be an entry whose interval \([a, b]\) satisfies \(a \le b\). Then the tree returned by keyed insertion of \(e\) into \(T\) also has every stored interval \([a, b]\) satisfying \(a \le b\).
theorem validInvariant_insertKeyWithCost (newEntry : Entry)
(hnew : newEntry.interval.Valid) {tree : Tree}
(hv : tree.ValidInvariant) :
(tree.insertKeyWithCost newEntry).1.ValidInvariantstructure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 16 · Used by 1
TheoremRemoving the minimum preserves interval validity#✓fully proved
Let \(T\) be an interval tree in which every stored interval is valid (its low endpoint is at most its high endpoint). If the instrumented removal of the leftmost entry of \(T\) succeeds, returning that entry \(m\), the remaining tree \(T'\) and a cost record \(c\), then every interval stored in \(T'\) is valid.
theorem validInvariant_removeMinWithCost {tree : Tree} {minimum : Entry}
{rest : Tree} {cost : Cost}
(h : tree.removeMinWithCost = some (minimum, rest, cost))
(hv : tree.ValidInvariant) : rest.ValidInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 14 · Used by 1
TheoremKeyed erasure preserves interval validity#✓fully proved
Let \(T\) be an interval tree in which every stored interval \([a, b]\) satisfies \(a \le b\). Then for every key \((\ell, i)\) with \(\ell\) an integer and \(i\) a natural number, the tree returned by keyed erasure of \((\ell, i)\) from \(T\) also has every stored interval \([a, b]\) satisfying \(a \le b\).
theorem validInvariant_eraseKeyWithCost (key : Int × Nat) {tree : Tree}
(hv : tree.ValidInvariant) :
(tree.eraseKeyWithCost key).1.ValidInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 19 · Used by 2
Interval Tree
StructureIndexed interval tree#✓fully proved
An indexed interval tree consists of a root interval tree together with an identifier index: a finite map, implemented as a balanced search tree, from natural-number identifiers to integer low endpoints.
structure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat Intinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 1 · Used by 11
Indexed Interval Tree
DefinitionInsertion by identifier with cost#✓fully proved
Let \(T\) be an indexed interval tree and let \(e\) be an entry with identifier \(i\) and interval \([a, b]\). Inserting \(e\) into \(T\) first tests \(a \le b\). If \(a > b\), it returns no tree, at a cost of one endpoint comparison. Otherwise, if the identifier index of \(T\) maps \(i\) to a low endpoint \(\ell\), the entry with key \((\ell, i)\) is erased from the root tree of \(T\) by keyed erasure; if \(i\) is not in the index, the root tree is kept, at zero cost. Then \(e\) is inserted into the resulting tree by keyed insertion. The result is the indexed interval tree with this new root tree and with the index updated to map \(i\) to \(a\), and the cost is the cost of the erasure plus the cost of the insertion plus one endpoint comparison and two index operations.
def insertWithCost
(tree : IndexedIntervalTree) (entry : Entry) : Option IndexedIntervalTree × Cost :=
if entry.interval.valid then
let (withoutOld, eraseCost) :=
match tree.idIndex.get? entry.id with
| none => (tree.root, ({} : Cost))
| some oldLow => tree.root.eraseKeyWithCost (oldLow, entry.id)
let (newRoot, insertCost) := withoutOld.insertKeyWithCost entry
(some ⟨newRoot, tree.idIndex.insert entry.id entry.interval.low⟩,
eraseCost + insertCost +
{ endpointComparisons := 1, indexOperations := 2 })
else
(none, { endpointComparisons := 1 })structure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 8 · Used by 1
DefinitionErasure by identifier with cost#✓fully proved
To erase identifier \(i\) from an indexed interval tree, look \(i\) up in the identifier index. If it is absent, the tree is returned unchanged at a cost of one index operation. If the index maps \(i\) to a low endpoint \(\ell\), the entry with key \((\ell, i)\) is erased from the underlying interval tree, \(i\) is removed from the index, and the cost is the cost of the keyed erasure plus two index operations.
When the representation invariant holds, this deletes exactly the stored entry with identifier \(i\).
def eraseWithCost (tree : IndexedIntervalTree) (id : Nat) : IndexedIntervalTree × Cost :=
match tree.idIndex.get? id with
| none => (tree, { indexOperations := 1 })
| some low =>
let (newRoot, eraseCost) := tree.root.eraseKeyWithCost (low, id)
(⟨newRoot, tree.idIndex.erase id⟩,
eraseCost + { indexOperations := 2 })structure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 4 · Used by 1
DefinitionForward identifier-index check#✓fully proved
For an indexed interval tree, the forward index check returns true exactly when the identifier index maps the identifier of every stored entry to the low endpoint of that entry's interval.
def indexForwardOK (tree : IndexedIntervalTree) : Bool :=
tree.root.entries.all fun entry =>
tree.idIndex.get? entry.id == some entry.interval.lowstructure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
Uses 4 · Used by 2
DefinitionBackward identifier-index check#✓fully proved
For an indexed interval tree, the backward index check returns true exactly when, for every identifier \(i\) that the identifier index maps to a low endpoint \(\ell\), some stored entry has identifier \(i\) and an interval with low endpoint \(\ell\).
def indexBackwardOK (tree : IndexedIntervalTree) : Bool :=
tree.idIndex.toList.all fun pair =>
tree.root.entries.any fun entry =>
entry.id == pair.1 && entry.interval.low == pair.2structure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
Uses 4 · Used by 2
DefinitionRepresentation check for the indexed interval tree#✓fully proved
For an indexed interval tree, the check returns true exactly when all of the following hold: at every node the cached height and size agree with the values recomputed from its children's cached heights and sizes, and the cached maximum high endpoint equals the largest of the node's own high endpoint and its children's cached maxima; the tree is AVL-balanced (sibling heights differ by at most one) with exact stored heights; the entry keys (low endpoint, identifier), ordered lexicographically, are strictly ordered as a binary search tree and every stored interval has low endpoint at most its high endpoint; the identifiers of the stored entries are pairwise distinct; the identifier index maps the identifier of every stored entry to that entry's low endpoint; and every identifier and low endpoint paired by the index belong to some stored entry.
def check (tree : IndexedIntervalTree) : Bool :=
tree.root.cacheOK && tree.root.balanced &&
tree.root.orderedValid none none && tree.root.uniqueIds &&
tree.indexForwardOK && tree.indexBackwardOKstructure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
DefinitionRepresentation invariant of an indexed interval tree#✓fully proved
An indexed interval tree \(T\) satisfies the representation invariant when its root tree has exact cached metadata (heights, sizes, and attained maximum high endpoints), is strictly ordered by the composite key (low endpoint, then identifier), is AVL balanced with exact stored heights, and stores only valid intervals; the identifiers of the stored entries are pairwise distinct; the identifier index maps the identifier of every stored entry to that entry's low endpoint; and every pair \((i, \ell)\) in the identifier index is the identifier and low endpoint of some stored entry.
The ordering of low endpoints used by search follows from the strict key ordering.
def Invariant (tree : IndexedIntervalTree) : Prop :=
tree.root.CacheInvariant ∧ tree.root.KeyOrdered ∧ tree.root.BalancedProp ∧
tree.root.ValidInvariant ∧
(tree.root.entries.map (·.id)).Nodup ∧
(∀ e ∈ tree.root.entries, tree.idIndex.get? e.id = some e.interval.low) ∧
∀ p ∈ tree.idIndex.toList,
∃ e ∈ tree.root.entries, e.id = p.1 ∧ e.interval.low = p.2structure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
Uses 8 · Used by 4
Tree
TheoremThe interval-tree smart constructor preserves the cache invariant#✓fully proved
If interval trees \(L\) and \(R\) satisfy the cache invariant (every cached maximum high endpoint, height and size is exact), then for every entry \(e\) the node that the smart constructor builds from \(L\), \(e\) and \(R\) also satisfies the cache invariant.
theorem cacheInvariant_mkNode {left right : Tree} (entry : Entry)
(leftCache : left.CacheInvariant) (rightCache : right.CacheInvariant) :
(mkNode left entry right).CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
def mkNode (left : Tree) (entry : Entry) (right : Tree) : Tree :=
.node (max left.height right.height + 1) (left.size + right.size + 1)
(nodeMax left entry right) left entry rightCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:208
Uses 8 · Used by 8
TheoremThe executable cache check implies the cache invariant#✓fully proved
If the executable cache check returns true on an interval tree \(t\), then \(t\) satisfies the cache invariant.
theorem cacheInvariant_of_cacheOK {tree : Tree} (checked : tree.cacheOK = true) :
tree.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 8 · Used by 1
TheoremRight rotation preserves the interval-tree cache invariant#✓fully proved
If an interval tree \(t\) satisfies the cache invariant, then so does the right rotation of \(t\), which leaves \(t\) unchanged when \(t\) is empty or has an empty left subtree.
theorem cacheInvariant_rotateRight {tree : Tree} (cache : tree.CacheInvariant) :
tree.rotateRight.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 7 · Used by 1
TheoremLeft rotation preserves the interval-tree cache invariant#✓fully proved
If an interval tree \(t\) satisfies the cache invariant, then so does the left rotation of \(t\), which leaves \(t\) unchanged when \(t\) is empty or has an empty right subtree.
theorem cacheInvariant_rotateLeft {tree : Tree} (cache : tree.CacheInvariant) :
tree.rotateLeft.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 7 · Used by 1
TheoremLeft-right rotation preserves the interval-tree cache invariant#✓fully proved
If an interval tree \(t\) satisfies the cache invariant, then so does the left-right double rotation of \(t\), which leaves \(t\) unchanged unless \(t\) has a nonempty left subtree whose right subtree is nonempty.
theorem cacheInvariant_rotateLeftRight {tree : Tree} (cache : tree.CacheInvariant) :
tree.rotateLeftRight.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 7 · Used by 1
TheoremRight-left rotation preserves the interval-tree cache invariant#✓fully proved
If an interval tree \(t\) satisfies the cache invariant, then so does the right-left double rotation of \(t\), which leaves \(t\) unchanged unless \(t\) has a nonempty right subtree whose left subtree is nonempty.
theorem cacheInvariant_rotateRightLeft {tree : Tree} (cache : tree.CacheInvariant) :
tree.rotateRightLeft.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 7 · Used by 1
TheoremRebalancing preserves the interval-tree cache invariant#✓fully proved
If an interval tree \(t\) satisfies the cache invariant, then the tree returned by the rebalancing step at the root of \(t\) also satisfies the cache invariant.
theorem cacheInvariant_rebalanceWithCost {tree : Tree} (cache : tree.CacheInvariant) :
tree.rebalanceWithCost.1.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 13 · Used by 3
TheoremKeyed insertion preserves the interval-tree cache invariant#✓fully proved
Let \(T\) be an interval tree satisfying the cache invariant (every cached maximum high endpoint, height and size is exact), and let \(e\) be an entry. The tree returned by keyed insertion of \(e\) into \(T\) (the tree component of the result; the cost is ignored) also satisfies the cache invariant. This includes the case where an entry with the same key is replaced.
theorem cacheInvariant_insertKeyWithCost (newEntry : Entry) {tree : Tree}
(cache : tree.CacheInvariant) :
(tree.insertKeyWithCost newEntry).1.CacheInvariantstructure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
inductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 12 · Used by 1
TheoremRemoving the minimum preserves the interval-tree cache invariant#✓fully proved
Let \(t\) be an interval tree that satisfies the cache invariant. If removing the leftmost entry of \(t\) succeeds and returns an entry, a tree \(t'\) and an operation cost, then \(t'\) satisfies the cache invariant.
theorem cacheInvariant_removeMinWithCost {tree : Tree} (cache : tree.CacheInvariant) :
∀ {minimum : Entry} {result : Tree} {cost : Cost},
tree.removeMinWithCost = some (minimum, result, cost) → result.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
structure Cost where
nodeVisits : Nat := 0
keyComparisons : Nat := 0
endpointComparisons : Nat := 0
/-- Cached-maximum reads performed by search pruning only; see `Cost`. -/
maxCacheReads : Nat := 0
cacheWrites : Nat := 0
rotations : Nat := 0
indexOperations : Nat := 0
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:145
Uses 14 · Used by 1
TheoremKeyed deletion preserves the interval-tree cache invariant#✓fully proved
Let \(T\) be an interval tree satisfying the cache invariant (every cached maximum high endpoint, height and size is exact), and let \(k\) be a key (a pair of an integer low endpoint and a natural-number identifier). The tree returned by keyed deletion of \(k\) from \(T\) (the tree component of the result; the cost is ignored) also satisfies the cache invariant. This includes keys that do not occur in \(T\).
theorem cacheInvariant_eraseKeyWithCost (key : Int × Nat) {tree : Tree}
(cache : tree.CacheInvariant) : (tree.eraseKeyWithCost key).1.CacheInvariantinductive Tree where
| empty
| node
(height : Nat)
(size : Nat)
(maxHigh : Int)
(left : Tree)
(entry : Entry)
(right : Tree)
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:172
Uses 14 · Used by 2
Indexed Interval Tree
TheoremSoundness of the invariant checker#✓fully proved
If the executable checker returns true on an indexed interval tree \(T\), then \(T\) satisfies the representation invariant.
theorem invariant_of_check {tree : IndexedIntervalTree}
(h : tree.check = true) : tree.Invariantstructure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
Uses 20
TheoremSoundness of indexed interval-tree search#✓fully proved
The search of an indexed interval tree \(T\) for a query interval \(q = [c, d]\) returns nothing when \(c > d\), and otherwise returns the entry, if any, found by the instrumented overlap search of \(q\) in the root tree of \(T\). For every indexed interval tree \(T\), every query interval \(q\) and every entry \(e\), if this search returns \(e\), then \(e\) is one of the entries stored in the root tree of \(T\) and the interval of \(e\) overlaps \(q\).
The representation invariant of \(T\) is not needed.
theorem search_sound {tree : IndexedIntervalTree}
{query : Interval} {found : Entry}
(h : tree.search query = some found) :
found ∈ tree.root.entries ∧ found.interval.Overlaps querystructure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
TheoremCompleteness of indexed interval search#✓fully proved
Let \(T\) be an indexed interval tree satisfying its representation invariant, and let \(Q\) be a valid query interval (low endpoint at most high endpoint). If some entry stored in \(T\) has an interval that overlaps \(Q\) (each interval's low endpoint is at most the other's high endpoint), then searching \(T\) for \(Q\) returns some entry.
theorem search_complete_of_invariant {tree : IndexedIntervalTree}
(inv : tree.Invariant) {query : Interval} (hvalid : query.valid = true)
{witness : Entry} (member : witness ∈ tree.root.entries)
(overlap : witness.interval.Overlaps query) :
∃ found, tree.search query = some foundstructure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
structure Interval where
low : Int
high : Int
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:37
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 18
TheoremCorrectness of insertion into an indexed interval tree#✓fully proved
Let \(T\) be an indexed interval tree satisfying the representation invariant, and let \(x\) be an entry whose interval is valid (its low endpoint is at most its high endpoint). If inserting \(x\) into \(T\) succeeds with result \(T'\), then \(T'\) satisfies the representation invariant, \(x\) is stored in the root tree of \(T'\), and an entry \(e\) is stored in the root tree of \(T'\) if and only if either \(e = x\), or \(e\) is stored in the root tree of \(T\) and the identifier of \(e\) differs from the identifier of \(x\).
theorem insert_spec {tree : IndexedIntervalTree} (inv : tree.Invariant)
{entry : Entry} (hvalid : entry.interval.valid = true)
{result : IndexedIntervalTree} (hres : tree.insert entry = some result) :
result.Invariant ∧ entry ∈ result.root.entries ∧
∀ e, e ∈ result.root.entries ↔
e = entry ∨ (e ∈ tree.root.entries ∧ e.id ≠ entry.id)structure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
structure Entry where
id : Nat
interval : Interval
deriving Repr, DecidableEqCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:114
Uses 35
TheoremCorrectness of erasure from the indexed interval tree#✓fully proved
Let \(T\) be an indexed interval tree satisfying the representation invariant, and let \(i\) be a natural number. Then the tree obtained by erasing identifier \(i\) from \(T\) again satisfies the invariant, and an entry is stored in it if and only if it is stored in \(T\) and its identifier differs from \(i\).
In particular, if no stored entry has identifier \(i\), the stored entries are unchanged.
theorem erase_spec {tree : IndexedIntervalTree} (inv : tree.Invariant)
(id : Nat) :
(tree.erase id).Invariant ∧
∀ e, e ∈ (tree.erase id).root.entries ↔
e ∈ tree.root.entries ∧ e.id ≠ idstructure IndexedIntervalTree where
root : Tree
idIndex : Std.TreeMap Nat IntCSLibExt/Algorithms/Lean/DataStructures/IntervalTree.lean:2227
Uses 27
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.