Skip to content

Radix trie

36 fully proved

Radix Trie

InductiveRadix trie#✓fully proved

For types \(\alpha\) and \(\beta\), a radix trie with keys that are lists over \(\alpha\) and values in \(\beta\) is a node made of an optional value in \(\beta\) and a finite list of child edges, each a pair of a label, which is a list over \(\alpha\), and a radix trie (the subtree at the end of the edge).

No invariant is built into the type: labels may be empty and sibling labels may share first symbols. The radix-trie invariant is imposed separately.

inductive RadixTrie (α : Type u) (β : Type v) where
  | node : Option β → List (List α × RadixTrie α β) → RadixTrie α β
Used by 25
Used byRadix trie built from a list of key-value pairs · Empty radix trie · The empty radix trie is valid · Entries of a radix trie · Edge search by first symbol · Prefix search in a radix trie · Prefix search is correct on valid radix tries · Insertion into a radix trie · Insertion preserves validity of radix tries · Stored keys of a radix trie · Stored keys of a valid radix trie are distinct · Radix trie lookup · Lookup in the empty radix trie · Lookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie · Radix trie lookup of a nonempty key at a node · Stored keys of a valid radix trie are the keys with a successful lookup · Sibling edge labels start with distinct symbols · Replacing the child edge for a symbol · Path-compressed root · Children of a valid node are path-compressed · Valid radix trie · The stored keys of a suffix tree are its terminated suffixes · Suffix tree

DefinitionEmpty radix trie#✓fully proved

The empty radix trie is the single node that stores no value and has no child edges; it contains no key-value entries.

def empty {α : Type u} {β : Type v} : RadixTrie α β :=
  .node none []
Uses 1 · Used by 3
Statement usesRadix trie
Used byRadix trie built from a list of key-value pairs · The empty radix trie is valid · Lookup in the empty radix trie

DefinitionLongest common prefix#✓fully proved

For lists \(s\) and \(t\) over a type with decidable equality, the longest common prefix of \(s\) and \(t\) is defined by recursion: it is empty if \(s\) or \(t\) is empty; if \(s\) has first element \(a\) and rest \(s'\), and \(t\) has first element \(b\) and rest \(t'\), it is \(a\) followed by the longest common prefix of \(s'\) and \(t'\) when \(a = b\), and empty when \(a \ne b\).

def commonPrefix {α : Type u} [DecidableEq α] : List α → List α → List α
  | [], _ => []
  | _, [] => []
  | a :: xs, b :: ys => if a = b then a :: commonPrefix xs ys else []
Used by 16
Used byA list is its common prefix with another list followed by the rest · When the common prefix is the second list, the first list extends it · A shared prefix factors out of the longest common prefix · Longest common prefix in terms of dropped remainders · The longest common prefix of a list and its prefix · Longest common prefix of a list with itself · Characterization of the longest common prefix · Prefix search in a radix trie · Prefix search is correct on valid radix tries · Insertion into a radix trie · Insertion preserves validity of radix tries · Radix trie lookup · Lookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie · Radix trie lookup of a nonempty key at a node

TheoremLongest common prefix of a list with itself#✓fully proved

For every list \(s\) over a type with decidable equality, the longest common prefix of \(s\) and \(s\) is \(s\).

theorem commonPrefix_self {α : Type u} [DecidableEq α] (xs : List α) :
    commonPrefix xs xs = xs
Uses 1 · Used by 1
Statement usesLongest common prefix
Used byLookup of a key just inserted into a radix trie

TheoremA shared prefix factors out of the longest common prefix#✓fully proved

Write \(uv\) for the list \(u\) followed by the list \(v\). For lists \(p\), \(s\) and \(t\) over a type with decidable equality, the longest common prefix of \(ps\) and \(pt\) is \(p\) followed by the longest common prefix of \(s\) and \(t\).

theorem commonPrefix_append_append {α : Type u} [DecidableEq α]
    (P xs ys : List α) :
    commonPrefix (P ++ xs) (P ++ ys) = P ++ commonPrefix xs ys
Uses 1 · Used by 2
Statement usesLongest common prefix
Used byThe longest common prefix of a list and its prefix · Insertion into a radix trie leaves lookups of other keys unchanged

TheoremCharacterization of the longest common prefix#✓fully proved

Let \(s\) and \(t\) be lists over a type with decidable equality, with longest common prefix \(p\). Then there are lists \(s'\) and \(t'\) such that \(s\) is \(p\) followed by \(s'\), \(t\) is \(p\) followed by \(t'\), and either \(s'\) is empty, or \(t'\) is empty, or \(s'\) and \(t'\) are both nonempty with different first elements.

theorem commonPrefix_spec {α : Type u} [DecidableEq α] (xs ys : List α) :
    ∃ xs' ys', xs = commonPrefix xs ys ++ xs' ∧ ys = commonPrefix xs ys ++ ys' ∧
      (xs' = [] ∨ ys' = [] ∨
        ∃ x xs'' y ys'', xs' = x :: xs'' ∧ ys' = y :: ys'' ∧ x ≠ y)
Uses 1 · Used by 3
Statement usesLongest common prefix
Used byA list is its common prefix with another list followed by the rest · Longest common prefix in terms of dropped remainders · Prefix search is correct on valid radix tries

TheoremA list is its common prefix with another list followed by the rest#✓fully proved

Let \(s\) and \(t\) be lists over a type with decidable equality, and let \(p\) be the longest common prefix of \(s\) and \(t\). Then \(s\) is \(p\) followed by the list obtained by dropping the first \(|p|\) elements of \(s\), where \(|p|\) is the length of \(p\).

theorem append_drop_commonPrefix_left {α : Type u} [DecidableEq α]
    (xs ys : List α) :
    xs = commonPrefix xs ys ++ xs.drop (commonPrefix xs ys).length
Uses 2 · Used by 2
Statement usesLongest common prefix
Proof usesCharacterization of the longest common prefix
Used byWhen the common prefix is the second list, the first list extends it · Prefix search is correct on valid radix tries

TheoremLongest common prefix in terms of dropped remainders#✓fully proved

Let \(s\) and \(t\) be lists over a type with decidable equality, let \(p\) be their longest common prefix, of length \(n\), and let \(s'\) and \(t'\) be the lists obtained from \(s\) and \(t\) by dropping their first \(n\) elements. Then \(s\) is \(p\) followed by \(s'\), \(t\) is \(p\) followed by \(t'\), and either \(s'\) is empty, or \(t'\) is empty, or \(s'\) and \(t'\) are both nonempty with different first elements.

theorem commonPrefix_drop_spec {α : Type u} [DecidableEq α] (xs ys : List α) :
    xs = commonPrefix xs ys ++ xs.drop (commonPrefix xs ys).length ∧
      ys = commonPrefix xs ys ++ ys.drop (commonPrefix xs ys).length ∧
      (xs.drop (commonPrefix xs ys).length = [] ∨
        ys.drop (commonPrefix xs ys).length = [] ∨
        ∃ x xs'' y ys'', xs.drop (commonPrefix xs ys).length = x :: xs'' ∧
          ys.drop (commonPrefix xs ys).length = y :: ys'' ∧ x ≠ y)
Uses 2 · Used by 3
Statement usesLongest common prefix
Proof usesCharacterization of the longest common prefix
Used byInsertion preserves validity of radix tries · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie

TheoremWhen the common prefix is the second list, the first list extends it#✓fully proved

Let \(s\) and \(t\) be lists over a type with decidable equality. If the longest common prefix of \(s\) and \(t\) is \(t\), then \(s\) is \(t\) followed by the list obtained by dropping the first \(|t|\) elements of \(s\), where \(|t|\) is the length of \(t\).

theorem append_of_commonPrefix_eq {α : Type u} [DecidableEq α] {xs ys : List α}
    (h : commonPrefix xs ys = ys) : xs = ys ++ xs.drop ys.length
Uses 2 · Used by 2
Statement usesLongest common prefix
Proof usesA list is its common prefix with another list followed by the rest
Used byLookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged

TheoremThe longest common prefix of a list and its prefix#✓fully proved

Let \(s\), \(t\) and \(u\) be lists over a type with decidable equality. If \(s\) is \(t\) followed by \(u\), then the longest common prefix of \(s\) and \(t\) is \(t\).

theorem commonPrefix_eq_of_append {α : Type u} [DecidableEq α] {xs ys t : List α}
    (h : xs = ys ++ t) : commonPrefix xs ys = ys
Uses 2 · Used by 4
Statement usesLongest common prefix
Proof usesA shared prefix factors out of the longest common prefix
Used byPrefix search is correct on valid radix tries · Lookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie

DefinitionEdge search by first symbol#✓fully proved

Given a symbol \(c\) and a list of edges, each a pair of a label (a list of symbols) and a subtree, this returns the first edge in the list whose label starts with \(c\), or nothing if no label starts with \(c\).

def findEdge {α : Type u} {β : Type v} [DecidableEq α] (c : α) :
    List (List α × RadixTrie α β) → Option (List α × RadixTrie α β)
  | [] => none
  | (label, child) :: rest =>
      if label.head? = some c then some (label, child) else findEdge c rest
Uses 1 · Used by 8
Statement usesRadix trie
Used byPrefix search in a radix trie · Prefix search is correct on valid radix tries · Insertion into a radix trie · Insertion preserves validity of radix tries · Lookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie · Radix trie lookup of a nonempty key at a node

DefinitionReplacing the child edge for a symbol#✓fully proved

Given a symbol \(c\), an edge \(e\) (a pair of a label and a radix trie) and a list of child edges, this operation replaces the first edge of the list whose label starts with \(c\) by \(e\) and keeps all other edges in order. If no label in the list starts with \(c\), it appends \(e\) at the end of the list.

def replaceEdge {α : Type u} {β : Type v} [DecidableEq α] (c : α)
    (newEdge : List α × RadixTrie α β) :
    List (List α × RadixTrie α β) → List (List α × RadixTrie α β)
  | [] => [newEdge]
  | (label, child) :: rest =>
      if label.head? = some c then newEdge :: rest
      else (label, child) :: replaceEdge c newEdge rest
Uses 1 · Used by 4
Statement usesRadix trie
Used byInsertion into a radix trie · Insertion preserves validity of radix tries · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie

DefinitionRadix trie lookup#✓fully proved

Looking up a key, a list over \(\alpha\), in a radix trie returns an optional value. At a node, the empty key returns the value stored at the node, if any. A nonempty key \(k\) with first symbol \(c\) goes to the first child edge whose label starts with \(c\). If there is no such edge, or its label \(\ell\) is not a prefix of \(k\), the lookup returns no value; otherwise it continues in the subtree of that edge with \(k\) minus its first \(|\ell|\) symbols.

def lookup {α : Type u} {β : Type v} [DecidableEq α] :
    RadixTrie α β → List α → Option β
  | .node value _, [] => value
  | .node _ children, key@(_ :: _) => lookupChildren children key
where
  lookupChildren : List (List α × RadixTrie α β) → List α → Option β
    | [], _ => none
    | (label, child) :: rest, key@(c :: _) =>
        if label.head? = some c then
          if commonPrefix key label = label then
            lookup child (key.drop label.length)
          else none
        else lookupChildren rest key
    | _ :: _, [] => none
Uses 2 · Used by 12
Statement usesRadix trie · Longest common prefix
Used byEvery listed key is present in the built radix trie · Lookup in a radix trie built from a list with distinct keys · Lookup in the empty radix trie · Lookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie · Radix trie lookup of a nonempty key at a node · Keys of a radix trie built from a list · Stored keys of a valid radix trie are the keys with a successful lookup · Lookups in a radix trie built from a list come from the list · Lookup in the suffix tree returns starting indices · Lookup of a suffix returns its starting index

TheoremRadix trie lookup of a nonempty key at a node#✓fully proved

Let \(k\) be a nonempty key with first symbol \(c\), and consider a node with children \(C\) (a list of edges, each a label with a subtree), whatever value the node stores. If no edge of \(C\) has a label starting with \(c\), looking up \(k\) at the node returns no value. Otherwise let \((\ell, T')\) be the first such edge of \(C\): if the longest common prefix of \(k\) and \(\ell\) is \(\ell\), the lookup returns the lookup in \(T'\) of the key obtained from \(k\) by dropping its first \(|\ell|\) symbols, and otherwise it returns no value.

theorem lookup_node_cons {α : Type u} {β : Type v} [DecidableEq α]
    (value : Option β) (children : List (List α × RadixTrie α β)) (c : α)
    (ks : List α) :
    lookup (.node value children) (c :: ks) =
      match findEdge c children with
Uses 4 · Used by 4
Statement usesRadix trie · Longest common prefix · Edge search by first symbol · Radix trie lookup
Used byLookup in the empty radix trie · Lookup agrees with the entries of a valid radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie

TheoremLookup in the empty radix trie#✓fully proved

For every key \(k\), looking up \(k\) in the empty radix trie returns no value.

@[simp]
theorem lookup_empty {α : Type u} {β : Type v} [DecidableEq α]
    (keys : List α) : (empty : RadixTrie α β).lookup keys = none
Uses 4 · Used by 1
Statement usesEmpty radix trie · Radix trie lookup
Proof usesRadix trie · Radix trie lookup of a nonempty key at a node
Used byLookups in a radix trie built from a list come from the list

DefinitionInsertion into a radix trie#✓fully proved

Inserting a value \(v\) at a key \(k\) (a list of symbols) into a radix trie works as follows. If \(k\) is empty, the root's value becomes \(v\). Otherwise let \(c\) be the first symbol of \(k\). If no child edge of the root has a label starting with \(c\), a new edge labelled \(k\) leading to a leaf storing \(v\) is added after the existing edges. Otherwise take the first such edge, with label \(\ell\) and subtree \(s\), let \(q\) be the longest common prefix of \(k\) and \(\ell\), and replace that edge in place. If \(k = \ell = q\), the edge keeps label \(\ell\) and leads to \(s\) with its root value set to \(v\). If \(k = q\) but \(\ell\) is longer, the edge is labelled \(q\) and leads to a new node storing \(v\) whose only edge is the rest of \(\ell\) leading to \(s\). If \(\ell = q\) but \(k\) is longer, the edge keeps label \(\ell\) and leads to \(s\) with \(v\) inserted at the rest of \(k\). If both are longer than \(q\), the edge is labelled \(q\) and leads to a new node with no value and two edges: the rest of \(\ell\) leading to \(s\), then the rest of \(k\) leading to a leaf storing \(v\).

Cslib.Algorithms.Lean.RadixTrie.insert · 39 lines 
def insert {α : Type u} {β : Type v} [DecidableEq α]
    (trie : RadixTrie α β) (key : List α) (value : β) : RadixTrie α β :=
  match trie, key with
  | .node _ children, [] => .node (some value) children
  | .node current children, (c :: ks) =>
      match _hfind : findEdge c children with
      | none => .node current (replaceEdge c ((c :: ks), .node (some value) []) children)
      | some (label, child) =>
          if (c :: ks).drop (commonPrefix (c :: ks) label).length = [] then
            if label.drop (commonPrefix (c :: ks) label).length = [] then
              .node current (replaceEdge c (label, child.insert [] value) children)
            else
              .node current (replaceEdge c
                (commonPrefix (c :: ks) label,
                  .node (some value)
                    [(label.drop (commonPrefix (c :: ks) label).length, child)])
                children)
          else if label.drop (commonPrefix (c :: ks) label).length = [] then
            .node current (replaceEdge c
              (label, child.insert
                ((c :: ks).drop (commonPrefix (c :: ks) label).length) value)
              children)
          else
            .node current (replaceEdge c
              (commonPrefix (c :: ks) label,
                .node none
                  [(label.drop (commonPrefix (c :: ks) label).length, child),
                    ((c :: ks).drop (commonPrefix (c :: ks) label).length,
                      .node (some value) [])])
              children)
termination_by key.length
decreasing_by
  all_goals
    have hhead := findEdge_some_head _hfind
    obtain ⟨ls, rfl⟩ := exists_cons_of_head?_eq_some hhead
    have hcp : commonPrefix (c :: ks) (c :: ls) = c :: commonPrefix ks ls := by
      rw [commonPrefix_cons_cons, ite_eq_left rfl]
    simp only [List.length_drop, hcp, List.length_cons, List.length_nil]
    omega
Uses 4 · Used by 7
Statement usesRadix trie · Longest common prefix · Edge search by first symbol · Replacing the child edge for a symbol
Used byRadix trie built from a list of key-value pairs · Insertion preserves validity of radix tries · Every listed key is present in the built radix trie · Lookup in a radix trie built from a list with distinct keys · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie · Lookups in a radix trie built from a list come from the list

TheoremLookup of a key just inserted into a radix trie#✓fully proved

For every radix trie \(T\), key \(k\) and value \(v\), looking up \(k\) in the trie obtained from \(T\) by inserting \(v\) at \(k\) returns \(v\).

@[simp]
theorem lookup_insert_same {α : Type u} {β : Type v} [DecidableEq α]
    (trie : RadixTrie α β) (keys : List α) (value : β) :
    (trie.insert keys value).lookup keys = some value
Uses 10 · Used by 3
Statement usesRadix trie · Insertion into a radix trie · Radix trie lookup
Proof usesLongest common prefix · Longest common prefix in terms of dropped remainders · The longest common prefix of a list and its prefix · Longest common prefix of a list with itself · Edge search by first symbol · Radix trie lookup of a nonempty key at a node · Replacing the child edge for a symbol
Used byEvery listed key is present in the built radix trie · Lookup in a radix trie built from a list with distinct keys · Lookups in a radix trie built from a list come from the list

TheoremInsertion into a radix trie leaves lookups of other keys unchanged#✓fully proved

For every radix trie \(T\), all keys \(k \ne k'\) and every value \(v\), looking up \(k\) in the trie obtained from \(T\) by inserting \(v\) at \(k'\) gives the same result as looking up \(k\) in \(T\).

@[simp]
theorem lookup_insert_of_ne {α : Type u} {β : Type v} [DecidableEq α]
    (trie : RadixTrie α β) {insertedKeys keys : List α} (value : β)
    (h : keys ≠ insertedKeys) :
    (trie.insert insertedKeys value).lookup keys = trie.lookup keys
Uses 11 · Used by 3
Statement usesRadix trie · Insertion into a radix trie · Radix trie lookup
Proof usesWhen the common prefix is the second list, the first list extends it · Longest common prefix · A shared prefix factors out of the longest common prefix · Longest common prefix in terms of dropped remainders · The longest common prefix of a list and its prefix · Edge search by first symbol · Radix trie lookup of a nonempty key at a node · Replacing the child edge for a symbol
Used byEvery listed key is present in the built radix trie · Lookup in a radix trie built from a list with distinct keys · Lookups in a radix trie built from a list come from the list

DefinitionPath-compressed root#✓fully proved

A radix trie is path-compressed at its root when its root node stores a value or has at least two child edges.

A value-free node with at most one child could be merged into the edge above it, which a radix trie rules out for every node reached by an edge; the root of the whole trie has no incoming edge and is exempt.

def RootCompact {α : Type u} {β : Type v} : RadixTrie α β → Prop
  | .node cv cc => cv ≠ none ∨ 2 ≤ cc.length
Uses 1 · Used by 8
Statement usesRadix trie
Used byThe empty radix trie is valid · Prefix search is correct on valid radix tries · Insertion preserves validity of radix tries · Stored keys of a valid radix trie are distinct · Lookup agrees with the entries of a valid radix trie · Sibling edge labels start with distinct symbols · Children of a valid node are path-compressed · Valid radix trie

InductiveValid radix trie#✓fully proved

Validity of radix tries is defined inductively: a node is valid when every label of its child edges is nonempty, the first symbols of the labels of its child edges are pairwise distinct, and for each child edge the subtree at its end is valid and path-compressed at its root (its root stores a value or has at least two child edges).

Thus every value-free node other than the root has at least two children, so no unary value-free node remains to be merged into its parent edge.

inductive Valid {α : Type u} {β : Type v} : RadixTrie α β → Prop where
  | node {value : Option β} {children : List (List α × RadixTrie α β)}
      (nonempty : ∀ e ∈ children, e.1 ≠ [])
      (distinct : (children.map (fun e => e.1.head?)).Nodup)
      (childrenValid : ∀ e ∈ children, Valid e.2)
      (compact : ∀ e ∈ children, RootCompact e.2) :
      Valid (.node value children)
Uses 2 · Used by 11
Statement usesRadix trie · Path-compressed root
Used byThe empty radix trie is valid · Prefix search is correct on valid radix tries · Insertion preserves validity of radix tries · Stored keys of a valid radix trie are distinct · Lookup agrees with the entries of a valid radix trie · Keys of a radix trie built from a list · Stored keys of a valid radix trie are the keys with a successful lookup · Sibling edge labels start with distinct symbols · Children of a valid node are path-compressed · Suffix-tree search finds exactly the prefixes of suffixes · The suffix tree stores one key per suffix

TheoremThe empty radix trie is valid#✓fully proved

For all types \(\alpha\) and \(\beta\), the empty radix trie whose keys are lists over \(\alpha\) and whose values lie in \(\beta\) is valid.

theorem Valid.empty {α : Type u} {β : Type v} : Valid (empty : RadixTrie α β)
Uses 4 · Used by 3
Statement usesValid radix trie · Empty radix trie
Proof usesRadix trie · Path-compressed root
Used byKeys of a radix trie built from a list · Suffix-tree search finds exactly the prefixes of suffixes · The suffix tree stores one key per suffix

TheoremSibling edge labels start with distinct symbols#✓fully proved

If a radix-trie node with child edges \((\ell_1, t_1), \dots, (\ell_n, t_n)\) is valid, then the first symbols of the labels \(\ell_1, \dots, \ell_n\) are pairwise distinct.

theorem Valid.nodup_child_heads {α : Type u} {β : Type v} {value : Option β}
    {children : List (List α × RadixTrie α β)}
    (h : Valid (.node value children)) :
    (children.map (fun e => e.1.head?)).Nodup
Uses 3
Statement usesRadix trie · Valid radix trie
Proof usesPath-compressed root

TheoremChildren of a valid node are path-compressed#✓fully proved

If a radix-trie node is valid, then for each of its child edges, the subtree at the end of that edge is path-compressed at its root: its root stores a value or has at least two child edges.

theorem Valid.rootCompact_child {α : Type u} {β : Type v} {value : Option β}
    {children : List (List α × RadixTrie α β)}
    (h : Valid (.node value children)) {e : List α × RadixTrie α β}
    (he : e ∈ children) :
    RootCompact e.2
Uses 3
Statement usesRadix trie · Path-compressed root · Valid radix trie

TheoremInsertion preserves validity of radix tries#✓fully proved

If \(t\) is a valid radix trie, then for every key \(k\) and value \(v\), the trie obtained by inserting \(v\) at \(k\) in \(t\) is valid.

theorem Valid.insert {α : Type u} {β : Type v} [DecidableEq α]
    {trie : RadixTrie α β} (h : Valid trie) (keys : List α) (value : β) :
    Valid (trie.insert keys value)
Uses 8 · Used by 3
Statement usesRadix trie · Valid radix trie · Insertion into a radix trie
Proof usesPath-compressed root · Longest common prefix · Longest common prefix in terms of dropped remainders · Edge search by first symbol · Replacing the child edge for a symbol
Used byKeys of a radix trie built from a list · Suffix-tree search finds exactly the prefixes of suffixes · The suffix tree stores one key per suffix

DefinitionEntries of a radix trie#✓fully proved

The entries of a radix trie are its key-value pairs, listed recursively. For a node with child edges \((\ell_1, t_1), \dots, (\ell_n, t_n)\) in stored order, the list starts with the pair \((\varepsilon, v)\), where \(\varepsilon\) is the empty key, if the node stores a value \(v\); it continues with the entries of \(t_1\) with \(\ell_1\) prepended to every key, then the entries of \(t_2\) with \(\ell_2\) prepended, and so on up to \(t_n\).

def entries {α : Type u} {β : Type v} : RadixTrie α β → List (List α × β)
  | .node value children =>
      (match value with
       | none => []
       | some result => [([], result)]) ++ childEntries children
where
  childEntries : List (List α × RadixTrie α β) → List (List α × β)
    | [] => []
    | (label, child) :: children =>
        child.entries.map (fun (keys, result) => (label ++ keys, result)) ++
          childEntries children
Uses 1 · Used by 5
Statement usesRadix trie
Used byPrefix search is correct on valid radix tries · Stored keys of a radix trie · Stored keys of a valid radix trie are distinct · Lookup agrees with the entries of a valid radix trie · Stored keys of a valid radix trie are the keys with a successful lookup

DefinitionStored keys of a radix trie#✓fully proved

The stored keys of a radix trie form the list of the keys of its entries, in the same order.

def keys {α : Type u} {β : Type v} (trie : RadixTrie α β) : List (List α) :=
  trie.entries.map Prod.fst
Uses 2 · Used by 8
Statement usesRadix trie · Entries of a radix trie
Used byPrefix search in a radix trie · Prefix search is correct on valid radix tries · Stored keys of a valid radix trie are distinct · Keys of a radix trie built from a list · Stored keys of a valid radix trie are the keys with a successful lookup · Suffix-tree search finds exactly the prefixes of suffixes · The stored keys of a suffix tree are its terminated suffixes · Stored keys of the suffix tree

TheoremLookup agrees with the entries of a valid radix trie#✓fully proved

For a valid radix trie \(T\), every key \(k\) and every value \(v\), looking up \(k\) in \(T\) returns \(v\) if and only if the pair \((k, v)\) occurs in the list of entries of \(T\).

theorem lookup_eq_some_iff_mem_entries {α : Type u} {β : Type v}
    [DecidableEq α] {trie : RadixTrie α β} (h : Valid trie) (keys : List α)
    (value : β) :
    trie.lookup keys = some value ↔ (keys, value) ∈ trie.entries
Uses 10 · Used by 1
Statement usesRadix trie · Valid radix trie · Entries of a radix trie · Radix trie lookup
Proof usesPath-compressed root · When the common prefix is the second list, the first list extends it · Longest common prefix · The longest common prefix of a list and its prefix · Edge search by first symbol · Radix trie lookup of a nonempty key at a node
Used byStored keys of a valid radix trie are the keys with a successful lookup

TheoremStored keys of a valid radix trie are the keys with a successful lookup#✓fully proved

For a valid radix trie \(T\) and every key \(k\), \(k\) is a stored key of \(T\) if and only if looking up \(k\) in \(T\) returns some value.

theorem mem_keys_iff {α : Type u} {β : Type v} [DecidableEq α]
    {trie : RadixTrie α β} (h : Valid trie) (key : List α) :
    key ∈ trie.keys ↔ ∃ value, trie.lookup key = some value
Uses 6 · Used by 1
Statement usesRadix trie · Valid radix trie · Stored keys of a radix trie · Radix trie lookup
Proof usesEntries of a radix trie · Lookup agrees with the entries of a valid radix trie
Used byKeys of a radix trie built from a list

TheoremStored keys of a valid radix trie are distinct#✓fully proved

If \(t\) is a valid radix trie, then its list of stored keys has no duplicates.

theorem Valid.keys_nodup {γ : Type u} {β : Type v} {t : RadixTrie γ β} (h : Valid t) :
    t.keys.Nodup
Uses 5 · Used by 1
Statement usesRadix trie · Valid radix trie · Stored keys of a radix trie
Proof usesPath-compressed root · Entries of a radix trie
Used byThe suffix tree stores one key per suffix

DefinitionPrefix search in a radix trie#✓fully proved

For a radix trie \(t\) and a pattern \(p\) (a list of symbols), prefix search returns a boolean computed as follows. If \(p\) is empty, it is true exactly when \(t\) stores at least one key. Otherwise let \(c\) be the first symbol of \(p\) and take the first child edge of the root whose label starts with \(c\); if there is none, the answer is false. If that edge has label \(\ell\) and subtree \(s\), then: when \(p\) is a prefix of \(\ell\), the answer is whether \(s\) stores at least one key; otherwise, when \(\ell\) is a prefix of \(p\), the search continues in \(s\) with \(p\) minus its first \(|\ell|\) symbols; otherwise the answer is false.

On valid radix tries this decides whether some stored key has \(p\) as a prefix.

Cslib.Algorithms.Lean.RadixTrie.hasPrefix · 18 lines 
def hasPrefix {γ : Type u} {β : Type v} [DecidableEq γ] (t : RadixTrie γ β)
    (p : List γ) : Bool :=
  match t, p with
  | t, [] => !t.keys.isEmpty
  | .node _ children, (c :: cs) =>
      match _hfind : findEdge c children with
      | none => false
      | some (label, child) =>
          if commonPrefix (c :: cs) label = (c :: cs) then !child.keys.isEmpty
          else if commonPrefix (c :: cs) label = label then
            hasPrefix child ((c :: cs).drop label.length)
          else false
termination_by p.length
decreasing_by
  have hhead := findEdge_some_head _hfind
  obtain ⟨ls, rfl⟩ := exists_cons_of_head?_eq_some hhead
  simp only [List.length_drop, List.length_cons]
  omega
Uses 4 · Used by 3
Statement usesRadix trie · Longest common prefix · Edge search by first symbol · Stored keys of a radix trie
Used byPrefix search is correct on valid radix tries · Suffix-tree search finds exactly the prefixes of suffixes · Suffix-tree search finds exactly the infixes

TheoremPrefix search is correct on valid radix tries#✓fully proved

For a valid radix trie \(t\) and a list \(p\) of symbols, prefix search for \(p\) in \(t\) succeeds if and only if some stored key \(k\) of \(t\) has \(p\) as a prefix.

theorem hasPrefix_eq_true_iff {γ : Type u} {β : Type v} [DecidableEq γ]
    {t : RadixTrie γ β} (h : Valid t) (p : List γ) :
    t.hasPrefix p = true ↔ ∃ k ∈ t.keys, p <+: k
Uses 11 · Used by 1
Statement usesRadix trie · Valid radix trie · Prefix search in a radix trie · Stored keys of a radix trie
Proof usesPath-compressed root · A list is its common prefix with another list followed by the rest · Longest common prefix · The longest common prefix of a list and its prefix · Characterization of the longest common prefix · Entries of a radix trie · Edge search by first symbol
Used bySuffix-tree search finds exactly the prefixes of suffixes

DefinitionRadix trie built from a list of key-value pairs#✓fully proved

The trie built from the empty list is the empty trie, and the trie built from a list with head \((k, v)\) and tail \(L\) is the trie built from \(L\) with the value \(v\) inserted at the key \(k\). Later pairs in the list are thus inserted first, so on duplicate keys the head-most value wins.

def buildFrom {γ : Type u} {β : Type v} [DecidableEq γ] :
    List (List γ × β) → RadixTrie γ β
  | [] => empty
  | (k, v) :: L => (buildFrom L).insert k v
Uses 3 · Used by 8
Statement usesRadix trie · Empty radix trie · Insertion into a radix trie
Used byEvery listed key is present in the built radix trie · Lookup in a radix trie built from a list with distinct keys · Keys of a radix trie built from a list · Lookups in a radix trie built from a list come from the list · Suffix-tree search finds exactly the prefixes of suffixes · The stored keys of a suffix tree are its terminated suffixes · The suffix tree stores one key per suffix · Suffix tree

TheoremEvery listed key is present in the built radix trie#✓fully proved

For a list \(L\) of key-value pairs, if \((k, v)\) belongs to \(L\), then looking up \(k\) in the radix trie built from \(L\) returns some value.

theorem lookup_buildFrom_exists_of_mem {γ : Type u} {β : Type v} [DecidableEq γ]
    {L : List (List γ × β)} {k : List γ} {v : β} (h : (k, v) ∈ L) :
    ∃ v', (buildFrom L).lookup k = some v'
Uses 5 · Used by 1
Statement usesRadix trie built from a list of key-value pairs · Radix trie lookup
Proof usesInsertion into a radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie
Used byKeys of a radix trie built from a list

TheoremLookups in a radix trie built from a list come from the list#✓fully proved

For every list \(L\) of key-value pairs, if looking up a key \(k\) in the radix trie built from \(L\) returns a value \(v\), then the pair \((k, v)\) occurs in \(L\).

theorem mem_of_lookup_buildFrom {γ : Type u} {β : Type v} [DecidableEq γ]
    {L : List (List γ × β)} {k : List γ} {v : β}
    (h : (buildFrom L).lookup k = some v) : (k, v) ∈ L
Uses 6 · Used by 2
Statement usesRadix trie built from a list of key-value pairs · Radix trie lookup
Proof usesInsertion into a radix trie · Lookup in the empty radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie
Used byKeys of a radix trie built from a list · Lookup in the suffix tree returns starting indices

TheoremKeys of a radix trie built from a list#✓fully proved

For every list \(L\) of key-value pairs and every key \(k\), \(k\) is a stored key of the radix trie built from \(L\) if and only if the pair \((k, v)\) occurs in \(L\) for some value \(v\).

theorem mem_keys_buildFrom {γ : Type u} {β : Type v} [DecidableEq γ]
    {L : List (List γ × β)} {k : List γ} :
    k ∈ (buildFrom L).keys ↔ ∃ v, (k, v) ∈ L
Uses 9 · Used by 1
Statement usesRadix trie built from a list of key-value pairs · Stored keys of a radix trie
Proof usesValid radix trie · The empty radix trie is valid · Insertion preserves validity of radix tries · Radix trie lookup · Every listed key is present in the built radix trie · Stored keys of a valid radix trie are the keys with a successful lookup · Lookups in a radix trie built from a list come from the list
Used byThe stored keys of a suffix tree are its terminated suffixes

TheoremLookup in a radix trie built from a list with distinct keys#✓fully proved

Let \(L\) be a list of key-value pairs, whose keys are lists over \(\gamma\), in which no key occurs twice. If the pair \((k, v)\) occurs in \(L\), then looking up \(k\) in the radix trie built from \(L\) returns \(v\).

theorem lookup_buildFrom_of_mem {γ : Type u} {β : Type v} [DecidableEq γ]
    {L : List (List γ × β)} (hnd : (L.map Prod.fst).Nodup) {k : List γ} {v : β}
    (h : (k, v) ∈ L) : (buildFrom L).lookup k = some v
Uses 5 · Used by 1
Statement usesRadix trie built from a list of key-value pairs · Radix trie lookup
Proof usesInsertion into a radix trie · Insertion into a radix trie leaves lookups of other keys unchanged · Lookup of a key just inserted into a radix trie
Used byLookup of a suffix returns its starting index

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.