Treap

51 fully proved

Treap

InductiveTreap trees#✓fully proved

For a type \(\kappa\) of keys and a type \(\nu\) of values, a treap tree is either empty or a node made of a left subtree, a key in \(\kappa\), a value in \(\nu\), a natural-number priority and a right subtree. Trees are finite, and no ordering of keys or priorities is imposed; the treap invariants are stated separately.

public inductive Tree (κ : Type u) (ν : Type v) where
  | empty
  | node (left : Tree κ ν) (key : κ) (value : ν) (priority : Nat)
      (right : Tree κ ν)
  deriving DecidableEq, Repr

Used by 50

Used byTreap predicate holding at every node · Treap all-nodes predicate via node membership · Treap all-nodes predicate on keys via key membership · Treap inorder contents · Treap inorder traversal onto a suffix · Treap inorder contents after erasure · Treap inorder contents after insertion · Treap merge concatenates inorder contents · Treap inorder contents of a node · Treap inorder contents split at a pivot · Treap deletion · Heap order of treap priorities · Merging preserves heap order · Treap split preserves heap order · The root of a heap-ordered tree has minimal priority · Treap insertion · Keys occurring in the inorder contents · Inorder key list of a treap · Inorder keys of a node · Treap keys are distinct · Treap lookup · Treap lookup agrees with the inorder contents · Treap lookup finds exactly the stored entries · Erased keys are not found · Treap lookup after insertion · Lookup with cost · Lookup cost is at most the tree size · Costed lookup returns the ordinary lookup result · Inorder contents list the treap's entries · Key membership in a treap tree · Keys of a merged treap · Entry membership implies key membership in a treap · The inorder key list lists exactly the keys of a treap · Entry membership in a treap tree · Treap merge · Ordered treap tree · Inorder keys of an ordered treap are strictly increasing · Treap merge preserves search-tree order · Treap split preserves search-tree order · Root priority of a treap tree · Separated treap trees · Size of a treap tree · Treap split · Split bounds for an ordered treap · Result of a treap split · Valid treap · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Merging separated treaps preserves validity · Splitting a treap preserves validity

Tree

DefinitionTreap predicate holding at every node#✓fully proved

Let \(p\) be a predicate on a key, a value and a natural-number priority. A tree satisfies \(p\) at every node when \(p(k, v, n)\) holds for the key \(k\), value \(v\) and priority \(n\) of each of its nodes. By recursion, this holds for the empty tree, and holds for a node exactly when it holds for the left subtree, \(p\) holds at the node's key, value and priority, and it holds for the right subtree.

public def AllNodes {κ : Type u} {ν : Type v} (p : κ → ν → Nat → Prop) :
    Tree κ ν → Prop
  | .empty => True
  | .node left key value priority right =>
      AllNodes p left ∧ p key value priority ∧ AllNodes p right

Uses 1 · Used by 15

Statement usesTreap trees

Used byTreap all-nodes predicate via node membership · Treap all-nodes predicate on keys via key membership · Heap order of treap priorities · Merging preserves heap order · Treap split preserves heap order · The root of a heap-ordered tree has minimal priority · Treap lookup finds exactly the stored entries · Erased keys are not found · Ordered treap tree · Inorder keys of an ordered treap are strictly increasing · Treap merge preserves search-tree order · Treap split preserves search-tree order · Split bounds for an ordered treap · Erasing from a treap preserves validity · Inserting into a treap preserves validity

DefinitionEntry membership in a treap tree#✓fully proved

A key \(k\), value \(v\) and priority \(p\) form an entry of a treap tree when some node stores exactly \(k\), \(v\) and \(p\): the empty tree has no entries, and \((k, v, p)\) is an entry of a node with left subtree \(L\), root key \(r\), root value \(w\), root priority \(q\) and right subtree \(R\) exactly when it is an entry of \(L\), or \(k = r\), \(v = w\) and \(p = q\), or it is an entry of \(R\).

public def MemNode {κ : Type u} {ν : Type v} (key : κ) (value : ν)
    (priority : Nat) : Tree κ ν → Prop
  | .empty => False
  | .node left rootKey rootValue rootPriority right =>
      MemNode key value priority left ∨
        (key = rootKey ∧ value = rootValue ∧ priority = rootPriority) ∨
        MemNode key value priority right

Uses 1 · Used by 8

Statement usesTreap trees

Used byTreap all-nodes predicate via node membership · Merging preserves heap order · Treap lookup agrees with the inorder contents · Treap lookup finds exactly the stored entries · Inorder contents list the treap's entries · Entry membership implies key membership in a treap · Treap merge preserves search-tree order · Split bounds for an ordered treap

DefinitionKey membership in a treap tree#✓fully proved

A key \(k\) is a key of a treap tree when it is stored at some node: no key belongs to the empty tree, and \(k\) belongs to a node with left subtree \(L\), root key \(r\) and right subtree \(R\) exactly when \(k\) belongs to \(L\), or \(k = r\), or \(k\) belongs to \(R\).

Membership is structural and does not assume the search-tree or heap invariants.

public def MemKey {κ : Type u} {ν : Type v} (key : κ) : Tree κ ν → Prop
  | .empty => False
  | .node left rootKey _ _ right =>
      MemKey key left ∨ key = rootKey ∨ MemKey key right

Uses 1 · Used by 12

Statement usesTreap trees

Used byTreap all-nodes predicate on keys via key membership · Keys occurring in the inorder contents · Treap lookup finds exactly the stored entries · Erased keys are not found · Keys of a merged treap · Entry membership implies key membership in a treap · The inorder key list lists exactly the keys of a treap · Inorder keys of an ordered treap are strictly increasing · Treap merge preserves search-tree order · Separated treap trees · Erasing from a treap preserves validity · Inserting into a treap preserves validity

DefinitionTreap inorder traversal onto a suffix#✓fully proved

For a tree \(t\) and a list \(s\) of key-value pairs, the traversal of \(t\) onto \(s\) is defined by recursion: for the empty tree it is \(s\), and for a node with left subtree \(l\), key \(k\), value \(v\) and right subtree \(r\) it is the traversal of \(l\) onto the list obtained by putting \((k, v)\) in front of the traversal of \(r\) onto \(s\). The result is the key-value pairs of \(t\) in inorder, priorities dropped, followed by \(s\).

No ancestor recopies a completed traversal, so the traversal takes linear time.

public def contentsAux {κ : Type u} {ν : Type v} :
    Tree κ ν → List (κ × ν) → List (κ × ν)
  | .empty, suffix => suffix
  | .node left key value _ right, suffix =>
      contentsAux left ((key, value) :: contentsAux right suffix)

Uses 1 · Used by 5

Statement usesTreap trees

Used byTreap inorder contents · Treap inorder contents after insertion · Treap merge concatenates inorder contents · Treap inorder contents of a node · Treap inorder contents split at a pivot

DefinitionTreap inorder contents#✓fully proved

The contents of a tree \(t\) is the list of its key-value pairs in inorder (left subtree, then node, then right subtree), with priorities dropped. It is defined as the inorder traversal of \(t\) onto the empty list, which takes linear time.

public def contents {κ : Type u} {ν : Type v} (tree : Tree κ ν) : List (κ × ν) :=
  contentsAux tree []

Uses 2 · Used by 12

Statement usesTreap trees · Treap inorder traversal onto a suffix

Used byTreap inorder contents after erasure · Treap inorder contents after insertion · Treap merge concatenates inorder contents · Treap inorder contents of a node · Treap inorder contents split at a pivot · Keys occurring in the inorder contents · Inorder key list of a treap · Inorder keys of a node · Treap lookup agrees with the inorder contents · Erased keys are not found · Treap lookup after insertion · Inorder contents list the treap's entries

TheoremTreap inorder contents of a node#✓fully proved

For trees \(l\) and \(r\), a key \(k\), a value \(v\) and a natural-number priority \(n\), the inorder list of key-value pairs of the node with left subtree \(l\), key \(k\), value \(v\), priority \(n\) and right subtree \(r\) is the inorder list of \(l\), followed by \((k, v)\), followed by the inorder list of \(r\).

public theorem contents_node {κ : Type u} {ν : Type v}
    (left : Tree κ ν) (key : κ) (value : ν) (priority : Nat) (right : Tree κ ν) :
    contents (.node left key value priority right) =
      contents left ++ (key, value) :: contents right

Uses 3 · Used by 6

Statement usesTreap trees · Treap inorder contents

Proof usesTreap inorder traversal onto a suffix

Used byTreap inorder contents after insertion · Treap merge concatenates inorder contents · Treap inorder contents split at a pivot · Keys occurring in the inorder contents · Inorder keys of a node · Inorder contents list the treap's entries

DefinitionSize of a treap tree#✓fully proved

The size of a tree is its number of nodes, computed recursively: the empty tree has size \(0\), and a node with left subtree \(L\) and right subtree \(R\) has size equal to the size of \(L\) plus one plus the size of \(R\).

public def size {κ : Type u} {ν : Type v} : Tree κ ν → Nat
  | .empty => 0
  | .node left _ _ _ right => size left + 1 + size right

Uses 1 · Used by 6

Statement usesTreap trees

Used byTreap merge concatenates inorder contents · Merging preserves heap order · Lookup cost is at most the tree size · Keys of a merged treap · Treap merge · Treap merge preserves search-tree order

DefinitionOrdered treap tree#✓fully proved

For a key type equipped with a relation \(<\), a treap tree is ordered when it is empty, or when it is a node with key \(k\) whose left and right subtrees are both ordered, every key \(x\) in the left subtree satisfies \(x < k\), and every key \(y\) in the right subtree satisfies \(k < y\).

public def Ordered {κ : Type u} {ν : Type v} [LT κ] : Tree κ ν → Prop
  | .empty => True
  | .node left key _ _ right =>
      Ordered left ∧ Ordered right ∧
        AllNodes (fun childKey _ _ => childKey < key) left ∧
        AllNodes (fun childKey _ _ => key < childKey) right

Uses 2 · Used by 14

Statement usesTreap trees · Treap predicate holding at every node

Used byTreap keys are distinct · Treap lookup agrees with the inorder contents · Treap lookup finds exactly the stored entries · Erased keys are not found · Treap lookup after insertion · Inorder keys of an ordered treap are strictly increasing · Treap merge preserves search-tree order · Treap split preserves search-tree order · Split bounds for an ordered treap · Valid treap · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Merging separated treaps preserves validity · Splitting a treap preserves validity

DefinitionHeap order of treap priorities#✓fully proved

A tree is heap-ordered when the priority of every node is at most the priority of every node below it. Recursively, the empty tree is heap-ordered, and a node with priority \(p\) is heap-ordered when its left and right subtrees are heap-ordered and every node in them has priority at least \(p\).

public def HeapOrdered {κ : Type u} {ν : Type v} : Tree κ ν → Prop
  | .empty => True
  | .node left _ _ priority right =>
      HeapOrdered left ∧ HeapOrdered right ∧
        AllNodes (fun _ _ childPriority => priority ≤ childPriority) left ∧
        AllNodes (fun _ _ childPriority => priority ≤ childPriority) right

Uses 2 · Used by 10

Statement usesTreap trees · Treap predicate holding at every node

Used byMerging preserves heap order · Treap split preserves heap order · The root of a heap-ordered tree has minimal priority · Erased keys are not found · Treap lookup after insertion · Valid treap · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Merging separated treaps preserves validity · Splitting a treap preserves validity

DefinitionValid treap#✓fully proved

A binary tree whose nodes each carry a key, a value and a natural-number priority, with keys compared by a relation \(<\) (any LT instance; no order axioms are assumed), is a valid treap when it satisfies both of the following at every node: every key in the left subtree is less than the node's key and the node's key is less than every key in the right subtree (search-tree order with respect to \(<\)), and the node's priority is at most the priority of every node in its left and right subtrees (min-heap order on priorities).

public def Valid {κ : Type u} {ν : Type v} [LT κ] (tree : Tree κ ν) : Prop :=
  Ordered tree ∧ HeapOrdered tree

Uses 3 · Used by 6

Statement usesTreap trees · Heap order of treap priorities · Ordered treap tree

Used byErased keys are not found · Treap lookup after insertion · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Merging separated treaps preserves validity · Splitting a treap preserves validity

DefinitionTreap lookup#✓fully proved

Looking up a key \(k\) in a tree with keys in a linearly ordered type follows the binary search tree comparisons. The empty tree gives no value. At a node with key \(r\) and value \(v\), the lookup continues in the left subtree if \(k < r\), continues in the right subtree if \(r < k\), and otherwise returns \(v\).

public def lookup {κ : Type u} {ν : Type v} [LinearOrder κ] (key : κ) :
    Tree κ ν → Option ν
  | .empty => none
  | .node left rootKey value _ right =>
      if key < rootKey then lookup key left
      else if rootKey < key then lookup key right
      else some value

Uses 1 · Used by 5

Statement usesTreap trees

Used byTreap lookup agrees with the inorder contents · Treap lookup finds exactly the stored entries · Erased keys are not found · Treap lookup after insertion · Costed lookup returns the ordinary lookup result

DefinitionLookup with cost#✓fully proved

The costed lookup of a key \(k\) in a tree with keys in a linearly ordered type returns a possibly absent value together with a natural number counting the visited nodes. On the empty tree it returns no value and cost \(0\). At a node with key \(r\) and value \(v\), if \(k < r\) it returns the result of the costed lookup of \(k\) in the left subtree with cost increased by \(1\); if \(r < k\) it does the same with the right subtree; otherwise it returns \(v\) with cost \(1\).

public def lookupWithCost {κ : Type u} {ν : Type v} [LinearOrder κ] (key : κ) :
    Tree κ ν → Option ν × Nat
  | .empty => (none, 0)
  | .node left rootKey value _ right =>
      if key < rootKey then
        let result := lookupWithCost key left
        (result.1, result.2 + 1)
      else if rootKey < key then
        let result := lookupWithCost key right
        (result.1, result.2 + 1)
      else (some value, 1)

Uses 1 · Used by 2

Statement usesTreap trees

Used byLookup cost is at most the tree size · Costed lookup returns the ordinary lookup result

DefinitionRoot priority of a treap tree#✓fully proved

The root priority of a treap tree is an optional natural number: it is absent for the empty tree, and for a node it is the priority stored at that node.

public def rootPriority {κ : Type u} {ν : Type v} : Tree κ ν → Option Nat
  | .empty => none
  | .node _ _ _ priority _ => some priority

Uses 1

Statement usesTreap trees

DefinitionTreap merge#✓fully proved

The merge of two treap trees is defined recursively. Merging the empty tree with a tree \(T\), or \(T\) with the empty tree, gives \(T\). If both trees are nodes, with root priorities \(p\) for the first and \(q\) for the second, then when \(p \le q\) the result keeps the root of the first tree and its left subtree, and its right subtree is the merge of the first tree's right subtree with the second tree; otherwise the result keeps the root of the second tree and its right subtree, and its left subtree is the merge of the first tree with the second tree's left subtree.

public def merge {κ : Type u} {ν : Type v} : Tree κ ν → Tree κ ν → Tree κ ν
  | .empty, right => right
  | left, .empty => left
  | .node leftLeft leftKey leftValue leftPriority leftRight,
      .node rightLeft rightKey rightValue rightPriority rightRight =>
    if leftPriority ≤ rightPriority then
      .node leftLeft leftKey leftValue leftPriority
        (merge leftRight (.node rightLeft rightKey rightValue rightPriority rightRight))
    else
      .node
        (merge (.node leftLeft leftKey leftValue leftPriority leftRight) rightLeft)
        rightKey rightValue rightPriority rightRight
termination_by left right => size left + size right
decreasing_by all_goals (simp_wf; simp [size] <;> omega)

Uses 2 · Used by 9

Statement usesTreap trees · Size of a treap tree

Used byTreap inorder contents after insertion · Treap merge concatenates inorder contents · Treap deletion · Merging preserves heap order · Treap insertion · Keys of a merged treap · Treap merge preserves search-tree order · Inserting into a treap preserves validity · Merging separated treaps preserves validity

StructureResult of a treap split#✓fully proved

For key type \(\kappa\) and value type \(\nu\), a split result consists of a lower tree, an optional entry given by a value in \(\nu\) together with a natural-number priority, and an upper tree, where both trees are treap trees with keys in \(\kappa\) and values in \(\nu\).

The structure imposes no constraint; on an ordered tree, splitting at a pivot fills the lower tree with the keys below the pivot, the upper tree with the keys above it, and the entry with the pivot's value and priority when the pivot occurs.

public structure SplitResult (κ : Type u) (ν : Type v) where
  /-- The subtree containing keys below the pivot. -/
  less : Tree κ ν
  /-- The pivot's value and priority when it was present. -/
  found : Option (ν × Nat)
  /-- The subtree containing keys above the pivot. -/
  greater : Tree κ ν
  deriving DecidableEq, Repr

Uses 1 · Used by 14

Statement usesTreap trees

Used byTreap inorder contents after erasure · Treap inorder contents after insertion · Treap inorder contents split at a pivot · Treap deletion · Treap split preserves heap order · Treap insertion · Erased keys are not found · Treap lookup after insertion · Treap split preserves search-tree order · Treap split · Split bounds for an ordered treap · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Splitting a treap preserves validity

DefinitionTreap split#✓fully proved

Let the keys come from a linear order, and write \((L, k, v, q, R)\) for the node with left subtree \(L\), key \(k\), value \(v\), priority \(q\) and right subtree \(R\). Splitting a tree at a pivot \(p\) returns a split result, defined by recursion on the tree. The empty tree splits into two empty trees and no entry. For a node \((L, k, v, q, R)\): if \(k < p\), split \(R\) at \(p\) into a lower tree \(R_1\), an optional entry \(e\) and an upper tree \(R_2\), and return the lower tree \((L, k, v, q, R_1)\), the entry \(e\) and the upper tree \(R_2\); if \(p < k\), split \(L\) at \(p\) into \(L_1\), \(e\) and \(L_2\), and return the lower tree \(L_1\), the entry \(e\) and the upper tree \((L_2, k, v, q, R)\); otherwise \(k = p\), and return the lower tree \(L\), the entry \((v, q)\) and the upper tree \(R\).

On an ordered tree, the lower tree holds the keys below \(p\), the upper tree holds the keys above \(p\), and the entry is the value and priority stored at \(p\) when \(p\) occurs.

public def split {κ : Type u} {ν : Type v} [LinearOrder κ] (pivot : κ) :
    Tree κ ν → SplitResult κ ν
  | .empty => ⟨.empty, none, .empty⟩
  | .node left key value priority right =>
      if key < pivot then
        let result := split pivot right
        ⟨.node left key value priority result.less, result.found, result.greater⟩
      else if pivot < key then
        let result := split pivot left
        ⟨result.less, result.found,
          .node result.greater key value priority right⟩
      else ⟨left, some (value, priority), right⟩

Uses 2 · Used by 13

Statement usesTreap trees · Result of a treap split

Used byTreap inorder contents after erasure · Treap inorder contents after insertion · Treap inorder contents split at a pivot · Treap deletion · Treap split preserves heap order · Treap insertion · Erased keys are not found · Treap lookup after insertion · Treap split preserves search-tree order · Split bounds for an ordered treap · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Splitting a treap preserves validity

DefinitionTreap insertion#✓fully proved

For a key \(k\) of a linearly ordered key type, a value \(v\), a priority \(p\) and a tree \(t\), inserting \(k\) with value \(v\) and priority \(p\) into \(t\) splits \(t\) at \(k\), drops the entry the split finds at \(k\) if any, merges the part below \(k\) with the single node \((k, v, p)\), and then merges the result with the part above \(k\); all merges are priority-guided.

public def insert {κ : Type u} {ν : Type v} [LinearOrder κ] (key : κ)
    (value : ν) (priority : Nat) (tree : Tree κ ν) : Tree κ ν :=
  let result := split key tree
  merge (merge result.less (.node .empty key value priority .empty)) result.greater

Uses 4 · Used by 3

Statement usesTreap trees · Result of a treap split · Treap merge · Treap split

Used byTreap inorder contents after insertion · Treap lookup after insertion · Inserting into a treap preserves validity

DefinitionTreap deletion#✓fully proved

For a key \(k\) of a linearly ordered key type and a tree \(t\), deleting \(k\) from \(t\) splits \(t\) at \(k\) and returns the priority-guided merge of the part of the split below \(k\) with the part above \(k\); the entry the split finds at \(k\), if any, is dropped.

public def erase {κ : Type u} {ν : Type v} [LinearOrder κ] (key : κ)
    (tree : Tree κ ν) : Tree κ ν :=
  let result := split key tree
  merge result.less result.greater

Uses 4 · Used by 3

Statement usesTreap trees · Result of a treap split · Treap merge · Treap split

Used byTreap inorder contents after erasure · Erased keys are not found · Erasing from a treap preserves validity

TheoremTreap all-nodes predicate via node membership#✓fully proved

Let \(p\) be a predicate on a key, a value and a natural-number priority, and let \(t\) be a tree. Then \(p\) holds at every node of \(t\) if and only if \(p(k, v, n)\) holds for every key \(k\), value \(v\) and priority \(n\) such that the entry \((k, v, n)\) occurs as a node of \(t\).

public theorem allNodes_iff_forall_mem {κ : Type u} {ν : Type v}
    {p : κ → ν → Nat → Prop} {tree : Tree κ ν} :
    AllNodes p tree ↔ ∀ key value priority, MemNode key value priority tree →
      p key value priority

Uses 3 · Used by 3

Statement usesTreap trees · Treap predicate holding at every node · Entry membership in a treap tree

Used byMerging preserves heap order · Treap merge preserves search-tree order · Split bounds for an ordered treap

TheoremEntry membership implies key membership in a treap#✓fully proved

If a key \(k\), value \(v\) and priority \(p\) form an entry of a treap tree \(t\), that is, some node of \(t\) stores exactly \(k\), \(v\) and \(p\), then \(k\) is a key of \(t\).

public theorem memKey_of_memNode {κ : Type u} {ν : Type v} {key : κ} {value : ν}
    {priority : Nat} {tree : Tree κ ν} (h : MemNode key value priority tree) :
    key ∈ tree

Uses 3 · Used by 2

Statement usesTreap trees · Key membership in a treap tree · Entry membership in a treap tree

Used byTreap lookup finds exactly the stored entries · Treap merge preserves search-tree order

TheoremInorder contents list the treap's entries#✓fully proved

For every tree \(t\), key \(k\) and value \(v\), the pair \((k, v)\) occurs in the inorder key-value list of \(t\) if and only if \(t\) has a node with key \(k\) and value \(v\), for some priority.

public theorem mem_contents {κ : Type u} {ν : Type v} {key : κ} {value : ν}
    {tree : Tree κ ν} :
    (key, value) ∈ contents tree ↔ ∃ priority, MemNode key value priority tree

Uses 4 · Used by 1

Statement usesTreap trees · Entry membership in a treap tree · Treap inorder contents

Proof usesTreap inorder contents of a node

Used byTreap lookup agrees with the inorder contents

TheoremKeys occurring in the inorder contents#✓fully proved

For a key \(k\) and a tree \(t\), some pair \((k, v)\) occurs in the inorder list of key-value pairs of \(t\) if and only if \(k\) is the key of some node of \(t\).

public theorem key_mem_contents {κ : Type u} {ν : Type v} {key : κ}
    {tree : Tree κ ν} :
    (∃ value, (key, value) ∈ contents tree) ↔ key ∈ tree

Uses 4 · Used by 1

Statement usesTreap trees · Key membership in a treap tree · Treap inorder contents

Proof usesTreap inorder contents of a node

Used byErased keys are not found

TheoremTreap all-nodes predicate on keys via key membership#✓fully proved

Let \(p\) be a predicate on keys and let \(t\) be a tree. Then the key of every node of \(t\) satisfies \(p\) if and only if \(p(k)\) holds for every key \(k\) that occurs in \(t\).

public theorem allNodes_key_iff {κ : Type u} {ν : Type v} {p : κ → Prop}
    {tree : Tree κ ν} :
    AllNodes (fun key _ _ => p key) tree ↔ ∀ key, key ∈ tree → p key

Uses 3 · Used by 5

Statement usesTreap trees · Treap predicate holding at every node · Key membership in a treap tree

Used byTreap lookup finds exactly the stored entries · Erased keys are not found · Inorder keys of an ordered treap are strictly increasing · Erasing from a treap preserves validity · Inserting into a treap preserves validity

DefinitionInorder key list of a treap#✓fully proved

The inorder key list of a tree \(t\) is the list of first components of the inorder list of key-value pairs of \(t\), that is, the keys of \(t\) in inorder.

public def keys {κ : Type u} {ν : Type v} (tree : Tree κ ν) : List κ :=
  (contents tree).map Prod.fst

Uses 2 · Used by 4

Statement usesTreap trees · Treap inorder contents

Used byInorder keys of a node · Treap keys are distinct · The inorder key list lists exactly the keys of a treap · Inorder keys of an ordered treap are strictly increasing

TheoremInorder keys of a node#✓fully proved

For trees \(l\) and \(r\), a key \(k\), a value \(v\) and a priority \(p\), the inorder key list of the node with left subtree \(l\), entry \((k, v, p)\) and right subtree \(r\) is the inorder key list of \(l\), followed by \(k\), followed by the inorder key list of \(r\).

public theorem keys_node {κ : Type u} {ν : Type v}
    (left : Tree κ ν) (key : κ) (value : ν) (priority : Nat) (right : Tree κ ν) :
    keys (.node left key value priority right) =
      keys left ++ key :: keys right

Uses 4 · Used by 2

Statement usesTreap trees · Inorder key list of a treap

Proof usesTreap inorder contents · Treap inorder contents of a node

Used byThe inorder key list lists exactly the keys of a treap · Inorder keys of an ordered treap are strictly increasing

TheoremThe inorder key list lists exactly the keys of a treap#✓fully proved

For every treap tree \(t\) and key \(k\), \(k\) occurs in the inorder key list of \(t\) if and only if \(k\) is a key of \(t\).

public theorem mem_keys {κ : Type u} {ν : Type v} {key : κ} {tree : Tree κ ν} :
    key ∈ keys tree ↔ key ∈ tree

Uses 4 · Used by 1

Statement usesTreap trees · Key membership in a treap tree · Inorder key list of a treap

Proof usesInorder keys of a node

Used byInorder keys of an ordered treap are strictly increasing

TheoremInorder keys of an ordered treap are strictly increasing#✓fully proved

Let the keys come from a linearly ordered type. If a treap tree \(t\) is ordered, then its inorder key list is strictly increasing: each key in the list is smaller than every key after it.

public theorem ordered_keys {κ : Type u} {ν : Type v} [LinearOrder κ]
    {tree : Tree κ ν} (hOrdered : Ordered tree) :
    List.Pairwise (· < ·) (keys tree)

Uses 8 · Used by 1

Statement usesTreap trees · Ordered treap tree · Inorder key list of a treap

Proof usesTreap predicate holding at every node · Key membership in a treap tree · Treap all-nodes predicate on keys via key membership · Inorder keys of a node · The inorder key list lists exactly the keys of a treap

Used byTreap keys are distinct

TheoremTreap keys are distinct#✓fully proved

For a linearly ordered key type, if a tree is ordered as a binary search tree (at every node, every key in the left subtree is smaller and every key in the right subtree is larger than the node's key), then its inorder key list has no duplicates.

public theorem keys_nodup {κ : Type u} {ν : Type v} [LinearOrder κ]
    {tree : Tree κ ν} (hOrdered : Ordered tree) : (keys tree).Nodup

Uses 4

Statement usesTreap trees · Ordered treap tree · Inorder key list of a treap

Proof usesInorder keys of an ordered treap are strictly increasing

TheoremTreap lookup finds exactly the stored entries#✓fully proved

Let \(t\) be a tree with keys in a linearly ordered type that is ordered as a binary search tree (every key in a left subtree is smaller and every key in a right subtree is larger than the node's key). For every key \(k\) and value \(v\), looking up \(k\) in \(t\) returns \(v\) if and only if \(t\) has a node with key \(k\) and value \(v\), for some priority.

public theorem lookup_eq_some_iff {κ : Type u} {ν : Type v} [LinearOrder κ]
    {query : κ} {value : ν} {tree : Tree κ ν} (hOrdered : Ordered tree) :
    lookup query tree = some value ↔ ∃ priority, MemNode query value priority tree

Uses 8 · Used by 1

Statement usesTreap trees · Entry membership in a treap tree · Ordered treap tree · Treap lookup

Proof usesTreap predicate holding at every node · Key membership in a treap tree · Treap all-nodes predicate on keys via key membership · Entry membership implies key membership in a treap

Used byTreap lookup agrees with the inorder contents

TheoremTreap lookup agrees with the inorder contents#✓fully proved

Let \(t\) be a tree with keys in a linearly ordered type that is ordered as a binary search tree (every key in a left subtree is smaller and every key in a right subtree is larger than the node's key). For every key \(k\) and value \(v\), looking up \(k\) in \(t\) returns \(v\) if and only if the pair \((k, v)\) occurs in the inorder key-value list of \(t\).

public theorem lookup_contents {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {value : ν} {tree : Tree κ ν} (hOrdered : Ordered tree) :
    lookup key tree = some value ↔ (key, value) ∈ contents tree

Uses 7 · Used by 2

Statement usesTreap trees · Ordered treap tree · Treap inorder contents · Treap lookup

Proof usesEntry membership in a treap tree · Treap lookup finds exactly the stored entries · Inorder contents list the treap's entries

Used byErased keys are not found · Treap lookup after insertion

TheoremCosted lookup returns the ordinary lookup result#✓fully proved

For every tree \(t\) with keys in a linearly ordered type and every key \(k\), the value component of the costed lookup of \(k\) in \(t\) (ignoring the visit count) equals the result of looking up \(k\) in \(t\).

public theorem lookupWithCost_result {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {tree : Tree κ ν} : (lookupWithCost key tree).1 = lookup key tree

Uses 3

Statement usesTreap trees · Treap lookup · Lookup with cost

TheoremLookup cost is at most the tree size#✓fully proved

For every tree \(t\) with keys in a linearly ordered type and every key \(k\), the number of nodes visited by the costed lookup of \(k\) in \(t\) is at most the number of nodes of \(t\).

public theorem lookupWithCost_le_size {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {tree : Tree κ ν} : (lookupWithCost key tree).2 ≤ size tree

Uses 3

Statement usesTreap trees · Lookup with cost · Size of a treap tree

TheoremThe root of a heap-ordered tree has minimal priority#✓fully proved

If a nonempty tree whose root has priority \(p\) is heap-ordered, then every node of the tree, the root included, has priority at least \(p\).

public theorem heap_root_min {κ : Type u} {ν : Type v} {left right : Tree κ ν}
    {key : κ} {value : ν} {priority : Nat}
    (hHeap : HeapOrdered (.node left key value priority right)) :
    AllNodes (fun _ _ childPriority => priority ≤ childPriority)
      (.node left key value priority right)

Uses 3 · Used by 1

Statement usesTreap trees · Treap predicate holding at every node · Heap order of treap priorities

Used byMerging preserves heap order

TheoremKeys of a merged treap#✓fully proved

For all trees \(l\) and \(r\) and every key \(k\), \(k\) is the key of some node of the merge of \(l\) and \(r\) if and only if \(k\) is the key of some node of \(l\) or of some node of \(r\).

public theorem memKey_merge {κ : Type u} {ν : Type v} {key : κ}
    (left right : Tree κ ν) :
    key ∈ merge left right ↔ key ∈ left ∨ key ∈ right

Uses 4 · Used by 1

Statement usesTreap trees · Key membership in a treap tree · Treap merge

Proof usesSize of a treap tree

Used byInserting into a treap preserves validity

TheoremTreap merge concatenates inorder contents#✓fully proved

For trees \(l\) and \(r\), the inorder list of key-value pairs of the priority-guided merge of \(l\) and \(r\) is the inorder list of \(l\) followed by the inorder list of \(r\).

public theorem contents_merge {κ : Type u} {ν : Type v} (left right : Tree κ ν) :
    contents (merge left right) = contents left ++ contents right

Uses 6 · Used by 2

Statement usesTreap trees · Treap inorder contents · Treap merge

Proof usesTreap inorder traversal onto a suffix · Treap inorder contents of a node · Size of a treap tree

Used byTreap inorder contents after erasure · Treap inorder contents after insertion

DefinitionSeparated treap trees#✓fully proved

For keys equipped with a binary relation \(<\), two trees \(L\) and \(R\) are separated when \(a < b\) for every key \(a\) occurring at a node of \(L\) and every key \(b\) occurring at a node of \(R\).

public def Separated {κ : Type u} {ν : Type v} [LT κ]
    (left right : Tree κ ν) : Prop :=
  ∀ leftKey, leftKey ∈ left → ∀ rightKey, rightKey ∈ right → leftKey < rightKey

Uses 2 · Used by 4

Statement usesTreap trees · Key membership in a treap tree

Used byTreap merge preserves search-tree order · Erasing from a treap preserves validity · Inserting into a treap preserves validity · Merging separated treaps preserves validity

TheoremTreap merge preserves search-tree order#✓fully proved

Let the keys come from a linearly ordered type. If treap trees \(L\) and \(R\) are both ordered and every key of \(L\) is smaller than every key of \(R\), then the merge of \(L\) and \(R\) is ordered.

public theorem ordered_merge {κ : Type u} {ν : Type v} [LinearOrder κ]
    (left right : Tree κ ν) (hLeft : Ordered left) (hRight : Ordered right)
    (hSeparated : Separated left right) : Ordered (merge left right)

Uses 10 · Used by 1

Statement usesTreap trees · Ordered treap tree · Separated treap trees · Treap merge

Proof usesTreap predicate holding at every node · Key membership in a treap tree · Entry membership in a treap tree · Treap all-nodes predicate via node membership · Entry membership implies key membership in a treap · Size of a treap tree

Used byMerging separated treaps preserves validity

TheoremMerging preserves heap order#✓fully proved

If two trees \(l\) and \(r\) are both heap-ordered in their priorities, then the priority-guided merge of \(l\) and \(r\) is heap-ordered.

public theorem heapOrdered_merge {κ : Type u} {ν : Type v}
    (left right : Tree κ ν) (hLeft : HeapOrdered left)
    (hRight : HeapOrdered right) : HeapOrdered (merge left right)

Uses 8 · Used by 1

Statement usesTreap trees · Heap order of treap priorities · Treap merge

Proof usesTreap predicate holding at every node · Entry membership in a treap tree · Treap all-nodes predicate via node membership · The root of a heap-ordered tree has minimal priority · Size of a treap tree

Used byMerging separated treaps preserves validity

TheoremTreap split preserves search-tree order#✓fully proved

Let the keys come from a linearly ordered type and let \(t\) be an ordered treap tree. For every pivot key \(k\), the lower tree and the upper tree produced by splitting \(t\) at \(k\) are both ordered.

public theorem ordered_split {κ : Type u} {ν : Type v} [LinearOrder κ]
    {pivot : κ} {tree : Tree κ ν} (hOrdered : Ordered tree) :
    Ordered (split pivot tree).less ∧ Ordered (split pivot tree).greater

Uses 5 · Used by 1

Statement usesTreap trees · Ordered treap tree · Result of a treap split · Treap split

Proof usesTreap predicate holding at every node

Used bySplitting a treap preserves validity

TheoremTreap split preserves heap order#✓fully proved

Let the keys come from a linearly ordered type and let \(t\) be a heap-ordered treap tree. For every pivot key \(k\), the lower tree and the upper tree produced by splitting \(t\) at \(k\) are both heap-ordered.

public theorem heapOrdered_split {κ : Type u} {ν : Type v} [LinearOrder κ]
    {pivot : κ} {tree : Tree κ ν} (hHeap : HeapOrdered tree) :
    HeapOrdered (split pivot tree).less ∧ HeapOrdered (split pivot tree).greater

Uses 5 · Used by 1

Statement usesTreap trees · Heap order of treap priorities · Result of a treap split · Treap split

Proof usesTreap predicate holding at every node

Used bySplitting a treap preserves validity

TheoremSplit bounds for an ordered treap#✓fully proved

Let the keys come from a linear order and let \(T\) be an ordered tree. For every pivot \(p\), every key of the lower tree obtained by splitting \(T\) at \(p\) is strictly less than \(p\), and every key of the upper tree is strictly greater than \(p\).

public theorem split_bounds {κ : Type u} {ν : Type v} [LinearOrder κ]
    {pivot : κ} {tree : Tree κ ν} (hOrdered : Ordered tree) :
    AllNodes (fun key _ _ => key < pivot) (split pivot tree).less ∧
      AllNodes (fun key _ _ => pivot < key) (split pivot tree).greater

Uses 7 · Used by 3

Statement usesTreap trees · Treap predicate holding at every node · Ordered treap tree · Result of a treap split · Treap split

Proof usesEntry membership in a treap tree · Treap all-nodes predicate via node membership

Used byErased keys are not found · Erasing from a treap preserves validity · Inserting into a treap preserves validity

TheoremSplitting a treap preserves validity#✓fully proved

Let the keys come from a linear order. If a tree is a valid treap, then for every pivot \(p\), both the lower tree and the upper tree obtained by splitting it at \(p\) are valid treaps.

public theorem valid_split {κ : Type u} {ν : Type v} [LinearOrder κ]
    {pivot : κ} {tree : Tree κ ν} (hValid : Valid tree) :
    Valid (split pivot tree).less ∧ Valid (split pivot tree).greater

Uses 8 · Used by 2

Statement usesTreap trees · Result of a treap split · Valid treap · Treap split

Proof usesHeap order of treap priorities · Ordered treap tree · Treap split preserves heap order · Treap split preserves search-tree order

Used byErasing from a treap preserves validity · Inserting into a treap preserves validity

TheoremMerging separated treaps preserves validity#✓fully proved

Let the keys come from a linear order. If \(L\) and \(R\) are valid treaps and every key of \(L\) is strictly less than every key of \(R\), then the merge of \(L\) and \(R\) is a valid treap.

public theorem valid_merge {κ : Type u} {ν : Type v} [LinearOrder κ]
    {left right : Tree κ ν} (hLeft : Valid left) (hRight : Valid right)
    (hSeparated : Separated left right) : Valid (merge left right)

Uses 8 · Used by 2

Statement usesTreap trees · Separated treap trees · Valid treap · Treap merge

Proof usesHeap order of treap priorities · Ordered treap tree · Merging preserves heap order · Treap merge preserves search-tree order

Used byErasing from a treap preserves validity · Inserting into a treap preserves validity

TheoremInserting into a treap preserves validity#✓fully proved

Let the keys come from a linear order. If a tree is a valid treap, that is, its keys are in strict binary-search-tree order and its priorities are in min-heap order, then for every key \(k\), value \(v\) and natural-number priority \(q\), the tree obtained by inserting \(k\) with value \(v\) and priority \(q\) is again a valid treap.

public theorem valid_insert {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {value : ν} {priority : Nat} {tree : Tree κ ν}
    (hValid : Valid tree) : Valid (insert key value priority tree)

Uses 16 · Used by 1

Statement usesTreap trees · Valid treap · Treap insertion

Proof usesTreap predicate holding at every node · Heap order of treap priorities · Key membership in a treap tree · Ordered treap tree · Separated treap trees · Result of a treap split · Treap all-nodes predicate on keys via key membership · Keys of a merged treap · Treap merge · Treap split · Split bounds for an ordered treap · Merging separated treaps preserves validity · Splitting a treap preserves validity

Used byTreap lookup after insertion

TheoremErasing from a treap preserves validity#✓fully proved

Let the keys come from a linear order. If a tree is a valid treap, that is, its keys are in strict binary-search-tree order and its priorities are in min-heap order, then for every key \(k\) the tree obtained by erasing \(k\) from it is again a valid treap.

public theorem valid_erase {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {tree : Tree κ ν} (hValid : Valid tree) :
    Valid (erase key tree)

Uses 14 · Used by 1

Statement usesTreap trees · Valid treap · Treap deletion

Proof usesTreap predicate holding at every node · Heap order of treap priorities · Key membership in a treap tree · Ordered treap tree · Separated treap trees · Result of a treap split · Treap all-nodes predicate on keys via key membership · Treap split · Split bounds for an ordered treap · Merging separated treaps preserves validity · Splitting a treap preserves validity

Used byErased keys are not found

TheoremTreap inorder contents split at a pivot#✓fully proved

Let the keys come from a linearly ordered type, let \(t\) be a tree and \(k\) a pivot key, and let splitting \(t\) at \(k\) produce a lower tree \(L\), an optional value-priority pair found at \(k\), and an upper tree \(G\). Then the inorder list of key-value pairs of \(t\) is the inorder list of \(L\), followed by \((k, v)\) if the split found a pair with value \(v\) (and by nothing if it found none), followed by the inorder list of \(G\).

public theorem contents_split {κ : Type u} {ν : Type v} [LinearOrder κ]
    (pivot : κ) (tree : Tree κ ν) :
    contents tree = contents (split pivot tree).less ++
      ((split pivot tree).found.map fun result => (pivot, result.1)).toList ++
      contents (split pivot tree).greater

Uses 6

Statement usesTreap trees · Result of a treap split · Treap inorder contents · Treap split

Proof usesTreap inorder traversal onto a suffix · Treap inorder contents of a node

TheoremTreap inorder contents after insertion#✓fully proved

Let the keys come from a linearly ordered type, let \(t\) be a tree, \(k\) a key, \(v\) a value and \(n\) a natural-number priority, and let \(L\) and \(G\) be the lower and upper trees produced by splitting \(t\) at \(k\). Then the inorder list of key-value pairs of the tree obtained by inserting \(k\) with value \(v\) and priority \(n\) into \(t\) is the inorder list of \(L\), followed by \((k, v)\), followed by the inorder list of \(G\).

public theorem contents_insert {κ : Type u} {ν : Type v} [LinearOrder κ]
    (key : κ) (value : ν) (priority : Nat) (tree : Tree κ ν) :
    contents (insert key value priority tree) =
      contents (split key tree).less ++ (key, value) :: contents (split key tree).greater

Uses 9 · Used by 1

Statement usesTreap trees · Result of a treap split · Treap inorder contents · Treap insertion · Treap split

Proof usesTreap inorder traversal onto a suffix · Treap merge concatenates inorder contents · Treap inorder contents of a node · Treap merge

Used byTreap lookup after insertion

TheoremTreap inorder contents after erasure#✓fully proved

Let the keys come from a linearly ordered type, let \(t\) be a tree and \(k\) a key, and let \(L\) and \(G\) be the lower and upper trees produced by splitting \(t\) at \(k\). Then the inorder list of key-value pairs of the tree obtained by erasing \(k\) from \(t\) is the inorder list of \(L\) followed by the inorder list of \(G\).

public theorem contents_erase {κ : Type u} {ν : Type v} [LinearOrder κ]
    (key : κ) (tree : Tree κ ν) :
    contents (erase key tree) =
      contents (split key tree).less ++ contents (split key tree).greater

Uses 6 · Used by 1

Statement usesTreap trees · Result of a treap split · Treap inorder contents · Treap deletion · Treap split

Proof usesTreap merge concatenates inorder contents

Used byErased keys are not found

TheoremTreap lookup after insertion#✓fully proved

Let \(t\) be a valid treap with keys in a linearly ordered type, that is, \(t\) is ordered as a binary search tree by key and as a min-heap by priority. For every key \(k\), value \(v\) and priority \(p \in \mathbb{N}\), looking up \(k\) in the tree obtained by inserting \(k\) with value \(v\) and priority \(p\) into \(t\) returns \(v\).

public theorem lookup_insert_eq {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {value : ν} {priority : Nat} {tree : Tree κ ν}
    (hValid : Valid tree) : lookup key (insert key value priority tree) = some value

Uses 12

Statement usesTreap trees · Valid treap · Treap insertion · Treap lookup

Proof usesHeap order of treap priorities · Ordered treap tree · Result of a treap split · Treap inorder contents · Treap inorder contents after insertion · Treap lookup agrees with the inorder contents · Treap split · Inserting into a treap preserves validity

TheoremErased keys are not found#✓fully proved

Let \(t\) be a valid treap with keys in a linearly ordered type, that is, \(t\) is ordered as a binary search tree by key and as a min-heap by priority. For every key \(k\), looking up \(k\) in the tree obtained by erasing \(k\) from \(t\) returns no value.

public theorem lookup_erase_eq_none {κ : Type u} {ν : Type v} [LinearOrder κ]
    {key : κ} {tree : Tree κ ν} (hValid : Valid tree) :
    lookup key (erase key tree) = none

Uses 17

Statement usesTreap trees · Valid treap · Treap deletion · Treap lookup

Proof usesTreap predicate holding at every node · Heap order of treap priorities · Key membership in a treap tree · Ordered treap tree · Result of a treap split · Treap all-nodes predicate on keys via key membership · Treap inorder contents · Treap inorder contents after erasure · Keys occurring in the inorder contents · Treap lookup agrees with the inorder contents · Treap split · Split bounds for an ordered treap · Erasing from a treap preserves validity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.