Skip list

StructureSkip-list node#✓fully proved

A skip-list node consists of a key, a value and a natural number, the height of its tower. The node itself does not require the height to be positive; positivity is part of the validity invariant of skip lists.

public structure SkipList.Entry (α : Type u) (β : Type v) where
  key : α
  value : β
  height : Nat
deriving DecidableEq, Repr

Used by 33

Used byBottom-level abstraction of a skip list · Keys of a valid skip list are distinct · One level of skip-list search · One search step returns a suffix · Empty skip list · Skip-list erasure · Erasing the key of the first entry · Erasing past a smaller first entry · Erasing a key below the first entry · Erasure on a valid skip list filters out the key · Stored tower height of a key · The erased key has no stored height · Erasure preserves the heights of other keys · Height of a newly inserted key · Reinsertion preserves tower height · Skip-list insertion · Level of a skip list · Erasure removes the key from every level · Skip-list levels are sorted by key · Each skip-list level is a subsequence of the level below · Skip-list lookup · Skip-list search agrees with bottom-level lookup · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · Lookup after insertion returns the inserted value · Skip-list insertion does not change lookup of other keys · Skip-list search window · The search window is a suffix of the bottom level · Skip list · Valid skip list · The empty skip list is valid · Erasure preserves skip-list validity · Insertion preserves skip-list validity

StructureSkip list#✓fully proved

A deterministic skip list with keys in \(\alpha\) and values in \(\beta\) is represented by the list of its bottom-level nodes, each node an entry carrying a key in \(\alpha\), a value in \(\beta\) and a tower height, a natural number. No ordering or height condition is imposed by this structure.

public structure SkipList (α : Type u) (β : Type v) where
  entries : List (SkipList.Entry α β)
deriving DecidableEq, Repr

Uses 1 · Used by 32

Statement usesSkip-list node

Used byBottom-level abstraction of a skip list · Keys of a valid skip list are distinct · Empty skip list · Skip-list erasure · Erasing the key of the first entry · Erasing past a smaller first entry · Erasing a key below the first entry · Erasing from the empty skip list · Erasure on a valid skip list filters out the key · Stored tower height of a key · The erased key has no stored height · Erasure preserves the heights of other keys · Height of a newly inserted key · Reinsertion preserves tower height · Skip-list insertion · Level of a skip list · Erasure removes the key from every level · Keys on each skip-list level are distinct · Skip-list levels are sorted by key · Each skip-list level is a subsequence of the level below · Skip-list lookup · Skip-list search agrees with bottom-level lookup · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · Lookup after insertion returns the inserted value · Skip-list insertion does not change lookup of other keys · Skip-list search window · The search window is a suffix of the bottom level · Valid skip list · The empty skip list is valid · Erasure preserves skip-list validity · Insertion preserves skip-list validity

DefinitionEmpty skip list#✓fully proved

The empty skip list is the skip list with no nodes.

public def empty {α : Type u} {β : Type v} : SkipList α β :=
  ⟨[]⟩

Uses 2 · Used by 2

Statement usesSkip list · Skip-list node

Used byErasing from the empty skip list · The empty skip list is valid

DefinitionValid skip list#✓fully proved

Let \(\alpha\) be a linearly ordered type. A skip list with keys in \(\alpha\) and values in \(\beta\) is valid when the keys of its bottom-level nodes are strictly increasing along the list and every node has a tower of positive height.

public def Valid {α : Type u} {β : Type v} [LinearOrder α] (list : SkipList α β) : Prop :=
  list.entries.Pairwise (fun left right => left.key < right.key) ∧
    ∀ entry ∈ list.entries, 0 < entry.height

Uses 2 · Used by 13

Statement usesSkip list · Skip-list node

Used byKeys of a valid skip list are distinct · Erasure on a valid skip list filters out the key · The erased key has no stored height · Erasure preserves the heights of other keys · Reinsertion preserves tower height · Erasure removes the key from every level · Keys on each skip-list level are distinct · Skip-list levels are sorted by key · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · The empty skip list is valid · Erasure preserves skip-list validity · Insertion preserves skip-list validity

DefinitionLevel of a skip list#✓fully proved

For a skip list and a level index \(i\) (levels are numbered from \(0\) at the bottom), level \(i\) is the list of key-value pairs \((k, v)\) of the stored nodes whose tower height \(h\) satisfies \(i < h\), in the order in which these nodes appear in the bottom-level list of the skip list.

public def level {α : Type u} {β : Type v} (index : Nat) (list : SkipList α β) :
    List (α × β) :=
  (list.entries.filter fun entry => index < entry.height).map fun entry =>
    (entry.key, entry.value)

Uses 2 · Used by 4

Statement usesSkip list · Skip-list node

Used byErasure removes the key from every level · Keys on each skip-list level are distinct · Skip-list levels are sorted by key · Each skip-list level is a subsequence of the level below

DefinitionBottom-level abstraction of a skip list#✓fully proved

The bottom-level abstraction of a skip list is the association list obtained from its bottom-level nodes, in order, by keeping the key-value pair \((k, v)\) of each node and forgetting its tower height.

public def abstraction {α : Type u} {β : Type v} (list : SkipList α β) :
    List (α × β) :=
  list.entries.map fun entry => (entry.key, entry.value)

Uses 2 · Used by 6

Statement usesSkip list · Skip-list node

Used byKeys of a valid skip list are distinct · Skip-list search agrees with bottom-level lookup · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · Lookup after insertion returns the inserted value · Skip-list insertion does not change lookup of other keys

DefinitionStored tower height of a key#✓fully proved

For a key \(k\) and a skip list \(S\), the stored tower height of \(k\) in \(S\) is the tower height of the first bottom-level node of \(S\) whose key equals \(k\) under the given Boolean equality test on keys; it is undefined when no node has key \(k\).

public def heightOf {α : Type u} {β : Type v} [BEq α]
    (key : α) (list : SkipList α β) : Option Nat :=
  (list.entries.map fun entry => (entry.key, entry.height)).lookup key

Uses 2 · Used by 4

Statement usesSkip list · Skip-list node

Used byThe erased key has no stored height · Erasure preserves the heights of other keys · Height of a newly inserted key · Reinsertion preserves tower height

DefinitionOne level of skip-list search#✓fully proved

Let \(k\) be a search key, \(i\) a zero-based level and \(L\) a list of skip-list nodes. Let \(P\) be the longest prefix of \(L\) whose nodes all have keys less than \(k\). If some node of \(P\) has tower height greater than \(i\) (so it is visible at level \(i\)), advancing at level \(i\) returns the part of \(L\) after the last such node; otherwise it returns \(L\) unchanged.

The returned suffix is the window that every lower level continues to scan.

public def advanceAtLevel {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (index : Nat) (entries : List (Entry α β)) : List (Entry α β) :=
  (go entries).getD entries
where
  go : List (Entry α β) → Option (List (Entry α β))
    | [] => none
    | entry :: entries =>
        if entry.key < key then
          match go entries with
          | some suffix => some suffix
          | none => if index < entry.height then some entries else none
        else none

Uses 1 · Used by 4

Statement usesSkip-list node

Used byOne search step returns a suffix · Skip-list search agrees with bottom-level lookup · Skip-list search window · The search window is a suffix of the bottom level

DefinitionSkip-list search window#✓fully proved

Let \(k\) be a key and let \(H\) be the greatest tower height in a skip list (\(H = 0\) if the list is empty or every tower has height \(0\)). Start with the full list of bottom-level nodes, and for each level \(i\) from \(H - 1\) down to \(0\) in turn (no levels when \(H = 0\)) replace the current list by the result of advancing at level \(i\): within the longest initial segment of the current list whose keys are all less than \(k\), take the last node whose tower height exceeds \(i\) and keep only the nodes after it, leaving the list unchanged if there is no such node. The search window for \(k\) is the list that remains after these steps.

public def searchWindow {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (list : SkipList α β) : List (Entry α β) :=
  let maximumHeight :=
    list.entries.foldl (fun result entry => max result entry.height) 0
  go (List.range maximumHeight).reverse list.entries
where
  go : List Nat → List (Entry α β) → List (Entry α β)
    | [], entries => entries
    | index :: indices, entries =>
        go indices (advanceAtLevel key index entries)

Uses 3 · Used by 2

Statement usesSkip list · Skip-list node · One level of skip-list search

Used bySkip-list lookup · The search window is a suffix of the bottom level

DefinitionSkip-list lookup#✓fully proved

The lookup of a key \(k\) in a skip list computes the search window for \(k\), the suffix of the bottom-level nodes reached by descending from the highest level to level \(0\), and returns the value of the first node in the window whose key is \(k\), or no value if the window has no such node.

public def lookup {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (list : SkipList α β) : Option β :=
  ((searchWindow key list).map fun entry => (entry.key, entry.value)).lookup key

Uses 3 · Used by 5

Statement usesSkip list · Skip-list node · Skip-list search window

Used bySkip-list search agrees with bottom-level lookup · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · Lookup after insertion returns the inserted value · Skip-list insertion does not change lookup of other keys

DefinitionSkip-list insertion#✓fully proved

To insert key \(k\) with value \(v\) and requested height \(h\) into a skip list, scan its bottom-level nodes in order, keeping every node whose key is less than \(k\). At the first node whose key is not less than \(k\): if its key equals \(k\), its value is replaced by \(v\) and its tower height is kept; if its key is greater than \(k\), a new node with key \(k\), value \(v\) and tower height \(\max(1, h)\) is placed before it. If every key is less than \(k\), the new node is appended at the end.

public def insert {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (value : β) (requestedHeight : Nat) (list : SkipList α β) : SkipList α β :=
  ⟨go list.entries⟩
where
  go : List (Entry α β) → List (Entry α β)
    | [] => [{ key, value, height := max 1 requestedHeight }]
    | entry :: entries =>
        if key < entry.key then
          { key, value, height := max 1 requestedHeight } :: entry :: entries
        else if entry.key < key then
          entry :: go entries
        else
          { entry with value := value } :: entries

Uses 2 · Used by 5

Statement usesSkip list · Skip-list node

Used byHeight of a newly inserted key · Reinsertion preserves tower height · Lookup after insertion returns the inserted value · Skip-list insertion does not change lookup of other keys · Insertion preserves skip-list validity

TheoremThe empty skip list is valid#✓fully proved

For every linearly ordered type \(\alpha\) and every type \(\beta\), the empty skip list with keys in \(\alpha\) and values in \(\beta\) is valid.

public theorem valid_empty {α : Type u} {β : Type v} [LinearOrder α] :
    Valid (empty : SkipList α β)

Uses 4

Statement usesValid skip list · Empty skip list

Proof usesSkip list · Skip-list node

TheoremSkip-list levels are sorted by key#✓fully proved

If a skip list is valid, then for every level index \(i\) (levels are numbered from \(0\) at the bottom), the keys in the list of key-value pairs visible at level \(i\) are strictly increasing: every pair has a strictly smaller key than every pair after it.

public theorem level_pairwise {α : Type u} {β : Type v} [LinearOrder α]
    {list : SkipList α β} (valid : Valid list) (index : Nat) :
    (level index list).Pairwise (fun left right => left.1 < right.1)

Uses 4 · Used by 1

Statement usesSkip list · Valid skip list · Level of a skip list

Proof usesSkip-list node

Used byKeys on each skip-list level are distinct

TheoremEach skip-list level is a subsequence of the level below#✓fully proved

For every skip list and every level index \(i\) (levels are numbered from \(0\) at the bottom), the list of key-value pairs visible at level \(i + 1\) is a subsequence, not necessarily contiguous, of the list of key-value pairs visible at level \(i\).

public theorem level_succ_sublist_level {α : Type u} {β : Type v}
    (index : Nat) (list : SkipList α β) :
    (level (index + 1) list).Sublist (level index list)

Uses 3

Statement usesSkip list · Level of a skip list

Proof usesSkip-list node

TheoremKeys of a valid skip list are distinct#✓fully proved

If a skip list is valid, then the keys of the pairs in its bottom-level abstraction, read in order, form a list without duplicates.

public theorem abstraction_keys_nodup {α : Type u} {β : Type v} [LinearOrder α]
    {list : SkipList α β} (valid : Valid list) :
    ((abstraction list).map Prod.fst).Nodup

Uses 4

Statement usesSkip list · Valid skip list · Bottom-level abstraction of a skip list

Proof usesSkip-list node

TheoremKeys on each skip-list level are distinct#✓fully proved

If a skip list is valid, then for every level index \(i\) (levels are numbered from \(0\) at the bottom), no key occurs twice in the list of key-value pairs visible at level \(i\).

public theorem level_keys_nodup {α : Type u} {β : Type v} [LinearOrder α]
    {list : SkipList α β} (valid : Valid list) (index : Nat) :
    ((level index list).map Prod.fst).Nodup

Uses 4

Statement usesSkip list · Valid skip list · Level of a skip list

Proof usesSkip-list levels are sorted by key

TheoremOne search step returns a suffix#✓fully proved

For every search key, every level \(i\) and every list \(L\) of skip-list nodes, advancing the search at level \(i\) on \(L\) returns a suffix of \(L\).

public theorem advanceAtLevel_suffix {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (index : Nat) (entries : List (Entry α β)) :
    advanceAtLevel key index entries <:+ entries

Uses 2 · Used by 1

Statement usesSkip-list node · One level of skip-list search

Used byThe search window is a suffix of the bottom level

TheoremThe search window is a suffix of the bottom level#✓fully proved

For every skip list and every key \(k\), the search window for \(k\) is a suffix of the list of the skip list's bottom-level nodes.

public theorem searchWindow_suffix {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (list : SkipList α β) :
    searchWindow key list <:+ list.entries

Uses 5

Statement usesSkip list · Skip-list node · Skip-list search window

Proof usesOne level of skip-list search · One search step returns a suffix

TheoremSkip-list search agrees with bottom-level lookup#✓fully proved

For every skip list and every key \(k\), the top-down skip-list lookup of \(k\) returns the same result as looking up \(k\) in the bottom-level abstraction, the list of key-value pairs of all stored nodes in order: the value of the first pair with key \(k\), or no value if there is none.

public theorem lookup_eq_abstraction {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (list : SkipList α β) :
    lookup key list = (abstraction list).lookup key

Uses 5 · Used by 4

Statement usesSkip list · Bottom-level abstraction of a skip list · Skip-list lookup

Proof usesSkip-list node · One level of skip-list search

Used byErased keys are absent from a skip list · Erasure preserves lookups of other keys · Lookup after insertion returns the inserted value · Skip-list insertion does not change lookup of other keys

TheoremInsertion preserves skip-list validity#✓fully proved

Let \(\alpha\) be a linearly ordered type and \(\beta\) a type. If a skip list with keys in \(\alpha\) and values in \(\beta\) is valid, then for every key \(k \in \alpha\), value \(v \in \beta\) and requested height \(h \in \mathbb{N}\) (including \(h = 0\)), inserting \(k\) with value \(v\) and requested height \(h\) yields a valid skip list. This covers both a new key and a key already present, whose value is replaced.

public theorem valid_insert {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {value : β} {requestedHeight : Nat} {list : SkipList α β}
    (valid : Valid list) : Valid (insert key value requestedHeight list)

Uses 4

Statement usesSkip list · Valid skip list · Skip-list insertion

Proof usesSkip-list node

TheoremLookup after insertion returns the inserted value#✓fully proved

For every skip list, key \(k\), value \(v\) and requested height \(h\), looking up \(k\) after inserting \(k\) with value \(v\) and requested height \(h\) returns \(v\).

public theorem lookup_insert {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (value : β) (requestedHeight : Nat) (list : SkipList α β) :
    lookup key (insert key value requestedHeight list) = some value

Uses 6

Statement usesSkip list · Skip-list insertion · Skip-list lookup

Proof usesSkip-list node · Bottom-level abstraction of a skip list · Skip-list search agrees with bottom-level lookup

TheoremSkip-list insertion does not change lookup of other keys#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every skip list \(S\) with keys in \(\alpha\) and values in \(\beta\), all keys \(k\) and \(k'\) in \(\alpha\) with \(k' \ne k\), every value \(v \in \beta\) and every requested height \(h \in \mathbb{N}\), looking up \(k'\) in the skip list obtained by inserting \(k\) with value \(v\) and requested height \(h\) into \(S\) gives the same result as looking up \(k'\) in \(S\).

public theorem lookup_insert_of_ne {α : Type u} {β : Type v} [LinearOrder α]
    (key other : α) (value : β) (requestedHeight : Nat) (list : SkipList α β)
    (different : other ≠ key) :
    lookup other (insert key value requestedHeight list) = lookup other list

Uses 6

Statement usesSkip list · Skip-list insertion · Skip-list lookup

Proof usesSkip-list node · Bottom-level abstraction of a skip list · Skip-list search agrees with bottom-level lookup

TheoremReinsertion preserves tower height#✓fully proved

Let \(S\) be a valid skip list in which the key \(k\) has stored tower height \(h_0\). Then after inserting \(k\) into \(S\) with any value and any requested height, the stored tower height of \(k\) is still \(h_0\).

public theorem heightOf_insert_of_present {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (value : β) (requestedHeight existingHeight : Nat)
    (list : SkipList α β) (valid : Valid list)
    (present : heightOf key list = some existingHeight) :
    heightOf key (insert key value requestedHeight list) = some existingHeight

Uses 5

Statement usesSkip list · Valid skip list · Stored tower height of a key · Skip-list insertion

Proof usesSkip-list node

TheoremHeight of a newly inserted key#✓fully proved

If a key \(k\) does not occur in a skip list \(S\), then after inserting \(k\) into \(S\) with any value and requested height \(h\), the stored tower height of \(k\) is \(\max(1, h)\).

public theorem heightOf_insert_of_absent {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (value : β) (requestedHeight : Nat)
    (list : SkipList α β)
    (absent : heightOf key list = none) :
    heightOf key (insert key value requestedHeight list) =
      some (max 1 requestedHeight)

Uses 4

Statement usesSkip list · Stored tower height of a key · Skip-list insertion

Proof usesSkip-list node

DefinitionSkip-list erasure#✓fully proved

Given a key \(k\) from a linearly ordered type and a skip list \(S\), the erasure of \(k\) from \(S\) is the skip list obtained by scanning the entries of \(S\) in order: an entry whose key is less than \(k\) is kept and the scan continues; at the first entry whose key is greater than \(k\) the scan stops, and that entry and all later ones are kept; at the first entry whose key equals \(k\) that entry is removed, the scan stops, and all later entries are kept. Every kept entry keeps its key, value and tower height.

public def erase {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) (list : SkipList α β) : SkipList α β :=
  ⟨go list.entries⟩
where
  go : List (Entry α β) → List (Entry α β)
    | [] => []
    | entry :: entries =>
        if key < entry.key then
          entry :: entries
        else if entry.key < key then
          entry :: go entries
        else
          entries

Uses 2 · Used by 11

Statement usesSkip list · Skip-list node

Used byErasing the key of the first entry · Erasing past a smaller first entry · Erasing a key below the first entry · Erasing from the empty skip list · Erasure on a valid skip list filters out the key · The erased key has no stored height · Erasure preserves the heights of other keys · Erasure removes the key from every level · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · Erasure preserves skip-list validity

TheoremErasing from the empty skip list#✓fully proved

For every key \(k\), erasing \(k\) from the empty skip list gives the empty skip list.

@[simp] public theorem erase_empty {α : Type u} {β : Type v} [LinearOrder α]
    (key : α) : erase key (empty : SkipList α β) = empty

Uses 3

Statement usesSkip list · Empty skip list · Skip-list erasure

TheoremErasing a key below the first entry#✓fully proved

Let \(e\) be a skip-list entry and \(L\) a list of entries. If a key \(k\) is less than the key of \(e\), then erasing \(k\) from the skip list with entry list \(e\) followed by \(L\) leaves the entry list \(e\) followed by \(L\) unchanged.

public theorem erase_cons_of_lt {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {entry : Entry α β} {entries : List (Entry α β)}
    (before : key < entry.key) :
    (erase key ⟨entry :: entries⟩).entries = entry :: entries

Uses 3

Statement usesSkip list · Skip-list node · Skip-list erasure

TheoremErasing past a smaller first entry#✓fully proved

Let \(e\) be a skip-list entry and \(L\) a list of entries. If the key of \(e\) is less than a key \(k\), then erasing \(k\) from the skip list with entry list \(e\) followed by \(L\) gives the entry list consisting of \(e\) followed by the entry list obtained by erasing \(k\) from the skip list with entry list \(L\).

public theorem erase_cons_of_gt {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {entry : Entry α β} {entries : List (Entry α β)}
    (after : entry.key < key) :
    (erase key ⟨entry :: entries⟩).entries =
      entry :: (erase key ⟨entries⟩).entries

Uses 3

Statement usesSkip list · Skip-list node · Skip-list erasure

TheoremErasing the key of the first entry#✓fully proved

Let \(e\) be a skip-list entry and \(L\) a list of entries, and consider the skip list whose entry list is \(e\) followed by \(L\). If a key \(k\) equals the key of \(e\), then erasing \(k\) from this skip list leaves the entry list \(L\).

public theorem erase_cons_of_eq {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {entry : Entry α β} {entries : List (Entry α β)}
    (matching : key = entry.key) :
    (erase key ⟨entry :: entries⟩).entries = entries

Uses 3

Statement usesSkip list · Skip-list node · Skip-list erasure

TheoremErasure on a valid skip list filters out the key#✓fully proved

If \(S\) is a valid skip list and \(k\) is a key, then the entry list of the skip list obtained by erasing \(k\) from \(S\) is the entry list of \(S\) with every entry whose key equals \(k\) removed, the remaining entries kept in their order.

public theorem erase_entries_filter {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {list : SkipList α β} (valid : Valid list) :
    (erase key list).entries =
      list.entries.filter (fun entry => decide (entry.key ≠ key))

Uses 4 · Used by 6

Statement usesSkip list · Skip-list node · Valid skip list · Skip-list erasure

Used byThe erased key has no stored height · Erasure preserves the heights of other keys · Erasure removes the key from every level · Erased keys are absent from a skip list · Erasure preserves lookups of other keys · Erasure preserves skip-list validity

TheoremErasure preserves skip-list validity#✓fully proved

Let \(L\) be a valid skip list, that is, its keys are strictly increasing and every stored tower has positive height. For every key \(k\), the skip list obtained from \(L\) by erasing \(k\) is again valid.

public theorem valid_erase {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {list : SkipList α β} (valid : Valid list) :
    Valid (erase key list)

Uses 5

Statement usesSkip list · Valid skip list · Skip-list erasure

Proof usesSkip-list node · Erasure on a valid skip list filters out the key

TheoremErased keys are absent from a skip list#✓fully proved

Let \(L\) be a valid skip list, that is, its keys are strictly increasing and every stored tower has positive height. For every key \(k\), looking up \(k\) in the skip list obtained from \(L\) by erasing \(k\) returns no value.

public theorem lookup_erase {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {list : SkipList α β} (valid : Valid list) :
    lookup key (erase key list) = none

Uses 8

Statement usesSkip list · Valid skip list · Skip-list erasure · Skip-list lookup

Proof usesSkip-list node · Bottom-level abstraction of a skip list · Erasure on a valid skip list filters out the key · Skip-list search agrees with bottom-level lookup

TheoremErasure preserves lookups of other keys#✓fully proved

If \(S\) is a valid skip list and \(k\), \(k'\) are keys with \(k' \ne k\), then looking up \(k'\) in the skip list obtained by erasing \(k\) from \(S\) gives the same result as looking up \(k'\) in \(S\): the same value, or no value in both.

public theorem lookup_erase_of_ne {α : Type u} {β : Type v} [LinearOrder α]
    {key other : α} {list : SkipList α β} (valid : Valid list)
    (different : other ≠ key) :
    lookup other (erase key list) = lookup other list

Uses 8

Statement usesSkip list · Valid skip list · Skip-list erasure · Skip-list lookup

Proof usesSkip-list node · Bottom-level abstraction of a skip list · Erasure on a valid skip list filters out the key · Skip-list search agrees with bottom-level lookup

TheoremThe erased key has no stored height#✓fully proved

If \(S\) is a valid skip list and \(k\) is a key, then after erasing \(k\) from \(S\) the key \(k\) has no stored tower height.

public theorem heightOf_erase {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {list : SkipList α β} (valid : Valid list) :
    heightOf key (erase key list) = none

Uses 6

Statement usesSkip list · Valid skip list · Skip-list erasure · Stored tower height of a key

Proof usesSkip-list node · Erasure on a valid skip list filters out the key

TheoremErasure preserves the heights of other keys#✓fully proved

If \(S\) is a valid skip list and \(k\), \(k'\) are keys with \(k' \ne k\), then the stored tower height of \(k'\) in the skip list obtained by erasing \(k\) from \(S\) is the same as in \(S\); in particular \(k'\) has no stored height in one exactly when it has none in the other.

public theorem heightOf_erase_of_ne {α : Type u} {β : Type v} [LinearOrder α]
    {key other : α} {list : SkipList α β} (valid : Valid list)
    (different : other ≠ key) :
    heightOf other (erase key list) = heightOf other list

Uses 6

Statement usesSkip list · Valid skip list · Skip-list erasure · Stored tower height of a key

Proof usesSkip-list node · Erasure on a valid skip list filters out the key

TheoremErasure removes the key from every level#✓fully proved

If \(S\) is a valid skip list, \(k\) is a key and \(i\) is a natural number, then the level-\(i\) list of key-value pairs (levels numbered from \(0\)) of the skip list obtained by erasing \(k\) from \(S\) is the level-\(i\) list of \(S\) with every pair whose key equals \(k\) removed, the remaining pairs kept in their order.

public theorem level_erase {α : Type u} {β : Type v} [LinearOrder α]
    {key : α} {list : SkipList α β} (valid : Valid list) (index : Nat) :
    level index (erase key list) =
      (level index list).filter (fun pair => decide (pair.1 ≠ key))

Uses 6

Statement usesSkip list · Valid skip list · Skip-list erasure · Level of a skip list

Proof usesSkip-list node · Erasure on a valid skip list filters out the key

36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.