Skip to content

X-fast trie

28 fully proved

X-fast trie

Structurex-fast trie#✓fully proved

An x-fast trie over \(w\)-bit keys consists of a finite set of stored keys in \(\{0, \dots, 2^w - 1\}\) together with, for each level \(l \in \{0, \dots, w\}\), a finite set of natural numbers, intended to hold the \(l\)-bit prefixes of the stored keys.

The classical per-level hash tables are modeled as finite sets, so no \(O(\log w)\) successor bound (or any other running-time bound) is claimed.

public structure XFastTrie (w : Nat) where
  /-- The stored keys. -/
  contents : Finset (Fin (2 ^ w))
  /-- `levels l` holds the `l`-bit prefixes of the stored keys, for `l ≤ w`. -/
  levels : Fin (w + 1) → Finset Nat
Used by 38
Used byKeys of a y-fast trie · Keys of an x-fast trie after insertion · The empty x-fast trie · Level probe of an x-fast trie · Level probes of a valid x-fast trie · Insertion into an x-fast trie · Membership in a y-fast trie via representatives' buckets · Keys of a valid y-fast trie are the keys in buckets · Membership query in an x-fast trie · The membership test of a valid x-fast trie is exact · An inserted key passes the membership test · Predecessor query in an x-fast trie · When an x-fast trie has no predecessor · Characterization of the x-fast trie predecessor · Representatives of a valid y-fast trie are stored keys · Successor in an x-fast trie · When an x-fast trie has no successor · Characterization of the x-fast trie successor · Valid x-fast trie · Valid y-fast trie skeleton · The empty x-fast trie is valid · Insertion preserves validity of an x-fast trie · y-fast trie skeleton · Keys of the trie of representatives · The empty grouped y-fast trie · Grouped y-fast trie · Correctness of the y-fast trie membership query · Representative trie of a list · Building from a nonempty list with group bound zero gives an invalid trie · Grouped y-fast trie from a list of groups · Least representative at or above a key · Successor query in a grouped y-fast trie · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key · Validity of a grouped y-fast trie · The empty grouped y-fast trie is valid · Inserting a list of keys into the empty x-fast trie gives a valid trie · Assembling a valid grouped y-fast trie from groups

DefinitionBit prefix of a key#✓fully proved

For natural numbers \(l\) and \(w\) and a \(w\)-bit key \(x < 2^w\), the length-\(l\) prefix of \(x\) is the natural number \(\lfloor x / 2^{w-l} \rfloor\), where \(w - l\) is truncated subtraction (it is \(0\) when \(l > w\)). For \(l \le w\) these are the top \(l\) bits of \(x\), a number below \(2^l\).

public def prefixOf {w : Nat} (l : Nat) (x : Fin (2 ^ w)) : Nat :=
  x.val / 2 ^ (w - l)
Used by 11
Used byLevel probe of an x-fast trie · Level probes of a valid x-fast trie · Insertion into an x-fast trie · The membership test of a valid x-fast trie is exact · An inserted key passes the membership test · The full-length prefix of a key is the key · A prefix fits in its length · The empty prefix is zero · Valid x-fast trie · The empty x-fast trie is valid · Insertion preserves validity of an x-fast trie

TheoremThe empty prefix is zero#✓fully proved

For every \(w\)-bit key \(x < 2^w\), the length-\(0\) prefix of \(x\) (the trie root) is \(0\).

public theorem prefixOf_zero {w : Nat} (x : Fin (2 ^ w)) : prefixOf 0 x = 0
Uses 1
Statement usesBit prefix of a key

TheoremThe full-length prefix of a key is the key#✓fully proved

For every \(w\)-bit key \(x < 2^w\), the length-\(w\) prefix of \(x\) equals \(x\).

public theorem prefixOf_full {w : Nat} (x : Fin (2 ^ w)) : prefixOf w x = x.val
Uses 1 · Used by 1
Statement usesBit prefix of a key
Used byThe membership test of a valid x-fast trie is exact

TheoremA prefix fits in its length#✓fully proved

For natural numbers \(l \le w\) and a \(w\)-bit key \(x < 2^w\), the length-\(l\) prefix of \(x\) is less than \(2^l\).

public theorem prefixOf_lt {w l : Nat} (hl : l ≤ w) (x : Fin (2 ^ w)) :
    prefixOf l x < 2 ^ l
Uses 1
Statement usesBit prefix of a key

DefinitionValid x-fast trie#✓fully proved

An x-fast trie \(t\) over \(w\)-bit keys is valid when, for every level \(l \in \{0, \dots, w\}\), the level-\(l\) set of \(t\) equals the set of \(l\)-bit prefixes (top \(l\) bits) of the stored keys of \(t\).

public def Valid {w : Nat} (t : XFastTrie w) : Prop :=
  ∀ l : Fin (w + 1), t.levels l = t.contents.image (fun y => prefixOf l.val y)
Uses 2 · Used by 15
Statement usesx-fast trie · Bit prefix of a key
Used byLevel probes of a valid x-fast trie · Keys of a valid y-fast trie are the keys in buckets · The membership test of a valid x-fast trie is exact · Representatives of a valid y-fast trie are stored keys · Valid y-fast trie skeleton · The empty x-fast trie is valid · Insertion preserves validity of an x-fast trie · Correctness of the y-fast trie membership query · Building from a nonempty list with group bound zero gives an invalid trie · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key · Validity of a grouped y-fast trie · The empty grouped y-fast trie is valid · Inserting a list of keys into the empty x-fast trie gives a valid trie · Assembling a valid grouped y-fast trie from groups

DefinitionThe empty x-fast trie#✓fully proved

The empty x-fast trie over \(w\)-bit keys stores no keys, and the prefix set at each of its levels \(0, 1, \dots, w\) is empty.

public def empty {w : Nat} : XFastTrie w :=
  ⟨∅, fun _ => ∅⟩
Uses 1 · Used by 5
Statement usesx-fast trie
Used byThe empty x-fast trie is valid · Keys of the trie of representatives · The empty grouped y-fast trie · Representative trie of a list · Inserting a list of keys into the empty x-fast trie gives a valid trie

DefinitionInsertion into an x-fast trie#✓fully proved

Inserting a \(w\)-bit key \(x\) into an x-fast trie \(t\) adds \(x\) to the keys stored in \(t\) and, for each level \(0 \le l \le w\), adds the \(l\)-bit prefix of \(x\) to the prefix set at level \(l\).

public def insert {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) : XFastTrie w :=
  ⟨Insert.insert x t.contents, fun l => Insert.insert (prefixOf l.val x) (t.levels l)⟩
Uses 2 · Used by 6
Statement usesx-fast trie · Bit prefix of a key
Used byKeys of an x-fast trie after insertion · An inserted key passes the membership test · Insertion preserves validity of an x-fast trie · Keys of the trie of representatives · Representative trie of a list · Inserting a list of keys into the empty x-fast trie gives a valid trie

TheoremThe empty x-fast trie is valid#✓fully proved

For every \(w\), the empty x-fast trie over \(w\)-bit keys, which has no stored keys and every level empty, is valid.

public theorem valid_empty {w : Nat} : (empty : XFastTrie w).Valid
Uses 4 · Used by 2
Statement usesValid x-fast trie · The empty x-fast trie
Proof usesx-fast trie · Bit prefix of a key
Used byThe empty grouped y-fast trie is valid · Inserting a list of keys into the empty x-fast trie gives a valid trie

TheoremInsertion preserves validity of an x-fast trie#✓fully proved

If \(t\) is a valid x-fast trie over \(w\)-bit keys and \(x \in \{0, \dots, 2^w - 1\}\), then the x-fast trie obtained from \(t\) by inserting \(x\) is valid.

public theorem valid_insert {w : Nat} (t : XFastTrie w) (hv : t.Valid)
    (x : Fin (2 ^ w)) : (t.insert x).Valid
Uses 4 · Used by 1
Statement usesx-fast trie · Valid x-fast trie · Insertion into an x-fast trie
Proof usesBit prefix of a key
Used byInserting a list of keys into the empty x-fast trie gives a valid trie

TheoremKeys of an x-fast trie after insertion#✓fully proved

For every x-fast trie \(t\) over \(w\)-bit keys and every \(w\)-bit key \(x\), the set of keys stored in the trie obtained by inserting \(x\) into \(t\) is the set of keys stored in \(t\) with \(x\) added.

@[simp]
public theorem contents_insert {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) :
    (t.insert x).contents = Insert.insert x t.contents
Uses 2
Statement usesx-fast trie · Insertion into an x-fast trie

DefinitionLevel probe of an x-fast trie#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys, a level \(0 \le l \le w\) and a \(w\)-bit key \(x\), the probe of level \(l\) of \(t\) at \(x\) returns true exactly when the \(l\)-bit prefix of \(x\) belongs to the prefix set stored at level \(l\) of \(t\).

When \(t\) is valid, this holds exactly when some key stored in \(t\) has the same \(l\)-bit prefix as \(x\).

public def hasPrefix {w : Nat} (t : XFastTrie w) (l : Fin (w + 1)) (x : Fin (2 ^ w)) :
    Bool :=
  decide (prefixOf l.val x ∈ t.levels l)
Uses 2 · Used by 4
Statement usesx-fast trie · Bit prefix of a key
Used byLevel probes of a valid x-fast trie · Membership query in an x-fast trie · The membership test of a valid x-fast trie is exact · An inserted key passes the membership test

TheoremLevel probes of a valid x-fast trie#✓fully proved

Let \(t\) be a valid x-fast trie over \(w\)-bit keys, let \(0 \le l \le w\) and let \(x\) be a \(w\)-bit key. The probe of level \(l\) of \(t\) at \(x\) succeeds if and only if some key \(y\) stored in \(t\) has the same \(l\)-bit prefix as \(x\).

public theorem hasPrefix_iff {w : Nat} (t : XFastTrie w) (hv : t.Valid)
    (l : Fin (w + 1)) (x : Fin (2 ^ w)) :
    t.hasPrefix l x = true ↔ ∃ y ∈ t.contents, prefixOf l.val y = prefixOf l.val x
Uses 4 · Used by 1
Statement usesx-fast trie · Valid x-fast trie · Level probe of an x-fast trie · Bit prefix of a key
Used byThe membership test of a valid x-fast trie is exact

DefinitionMembership query in an x-fast trie#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys and a key \(x < 2^w\), the membership query of \(x\) in \(t\) answers true exactly when the length-\(w\) prefix of \(x\), which is \(x\) itself, lies in the prefix set that \(t\) stores for level \(w\): a single probe of the deepest level, as in the classical structure.

public def member {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) : Bool :=
  t.hasPrefix ⟨w, Nat.lt_succ_self w⟩ x
Uses 2 · Used by 4
Statement usesx-fast trie · Level probe of an x-fast trie
Used byThe membership test of a valid x-fast trie is exact · An inserted key passes the membership test · Correctness of the y-fast trie membership query · Least representative at or above a key

TheoremThe membership test of a valid x-fast trie is exact#✓fully proved

For a valid x-fast trie \(t\) over \(w\)-bit keys and a \(w\)-bit key \(x\), the membership test of \(t\) at \(x\), which probes the deepest level \(w\), returns true if and only if \(x\) is stored in \(t\).

public theorem member_iff {w : Nat} (t : XFastTrie w) (hv : t.Valid) (x : Fin (2 ^ w)) :
    t.member x = true ↔ x ∈ t.contents
Uses 7 · Used by 1
Statement usesx-fast trie · Valid x-fast trie · Membership query in an x-fast trie
Proof usesLevel probe of an x-fast trie · Level probes of a valid x-fast trie · Bit prefix of a key · The full-length prefix of a key is the key
Used byCorrectness of the y-fast trie membership query

TheoremAn inserted key passes the membership test#✓fully proved

For every x-fast trie \(t\) over \(w\)-bit keys and every \(w\)-bit key \(x\), the membership test at \(x\) of the trie obtained by inserting \(x\) into \(t\) returns true.

No validity assumption on \(t\) is needed: insertion puts the full-length prefix of \(x\) directly into the deepest level, which is the level the membership test probes.

public theorem member_insert_self {w : Nat} (t : XFastTrie w)
    (x : Fin (2 ^ w)) : (t.insert x).member x = true
Uses 5
Statement usesx-fast trie · Insertion into an x-fast trie · Membership query in an x-fast trie
Proof usesLevel probe of an x-fast trie · Bit prefix of a key

DefinitionSuccessor in an x-fast trie#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys and a key \(x \in \{0, \dots, 2^w - 1\}\), the successor of \(x\) in \(t\) is the least stored key of \(t\) that is greater than \(x\) when some stored key is greater than \(x\); otherwise \(x\) has no successor in \(t\).

It is computed directly from the stored key set rather than by the classical binary search over the levels, so no \(O(\log w)\) time bound is claimed.

public def successor {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) :
    Option (Fin (2 ^ w)) :=
  if h : (t.contents.filter (fun y => x < y)).Nonempty then
    some ((t.contents.filter (fun y => x < y)).min' h)
  else
    none
Uses 1 · Used by 7
Statement usesx-fast trie
Used byWhen an x-fast trie has no successor · Characterization of the x-fast trie successor · Correctness of the y-fast trie membership query · Least representative at or above a key · Successor query in a grouped y-fast trie · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key

DefinitionPredecessor query in an x-fast trie#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys and a key \(x < 2^w\), the predecessor of \(x\) in \(t\) is the greatest key stored in \(t\) that is smaller than \(x\), if such a key exists; otherwise the query returns no key.

public def predecessor {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) :
    Option (Fin (2 ^ w)) :=
  if h : (t.contents.filter (fun y => y < x)).Nonempty then
    some ((t.contents.filter (fun y => y < x)).max' h)
  else
    none
Uses 1 · Used by 2
Statement usesx-fast trie
Used byWhen an x-fast trie has no predecessor · Characterization of the x-fast trie predecessor

TheoremCharacterization of the x-fast trie successor#✓fully proved

Let \(t\) be an x-fast trie over \(w\)-bit keys and let \(x\) and \(y\) be keys in \(\{0, \dots, 2^w - 1\}\). The successor of \(x\) in \(t\) exists and equals \(y\) if and only if \(y\) is a stored key of \(t\), \(x < y\), and \(y \le z\) for every stored key \(z\) of \(t\) with \(x < z\).

public theorem successor_eq_some_iff {w : Nat} (t : XFastTrie w) (x y : Fin (2 ^ w)) :
    t.successor x = some y ↔
      y ∈ t.contents ∧ x < y ∧ ∀ z ∈ t.contents, x < z → y ≤ z
Uses 2 · Used by 3
Statement usesx-fast trie · Successor in an x-fast trie
Used byCorrectness of the y-fast trie membership query · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key

TheoremWhen an x-fast trie has no successor#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys and a key \(x < 2^w\), the successor query of \(x\) in \(t\) returns no key if and only if no key stored in \(t\) is greater than \(x\).

public theorem successor_eq_none_iff {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) :
    t.successor x = none ↔ ∀ z ∈ t.contents, ¬ x < z
Uses 2 · Used by 3
Statement usesx-fast trie · Successor in an x-fast trie
Used byCorrectness of the y-fast trie membership query · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key

TheoremCharacterization of the x-fast trie predecessor#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys and keys \(x, y < 2^w\), the predecessor query of \(x\) in \(t\) returns \(y\) if and only if \(y\) is stored in \(t\), \(y < x\), and every key \(z\) stored in \(t\) with \(z < x\) satisfies \(z \le y\).

public theorem predecessor_eq_some_iff {w : Nat} (t : XFastTrie w) (x y : Fin (2 ^ w)) :
    t.predecessor x = some y ↔
      y ∈ t.contents ∧ y < x ∧ ∀ z ∈ t.contents, z < x → z ≤ y
Uses 2
Statement usesx-fast trie · Predecessor query in an x-fast trie

TheoremWhen an x-fast trie has no predecessor#✓fully proved

For an x-fast trie \(t\) over \(w\)-bit keys and a key \(x < 2^w\), the predecessor query of \(x\) in \(t\) returns no key if and only if no key stored in \(t\) is smaller than \(x\).

public theorem predecessor_eq_none_iff {w : Nat} (t : XFastTrie w) (x : Fin (2 ^ w)) :
    t.predecessor x = none ↔ ∀ z ∈ t.contents, ¬ z < x
Uses 2
Statement usesx-fast trie · Predecessor query in an x-fast trie

Y-fast trie

Structurey-fast trie skeleton#✓fully proved

A y-fast trie skeleton over \(w\)-bit keys consists of an x-fast trie over \(w\)-bit keys, whose stored keys are the representatives, together with a bucket \(B_r\), a finite set of keys, for every key \(r \in \{0, \dots, 2^w - 1\}\).

In the classical structure each bucket is a balanced search tree of \(\Theta(w)\) keys; here buckets are plain finite sets, the bucket ordering invariant and the split and merge maintenance are not modeled, and no complexity bound is claimed.

public structure YFastTrie (w : Nat) where
  /-- The x-fast trie over representative keys. -/
  reps : XFastTrie w
  /-- The bucket owned by each key; only representatives own nonempty buckets. -/
  buckets : Fin (2 ^ w) → Finset (Fin (2 ^ w))
Uses 1 · Used by 5
Statement usesx-fast trie
Used byKeys of a y-fast trie · Membership in a y-fast trie via representatives' buckets · Keys of a valid y-fast trie are the keys in buckets · Representatives of a valid y-fast trie are stored keys · Valid y-fast trie skeleton

DefinitionKeys of a y-fast trie#✓fully proved

Let \(t\) be a y-fast trie over \(w\)-bit keys, let \(R\) be the set of keys stored in the representative x-fast trie of \(t\), and for each \(r \in R\) let \(B(r)\) be the bucket owned by \(r\). The set of keys stored in \(t\) is the union of the buckets of its representatives, \(\bigcup_{r \in R} B(r)\).

It is computed from the representatives alone, not by filtering all \(2^w\) possible keys.

public def contents {w : Nat} (t : YFastTrie w) : Finset (Fin (2 ^ w)) :=
  t.reps.contents.biUnion t.buckets
Uses 2 · Used by 3
Statement usesx-fast trie · y-fast trie skeleton
Used byMembership in a y-fast trie via representatives' buckets · Keys of a valid y-fast trie are the keys in buckets · Representatives of a valid y-fast trie are stored keys

TheoremMembership in a y-fast trie via representatives' buckets#✓fully proved

For every y-fast trie \(t\) over \(w\)-bit keys and every \(w\)-bit key \(x\), \(x\) is stored in \(t\) if and only if \(x\) lies in the bucket owned by some representative of \(t\), that is, by some key stored in the representative x-fast trie of \(t\).

public theorem mem_contents_iff {w : Nat} (t : YFastTrie w) (x : Fin (2 ^ w)) :
    x ∈ t.contents ↔ ∃ r ∈ t.reps.contents, x ∈ t.buckets r
Uses 3 · Used by 2
Statement usesx-fast trie · y-fast trie skeleton · Keys of a y-fast trie
Used byKeys of a valid y-fast trie are the keys in buckets · Representatives of a valid y-fast trie are stored keys

DefinitionValid y-fast trie skeleton#✓fully proved

A y-fast trie skeleton \(t\) over \(w\)-bit keys, with bucket \(B_r\) owned by each key \(r\), is valid when its representative x-fast trie is valid, a key \(r\) is stored in the representative x-fast trie exactly when its bucket \(B_r\) is nonempty, and every key \(r\) stored in the representative x-fast trie lies in its own bucket \(B_r\).

So the representatives are sampled from the stored keys: a representative \(0\) whose bucket is \(\{1\}\) is not valid. The classical bucket ordering invariant (the keys of bucket \(B_r\) lie in the interval ending at \(r\)) is not required, so this is the invariant of the skeleton only.

public def Valid {w : Nat} (t : YFastTrie w) : Prop :=
  t.reps.Valid ∧ (∀ r, r ∈ t.reps.contents ↔ t.buckets r ≠ ∅) ∧
    ∀ r ∈ t.reps.contents, r ∈ t.buckets r
Uses 3 · Used by 2
Statement usesx-fast trie · Valid x-fast trie · y-fast trie skeleton
Used byKeys of a valid y-fast trie are the keys in buckets · Representatives of a valid y-fast trie are stored keys

TheoremRepresentatives of a valid y-fast trie are stored keys#✓fully proved

If a y-fast trie \(t\) over \(w\)-bit keys is valid, then every key of the representative x-fast trie of \(t\) is a stored key of \(t\).

public theorem rep_mem_contents_of_valid {w : Nat} {t : YFastTrie w}
    (hv : t.Valid) {r : Fin (2 ^ w)} (hr : r ∈ t.reps.contents) :
    r ∈ t.contents
Uses 6
Statement usesx-fast trie · y-fast trie skeleton · Valid y-fast trie skeleton · Keys of a y-fast trie
Proof usesValid x-fast trie · Membership in a y-fast trie via representatives' buckets

TheoremKeys of a valid y-fast trie are the keys in buckets#✓fully proved

If \(t\) is a valid y-fast trie over \(w\)-bit keys, then a \(w\)-bit key \(x\) is stored in \(t\) if and only if \(x\) lies in the bucket owned by some \(w\)-bit key \(r\) (such an owner \(r\) is then necessarily a representative).

public theorem mem_contents_iff_exists_of_valid {w : Nat} {t : YFastTrie w}
    (hv : t.Valid) (x : Fin (2 ^ w)) :
    x ∈ t.contents ↔ ∃ r, x ∈ t.buckets r
Uses 6
Statement usesy-fast trie skeleton · Valid y-fast trie skeleton · Keys of a y-fast trie
Proof usesx-fast trie · Valid x-fast trie · Membership in a y-fast trie via representatives' buckets

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.