Fractional cascading

DefinitionAlternating selection with a flag#✓fully proved

For a flag \(b\) (true or false) and a list \(\ell\), the alternating selection of \(\ell\) with initial flag \(b\) is defined by recursion on \(\ell\): the empty list gives the empty list; for a list with head \(a\) and tail \(\ell'\), if \(b\) is true it keeps \(a\) and continues on \(\ell'\) with flag false, and if \(b\) is false it drops \(a\) and continues on \(\ell'\) with flag true.

def sampleAux : Bool → List α → List α
  | _, [] => []
  | true, a :: xs => a :: sampleAux false xs
  | false, _ :: xs => sampleAux true xs

Used by 3

Used bySample of a catalog · Alternating selection gives a sublist · Doubled sample length bound

DefinitionSample of a catalog#✓fully proved

The sample of a list \([x_0, x_1, x_2, \dots]\) is the list \([x_0, x_2, x_4, \dots]\) of every other element, starting with the first, in their original order.

def sample (xs : List α) : List α :=
  sampleAux true xs

Uses 1 · Used by 16

Statement usesAlternating selection with a flag

Used byAugmenting a catalog by the next one · Length of one augmented catalog · Length bound for one augmented catalog · Augmented catalogs are bounded by the total input size · The sample has at most half the length, rounded up · The sample is no longer than the list · Lower bound in an augmented catalog splits · Lower bound in an augmented catalog is at most the sum · Lower bound in a sample is at most the lower bound in the catalog · Membership in an augmented catalog · Entries of an augmented catalog come from the two catalogs · Entries of a sample are entries of the catalog · One augmentation step yields a sorted list · The sample of a sorted list is sorted · The sample is a sublist · Doubled sample length bound

TheoremAlternating selection gives a sublist#✓fully proved

For every flag \(b\) (true or false) and every list \(\ell\), the alternating selection of \(\ell\) with initial flag \(b\) is a sublist of \(\ell\): it is obtained from \(\ell\) by deleting some elements and keeping the rest in order.

theorem sampleAux_sublist :
    ∀ (b : Bool) (xs : List α), (sampleAux b xs).Sublist xs

Uses 1 · Used by 1

Statement usesAlternating selection with a flag

Used byThe sample is a sublist

TheoremThe sample is a sublist#✓fully proved

For every list \(\ell\), the sample of \(\ell\) is a sublist of \(\ell\): it is obtained from \(\ell\) by deleting some elements and keeping the rest in order.

theorem sample_sublist (xs : List α) : (sample xs).Sublist xs

Uses 2 · Used by 4

Statement usesSample of a catalog

Proof usesAlternating selection gives a sublist

Used byThe sample is no longer than the list · Lower bound in a sample is at most the lower bound in the catalog · Entries of a sample are entries of the catalog · The sample of a sorted list is sorted

TheoremEntries of a sample are entries of the catalog#✓fully proved

For a catalog (finite list) \(L\), every entry of the sample of \(L\) (every other entry of \(L\), starting with the first) is an entry of \(L\).

theorem mem_of_mem_sample {v : α} {xs : List α} (hv : v ∈ sample xs) :
    v ∈ xs

Uses 2 · Used by 1

Statement usesSample of a catalog

Proof usesThe sample is a sublist

Used byEntries of an augmented catalog come from the two catalogs

TheoremDoubled sample length bound#✓fully proved

For every catalog \(L\), twice the length of the sample of \(L\) is at most the length of \(L\) plus one.

theorem two_mul_length_sample_le (xs : List α) :
    2 * (sample xs).length ≤ xs.length + 1

Uses 2 · Used by 1

Statement usesSample of a catalog

Proof usesAlternating selection with a flag

Used byThe sample has at most half the length, rounded up

TheoremThe sample has at most half the length, rounded up#✓fully proved

For every list \(xs\) (over any type), the sample of \(xs\) has length at most \(\lfloor (|xs| + 1)/2 \rfloor\), half the length of \(xs\) rounded up: for an even length \(2m\) the bound is \(m\), and for an odd length \(2m + 1\) it is \(m + 1\).

theorem length_sample_le (xs : List α) :
    (sample xs).length ≤ (xs.length + 1) / 2

Uses 2 · Used by 1

Statement usesSample of a catalog

Proof usesDoubled sample length bound

Used byLength bound for one augmented catalog

TheoremThe sample is no longer than the list#✓fully proved

For every list \(xs\) (over any type), the sample of \(xs\), every other element starting with the first, has length at most the length of \(xs\).

theorem length_sample_le_length (xs : List α) :
    (sample xs).length ≤ xs.length

Uses 2 · Used by 1

Statement usesSample of a catalog

Proof usesThe sample is a sublist

Used byAugmented catalogs are bounded by the total input size

TheoremThe sample of a sorted list is sorted#✓fully proved

If a list over a linear order is sorted in nondecreasing order, then so is its sample.

theorem pairwise_sample {xs : List α} (hxs : xs.Pairwise (· ≤ ·)) :
    (sample xs).Pairwise (· ≤ ·)

Uses 2

Statement usesSample of a catalog

Proof usesThe sample is a sublist

DefinitionSorted merge of two catalogs#✓fully proved

For lists \(\ell_1\) and \(\ell_2\) over a linearly ordered type, their sorted merge is the result of merge sort, with respect to \(\le\), applied to the concatenation of \(\ell_1\) followed by \(\ell_2\).

This models the merge of two sorted catalogs; the linear-time merge itself is not part of this statement.

def sortedMerge (xs ys : List α) : List α :=
  (xs ++ ys).mergeSort (· ≤ ·)

Used by 6

Used byAugmenting a catalog by the next one · Length of a sorted merge · Lower bound in a sorted merge splits · Elements of a sorted merge · A sorted merge is sorted · A sorted merge rearranges the concatenation

TheoremA sorted merge rearranges the concatenation#✓fully proved

For any lists \(\ell_1\) and \(\ell_2\) over a linear order, the sorted merge of \(\ell_1\) and \(\ell_2\) is a permutation of the concatenation of \(\ell_1\) followed by \(\ell_2\).

theorem perm_sortedMerge (xs ys : List α) :
    (sortedMerge xs ys).Perm (xs ++ ys)

Uses 1 · Used by 2

Statement usesSorted merge of two catalogs

Used byLower bound in a sorted merge splits · Elements of a sorted merge

TheoremLength of a sorted merge#✓fully proved

For catalogs (finite lists) \(L\) and \(M\) over a linearly ordered type, the sorted merge of \(L\) and \(M\) has length equal to the length of \(L\) plus the length of \(M\).

theorem length_sortedMerge (xs ys : List α) :
    (sortedMerge xs ys).length = xs.length + ys.length

Uses 1 · Used by 1

Statement usesSorted merge of two catalogs

Used byLength of one augmented catalog

TheoremA sorted merge is sorted#✓fully proved

For any lists \(\ell_1\) and \(\ell_2\) over a linear order, sorted or not, their sorted merge is sorted in nondecreasing order.

theorem pairwise_sortedMerge (xs ys : List α) :
    (sortedMerge xs ys).Pairwise (· ≤ ·)

Uses 1 · Used by 1

Statement usesSorted merge of two catalogs

Used byOne augmentation step yields a sorted list

TheoremElements of a sorted merge#✓fully proved

For lists \(\ell_1\) and \(\ell_2\) over a linear order and any element \(v\), \(v\) belongs to the sorted merge of \(\ell_1\) and \(\ell_2\) if and only if \(v\) belongs to \(\ell_1\) or to \(\ell_2\).

theorem mem_sortedMerge_iff {v : α} {xs ys : List α} :
    v ∈ sortedMerge xs ys ↔ v ∈ xs ∨ v ∈ ys

Uses 2 · Used by 1

Statement usesSorted merge of two catalogs

Proof usesA sorted merge rearranges the concatenation

Used byMembership in an augmented catalog

DefinitionLower bound of a value in a catalog#✓fully proved

For a value \(x\) of a linearly ordered type and a catalog (finite list) \(L\), the lower bound of \(x\) in \(L\) is the number of entries of \(L\) that are less than \(x\), counted with multiplicity. For a sorted catalog this is the first index whose entry is not less than \(x\), or the length of \(L\) if there is none.

def lowerBound (x : α) (xs : List α) : Nat :=
  (xs.filter (· < x)).length

Used by 10

Used byThe scan count equals the lower bound · Search positions are lower bounds, index by index · Lower bound in an augmented catalog splits · Lower bound in an augmented catalog is at most the sum · Lower bound is at most the catalog length · Lower bound in a sample is at most the lower bound in the catalog · Lower bound in a sorted merge splits · Correctness of searching every catalog · Search positions are boundary indices · Correctness of augmented search

TheoremLower bound is at most the catalog length#✓fully proved

For a value \(x\) and a catalog \(L\) over a linearly ordered type, the lower bound of \(x\) in \(L\) (the number of entries of \(L\) less than \(x\)) is at most the length of \(L\).

theorem lowerBound_le_length (x : α) (xs : List α) :
    lowerBound x xs ≤ xs.length

Uses 1 · Used by 1

Statement usesLower bound of a value in a catalog

Used bySearch positions are boundary indices

TheoremLower bound in a sorted merge splits#✓fully proved

For a value \(x\) and catalogs \(L\) and \(M\) over a linearly ordered type, the lower bound of \(x\) in the sorted merge of \(L\) and \(M\) equals the lower bound of \(x\) in \(L\) plus the lower bound of \(x\) in \(M\), where the lower bound of \(x\) in a catalog is the number of its entries less than \(x\).

theorem lowerBound_sortedMerge (x : α) (xs ys : List α) :
    lowerBound x (sortedMerge xs ys) = lowerBound x xs + lowerBound x ys

Uses 3 · Used by 1

Statement usesLower bound of a value in a catalog · Sorted merge of two catalogs

Proof usesA sorted merge rearranges the concatenation

Used byLower bound in an augmented catalog splits

TheoremLower bound in a sample is at most the lower bound in the catalog#✓fully proved

For a value \(x\) and a catalog \(L\) over a linearly ordered type, the number of entries less than \(x\) in the sample of \(L\) (every other entry of \(L\), starting with the first) is at most the number of entries of \(L\) less than \(x\).

theorem lowerBound_sample_le (x : α) (xs : List α) :
    lowerBound x (sample xs) ≤ lowerBound x xs

Uses 3 · Used by 1

Statement usesLower bound of a value in a catalog · Sample of a catalog

Proof usesThe sample is a sublist

Used byLower bound in an augmented catalog is at most the sum

DefinitionScan count of smaller elements#✓fully proved

For a value \(x\) and a catalog \(L\), the scan count of \(x\) in \(L\) is the number of elements of \(L\) that are \(< x\), computed by a direct scan: it is \(0\) for the empty catalog, and for a catalog with head \(a\) and tail \(L'\) it is the scan count of \(x\) in \(L'\), plus \(1\) if \(a < x\).

def countLT (x : α) : List α → Nat
  | [] => 0
  | a :: xs => countLT x xs + (if a < x then 1 else 0)

Used by 8

Used byThe scan count equals the lower bound · One search position per catalog · One augmented search position per catalog · Searching every catalog · Searching a nonempty list of catalogs · Correctness of searching every catalog · Searching every augmented catalog · Correctness of augmented search

TheoremThe scan count equals the lower bound#✓fully proved

For every value \(x\) and every catalog \(L\), the scan count of elements of \(L\) that are \(< x\) equals the lower bound of \(x\) in \(L\).

theorem countLT_eq_lowerBound (x : α) (xs : List α) :
    countLT x xs = lowerBound x xs

Uses 2 · Used by 2

Statement usesScan count of smaller elements · Lower bound of a value in a catalog

Used byCorrectness of searching every catalog · Correctness of augmented search

DefinitionAugmenting a catalog by the next one#✓fully proved

For catalogs \(c\) and \(a\), the augmentation of \(c\) by \(a\) is the sorted merge of \(c\) with the sample of \(a\) (every other element of \(a\), starting with the first). In fractional cascading, \(a\) is the next augmented catalog.

def augmentOne (c a : List α) : List α :=
  sortedMerge c (sample a)

Uses 2 · Used by 10

Statement usesSample of a catalog · Sorted merge of two catalogs

Used byAugmenting a catalog by the head of a list · Length of one augmented catalog · Length bound for one augmented catalog · Augmented catalogs are bounded by the total input size · Lower bound in an augmented catalog splits · Lower bound in an augmented catalog is at most the sum · Membership in an augmented catalog · Entries of an augmented catalog come from the two catalogs · One augmentation step yields a sorted list · The augmented catalogs of sorted catalogs are sorted

TheoremOne augmentation step yields a sorted list#✓fully proved

For any lists \(c\) and \(a\) over a linear order, sorted or not, the augmented catalog obtained by merging \(c\) with the sample of \(a\) is sorted in nondecreasing order.

theorem pairwise_augmentOne (c a : List α) :
    (augmentOne c a).Pairwise (· ≤ ·)

Uses 3 · Used by 1

Statement usesAugmenting a catalog by the next one

Proof usesA sorted merge is sorted · Sample of a catalog

Used byThe augmented catalogs of sorted catalogs are sorted

TheoremLength of one augmented catalog#✓fully proved

For lists \(c\) and \(a\) over a linearly ordered type, the augmented catalog obtained by merging \(c\) with the sample \(s(a)\) of \(a\) has length \(|c| + |s(a)|\).

theorem length_augmentOne (c a : List α) :
    (augmentOne c a).length = c.length + (sample a).length

Uses 3 · Used by 2

Statement usesAugmenting a catalog by the next one · Sample of a catalog

Proof usesLength of a sorted merge

Used byLength bound for one augmented catalog · Augmented catalogs are bounded by the total input size

TheoremLength bound for one augmented catalog#✓fully proved

For lists \(c\) and \(a\) over a linearly ordered type, the augmented catalog obtained by merging \(c\) with the sample of \(a\) has length at most \(|c| + \lfloor (|a| + 1)/2 \rfloor\), the length of \(c\) plus half the length of \(a\) rounded up.

theorem length_augmentOne_le (c a : List α) :
    (augmentOne c a).length ≤ c.length + (a.length + 1) / 2

Uses 4

Statement usesAugmenting a catalog by the next one

Proof usesLength of one augmented catalog · The sample has at most half the length, rounded up · Sample of a catalog

TheoremMembership in an augmented catalog#✓fully proved

For catalogs \(c\) and \(a\) over a linearly ordered type, a value \(v\) is an entry of the augmented catalog of \(c\) with \(a\) (the sorted merge of \(c\) with the sample of \(a\)) if and only if \(v\) is an entry of \(c\) or an entry of the sample of \(a\).

theorem mem_augmentOne_iff {v : α} {c a : List α} :
    v ∈ augmentOne c a ↔ v ∈ c ∨ v ∈ sample a

Uses 3 · Used by 1

Statement usesAugmenting a catalog by the next one · Sample of a catalog

Proof usesElements of a sorted merge

Used byEntries of an augmented catalog come from the two catalogs

TheoremEntries of an augmented catalog come from the two catalogs#✓fully proved

For catalogs \(c\) and \(a\) over a linearly ordered type, every entry \(v\) of the augmented catalog of \(c\) with \(a\) (the sorted merge of \(c\) with the sample of \(a\)) is an entry of \(c\) or an entry of \(a\).

theorem mem_augmentOne_imp {v : α} {c a : List α}
    (hv : v ∈ augmentOne c a) : v ∈ c ∨ v ∈ a

Uses 4

Statement usesAugmenting a catalog by the next one

Proof usesMembership in an augmented catalog · Entries of a sample are entries of the catalog · Sample of a catalog

TheoremLower bound in an augmented catalog splits#✓fully proved

For a value \(x\) and catalogs \(c\) and \(a\) over a linearly ordered type, the lower bound of \(x\) in the augmented catalog of \(c\) with \(a\) (the sorted merge of \(c\) with the sample of \(a\)) equals the lower bound of \(x\) in \(c\) plus the lower bound of \(x\) in the sample of \(a\), where the lower bound of \(x\) in a catalog is the number of its entries less than \(x\).

theorem lowerBound_augmentOne (x : α) (c a : List α) :
    lowerBound x (augmentOne c a) =
      lowerBound x c + lowerBound x (sample a)

Uses 4 · Used by 1

Statement usesAugmenting a catalog by the next one · Lower bound of a value in a catalog · Sample of a catalog

Proof usesLower bound in a sorted merge splits

Used byLower bound in an augmented catalog is at most the sum

TheoremLower bound in an augmented catalog is at most the sum#✓fully proved

For a value \(x\) and catalogs \(c\) and \(a\) over a linearly ordered type, the lower bound of \(x\) in the augmented catalog of \(c\) with \(a\) (the sorted merge of \(c\) with the sample of \(a\)) is at most the lower bound of \(x\) in \(c\) plus the lower bound of \(x\) in \(a\), where the lower bound of \(x\) in a catalog is the number of its entries less than \(x\).

theorem lowerBound_augmentOne_le (x : α) (c a : List α) :
    lowerBound x (augmentOne c a) ≤ lowerBound x c + lowerBound x a

Uses 5

Statement usesAugmenting a catalog by the next one · Lower bound of a value in a catalog

Proof usesLower bound in an augmented catalog splits · Lower bound in a sample is at most the lower bound in the catalog · Sample of a catalog

DefinitionAugmenting a catalog by the head of a list#✓fully proved

Given a catalog \(c\) and a list \(L\) of catalogs, the result is \(c\) itself if \(L\) is empty, and otherwise the sorted merge of \(c\) with the sample (every other element, starting with the first) of the first catalog of \(L\).

def augmentHead (c : List α) : List (List α) → List α
  | [] => c
  | a :: _ => augmentOne c a

Uses 1 · Used by 3

Statement usesAugmenting a catalog by the next one

Used byAugmented catalogs · Augmented catalogs are bounded by the total input size · The augmented catalogs of sorted catalogs are sorted

DefinitionAugmented catalogs#✓fully proved

For a list of catalogs \(c_1, \dots, c_k\), the augmented catalogs \(A_1, \dots, A_k\) are built from the last one backwards: \(A_k = c_k\), and for \(i < k\), \(A_i\) is the sorted merge of \(c_i\) with the sample (every other element, starting with the first) of \(A_{i+1}\). The empty list of catalogs has no augmented catalogs.

def augmented : List (List α) → List (List α)
  | [] => []
  | c :: cs =>
      let rest := augmented cs
      augmentHead c rest :: rest

Uses 1 · Used by 7

Statement usesAugmenting a catalog by the head of a list

Used byAugmenting a single catalog · Number of augmented catalogs · Augmented catalogs are bounded by the total input size · One augmented search position per catalog · The augmented catalogs of sorted catalogs are sorted · Searching every augmented catalog · Correctness of augmented search

TheoremNumber of augmented catalogs#✓fully proved

For every list \(cs\) of catalogs over a linearly ordered type, the list of augmented catalogs built from \(cs\) has the same length as \(cs\): there is one augmented catalog per catalog.

@[simp]
theorem length_augmented (cs : List (List α)) :
    (augmented cs).length = cs.length

Uses 1 · Used by 1

Statement usesAugmented catalogs

Used byOne augmented search position per catalog

TheoremAugmenting a single catalog#✓fully proved

For every catalog \(c\), the list of augmented catalogs of the one-element list \([c]\) is \([c]\): the only augmented catalog is \(c\) itself.

theorem augmented_singleton (c : List α) : augmented [c] = [c]

Uses 1

Statement usesAugmented catalogs

TheoremThe augmented catalogs of sorted catalogs are sorted#✓fully proved

If every catalog in a list of catalogs over a linear order is sorted in nondecreasing order, then every augmented catalog built from that list is sorted in nondecreasing order.

theorem pairwise_augmented {cs : List (List α)}
    (hcs : ∀ c ∈ cs, c.Pairwise (· ≤ ·)) :
    ∀ a ∈ augmented cs, a.Pairwise (· ≤ ·)

Uses 4

Statement usesAugmented catalogs

Proof usesAugmenting a catalog by the head of a list · Augmenting a catalog by the next one · One augmentation step yields a sorted list

TheoremAugmented catalogs are bounded by the total input size#✓fully proved

For every list \(cs = [c_1, \dots, c_k]\) of catalogs over a linearly ordered type, every augmented catalog built from \(cs\) has length at most \(|c_1| + \dots + |c_k|\).

theorem length_mem_augmented_le (cs : List (List α)) :
    ∀ a ∈ augmented cs, a.length ≤ (cs.map List.length).sum

Uses 6

Statement usesAugmented catalogs

Proof usesAugmenting a catalog by the head of a list · Augmenting a catalog by the next one · Length of one augmented catalog · The sample is no longer than the list · Sample of a catalog

DefinitionBridge pointer#✓fully proved

For a catalog \(L\) and a value \(v\), the bridge pointer of \(v\) into \(L\) is the number of elements of \(L\) that are \(\le v\).

When \(L\) is sorted, this is the index just past the elements of \(L\) that are \(\le v\).

def bridgePtr (next : List α) (v : α) : Nat :=
  (next.filter (· ≤ v)).length

Used by 4

Used byBridge pointers are at most the catalog length · Bridge pointer list · Bridge pointers are at most the next catalog's length · Number of bridge pointers

TheoremBridge pointers are at most the catalog length#✓fully proved

For every catalog \(L\) and value \(v\), the bridge pointer of \(v\) into \(L\) is at most the length of \(L\).

theorem bridgePtr_le_length (next : List α) (v : α) :
    bridgePtr next v ≤ next.length

Uses 1 · Used by 1

Statement usesBridge pointer

Used byBridge pointers are at most the next catalog's length

DefinitionBridge pointer list#✓fully proved

For catalogs \(C\) and \(L\), the bridge pointers of \(C\) into \(L\) form the list obtained by replacing each entry \(v\) of \(C\), in order, by the bridge pointer of \(v\) into \(L\).

def bridges (cur next : List α) : List Nat :=
  cur.map (bridgePtr next)

Uses 1 · Used by 2

Statement usesBridge pointer

Used byBridge pointers are at most the next catalog's length · Number of bridge pointers

TheoremNumber of bridge pointers#✓fully proved

For lists \(c\) and \(d\) over a linearly ordered type, the list of bridge pointers of \(c\) into \(d\) has the same length as \(c\): there is one bridge pointer per entry of \(c\).

@[simp]
theorem length_bridges (cur next : List α) :
    (bridges cur next).length = cur.length

Uses 2

Statement usesBridge pointer list

Proof usesBridge pointer

TheoremBridge pointers are at most the next catalog's length#✓fully proved

For lists \(c\) and \(d\) over a linearly ordered type, every entry \(p\) of the list of bridge pointers of \(c\) into \(d\) satisfies \(p \le |d|\), where \(|d|\) is the length of \(d\); so every recorded bridge pointer is a boundary index of \(d\).

theorem le_length_of_mem_bridges {cur next : List α} {p : Nat}
    (hp : p ∈ bridges cur next) : p ≤ next.length

Uses 3

Statement usesBridge pointer list

Proof usesBridge pointer · Bridge pointers are at most the catalog length

DefinitionSearching every catalog#✓fully proved

For a value \(x\) and a list of catalogs, the search returns, for each catalog in order, the number of its elements that are \(< x\), computed by a direct scan of that catalog. This is the lower-bound position of \(x\) in each catalog.

def searchAll (x : α) (catalogs : List (List α)) : List Nat :=
  catalogs.map (countLT x)

Uses 1 · Used by 6

Statement usesScan count of smaller elements

Used bySearch positions are lower bounds, index by index · One search position per catalog · Searching a nonempty list of catalogs · Correctness of searching every catalog · Search positions are boundary indices · Searching no catalogs

TheoremSearching no catalogs#✓fully proved

Searching the empty list of catalogs for any value \(x\) gives the empty list of positions.

@[simp]
theorem searchAll_nil (x : α) : searchAll x ([] : List (List α)) = []

Uses 1

Statement usesSearching every catalog

TheoremSearching a nonempty list of catalogs#✓fully proved

For a value \(x\), a catalog \(c\) and a list of catalogs \(cs\), searching \(c\) followed by \(cs\) for \(x\) gives first the direct-scan count of the elements of \(c\) that are \(< x\), followed by the positions obtained by searching \(cs\) for \(x\).

@[simp]
theorem searchAll_cons (x : α) (c : List α) (cs : List (List α)) :
    searchAll x (c :: cs) = countLT x c :: searchAll x cs

Uses 2

Statement usesScan count of smaller elements · Searching every catalog

TheoremOne search position per catalog#✓fully proved

For every value \(x\) and every list \(cs\) of catalogs over a linearly ordered type, searching each catalog of \(cs\) for \(x\) gives a list of positions of the same length as \(cs\).

@[simp]
theorem length_searchAll (x : α) (cs : List (List α)) :
    (searchAll x cs).length = cs.length

Uses 2

Statement usesSearching every catalog

Proof usesScan count of smaller elements

TheoremCorrectness of searching every catalog#✓fully proved

For a value \(x\) and a list of catalogs \(c_1, \dots, c_k\), searching every catalog for \(x\) returns the list whose \(i\)-th entry is the lower bound of \(x\) in \(c_i\), that is, the number of elements of \(c_i\) that are \(< x\).

theorem searchAll_eq_map_lowerBound (x : α) (cs : List (List α)) :
    searchAll x cs = cs.map (lowerBound x)

Uses 4 · Used by 1

Statement usesLower bound of a value in a catalog · Searching every catalog

Proof usesScan count of smaller elements · The scan count equals the lower bound

Used bySearch positions are lower bounds, index by index

TheoremSearch positions are lower bounds, index by index#✓fully proved

For every value \(x\), list of catalogs \(C_0, \dots, C_{k-1}\) and index \(i\): if \(i < k\), the \(i\)-th position returned by searching all catalogs for \(x\) is the lower bound of \(x\) in \(C_i\); if \(i \ge k\), the search result has no \(i\)-th entry.

theorem getElem?_searchAll (x : α) (cs : List (List α)) (i : Nat) :
    (searchAll x cs)[i]? = (cs[i]?).map (lowerBound x)

Uses 3 · Used by 1

Statement usesLower bound of a value in a catalog · Searching every catalog

Proof usesCorrectness of searching every catalog

Used bySearch positions are boundary indices

TheoremSearch positions are boundary indices#✓fully proved

Let \(x\) be a value and let \(cs\) be a list of catalogs whose entry at index \(i\) is the catalog \(c\). Then searching every catalog of \(cs\) for \(x\) gives, at index \(i\), the lower bound of \(x\) in \(c\) (the number of elements of \(c\) that are \(< x\)), and this lower bound is at most the length of \(c\).

theorem searchAll_le_of_mem {x : α} {cs : List (List α)} {i : Nat}
    {c : List α} (hc : cs[i]? = some c) :
    (searchAll x cs)[i]? = some (lowerBound x c) ∧
      lowerBound x c ≤ c.length

Uses 4

Statement usesLower bound of a value in a catalog · Searching every catalog

Proof usesSearch positions are lower bounds, index by index · Lower bound is at most the catalog length

DefinitionSearching every augmented catalog#✓fully proved

For a value \(x\) and a list of catalogs, the augmented search builds the augmented catalogs and returns, for each augmented catalog in order, the number of its elements that are \(< x\), computed by a direct scan of that catalog.

def searchAugmented (x : α) (cs : List (List α)) : List Nat :=
  (augmented cs).map (countLT x)

Uses 2 · Used by 2

Statement usesAugmented catalogs · Scan count of smaller elements

Used byOne augmented search position per catalog · Correctness of augmented search

TheoremOne augmented search position per catalog#✓fully proved

For every value \(x\) and every list \(cs\) of catalogs over a linearly ordered type, searching each augmented catalog built from \(cs\) for \(x\) gives a list of positions of the same length as \(cs\).

theorem length_searchAugmented (x : α) (cs : List (List α)) :
    (searchAugmented x cs).length = cs.length

Uses 4

Statement usesSearching every augmented catalog

Proof usesAugmented catalogs · Scan count of smaller elements · Number of augmented catalogs

TheoremCorrectness of augmented search#✓fully proved

For a value \(x\) and a list of catalogs \(cs\), searching every augmented catalog of \(cs\) for \(x\) returns, for each augmented catalog in order, the lower bound of \(x\) in it, that is, the number of its elements that are \(< x\).

theorem searchAugmented_eq_map_lowerBound (x : α) (cs : List (List α)) :
    searchAugmented x cs = (augmented cs).map (lowerBound x)

Uses 5

Statement usesAugmented catalogs · Lower bound of a value in a catalog · Searching every augmented catalog

Proof usesScan count of smaller elements · The scan count equals the lower bound

49 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.