DictionaryStream.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

A bounded dictionary driven by a stream cursor

The executable loop reads one key, updates the trie and its counters, and tail-calls with the next cursor. Lists and finite key sets below are proof views only; the loop stores neither a trace nor a set of all possible keys.

def OAI.LowSpaceSubsetSum.BinaryTrie.keySet line 16
theorem OAI.LowSpaceSubsetSum.BinaryTrie.mem_keySet line 22
theorem OAI.LowSpaceSubsetSum.BinaryTrie.card_keySet line 32
theorem OAI.LowSpaceSubsetSum.BinaryTrie.keySet_width line 49
theorem OAI.LowSpaceSubsetSum.BinaryTrie.keySet_insert line 67
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_fits_universe line 82
Source documentation
A fitting universe of keys prevents overflow, even when the stream contains arbitrarily many repetitions. The initial trie may already hold some keys from that same universe.
```
theorem build_fits_universe {C width : ℕ} {t : Tree} {keys : List (List Bool)}
    {U : Finset (List Bool)} (ht : HasWidth t width)
    (hwidth : ∀ key ∈ U, key.length = width)
    (htU : keySet t ⊆ U) (hkeys : ∀ key ∈ keys, key ∈ U) (hcap : U.card ≤ C) :
    (build C t keys).overflow = false := by
…
```
Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.HasWidth, OAI.LowSpaceSubsetSum.BinaryTrie.keySet, OAI.LowSpaceSubsetSum.BinaryTrie.build
theorem OAI.LowSpaceSubsetSum.BinaryTrie.build_complete_processed line 105
structure OAI.LowSpaceSubsetSum.BinaryTrie.StreamResult line 122

def OAI.LowSpaceSubsetSum.BinaryTrie.run line 131

Source documentation

Tail-recursive implementation. Every recursive call receives the updated cursor, trie and counters. A capacity violation stops immediately.

def run {σ : Type u} (C : ℕ) (read : σ → Option (List Bool × σ)) :
    ℕ → σ → Tree → ℕ → ℕ → StreamResult σ
  | 0, s, t, processed, queries => ⟨s, t, false, processed, queries⟩
  | fuel + 1, s, t, processed, queries =>
    match read s with
    | none => ⟨s, t, false, processed, queries + 1⟩
    | some (key, next) =>
      if contains t key then run C read fuel next t (processed + 1) (queries + 1)
      else
        let t' := insert t key
…

Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.StreamResult, OAI.LowSpaceSubsetSum.BinaryTrie.contains, OAI.LowSpaceSubsetSum.BinaryTrie.insert

def OAI.LowSpaceSubsetSum.BinaryTrie.readKeys line 145

Source documentation

Finite output trace, used only to state and prove the loop's behavior.

def readKeys {σ : Type u} (read : σ → Option (List Bool × σ)) :
    ℕ → σ → List (List Bool)
  | 0, _ => []
  | fuel + 1, s => match read s with
    | none => []
    | some (key, next) => key :: readKeys read fuel next

theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_spec line 152
theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_queries_le line 173

theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_queries_processed line 192

Source documentation

At most one reader query is spent detecting the end of the stream. The bound also holds for an overflow stop or an exhausted fuel budget.

theorem run_queries_processed {σ : Type u} (C : ℕ)
    (read : σ → Option (List Bool × σ)) (fuel : ℕ) (s : σ) (t : Tree)
    (processed queries : ℕ) :
    (run C read fuel s t processed queries).queries + processed ≤
      queries + (run C read fuel s t processed queries).processed + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.run

def OAI.LowSpaceSubsetSum.BinaryTrie.advance line 213
theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_cursor line 219
theorem OAI.LowSpaceSubsetSum.BinaryTrie.readKeys_eq_take line 238
theorem OAI.LowSpaceSubsetSum.BinaryTrie.advance_view line 254

theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_complete line 272

Source documentation

The actual cursor loop completes and retains exactly the streamed keys when they lie in a fixed-width universe whose cardinality fits the cap.

theorem run_complete {σ : Type u} {C width fuel : ℕ}
    (read : σ → Option (List Bool × σ)) (view : σ → List (List Bool))
    (hread : RowMerge.IsReader read view) (s : σ) {U : Finset (List Bool)}
    (hfuel : (view s).length ≤ fuel)
    (hwidth : ∀ key ∈ U, key.length = width)
    (hkeys : ∀ key ∈ view s, key ∈ U) (hcap : U.card ≤ C) :
    let r := run C read fuel s .empty 0 0
…

Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.BinaryTrie.run

theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_complete_distinct line 296
theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_complete_exhausts line 310
theorem OAI.LowSpaceSubsetSum.BinaryTrie.run_complete_from_values line 326