Trie

InductiveTrie#✓fully proved

A trie with keys that are lists over \(\alpha\) and values in \(\beta\) is a node consisting of an optional value in \(\beta\) and a finite list of children, each child being a pair of a letter in \(\alpha\) and a trie. The letters labelling the children need not be distinct.

inductive Trie (α : Type u) (β : Type v) where
  | node : Option β → List (α × Trie α β) → Trie α β

Used by 28

Used byDeletion from a trie · Deletion preserves trie validity · Empty trie · Validity of the empty trie · Entries of a trie · Trie insertion · Insertion preserves trie validity · Insertions at distinct keys commute in a trie · Empty trie nodes · Characterization of empty nodes · Trie lookup · Deletion does not affect other keys · A deleted key is absent · Trie lookup agrees with the entries · Lookup equivalence of tries · Trie insertion leaves other keys unchanged · Lookup after insertion in a trie · Setting a child leaves the other children unchanged · Looking up a child just set · Lookup-equivalent valid tries have the same entries · Valid trie nodes have distinct child keys · Reflexivity of trie lookup equivalence · Setting a child in a trie's child list · Setting a child preserves validity · Setting a child preserves the child-list part of validity · Symmetry of trie lookup equivalence · Transitivity of trie lookup equivalence · Valid trie

DefinitionEmpty trie#✓fully proved

The empty trie is the trie consisting of a single root node that stores no value and has no children, so it contains no key-value entries.

def empty {α : Type u} {β : Type v} : Trie α β :=
  .node none []

Uses 1 · Used by 6

Statement usesTrie

Used byValidity of the empty trie · Trie insertion · Insertion preserves trie validity · Lookup in the empty trie · Trie insertion leaves other keys unchanged · Lookup after insertion in a trie

DefinitionTrie lookup#✓fully proved

The lookup of a key (a list over \(\alpha\)) in a trie returns an optional value in \(\beta\), by recursion on the key. For the empty key it is the optional value stored at the root. For a key with first letter \(a\) followed by the key \(k\), it fails if no child of the root is labelled \(a\), and otherwise it is the lookup of \(k\) in the first child labelled \(a\).

def lookup {α : Type u} {β : Type v} [DecidableEq α]
    (trie : Trie α β) : List α → Option β
  | [] =>
      match trie with
      | .node value _ => value
  | key :: keys =>
      match trie with
      | .node _ children =>
          match children.lookup key with
          | none => none
          | some child => lookup child keys

Uses 1 · Used by 12

Statement usesTrie

Used byInsertions at distinct keys commute in a trie · Deletion does not affect other keys · A deleted key is absent · Lookup in the empty trie · Trie lookup agrees with the entries · Lookup equivalence of tries · Trie insertion leaves other keys unchanged · Lookup after insertion in a trie · Lookup-equivalent valid tries have the same entries · Reflexivity of trie lookup equivalence · Symmetry of trie lookup equivalence · Transitivity of trie lookup equivalence

DefinitionTrie insertion#✓fully proved

Inserting a value \(v\) at a key \(k\) (a list of letters) in a trie stores \(v\) at the node reached by following \(k\) from the root, replacing any value stored there. Along the way, a missing child is created as an empty trie and appended after its siblings, an existing child is updated in place, and all other values and children are unchanged.

Cslib.Algorithms.Lean.Trie.insert · 17 lines

def insert {α : Type u} {β : Type v} [DecidableEq α]
    (trie : Trie α β) : List α → β → Trie α β
  | [], value =>
      match trie with
      | .node _ children => .node (some value) children
  | key :: keys, value =>
      match trie with
      | .node current children =>
          let child := (children.lookup key).getD empty
          .node current (childInsert key (insert child keys value) children)
where
  childInsert (key : α) (child : Trie α β) :
      List (α × Trie α β) → List (α × Trie α β)
    | [] => [(key, child)]
    | (key', child') :: children =>
        if key = key' then (key, child) :: children
        else (key', child') :: childInsert key child children

Uses 2 · Used by 4

Statement usesTrie · Empty trie

Used byInsertion preserves trie validity · Insertions at distinct keys commute in a trie · Trie insertion leaves other keys unchanged · Lookup after insertion in a trie

InductiveValid trie#✓fully proved

Validity of tries is defined inductively: a trie node with optional value \(v\) and child list \(c\) is valid when the letters labelling the children in \(c\) are pairwise distinct and every child trie in \(c\) is valid.

inductive Valid {α : Type u} {β : Type v} : Trie α β → Prop where
  | node {value : Option β} {children : List (α × Trie α β)}
      (distinct : (children.map Prod.fst).Nodup)
      (childrenValid : ∀ child ∈ children, Valid child.2) :
      Valid (.node value children)

Uses 1 · Used by 8

Statement usesTrie

Used byDeletion preserves trie validity · Validity of the empty trie · Insertion preserves trie validity · Trie lookup agrees with the entries · Lookup-equivalent valid tries have the same entries · Valid trie nodes have distinct child keys · Setting a child preserves validity · Setting a child preserves the child-list part of validity

DefinitionEntries of a trie#✓fully proved

The entries of a trie are the list of its key-value pairs, where a key is a list of letters. If the root stores a value \(v\), the list begins with the pair consisting of the empty key and \(v\); it continues, for each child in the stored sibling order, with the entries \((k, w)\) of that child, in order, each rewritten as \((a k, w)\), where \(a\) is the letter labelling the child and \(a k\) is the key \(k\) with \(a\) prepended.

def entries {α : Type u} {β : Type v} : Trie α β → List (List α × β)
  | .node value children =>
      (match value with
       | none => []
       | some result => [([], result)]) ++ childEntries children
where
  childEntries : List (α × Trie α β) → List (List α × β)
    | [] => []
    | (key, child) :: children =>
        child.entries.map (fun (keys, result) => (key :: keys, result)) ++
          childEntries children

Uses 1 · Used by 2

Statement usesTrie

Used byTrie lookup agrees with the entries · Lookup-equivalent valid tries have the same entries

TheoremLookup in the empty trie#✓fully proved

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

@[simp]
theorem lookup_empty {α : Type u} {β : Type v} [DecidableEq α]
    (keys : List α) : (empty : Trie α β).lookup keys = none

Uses 2 · Used by 2

Statement usesEmpty trie · Trie lookup

Used byDeletion does not affect other keys · Trie insertion leaves other keys unchanged

TheoremLookup after insertion in a trie#✓fully proved

Let \(\alpha\) be a type with decidable equality. For every trie \(T\) with keys that are lists over \(\alpha\) and values in \(\beta\), every key \(k\) and every value \(v \in \beta\), 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 : Trie α β) (keys : List α) (value : β) :
    (trie.insert keys value).lookup keys = some value

Uses 4 · Used by 1

Statement usesTrie · Trie insertion · Trie lookup

Proof usesEmpty trie

Used byInsertions at distinct keys commute in a trie

TheoremTrie insertion leaves other keys unchanged#✓fully proved

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

@[simp]
theorem lookup_insert_of_ne {α : Type u} {β : Type v} [DecidableEq α]
    (trie : Trie α β) {insertedKeys keys : List α} (value : β)
    (h : keys ≠ insertedKeys) :
    (trie.insert insertedKeys value).lookup keys = trie.lookup keys

Uses 5 · Used by 1

Statement usesTrie · Trie insertion · Trie lookup

Proof usesEmpty trie · Lookup in the empty trie

Used byInsertions at distinct keys commute in a trie

TheoremValid trie nodes have distinct child keys#✓fully proved

If a trie node with optional value \(v\) and child list \(c\) is valid, then the letters labelling the children in \(c\) are pairwise distinct.

theorem Valid.nodup_child_keys {α : Type u} {β : Type v}
    {value : Option β} {children : List (α × Trie α β)}
    (h : Valid (.node value children)) :
    (children.map Prod.fst).Nodup

Uses 2

Statement usesTrie · Valid trie

TheoremValidity of the empty trie#✓fully proved

The empty trie is valid.

theorem Valid.empty {α : Type u} {β : Type v} :
    Valid (empty : Trie α β)

Uses 3

Statement usesValid trie · Empty trie

Proof usesTrie

TheoremInsertion preserves trie validity#✓fully proved

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

theorem Valid.insert {α : Type u} {β : Type v} [DecidableEq α]
    {trie : Trie α β} (h : Valid trie) (keys : List α) (value : β) :
    Valid (trie.insert keys value)

Uses 4

Statement usesTrie · Valid trie · Trie insertion

Proof usesEmpty trie

TheoremTrie lookup agrees with the entries#✓fully proved

For every valid trie \(T\), every key \(k\) and every value \(v\), looking up \(k\) in \(T\) returns \(v\) if and only if \((k, v)\) is one of the entries of \(T\).

theorem lookup_eq_some_iff_mem_entries {α : Type u} {β : Type v}
    [DecidableEq α] {trie : Trie α β} (h : Valid trie)
    (keys : List α) (value : β) :
    trie.lookup keys = some value ↔ (keys, value) ∈ trie.entries

Uses 4 · Used by 1

Statement usesTrie · Valid trie · Entries of a trie · Trie lookup

Used byLookup-equivalent valid tries have the same entries

DefinitionLookup equivalence of tries#✓fully proved

Two tries \(T\) and \(T'\) are lookup-equivalent when, for every key \(k\), looking up \(k\) in \(T\) gives the same result as looking up \(k\) in \(T'\).

def LookupEquiv {α : Type u} {β : Type v} [DecidableEq α]
    (left right : Trie α β) : Prop :=
  ∀ keys, left.lookup keys = right.lookup keys

Uses 2 · Used by 5

Statement usesTrie · Trie lookup

Used byInsertions at distinct keys commute in a trie · Lookup-equivalent valid tries have the same entries · Reflexivity of trie lookup equivalence · Symmetry of trie lookup equivalence · Transitivity of trie lookup equivalence

TheoremReflexivity of trie lookup equivalence#✓fully proved

Every trie is lookup-equivalent to itself.

theorem LookupEquiv.refl {α : Type u} {β : Type v} [DecidableEq α]
    (trie : Trie α β) : LookupEquiv trie trie

Uses 3

Statement usesTrie · Lookup equivalence of tries

Proof usesTrie lookup

TheoremSymmetry of trie lookup equivalence#✓fully proved

If a trie \(T\) is lookup-equivalent to a trie \(T'\), then \(T'\) is lookup-equivalent to \(T\).

theorem LookupEquiv.symm {α : Type u} {β : Type v} [DecidableEq α]
    {left right : Trie α β} (h : LookupEquiv left right) : LookupEquiv right left

Uses 3

Statement usesTrie · Lookup equivalence of tries

Proof usesTrie lookup

TheoremTransitivity of trie lookup equivalence#✓fully proved

If a trie \(T_1\) is lookup-equivalent to a trie \(T_2\) and \(T_2\) is lookup-equivalent to a trie \(T_3\), then \(T_1\) is lookup-equivalent to \(T_3\).

theorem LookupEquiv.trans {α : Type u} {β : Type v} [DecidableEq α]
    {first second third : Trie α β}
    (h₁ : LookupEquiv first second) (h₂ : LookupEquiv second third) :
    LookupEquiv first third

Uses 3

Statement usesTrie · Lookup equivalence of tries

Proof usesTrie lookup

TheoremLookup-equivalent valid tries have the same entries#✓fully proved

Let \(T\) and \(T'\) be valid tries with keys that are lists over \(\alpha\) and values in \(\beta\), and suppose \(T\) and \(T'\) are lookup-equivalent. Then for every key \(k\) and every value \(v \in \beta\), the pair \((k, v)\) occurs in the entry list of \(T\) if and only if it occurs in the entry list of \(T'\).

theorem LookupEquiv.mem_entries_iff {α : Type u} {β : Type v} [DecidableEq α]
    {left right : Trie α β} (h : LookupEquiv left right)
    (hleft : Valid left) (hright : Valid right) (keys : List α) (value : β) :
    (keys, value) ∈ left.entries ↔ (keys, value) ∈ right.entries

Uses 6

Statement usesTrie · Lookup equivalence of tries · Valid trie · Entries of a trie

Proof usesTrie lookup · Trie lookup agrees with the entries

TheoremInsertions at distinct keys commute in a trie#✓fully proved

For every trie \(T\), all keys \(k_1 \ne k_2\) and all values \(v_1, v_2\), inserting \(v_1\) at \(k_1\) and then \(v_2\) at \(k_2\) gives a trie that is lookup-equivalent to the one obtained by inserting \(v_2\) at \(k_2\) and then \(v_1\) at \(k_1\).

theorem LookupEquiv.insert_comm {α : Type u} {β : Type v}
    [DecidableEq α] (trie : Trie α β)
    {firstKeys secondKeys : List α} (h : firstKeys ≠ secondKeys)
    (firstValue secondValue : β) :
    LookupEquiv
      ((trie.insert firstKeys firstValue).insert secondKeys secondValue)
      ((trie.insert secondKeys secondValue).insert firstKeys firstValue)

Uses 6

Statement usesTrie · Lookup equivalence of tries · Trie insertion

Proof usesTrie lookup · Trie insertion leaves other keys unchanged · Lookup after insertion in a trie

DefinitionEmpty trie nodes#✓fully proved

The empty-node test is true on a trie node exactly when the node carries no value and has no children; when deletion leaves a child in this state, the child is removed from its parent.

def isEmptyNode {α : Type u} {β : Type v} : Trie α β → Bool
  | .node value children => value.isNone && children.isEmpty

Uses 1 · Used by 7

Statement usesTrie

Used byCharacterization of empty nodes · Deletion does not affect other keys · A deleted key is absent · Setting a child leaves the other children unchanged · Looking up a child just set · Setting a child in a trie's child list · Setting a child preserves the child-list part of validity

TheoremCharacterization of empty nodes#✓fully proved

The empty-node test is true on a trie \(t\) exactly when \(t\) is the node with no value and no children, that is, the empty trie.

theorem isEmptyNode_eq_true_iff {α : Type u} {β : Type v}
    {t : Trie α β} : isEmptyNode t = true ↔ t = .node none []

Uses 2 · Used by 1

Statement usesTrie · Empty trie nodes

Used byDeletion does not affect other keys

DefinitionSetting a child in a trie's child list#✓fully proved

Let \(L\) be a list of pairs \((k, c)\) of a key \(k\) in \(\alpha\) and a trie \(c\) (the children of a trie node), let \(a\) be a key and \(t\) a trie, and call \(t\) empty when it carries no value and has no children. Setting the child at \(a\) to \(t\) in \(L\) gives the following list. If no entry of \(L\) has key \(a\), the result is \(L\) itself when \(t\) is empty, and \(L\) with \((a, t)\) appended at the end otherwise. If some entry of \(L\) has key \(a\), the entries before the first such entry are kept; that entry is replaced in place by \((a, t)\), or removed when \(t\) is empty; and every later entry with key \(a\) is removed, while later entries with other keys are kept in their order.

Thus the order of the surviving entries is preserved and at most one entry with key \(a\) remains, even when \(L\) has repeated keys. Deletion from a trie uses this operation to prune empty nodes.

def setChild {α : Type u} {β : Type v} [DecidableEq α] (key : α)
    (child : Trie α β) :
    List (α × Trie α β) → List (α × Trie α β)
  | [] => if isEmptyNode child then [] else [(key, child)]
  | (k, c) :: rest =>
      if k = key then
        if isEmptyNode child then rest.filter (fun entry => entry.1 != key)
        else (key, child) :: rest.filter (fun entry => entry.1 != key)
      else (k, c) :: setChild key child rest

Uses 2 · Used by 8

Statement usesTrie · Empty trie nodes

Used byDeletion from a trie · Deletion preserves trie validity · Deletion does not affect other keys · A deleted key is absent · Setting a child leaves the other children unchanged · Looking up a child just set · Setting a child preserves validity · Setting a child preserves the child-list part of validity

TheoremLooking up a child just set#✓fully proved

Let \(L\) be a list of letter–trie pairs, \(a\) a letter and \(c\) a trie, and let \(L'\) be obtained from \(L\) by setting the child at \(a\) to \(c\) (removing the entries at \(a\) instead when \(c\) has neither value nor children). Looking up \(a\) in \(L'\) finds nothing when \(c\) has neither value nor children, and finds \(c\) otherwise.

theorem lookup_setChild_self {α : Type u} {β : Type v}
    [DecidableEq α] (key : α) (child : Trie α β)
    (children : List (α × Trie α β)) :
    (setChild key child children).lookup key =
      if isEmptyNode child then none else some child

Uses 3 · Used by 2

Statement usesTrie · Empty trie nodes · Setting a child in a trie's child list

Used byDeletion does not affect other keys · A deleted key is absent

TheoremSetting a child leaves the other children unchanged#✓fully proved

Let \(L\) be a list of letter–trie pairs, \(c\) a trie and \(a \ne b\) letters, and let \(L'\) be obtained from \(L\) by setting the child at \(b\) to \(c\) (removing the entries at \(b\) instead when \(c\) has neither value nor children). Then looking up \(a\) in \(L'\) gives the same result as looking up \(a\) in \(L\).

theorem lookup_setChild_of_ne {α : Type u} {β : Type v}
    [DecidableEq α] {k key : α} (hk : k ≠ key) (child : Trie α β)
    (children : List (α × Trie α β)) :
    (setChild key child children).lookup k = children.lookup k

Uses 3 · Used by 1

Statement usesTrie · Setting a child in a trie's child list

Proof usesEmpty trie nodes

Used byDeletion does not affect other keys

TheoremSetting a child preserves the child-list part of validity#✓fully proved

Let \(L\) be a list of letter–trie pairs whose letters are pairwise distinct and whose tries are all valid, let \(c\) be a valid trie and \(a\) a letter. Then the list obtained from \(L\) by setting the child at \(a\) to \(c\) (removing the entries at \(a\) instead when \(c\) has neither value nor children) again has pairwise distinct letters, and every trie in it is valid.

theorem setChild_valid {α : Type u} {β : Type v}
    [DecidableEq α] {key : α} {child : Trie α β}
    {children : List (α × Trie α β)}
    (hkeys : (children.map Prod.fst).Nodup)
    (hchildren : ∀ entry ∈ children, Valid entry.2)
    (hchild : Valid child) :
    ((setChild key child children).map Prod.fst).Nodup ∧
      ∀ entry ∈ setChild key child children, Valid entry.2

Uses 4 · Used by 2

Statement usesTrie · Valid trie · Setting a child in a trie's child list

Proof usesEmpty trie nodes

Used byDeletion preserves trie validity · Setting a child preserves validity

TheoremSetting a child preserves validity#✓fully proved

Let a trie node with value \(v\) and child list \(L\) be valid, let \(c\) be a valid trie and \(a\) a letter. Then the node with value \(v\) whose child list is obtained from \(L\) by setting the child at \(a\) to \(c\) (removing the entries at \(a\) instead when \(c\) has neither value nor children) is valid.

theorem Valid.setChild {α : Type u} {β : Type v}
    [DecidableEq α] {value : Option β} {children : List (α × Trie α β)}
    (h : Valid (.node value children)) {key : α} {child : Trie α β}
    (hchild : Valid child) :
    Valid (.node value (setChild key child children))

Uses 4

Statement usesTrie · Valid trie · Setting a child in a trie's child list

Proof usesSetting a child preserves the child-list part of validity

DefinitionDeletion from a trie#✓fully proved

Deleting a key \(k\) (a list of letters) from a trie \(t\) works by recursion on \(k\). If \(k\) is empty, the root of \(t\) loses its value and keeps its children. If \(k\) consists of a first letter \(a\) followed by a key \(k'\) and the root of \(t\) has no child at \(a\), then \(t\) is unchanged. Otherwise \(k'\) is deleted from the first child at \(a\). If the result has neither value nor children, every entry at \(a\) is removed from the root's child list; if not, the first entry at \(a\) is replaced by the result and any later entries at \(a\) are removed. The root's value and the other children, in their order, are kept.

Deleting an absent key leaves every lookup unchanged.

def delete {α : Type u} {β : Type v} [DecidableEq α] (trie : Trie α β) :
    List α → Trie α β
  | [] =>
      match trie with
      | .node _ children => .node none children
  | key :: keys =>
      match trie with
      | .node current children =>
          match children.lookup key with
          | none => .node current children
          | some child =>
              .node current (setChild key (delete child keys) children)

Uses 2 · Used by 3

Statement usesTrie · Setting a child in a trie's child list

Used byDeletion preserves trie validity · Deletion does not affect other keys · A deleted key is absent

TheoremA deleted key is absent#✓fully proved

For every trie \(t\) and every key \(k\), looking up \(k\) in the trie obtained from \(t\) by deleting \(k\) finds no value.

@[simp]
theorem lookup_delete_self {α : Type u} {β : Type v} [DecidableEq α]
    (trie : Trie α β) (keys : List α) :
    (trie.delete keys).lookup keys = none

Uses 6

Statement usesTrie · Deletion from a trie · Trie lookup

Proof usesEmpty trie nodes · Looking up a child just set · Setting a child in a trie's child list

TheoremDeletion does not affect other keys#✓fully proved

For every trie \(t\) and all keys \(k \ne k'\), looking up \(k\) in the trie obtained from \(t\) by deleting \(k'\) gives the same result as looking up \(k\) in \(t\).

@[simp]
theorem lookup_delete_of_ne {α : Type u} {β : Type v} [DecidableEq α]
    (trie : Trie α β) {deletedKeys keys : List α}
    (h : keys ≠ deletedKeys) :
    (trie.delete deletedKeys).lookup keys = trie.lookup keys

Uses 9

Statement usesTrie · Deletion from a trie · Trie lookup

Proof usesEmpty trie nodes · Characterization of empty nodes · Lookup in the empty trie · Setting a child leaves the other children unchanged · Looking up a child just set · Setting a child in a trie's child list

TheoremDeletion preserves trie validity#✓fully proved

If a trie \(t\) is valid, that is, every node has distinct child keys and valid child tries, then for every key \(k\) the trie obtained from \(t\) by deleting \(k\) is valid.

theorem Valid.delete {α : Type u} {β : Type v} [DecidableEq α]
    {trie : Trie α β} (h : Valid trie) (keys : List α) :
    Valid (trie.delete keys)

Uses 5

Statement usesTrie · Valid trie · Deletion from a trie

Proof usesSetting a child in a trie's child list · Setting a child preserves the child-list part of validity

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.