Y-fast trie

33 fully proved

Grouped y-fast trie

StructureGrouped y-fast trie#✓fully proved

For natural numbers \(w\) and \(B\), a grouped y-fast trie over \(w\)-bit keys with group bound \(B\) consists of an x-fast trie over \(w\)-bit keys, which holds the representatives, and a list of groups, each a list of \(w\)-bit keys. The structure itself imposes no condition on these fields; the intended invariants (the representative trie is a valid x-fast trie whose keys are exactly the group maxima, every group is nonempty, strictly sorted and of length at most \(B\), and the groups are in increasing order) are imposed by the validity predicate.

Each group is a sorted list standing in for a balanced search tree; no complexity bound is claimed.

public structure GroupedYFastTrie (w B : Nat) where
  /-- The x-fast trie over representative keys (group maxima). -/
  reps : XFastTrie w
  /-- The groups, in increasing order. -/
  groups : List (List (Fin (2 ^ w)))

Uses 1 · Used by 17

Statement usesx-fast trie

Used byKeys of a grouped y-fast trie · Keys of the grouped y-fast trie built from a list · The empty grouped y-fast trie · Group of a representative · Stored keys are the keys of the groups · Membership query of a grouped y-fast trie · Correctness of the y-fast trie membership query · Building from a nonempty list with group bound zero gives an invalid trie · Grouped y-fast trie from a list of groups · Grouped y-fast trie from a sorted list · 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 · Assembling a valid grouped y-fast trie from groups

DefinitionKeys of a grouped y-fast trie#✓fully proved

The key set of a grouped y-fast trie \(t\) is the finite set of all keys that occur in some group of \(t\).

public def contents {w B : Nat} (t : GroupedYFastTrie w B) : Finset (Fin (2 ^ w)) :=
  t.groups.flatten.toFinset

Uses 1 · Used by 9

Statement usesGrouped y-fast trie

Used byKeys of the grouped y-fast trie built from a list · Stored keys are the keys of the groups · The empty grouped y-fast trie has no members · Correctness of the y-fast trie membership query · Membership in a trie built from a sorted list · The empty grouped y-fast trie has no successors · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key · Successor in the trie built from a sorted list

TheoremStored keys are the keys of the groups#✓fully proved

For every grouped y-fast trie \(t\) over \(w\)-bit keys and every key \(x\), \(x\) lies in the contents of \(t\) if and only if \(x\) belongs to some group of \(t\).

public theorem mem_contents_iff {w B : Nat} (t : GroupedYFastTrie w B)
    (x : Fin (2 ^ w)) : x ∈ t.contents ↔ ∃ g ∈ t.groups, x ∈ g

Uses 2 · Used by 3

Statement usesGrouped y-fast trie · Keys of a grouped y-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

DefinitionOrdered list of groups#✓fully proved

A list of groups, each a list of \(w\)-bit keys, is group ordered when every key of an earlier group is smaller than every key of a later group.

public def GroupOrdered {w : Nat} (gs : List (List (Fin (2 ^ w)))) : Prop :=
  gs.Pairwise (fun g₁ g₂ => ∀ a ∈ g₁, ∀ b ∈ g₂, a < b)

Used by 8

Used byChunks of a sorted list are ordered · 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 · Assembling a valid grouped y-fast trie from groups

DefinitionValidity of a grouped y-fast trie#✓fully proved

A grouped y-fast trie \(t\) over keys in \(\{0, \dots, 2^w - 1\}\) with group bound \(B\) is valid when its representative trie is a valid x-fast trie; a key \(r\) is stored in the representative trie exactly when \(r\) is the last element of some group of \(t\); every group of \(t\) is nonempty, has at most \(B\) keys, and is strictly increasing; and the groups of \(t\) are ordered, that is, every key of an earlier group is smaller than every key of a later group.

public def Valid {w B : Nat} (t : GroupedYFastTrie w B) : Prop :=
  t.reps.Valid ∧
    (∀ r, r ∈ t.reps.contents ↔ ∃ g ∈ t.groups, g.getLast? = some r) ∧
    (∀ g ∈ t.groups, g ≠ [] ∧ g.length ≤ B ∧ g.Pairwise (· < ·)) ∧
    GroupOrdered t.groups

Uses 4 · Used by 7

Statement usesGrouped y-fast trie · Ordered list of groups · x-fast trie · Valid x-fast trie

Used byCorrectness 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 · The empty grouped y-fast trie is valid · Assembling a valid grouped y-fast trie from groups · Building from a sorted list gives a valid grouped y-fast trie

DefinitionGroup of a representative#✓fully proved

For a grouped y-fast trie \(t\) and a key \(r\), the group of \(r\) is the first group of \(t\), in the order of the groups, whose last element is \(r\), or the empty list if no group of \(t\) ends with \(r\).

In a valid trie every group is strictly increasing, so its last element is its maximum.

public def findGroup {w B : Nat} (t : GroupedYFastTrie w B) (r : Fin (2 ^ w)) :
    List (Fin (2 ^ w)) :=
  (t.groups.find? (fun g => decide (g.getLast? = some r))).getD []

Uses 1 · Used by 5

Statement usesGrouped y-fast trie

Used byMembership query of a grouped y-fast trie · Correctness of the y-fast trie membership query · 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

DefinitionLeast representative at or above a key#✓fully proved

For a grouped y-fast trie \(t\) and a key \(x\), the result is \(x\) itself if the membership test of the representative x-fast trie of \(t\) (a single probe of its deepest level) reports \(x\) as present. Otherwise it is the successor of \(x\) in the representative x-fast trie, that is, the least representative greater than \(x\), or nothing if there is none.

When \(t\) is valid, the result is the least representative \(r\) with \(x \le r\), and nothing when there is no such representative.

public def repGe {w B : Nat} (t : GroupedYFastTrie w B) (x : Fin (2 ^ w)) :
    Option (Fin (2 ^ w)) :=
  if t.reps.member x = true then some x else t.reps.successor x

Uses 4 · Used by 2

Statement usesGrouped y-fast trie · x-fast trie · Membership query in an x-fast trie · Successor in an x-fast trie

Used byMembership query of a grouped y-fast trie · Correctness of the y-fast trie membership query

DefinitionMembership query of a grouped y-fast trie#✓fully proved

Given a grouped y-fast trie \(t\) over \(w\)-bit keys and a key \(x\), the query first finds a representative \(r\): \(r = x\) if the membership probe of the representative x-fast trie accepts \(x\), and otherwise \(r\) is the successor of \(x\) in the representative trie. If there is no such \(r\), the query returns false. Otherwise it returns whether \(x\) belongs to the group owned by \(r\), namely the first group of \(t\) whose last element is \(r\) (the empty list if there is none).

public def member {w B : Nat} (t : GroupedYFastTrie w B) (x : Fin (2 ^ w)) : Bool :=
  match t.repGe x with
  | none => false
  | some r => decide (x ∈ t.findGroup r)

Uses 3 · Used by 3

Statement usesGrouped y-fast trie · Group of a representative · Least representative at or above a key

Used byThe empty grouped y-fast trie has no members · Correctness of the y-fast trie membership query · Membership in a trie built from a sorted list

TheoremCorrectness of the y-fast trie membership query#✓fully proved

Let \(t\) be a valid grouped y-fast trie over \(w\)-bit keys. Then for every key \(x\), the membership query on \(t\) (locate the least representative at least \(x\), then scan its group) returns true at \(x\) if and only if \(x\) lies in the contents of \(t\).

public theorem member_iff {w B : Nat} {t : GroupedYFastTrie w B} (hv : t.Valid)
    (x : Fin (2 ^ w)) : t.member x = true ↔ x ∈ t.contents

Uses 15 · Used by 2

Statement usesGrouped y-fast trie · Validity of a grouped y-fast trie · Keys of a grouped y-fast trie · Membership query of a grouped y-fast trie

Proof usesOrdered list of groups · Group of a representative · Stored keys are the keys of the groups · Least representative at or above a key · x-fast trie · Valid x-fast trie · Membership query in an x-fast trie · The membership test of a valid x-fast trie is exact · Successor in an x-fast trie · When an x-fast trie has no successor · Characterization of the x-fast trie successor

Used byThe empty grouped y-fast trie has no members · Membership in a trie built from a sorted list

DefinitionSuccessor query in a grouped y-fast trie#✓fully proved

For a grouped y-fast trie \(t\) and a key \(x\), let \(r\) be the least key greater than \(x\) stored in the representative x-fast trie of \(t\); if there is none, the query returns nothing. Otherwise let \(g\) be the first group of \(t\) whose last element is \(r\), or the empty list if no group has last element \(r\). The query then returns the first key of \(g\) greater than \(x\), or nothing if \(g\) has no such key.

public def successor {w B : Nat} (t : GroupedYFastTrie w B) (x : Fin (2 ^ w)) :
    Option (Fin (2 ^ w)) :=
  match t.reps.successor x with
  | none => none
  | some r => (t.findGroup r).find? (fun z => decide (x < z))

Uses 4 · Used by 4

Statement usesGrouped y-fast trie · Group of a representative · x-fast trie · Successor in an x-fast trie

Used byThe empty grouped y-fast trie has no successors · Successor query fails exactly when no larger key is stored · Successor query returns the least larger stored key · Successor in the trie built from a sorted list

TheoremSuccessor query returns the least larger stored key#✓fully proved

Let \(t\) be a valid grouped y-fast trie and let \(x\), \(y\) be keys. The successor query for \(x\) in \(t\) returns \(y\) if and only if \(y\) is stored in \(t\), \(x < y\), and \(y \le z\) for every key \(z\) stored in \(t\) with \(x < z\).

public theorem successor_eq_some_iff {w B : Nat} {t : GroupedYFastTrie w B}
    (hv : t.Valid) (x y : Fin (2 ^ w)) :
    t.successor x = some y ↔
      y ∈ t.contents ∧ x < y ∧ ∀ z ∈ t.contents, x < z → y ≤ z

Uses 12 · Used by 1

Statement usesGrouped y-fast trie · Validity of a grouped y-fast trie · Keys of a grouped y-fast trie · Successor query in a grouped y-fast trie

Proof usesOrdered list of groups · Group of a representative · Stored keys are the keys of the groups · x-fast trie · Valid x-fast trie · Successor in an x-fast trie · When an x-fast trie has no successor · Characterization of the x-fast trie successor

Used bySuccessor in the trie built from a sorted list

TheoremSuccessor query fails exactly when no larger key is stored#✓fully proved

Let \(t\) be a valid grouped y-fast trie and \(x\) a key. The successor query for \(x\) in \(t\) returns nothing if and only if no key stored in \(t\) is greater than \(x\).

public theorem successor_eq_none_iff {w B : Nat} {t : GroupedYFastTrie w B}
    (hv : t.Valid) (x : Fin (2 ^ w)) :
    t.successor x = none ↔ ∀ z ∈ t.contents, ¬ x < z

Uses 12 · Used by 1

Statement usesGrouped y-fast trie · Validity of a grouped y-fast trie · Keys of a grouped y-fast trie · Successor query in a grouped y-fast trie

Proof usesOrdered list of groups · Group of a representative · Stored keys are the keys of the groups · x-fast trie · Valid x-fast trie · Successor in an x-fast trie · When an x-fast trie has no successor · Characterization of the x-fast trie successor

Used byThe empty grouped y-fast trie has no successors

DefinitionThe empty grouped y-fast trie#✓fully proved

For every key length \(w\) and group bound \(B\), the empty grouped y-fast trie has the empty x-fast trie as its trie of representatives and has no groups.

public def empty {w B : Nat} : GroupedYFastTrie w B :=
  ⟨XFastTrie.empty, []⟩

Uses 3 · Used by 3

Statement usesGrouped y-fast trie · x-fast trie · The empty x-fast trie

Used byThe empty grouped y-fast trie has no members · The empty grouped y-fast trie has no successors · The empty grouped y-fast trie is valid

TheoremThe empty grouped y-fast trie is valid#✓fully proved

For every key width \(w\) and group bound \(B\), the empty grouped y-fast trie satisfies the grouped y-fast trie invariant.

public theorem valid_empty {w B : Nat} : (empty : GroupedYFastTrie w B).Valid

Uses 7 · Used by 2

Statement usesValidity of a grouped y-fast trie · The empty grouped y-fast trie

Proof usesGrouped y-fast trie · Ordered list of groups · x-fast trie · Valid x-fast trie · The empty x-fast trie is valid

Used byThe empty grouped y-fast trie has no members · The empty grouped y-fast trie has no successors

TheoremThe empty grouped y-fast trie has no members#✓fully proved

For all natural numbers \(w\) and \(B\) and every \(w\)-bit key \(x\), the membership query on the empty grouped y-fast trie over \(w\)-bit keys with group bound \(B\) returns false at \(x\).

public theorem member_empty {w B : Nat} (x : Fin (2 ^ w)) :
    (empty : GroupedYFastTrie w B).member x = false

Uses 5

Statement usesThe empty grouped y-fast trie · Membership query of a grouped y-fast trie

Proof usesKeys of a grouped y-fast trie · Correctness of the y-fast trie membership query · The empty grouped y-fast trie is valid

TheoremThe empty grouped y-fast trie has no successors#✓fully proved

For every key \(x\), the successor query for \(x\) in the empty grouped y-fast trie returns nothing.

public theorem successor_empty {w B : Nat} (x : Fin (2 ^ w)) :
    (empty : GroupedYFastTrie w B).successor x = none

Uses 5

Statement usesThe empty grouped y-fast trie · Successor query in a grouped y-fast trie

Proof usesKeys of a grouped y-fast trie · Successor query fails exactly when no larger key is stored · The empty grouped y-fast trie is valid

DefinitionRepresentative trie of a list#✓fully proved

For a list \(rs\) of \(w\)-bit keys, the representative x-fast trie of \(rs\) is obtained from the empty x-fast trie over \(w\)-bit keys by inserting the elements of \(rs\) one at a time, from first to last.

public def mkReps {w : Nat} (rs : List (Fin (2 ^ w))) : XFastTrie w :=
  rs.foldl (fun t r => t.insert r) XFastTrie.empty

Uses 3 · Used by 4

Statement usesx-fast trie · The empty x-fast trie · Insertion into an x-fast trie

Used byKeys of the trie of representatives · Grouped y-fast trie from a list of groups · Inserting a list of keys into the empty x-fast trie gives a valid trie · Assembling a valid grouped y-fast trie from groups

TheoremInserting a list of keys into the empty x-fast trie gives a valid trie#✓fully proved

For every list of \(w\)-bit keys, the x-fast trie obtained from the empty x-fast trie by inserting the keys of the list one at a time satisfies the x-fast trie invariant: each level holds exactly the prefixes of that length of the stored keys.

public theorem valid_mkReps {w : Nat} (rs : List (Fin (2 ^ w))) : (mkReps rs).Valid

Uses 7 · Used by 1

Statement usesRepresentative trie of a list · Valid x-fast trie

Proof usesx-fast trie · The empty x-fast trie · Insertion into an x-fast trie · The empty x-fast trie is valid · Insertion preserves validity of an x-fast trie

Used byAssembling a valid grouped y-fast trie from groups

TheoremKeys of the trie of representatives#✓fully proved

For every list \(L\) of \(w\)-bit keys, the x-fast trie obtained by inserting the elements of \(L\) one by one into the empty x-fast trie stores exactly the elements of \(L\): its key set is the set of elements of \(L\).

public theorem contents_mkReps {w : Nat} (rs : List (Fin (2 ^ w))) :
    (mkReps rs).contents = rs.toFinset

Uses 4 · Used by 1

Statement usesRepresentative trie of a list · x-fast trie

Proof usesThe empty x-fast trie · Insertion into an x-fast trie

Used byAssembling a valid grouped y-fast trie from groups

DefinitionGrouped y-fast trie from a list of groups#✓fully proved

For a list of groups \(g_1, \dots, g_k\), each a list of \(w\)-bit keys, and any group-size bound \(B\), this is the grouped y-fast trie whose groups are \(g_1, \dots, g_k\) in this order and whose representative x-fast trie is obtained from the empty x-fast trie by inserting the last element of each nonempty group, in order. No condition on the groups is checked here; when a group is sorted, its last element is its maximum.

public def ofGroups {w B : Nat} (gs : List (List (Fin (2 ^ w)))) :
    GroupedYFastTrie w B :=
  ⟨mkReps (gs.filterMap List.getLast?), gs⟩

Uses 3 · Used by 3

Statement usesGrouped y-fast trie · Representative trie of a list · x-fast trie

Used byKeys of the grouped y-fast trie built from a list · Grouped y-fast trie from a sorted list · Assembling a valid grouped y-fast trie from groups

TheoremAssembling a valid grouped y-fast trie from groups#✓fully proved

Let \(w\) and \(B\) be natural numbers and let \(g_1, \dots, g_k\) be a list of groups, each a list of keys in \(\{0, \dots, 2^w - 1\}\). Suppose every group is nonempty, has at most \(B\) keys, and is strictly increasing, and the groups are ordered: every key of an earlier group is smaller than every key of a later group. Then the grouped y-fast trie with group bound \(B\) assembled from these groups, whose representatives are the last elements of the groups, is valid.

public theorem valid_ofGroups {w B : Nat} {gs : List (List (Fin (2 ^ w)))}
    (hgroups : ∀ g ∈ gs, g ≠ [] ∧ g.length ≤ B ∧ g.Pairwise (· < ·))
    (hord : GroupOrdered gs) : (ofGroups gs : GroupedYFastTrie w B).Valid

Uses 9 · Used by 1

Statement usesOrdered list of groups · Validity of a grouped y-fast trie · Grouped y-fast trie from a list of groups

Proof usesGrouped y-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 · x-fast trie · Valid x-fast trie

Used byBuilding from a sorted list gives a valid grouped y-fast trie

DefinitionFuel-bounded chunking#✓fully proved

Given a bound \(B\), a fuel \(n\) and a list \(l\) of \(w\)-bit keys, the fuel-bounded chunking is the empty list of chunks when \(n = 0\) or \(l\) is empty; otherwise it is the chunk formed by the first \(\min(B, |l|)\) elements of \(l\), followed by the fuel-bounded chunking with bound \(B\) and fuel \(n - 1\) of the remaining elements of \(l\).

def chunkGroupsAux {w : Nat} (B : Nat) :
    Nat → List (Fin (2 ^ w)) → List (List (Fin (2 ^ w)))
  | 0, _ => []
  | _, [] => []
  | fuel + 1, l => l.take B :: chunkGroupsAux B fuel (l.drop B)

Used by 4

Used byChunking a list into groups · Chunks of a sorted list · Chunking with bound zero · Chunking preserves the list

DefinitionChunking a list into groups#✓fully proved

Given a bound \(B\) and a list \(l\) of \(w\)-bit keys, when \(B > 0\) the chunking of \(l\) cuts \(l\) from the left into consecutive chunks of exactly \(B\) elements each, except that the last chunk holds the remaining one to \(B\) elements; there are no chunks when \(l\) is empty. When \(B = 0\), the chunking has no chunks if \(l\) is empty and is the single chunk \(l\) otherwise.

So every chunk has at most \(B\) elements when \(B > 0\), but not when \(B = 0\) and \(l\) is nonempty.

public def chunkGroups {w : Nat} (B : Nat) (l : List (Fin (2 ^ w))) :
    List (List (Fin (2 ^ w))) :=
  if B = 0 then (if l = [] then [] else [l]) else chunkGroupsAux B l.length l

Uses 1 · Used by 7

Statement usesFuel-bounded chunking

Used byChunks of a sorted list · Chunking with bound zero · Keys of the grouped y-fast trie built from a list · Chunking preserves the list · Chunks of a sorted list are ordered · Grouped y-fast trie from a sorted list · Building from a sorted list gives a valid grouped y-fast trie

TheoremChunking with bound zero#✓fully proved

For every nonempty list \(l\) of \(w\)-bit keys, the chunking of \(l\) with bound \(B = 0\) consists of the single chunk \(l\).

public theorem chunkGroups_zero_of_ne {w : Nat} {l : List (Fin (2 ^ w))}
    (hl : l ≠ []) : chunkGroups 0 l = [l]

Uses 2 · Used by 1

Statement usesChunking a list into groups

Proof usesFuel-bounded chunking

Used byBuilding from a nonempty list with group bound zero gives an invalid trie

TheoremChunking preserves the list#✓fully proved

For every bound \(B\) (including \(B = 0\)) and every list \(l\) of \(w\)-bit keys, concatenating the chunks of the chunking of \(l\) with bound \(B\), in order, gives back \(l\).

public theorem flatten_chunkGroups {w : Nat} (B : Nat) (l : List (Fin (2 ^ w))) :
    (chunkGroups B l).flatten = l

Uses 2 · Used by 2

Statement usesChunking a list into groups

Proof usesFuel-bounded chunking

Used byKeys of the grouped y-fast trie built from a list · Chunks of a sorted list are ordered

TheoremChunks of a sorted list#✓fully proved

Let \(B > 0\) and let \(l\) be a strictly increasing list of \(w\)-bit keys. Then every chunk of the chunking of \(l\) into groups of at most \(B\) keys is nonempty, has at most \(B\) elements, and is strictly increasing.

public theorem chunkGroups_spec {w : Nat} {B : Nat} (hB : 0 < B)
    (l : List (Fin (2 ^ w))) (hsorted : l.Pairwise (· < ·)) :
    ∀ g ∈ chunkGroups B l, g ≠ [] ∧ g.length ≤ B ∧ g.Pairwise (· < ·)

Uses 2 · Used by 1

Statement usesChunking a list into groups

Proof usesFuel-bounded chunking

Used byBuilding from a sorted list gives a valid grouped y-fast trie

TheoremChunks of a sorted list are ordered#✓fully proved

Let \(B\) be a natural number and let \(l\) be a strictly increasing list of \(w\)-bit keys. Then the chunk groups of \(l\) with bound \(B\) are group ordered: every key of an earlier chunk is smaller than every key of a later chunk.

public theorem groupOrdered_chunkGroups {w : Nat} (B : Nat) (l : List (Fin (2 ^ w)))
    (hsorted : l.Pairwise (· < ·)) : GroupOrdered (chunkGroups B l)

Uses 3 · Used by 1

Statement usesOrdered list of groups · Chunking a list into groups

Proof usesChunking preserves the list

Used byBuilding from a sorted list gives a valid grouped y-fast trie

DefinitionGrouped y-fast trie from a sorted list#✓fully proved

For a group bound \(B\) and a list \(l\) of \(w\)-bit keys, this is the grouped y-fast trie whose groups, in order, are consecutive pieces of \(l\) that together make up \(l\), and whose representative x-fast trie is obtained from the empty x-fast trie by inserting the last element of each group, in order. If \(B > 0\), the groups are obtained by repeatedly cutting off the first \(B\) keys, so every group has exactly \(B\) keys except possibly the last, which has between one and \(B\) keys. If \(B = 0\), the only group is \(l\) itself. In both cases there are no groups when \(l\) is empty.

The construction is intended for strictly increasing \(l\). It yields a valid trie when \(B > 0\) and \(l\) is strictly increasing, and an invalid one when \(B = 0\) and \(l\) is nonempty.

public def ofSortedList {w : Nat} (B : Nat) (l : List (Fin (2 ^ w))) :
    GroupedYFastTrie w B :=
  ofGroups (chunkGroups B l)

Uses 3 · Used by 5

Statement usesGrouped y-fast trie · Chunking a list into groups · Grouped y-fast trie from a list of groups

Used byKeys of the grouped y-fast trie built from a list · Membership in a trie built from a sorted list · Building from a nonempty list with group bound zero gives an invalid trie · Successor in the trie built from a sorted list · Building from a sorted list gives a valid grouped y-fast trie

TheoremBuilding from a sorted list gives a valid grouped y-fast trie#✓fully proved

Let \(w\) and \(B\) be natural numbers with \(0 < B\), and let \(l\) be a strictly increasing list of keys in \(\{0, \dots, 2^w - 1\}\). Then the grouped y-fast trie with group bound \(B\) built from \(l\) by cutting it into consecutive groups of at most \(B\) keys is valid.

public theorem valid_ofSortedList {w B : Nat} (hB : 0 < B) {l : List (Fin (2 ^ w))}
    (hsorted : l.Pairwise (· < ·)) : (ofSortedList B l).Valid

Uses 6 · Used by 2

Statement usesValidity of a grouped y-fast trie · Grouped y-fast trie from a sorted list

Proof usesChunking a list into groups · Chunks of a sorted list · Chunks of a sorted list are ordered · Assembling a valid grouped y-fast trie from groups

Used byMembership in a trie built from a sorted list · Successor in the trie built from a sorted list

TheoremBuilding from a nonempty list with group bound zero gives an invalid trie#✓fully proved

For every natural number \(w\) and every nonempty list \(l\) of \(w\)-bit keys, the grouped y-fast trie with group bound \(B = 0\) built from \(l\) is not valid.

With \(B = 0\) the only group is \(l\) itself, which has more than \(0\) keys. For \(B > 0\) and strictly increasing \(l\), the grouped y-fast trie built from \(l\) is valid.

public theorem not_valid_ofSortedList_zero {w : Nat} {l : List (Fin (2 ^ w))}
    (hl : l ≠ []) : ¬ (ofSortedList 0 l).Valid

Uses 7

Statement usesValidity of a grouped y-fast trie · Grouped y-fast trie from a sorted list

Proof usesGrouped y-fast trie · Ordered list of groups · Chunking with bound zero · x-fast trie · Valid x-fast trie

TheoremKeys of the grouped y-fast trie built from a list#✓fully proved

For every group bound \(B\) (including \(B = 0\)) and every list \(l\) of \(w\)-bit keys, sorted or not, the key set of the grouped y-fast trie built from \(l\) with group bound \(B\) is exactly the set of elements of \(l\).

public theorem contents_ofSortedList {w B : Nat} (l : List (Fin (2 ^ w))) :
    (ofSortedList B l).contents = l.toFinset

Uses 6 · Used by 2

Statement usesKeys of a grouped y-fast trie · Grouped y-fast trie from a sorted list

Proof usesGrouped y-fast trie · Chunking a list into groups · Chunking preserves the list · Grouped y-fast trie from a list of groups

Used byMembership in a trie built from a sorted list · Successor in the trie built from a sorted list

TheoremMembership in a trie built from a sorted list#✓fully proved

Let \(B > 0\) and let \(l\) be a strictly increasing list of \(w\)-bit keys. Then for every key \(x\), the membership query on the grouped y-fast trie built from \(l\) with group bound \(B\) returns true at \(x\) if and only if \(x\) belongs to \(l\).

public theorem member_ofSortedList_iff {w B : Nat} (hB : 0 < B)
    {l : List (Fin (2 ^ w))} (hsorted : l.Pairwise (· < ·)) (x : Fin (2 ^ w)) :
    (ofSortedList B l).member x = true ↔ x ∈ l

Uses 6

Statement usesMembership query of a grouped y-fast trie · Grouped y-fast trie from a sorted list

Proof usesKeys of a grouped y-fast trie · Keys of the grouped y-fast trie built from a list · Correctness of the y-fast trie membership query · Building from a sorted list gives a valid grouped y-fast trie

TheoremSuccessor in the trie built from a sorted list#✓fully proved

Let \(B > 0\), let \(l\) be a strictly increasing list of \(w\)-bit keys, and let \(x\), \(y\) be keys. The successor query for \(x\) in the grouped y-fast trie built from \(l\) with group bound \(B\) returns \(y\) if and only if \(y\) belongs to \(l\), \(x < y\), and \(y \le z\) for every \(z\) in \(l\) with \(x < z\).

public theorem successor_ofSortedList_eq_some_iff {w B : Nat} (hB : 0 < B)
    {l : List (Fin (2 ^ w))} (hsorted : l.Pairwise (· < ·)) (x y : Fin (2 ^ w)) :
    (ofSortedList B l).successor x = some y ↔
      y ∈ l ∧ x < y ∧ ∀ z ∈ l, x < z → y ≤ z

Uses 6

Statement usesGrouped y-fast trie from a sorted list · Successor query in a grouped y-fast trie

Proof usesKeys of a grouped y-fast trie · Keys of the grouped y-fast trie built from a list · Successor query returns the least larger stored key · Building from a sorted list gives a valid grouped y-fast trie

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.