Trie.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Fixed-width binary dictionaries

An executable sparse binary trie for fixed-width keys, with exact membership and insertion semantics and a node-count bound. The array of retained records is separate; the trie is used to decide whether a key is new. This is the bounded dictionary component in the paper's stream implementation.

inductive OAI.LowSpaceSubsetSum.BinaryTrie.Tree line 18
def OAI.LowSpaceSubsetSum.BinaryTrie.contains line 24
def OAI.LowSpaceSubsetSum.BinaryTrie.insert line 31
def OAI.LowSpaceSubsetSum.BinaryTrie.nodes line 38
def OAI.LowSpaceSubsetSum.BinaryTrie.entries line 43

def OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth line 49

Source documentation

All present keys have the specified length. Empty subtrees are allowed.

def HasWidth : Tree → ℕ → Prop
  | .empty, _ => True
  | .leaf, width => width = 0
  | .node _ _, 0 => False
  | .node zero one, width + 1 => HasWidth zero width ∧ HasWidth one width

/-- No internal node is retained if both its branches are empty. -/

Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree

def OAI.LowSpaceSubsetSum.BinaryTrie.Compact line 56
Source documentation
No internal node is retained if both its branches are empty.
```
def Compact : Tree → Prop
  | .empty => True
  | .leaf => True
  | .node zero one => Compact zero ∧ Compact one ∧ (zero ≠ .empty ∨ one ≠ .empty)
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree
theorem OAI.LowSpaceSubsetSum.BinaryTrie.insert_ne_empty line 61
theorem OAI.LowSpaceSubsetSum.BinaryTrie.entries_pos_of_ne_empty line 66
theorem OAI.LowSpaceSubsetSum.BinaryTrie.insert_hasWidth line 81
theorem OAI.LowSpaceSubsetSum.BinaryTrie.insert_compact line 100
theorem OAI.LowSpaceSubsetSum.BinaryTrie.nodes_le_width_mul_entries line 117
Source documentation
The number of retained nodes is linear in key width times distinct keys.
```
theorem nodes_le_width_mul_entries {t : Tree} {width : ℕ}
    (ht : HasWidth t width) (hc : Compact t) : nodes t ≤ (width + 1) * entries t := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.Compact, OAI.LowSpaceSubsetSum.BinaryTrie.nodes, OAI.LowSpaceSubsetSum.BinaryTrie.entries
theorem OAI.LowSpaceSubsetSum.BinaryTrie.entries_insert line 136
Source documentation
One insertion adds a key exactly when membership previously failed.
```
theorem entries_insert {t : Tree} {key : List Bool} {width : ℕ}
    (ht : HasWidth t width) (hk : key.length = width) :
    entries (insert t key) = entries t + if contains t key then 0 else 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.entries, OAI.LowSpaceSubsetSum.BinaryTrie.insert, OAI.LowSpaceSubsetSum.BinaryTrie.contains
theorem OAI.LowSpaceSubsetSum.BinaryTrie.contains_insert_iff line 161
Source documentation
Exact set insertion semantics for keys of the fixed width.
```
theorem contains_insert_iff {t : Tree} {key query : List Bool} {width : ℕ}
    (ht : HasWidth t width) (hk : key.length = width) (hq : query.length = width) :
    contains (insert t key) query = true ↔ query = key ∨ contains t query = true := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.contains, OAI.LowSpaceSubsetSum.BinaryTrie.insert
def OAI.LowSpaceSubsetSum.BinaryTrie.lookupSteps line 192
Source documentation
The number of nodes examined by a membership lookup.
```
def lookupSteps : Tree → List Bool → ℕ
  | .node zero one, b :: key => 1 + lookupSteps (if b then one else zero) key
  | _, _ => 1
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree
theorem OAI.LowSpaceSubsetSum.BinaryTrie.lookupSteps_le line 196
theorem OAI.LowSpaceSubsetSum.BinaryTrie.nodes_insert_le line 212
theorem OAI.LowSpaceSubsetSum.BinaryTrie.nodes_insert_le_capacity line 235
Source documentation
A hard entry capacity also bounds nodes, including a first rejected key.
```
theorem nodes_insert_le_capacity {t : Tree} {key : List Bool} {width C : ℕ}
    (ht : HasWidth t width) (hc : Compact t) (hk : key.length = width)
    (hcap : entries t ≤ C) : nodes (insert t key) ≤ (width + 1) * (C + 1) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.Compact, OAI.LowSpaceSubsetSum.BinaryTrie.entries, OAI.LowSpaceSubsetSum.BinaryTrie.nodes, OAI.LowSpaceSubsetSum.BinaryTrie.insert