Browse chapters

Imports

import Mathlib
import CLRSLean.Probability.FiniteExpectation
import CLRSLean.FourthEdition.Chapter_11.Section_11_2_Chained_Hash_Tables

11.5. Perfect Hashing

This section formalises the two-level perfect-hashing scheme of CLRS §11.5: a static key set is stored using a primary universal hash into m = n buckets, and each bucket with n_j keys gets a secondary table of size m_j = n_j², which — by the birthday-style collision count — is collision-free with probability ≥ 1/2. The total expected secondary storage is O(n).

Main results:

Definition PerfectHashTable: two-level perfect hash data structure.
Theorem perfectSearch_iff_mem: membership correctness (perfectSearch T x ↔ x ∈ T.keys), establishing O(1) worst-case search.
Theorem perfectHash_collision_free_prob_ge_half (Theorem 11.9): when hashing n keys into m = n² slots under a universal family, the hash is collision-free with probability at least 1/2.
Theorem exists_collision_free_secondary: for n ≥ 2 keys into n² slots, an injective secondary hash exists.
Theorem perfectHash_expected_total_space_lt_2n (Theorem 11.10): when n keys are hashed uniformly and independently into m = n primary buckets, the expected total secondary storage E[Σ_j n_j²] is less than 2n (hence O(n)).
Theorem perfectHash_expected_trials_le_two: in a truncated model of t independent trials, the expected number of trials until a collision-free secondary hash is at most 2 (geometric bound with success probability ≥ 1/2).
Theorem perfectHash_expected_construction_time_le_const_n: the expected abstract budget constructionCost is less than 5n. This formula is not itself a counter attached to a table constructor.

The Construction companion supplies an executed finite-trial constructor with a guaranteed collision-free terminal fallback, array initialization and placement, and a separate expected-work refinement to this abstract budget. Secondary injectivity is required only for stored keys in the relevant bucket. The sampling model uses all local-index hash assignments under SUHA, not a constructed family of constant-time hash programs on arbitrary original keys. RAM, hash-code generation, and arithmetic implementation costs are excluded.

Notation conventions used in this section:

n : number of keys
m : number of primary buckets (and m = n for Theorem 11.10)
a : Fin n → Fin m : a hash assignment (SUHA independent-uniform model)
A : Fin t → (Fin n → Fin (n^2)) : a sequence of t independent trial hashes of n keys into n² slots (construction-trial model)
H : ι → (K → Fin m) : a universal family of hash functions
n_j : number of keys assigned to primary bucket j

              namespace CLRSnamespace Chapter11open CLRS.Probabilityopen Finsetopen scoped Classical

Two-level perfect hash model

A PerfectHashTable for a finite set of keys uses a primary hash into m buckets and, for each bucket j, a secondary hash that is collision-free on the keys assigned to that bucket. The deterministic two-level lookup completes in O(1) worst-case time (two table lookups, independent of n).

The fields sec and table are per-bucket; the invariant sec_inj ensures no two stored keys in the same primary bucket share a secondary slot. Nonmembers may collide with stored keys; lookup checks the stored value, so table j (sec j x) = some x identifies x uniquely.

The set of keys stored in the table.

Primary hash function mapping each key to a primary bucket.

For each primary bucket j, a secondary hash function mapping keys to slot indices. The codomain is ℕ; the actual table size per bucket is not needed for correctness, only for the probabilistic space bound.

The secondary table: for each bucket j and slot s, optionally a key.

The secondary hash is collision-free on the keys in each primary bucket: if x and y are both in keys, map to the same primary bucket, and get the same secondary slot, then x = y.

Every key is stored in the table at the slot determined by its primary and secondary hash.

If the table stores a key at a slot, that key maps to that slot.

              structure PerfectHashTable (K : Type) [DecidableEq K] (m : ℕ) : Type where  keys : Finset K  prim : K → Fin m  sec : Fin m → K → ℕ  table : Fin m → ℕ → Option K  sec_inj : ∀ (j : Fin m) (x y : K),
    x ∈ keys → y ∈ keys → prim x = j → prim y = j → sec j x = sec j y → x = y  table_stores_keys : ∀ x ∈ keys, table (prim x) (sec (prim x) x) = some x  table_only_keys : ∀ (j : Fin m) (s : ℕ) (x : K),
    table j s = some x → x ∈ keys ∧ prim x = j ∧ sec j x = s

Two-level perfect-hash search: compute the primary bucket j = prim x, the secondary slot s = sec j x, and check whether table j s holds x.

def perfectSearch [DecidableEq K] (T : PerfectHashTable K m) (x : K) : Prop :=
  T.table (T.prim x) (T.sec (T.prim x) x) = some x

Membership correctness of two-level perfect-hash search. A key x is found by perfectSearch exactly when x ∈ T.keys (CLRS §11.5). This establishes O(1) worst-case search time (two table lookups).

theorem perfectSearch_iff_mem [DecidableEq K] (T : PerfectHashTable K m) (x : K) :
    perfectSearch T x ↔ x ∈ T.keys := by
  constructor
  · intro h
    have hmem := T.table_only_keys (T.prim x) (T.sec (T.prim x) x) x h
    exact hmem.1
  · intro h
    exact T.table_stores_keys x h

Theorem 11.9: secondary collision-free with probability at least 1/2

The fintypeExpect operator is monotone: if X ω ≤ Y ω for all ω, then E[X] ≤ E[Y].

theorem fintypeExpect_mono {Ω : Type} [Fintype Ω] [DecidableEq Ω] {X Y : Ω → ℝ}
    (hXY : ∀ ω, X ω ≤ Y ω) : fintypeExpect X ≤ fintypeExpect Y := by
  unfold fintypeExpect
  refine div_le_div_of_nonneg_right (Finset.sum_le_sum (fun ω _ => hXY ω)) ?_
  positivity

fintypeExpect of a negated random variable is the negation of the expectation.

theorem fintypeExpect_neg {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X : Ω → ℝ) :
    fintypeExpect (fun ω => -X ω) = -fintypeExpect X := by
  simp [fintypeExpect, Finset.sum_neg_distrib, neg_div]

Number of colliding unordered pairs {i, j} with i < j under a hash assignment a : Fin n → Fin m. Each pair of distinct indices that hash to the same bucket contributes 1.

noncomputable def collisionCount {m n : ℕ} (a : Fin n → Fin m) : ℝ :=
  ∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)

collisionCount is nonnegative.


theorem collisionCount_nonneg {m n : ℕ} (a : Fin n → Fin m) : 0 ≤ collisionCount a := by
  unfold collisionCount
  apply Finset.sum_nonneg; intro i hi
  apply Finset.sum_nonneg; intro j hj
  by_cases h : i < j
  · have : 0 ≤ indicator (a i = a j) := by
      unfold indicator; split <;> norm_num
    simp [h, this]
  · simp [h, This simp argument is unused:
  indicator

Hint: Omit it from the simp argument list.
  simp [h,̵ ̵i̵n̵d̵i̵c̵a̵t̵o̵r̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`indicator]

Expected collisions under pairwise independent hashing (SUHA). For hash assignments a : Fin n → Fin m, the expected number of colliding unordered pairs is exactly n(n-1)/(2m).


theorem expectedCollisions_suha {m n : ℕ} (hm : 0 < m) :
    fintypeExpect (fun a : Fin n → Fin m => collisionCount a)
      = (n : ℝ) * ((n : ℝ) - 1) / (2 * (m : ℝ)) := by
  haveI : Nonempty (Fin m) := ⟨⟨0, hm⟩⟩
  unfold collisionCount
  have hE : fintypeExpect (fun a : Fin n → Fin m =>
      ∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0))
      = ∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 / (m : ℝ)) else 0) := by
    rw [fintypeExpect_sum Finset.univ (fun (i : Fin n) (a : Fin n → Fin m) =>
      ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0))]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    rw [fintypeExpect_sum Finset.univ (fun (j : Fin n) (a : Fin n → Fin m) =>
      if i < j then indicator (a i = a j) else 0)]
    refine Finset.sum_congr rfl (fun j _ => ?_)
    by_cases hlt : i < j
    · simp [hlt, pairCollisionProb i j (ne_of_lt hlt) hm]
    · have hcard : Fintype.card (Fin n → Fin m) ≠ 0 := Fintype.card_ne_zero
      simp [hlt, fintypeExpect_const hcard 0]
  have hpair : (∑ i : Fin n, ∑ j : Fin n, (if i < j then (1 / (m : ℝ)) else 0))
      = (1 / (m : ℝ)) * ((n : ℝ) * ((n : ℝ) - 1) / 2) := by
    rw [← sum_upper_triangle n, Finset.mul_sum]
    refine Finset.sum_congr rfl (fun i _ => ?_)
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun j _ => ?_)
    by_cases h : i < j <;> simp [h]
  rw [hE, hpair]
  ring

When n keys are hashed into m = n² slots under SUHA, the expected number of collisions is less than 1/2 (for n ≥ 2).


theorem expectedCollisions_sq_lt_half {n : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun a : Fin n → Fin (n^2) => collisionCount a) < 1/2 := by
  have hm : 0 < n^2 := by
    have hnpos : 0 < n := by omega
    positivity
  rw [expectedCollisions_suha hm]
  have hcalc : (n : ℝ) * ((n : ℝ) - 1) / (2 * ((n : ℝ)^2)) < 1/2 := by
    have hnpos' : (n : ℝ) > 0 := by exact_mod_cast (show 0 < n from by omega)
    have hpos : (0 : ℝ) < 2 * ((n : ℝ)^2) := by positivity
    field_simp [hpos.ne']
    nlinarith
  have hden : ((n ^ 2 : ℕ) : ℝ) = (n : ℝ)^2 := by simp
  simpa [hden] using hcalc

Markov's inequality for nonnegative-integer-valued random variables. If X : Ω → ℕ, then P[X ≥ 1] ≤ E[X].


theorem markov_integer {Ω : Type} [Fintype Ω] [DecidableEq Ω] (X : Ω → ℕ) :
    fintypeExpect (fun ω => if X ω ≥ 1 then (1 : ℝ) else 0) ≤
      fintypeExpect (fun ω => (X ω : ℝ)) := by
  have hpoint : ∀ ω, (if X ω ≥ 1 then (1 : ℝ) else 0) ≤ (X ω : ℝ) := by
    intro ω
    by_cases h : X ω ≥ 1
    · have h' : (1 : ℝ) ≤ (X ω : ℝ) := by exact_mod_cast h
      simp [h, h']
    · simp [h]
  exact fintypeExpect_mono hpoint

Theorem 11.9 (Perfect hashing: secondary collision-free with probability ≥ 1/2). Let n keys be hashed into m = n² slots under a universal family (or under SUHA). Then the hash assignment is collision-free with probability at least 1/2.

Equivalently, a secondary table of size n_j² for a bucket with n_j keys is collision-free with probability at least 1/2 (CLRS Theorem 11.9).

Try this: intro hzero i j heqTry this: intro hzero i j heqTry this: intro hzero i j heq
theorem perfectHash_collision_free_prob_ge_half {n : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun a : Fin n → Fin (n^2) =>
      indicator (∀ i j : Fin n, a i = a j → i = j))
    ≥ 1/2 := by
  have hm : 0 < n^2 := by
    have hnpos' : 0 < n := by omega
    positivity
  have hnpos : 0 < n := by omega
  haveI : Nonempty (Fin n) := ⟨⟨0, hnpos⟩⟩
  haveI : Nonempty (Fin n → Fin (n^2)) :=
    ⟨fun _ => ⟨0, show 0 < n^2 from hm⟩⟩
  have hcard : Fintype.card (Fin n → Fin (n^2)) ≠ 0 := Fintype.card_ne_zero

  -- `X a` is the number of colliding unordered pairs under `a`, as a ℕ.
  let X (a : Fin n → Fin (n^2)) : ℕ :=
    (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
      (Finset.univ : Finset (Fin n × Fin n))).card

  -- `X a = 0` exactly when `a` is injective (collision-free)
  have h_inj_iff : ∀ a : Fin n → Fin (n^2),
      (∀ i j : Fin n, a i = a j → i = j) ↔ X a = 0 := by
    intro a
    dsimp [X]
    constructor
    · intro hinj
      apply Finset.card_eq_zero.mpr
      apply Finset.not_nonempty_iff_eq_empty.mp
      intro hne
      rcases hne with ⟨p, hp⟩
      rcases Finset.mem_filter.mp hp with ⟨hp_univ, ⟨hlt, heq⟩⟩
      exact hlt.ne' (hinj p.1 p.2 heq).symm
    · Try this: intro hzero i j heqintro hzero
      intro i j heq
      by_contra! hne
      rcases lt_trichotomy i j with (hlt | heq' | hlt)
      · have hmem : (i, j) ∈ Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
            (Finset.univ : Finset (Fin n × Fin n)) := by
          simp [hlt, heq]
        have hcard_ne_zero : (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
              (Finset.univ : Finset (Fin n × Fin n))).card ≠ 0 :=
          Finset.card_ne_zero.mpr ⟨(i, j), hmem⟩
        rw [hzero] at hcard_ne_zero
        exact hcard_ne_zero rfl
      · exact hne heq'
      · have hmem : (j, i) ∈ Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
            (Finset.univ : Finset (Fin n × Fin n)) := by
          simp [hlt, heq.symm]
        have hcard_ne_zero : (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
              (Finset.univ : Finset (Fin n × Fin n))).card ≠ 0 :=
          Finset.card_ne_zero.mpr ⟨(j, i), hmem⟩
        rw [hzero] at hcard_ne_zero
        exact hcard_ne_zero rfl

  -- Rewrite the collision-free indicator in terms of `X`
  have h_indicator_eq : (fun a : Fin n → Fin (n^2) => indicator (∀ i j : Fin n, a i = a j → i = j))
      = (fun a : Fin n → Fin (n^2) => if X a = 0 then (1 : ℝ) else 0) := by
    funext a; simp [indicator, h_inj_iff a]

  rw [h_indicator_eq]

  -- Relate `collisionCount` (real-valued) to `X` (ℕ-valued)
  have h_collision_eq : (fun (a : Fin n → Fin (n^2)) => collisionCount a) =
      (fun (a : Fin n → Fin (n^2)) => (X a : ℝ)) := by
    funext a
    dsimp [collisionCount, X]
    have h1 : (∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)) =
        (∑ p : Fin n × Fin n, (if p.1 < p.2 then indicator (a p.1 = a p.2) else 0)) := by
      simp [Fintype.sum_prod_type]
    have h2 : (∑ p : Fin n × Fin n, (if p.1 < p.2 then indicator (a p.1 = a p.2) else 0)) =
        (∑ p : Fin n × Fin n, (if p.1 < p.2 ∧ a p.1 = a p.2 then (1 : ℝ) else 0)) := by
      refine Finset.sum_congr rfl (fun p _ => ?_)
      by_cases hlt : p.1 < p.2
      · simp [hlt, indicator]
      · simp [hlt, This simp argument is unused:
  indicator

Hint: Omit it from the simp argument list.
  simp [hlt,̵ ̵i̵n̵d̵i̵c̵a̵t̵o̵r̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`indicator]
    have h3 : (∑ p : Fin n × Fin n, (if p.1 < p.2 ∧ a p.1 = a p.2 then (1 : ℝ) else 0)) =
        (Finset.card (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
          (Finset.univ : Finset (Fin n × Fin n))) : ℝ) := by
      simp [This simp argument is unused:
  Finset.sum_filter

Hint: Omit it from the simp argument list.
  simp ̵[̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵f̵i̵l̵t̵e̵r̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.sum_filter]
    calc
      collisionCount a = (∑ i : Fin n, ∑ j : Fin n, (if i < j then indicator (a i = a j) else 0)) := rfl
      _ = (∑ p : Fin n × Fin n, (if p.1 < p.2 then indicator (a p.1 = a p.2) else 0)) := h1
      _ = (∑ p : Fin n × Fin n, (if p.1 < p.2 ∧ a p.1 = a p.2 then (1 : ℝ) else 0)) := h2
      _ = (Finset.card (Finset.filter (fun (p : Fin n × Fin n) => p.1 < p.2 ∧ a p.1 = a p.2)
          (Finset.univ : Finset (Fin n × Fin n))) : ℝ) := h3
      _ = (X a : ℝ) := rfl

  have h_expected_X_lt_half :
      fintypeExpect (fun a : Fin n → Fin (n^2) => (X a : ℝ)) < 1/2 := by
    rw [← h_collision_eq]
    exact expectedCollisions_sq_lt_half hn

  -- Markov inequality: P[X ≥ 1] ≤ E[X]
  have h_markov : fintypeExpect (fun a : Fin n → Fin (n^2) => if X a ≥ 1 then (1 : ℝ) else 0) ≤
      fintypeExpect (fun a : Fin n → Fin (n^2) => (X a : ℝ)) :=
    markov_integer X

  -- `indicator(X = 0) = 1 - indicator(X ≥ 1)`
  have h_decomp : (fun a : Fin n → Fin (n^2) => (if X a = 0 then (1 : ℝ) else 0)) =
      (fun a : Fin n → Fin (n^2) => (1 : ℝ) - (if X a ≥ 1 then (1 : ℝ) else 0)) := by
    funext a
    by_cases h : X a = 0
    · simp [h]
    · have hpos : X a ≥ 1 := Nat.one_le_of_lt (Nat.pos_of_ne_zero h)
      simp [h, hpos]

  rw [h_decomp]
  have h_expect_sub : fintypeExpect (fun a : Fin n → Fin (n^2) =>
      (1 : ℝ) - (if X a ≥ 1 then (1 : ℝ) else 0)) =
    (1 : ℝ) - fintypeExpect (fun a : Fin n → Fin (n^2) => (if X a ≥ 1 then (1 : ℝ) else 0)) := by
    calc
      fintypeExpect (fun a : Fin n → Fin (n^2) =>
          (1 : ℝ) - (if X a ≥ 1 then (1 : ℝ) else 0))
          = fintypeExpect (fun a : Fin n → Fin (n^2) =>
              (1 : ℝ) + (-(if X a ≥ 1 then (1 : ℝ) else 0))) := by
            refine congrArg fintypeExpect (funext fun a => ?_)
            rfl
      _ = fintypeExpect (fun _ : Fin n → Fin (n^2) => (1 : ℝ)) +
            fintypeExpect (fun a : Fin n → Fin (n^2) =>
              -(if X a ≥ 1 then (1 : ℝ) else 0)) :=
            fintypeExpect_add _ _
      _ = (1 : ℝ) + (-fintypeExpect (fun a : Fin n → Fin (n^2) =>
            (if X a ≥ 1 then (1 : ℝ) else 0))) := by
        simp [fintypeExpect_const hcard, fintypeExpect_neg]
      _ = (1 : ℝ) - fintypeExpect (fun a : Fin n → Fin (n^2) =>
            (if X a ≥ 1 then (1 : ℝ) else 0)) := by ring

  rw [h_expect_sub]
  have h_bound : fintypeExpect (fun a : Fin n → Fin (n^2) => if X a ≥ 1 then (1 : ℝ) else 0) < 1/2 := by
    linarith
  linarith

Theorem 11.10: expected total space O(n)

The number of keys (out of n) that hash to a given bucket j under assignment a.

noncomputable def bucketSize {m n : ℕ} (a : Fin n → Fin m) (j : Fin m) : ℝ :=
  ∑ i : Fin n, indicator (a i = j)

The total secondary storage for a hash assignment a: sum over buckets of the square of the bucket size, i.e. Σ_j n_j². This is the space used if each bucket j gets a secondary table of size n_j².

noncomputable def totalSecondarySpace {m n : ℕ} (a : Fin n → Fin m) : ℝ :=
  ∑ j : Fin m, (bucketSize a j) ^ 2

The algebraic identity Σ_j n_j² = Σ_i Σ_k indicator(a i = a k). This expands the sum of squares into a double sum over key pairs (CLRS proof of Theorem 11.10).


theorem totalSecondarySpace_eq_sum_indicator {m n : ℕ} (a : Fin n → Fin m) :
    totalSecondarySpace a = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) := by
  unfold totalSecondarySpace bucketSize
  calc
    ∑ j : Fin m, ((∑ i : Fin n, indicator (a i = j)) : ℝ) ^ 2
        = ∑ j : Fin m, (∑ i : Fin n, indicator (a i = j)) * (∑ k : Fin n, indicator (a k = j)) := by
          simp [sq]
    _ = ∑ j : Fin m, ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
      refine Finset.sum_congr rfl (fun j hj => ?_)
      calc
        (∑ i : Fin n, indicator (a i = j)) * (∑ k : Fin n, indicator (a k = j))
            = ∑ k : Fin n, (∑ i : Fin n, indicator (a i = j)) * indicator (a k = j) := by
              rw [Finset.mul_sum]
        _ = ∑ k : Fin n, ∑ i : Fin n, indicator (a i = j) * indicator (a k = j) := by
          refine Finset.sum_congr rfl (fun k hk => ?_)
          rw [Finset.sum_mul]
        _ = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
          rw [Finset.sum_comm]
    _ = ∑ i : Fin n, ∑ k : Fin n, ∑ j : Fin m, indicator (a i = j) * indicator (a k = j) := by
      calc
        ∑ j : Fin m, ∑ i : Fin n, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j)
            = ∑ i : Fin n, ∑ j : Fin m, ∑ k : Fin n, indicator (a i = j) * indicator (a k = j) := by
              rw [Finset.sum_comm]
        _ = ∑ i : Fin n, ∑ k : Fin n, ∑ j : Fin m, indicator (a i = j) * indicator (a k = j) := by
          refine Finset.sum_congr rfl (fun i hi => ?_)
          rw [Finset.sum_comm]
    _ = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) := by
      refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun k _ => ?_))
      simp [indicator, Finset.sum_ite_eq, Finset.mem_univ]

Theorem 11.10 (Expected total space is O(n)). When n keys are hashed uniformly and independently into m = n primary buckets, the expected total secondary storage E[Σ_j n_j²] is strictly less than 2n (CLRS Theorem 11.10).


theorem perfectHash_expected_total_space_lt_2n {n : ℕ} (hn : 0 < n) :
    fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) < 2 * (n : ℝ) := by
  have hm : 0 < n := hn
  haveI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
  have hcard : Fintype.card (Fin n → Fin n) ≠ 0 := Fintype.card_ne_zero

  -- Algebraic identity: Σ_j n_j² = n + Σ_{i≠k} indicator(a i = a k)
  have h_identity : ∀ a : Fin n → Fin n,
      totalSecondarySpace a = (n : ℝ) + ∑ i : Fin n, ∑ k : Fin n,
        (if i ≠ k then indicator (a i = a k) else 0) := by
    intro a
    calc
      totalSecondarySpace a = ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k) :=
        totalSecondarySpace_eq_sum_indicator a
      _ = (∑ i : Fin n, indicator (a i = a i)) +
          (∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
        calc
          ∑ i : Fin n, ∑ k : Fin n, indicator (a i = a k)
              = ∑ i : Fin n, (indicator (a i = a i) + ∑ k : Fin n,
                  (if i ≠ k then indicator (a i = a k) else 0)) := by
            refine Finset.sum_congr rfl (fun i hi => ?_)
            have h_inner : ∑ k : Fin n, indicator (a i = a k)
                = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := by
              calc
                ∑ k : Fin n, indicator (a i = a k)
                    = ∑ k : Fin n, ((if i = k then indicator (a i = a i) else 0) +
                        (if i ≠ k then indicator (a i = a k) else 0)) := by
                      refine Finset.sum_congr rfl (fun k hk => ?_)
                      by_cases hik : i = k
                      · subst hik; simp
                      · simp [hik]
                _ = (∑ k : Fin n, (if i = k then indicator (a i = a i) else 0)) +
                    (∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
                  simp [Finset.sum_add_distrib]
                _ = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := by
                  simp [Finset.sum_ite_eq, Finset.mem_univ]

            calc
              ∑ k : Fin n, indicator (a i = a k)
                  = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := h_inner
              _ = indicator (a i = a i) + ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := rfl
          _ = (∑ i : Fin n, indicator (a i = a i)) +
              (∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
            simp [Finset.sum_add_distrib]
      _ = (n : ℝ) + ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0) := by
        simp [indicator, Finset.sum_const, Finset.card_univ, Fintype.card_fin]

  -- Use the identity inside the expectation
  have h_expect_identity :
      fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) =
      (n : ℝ) + fintypeExpect (fun a : Fin n → Fin n =>
        ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
    calc
      fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) =
          fintypeExpect (fun a : Fin n → Fin n => (n : ℝ) + ∑ i : Fin n, ∑ k : Fin n,
            (if i ≠ k then indicator (a i = a k) else 0)) := by
            refine congrArg fintypeExpect (funext h_identity)
      _ = fintypeExpect (fun _ : Fin n → Fin n => (n : ℝ)) +
          fintypeExpect (fun a : Fin n → Fin n =>
            ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) :=
        fintypeExpect_add _ _
      _ = (n : ℝ) + fintypeExpect (fun a : Fin n → Fin n =>
            ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
        simp [fintypeExpect_const hcard, This simp argument is unused:
  Fintype.card_fin

Hint: Omit it from the simp argument list.
  simp [fintypeExpect_const hcard,̵ ̵F̵i̵n̵t̵y̵p̵e̵.̵c̵a̵r̵d̵_̵f̵i̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Fintype.card_fin]

  rw [h_expect_identity]

  -- Compute the remaining expectation: E[Σ_{i≠k} indicator(a i = a k)] = n*(n-1)*(1/n) = n-1
  have h_cross_expect :
      fintypeExpect (fun a : Fin n → Fin n =>
        ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0))
      = (n : ℝ) - 1 := by
    calc
      fintypeExpect (fun a : Fin n → Fin n =>
          ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0))
          = ∑ i : Fin n, fintypeExpect (fun a : Fin n → Fin n =>
              ∑ k : Fin n, (if i ≠ k then indicator (a i = a k) else 0)) := by
            rw [fintypeExpect_sum Finset.univ]
      _ = ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then
            fintypeExpect (fun a : Fin n → Fin n => indicator (a i = a k)) else 0) := by
        refine Finset.sum_congr rfl (fun i _ => ?_)
        rw [fintypeExpect_sum Finset.univ]
        refine Finset.sum_congr rfl (fun k _ => ?_)
        by_cases hne : i ≠ k
        · simp [hne, pairCollisionProb i k hne hm]
        · simp [hne, fintypeExpect_const hcard, This simp argument is unused:
  Fintype.card_fin

Hint: Omit it from the simp argument list.
  simp [hne, fintypeExpect_const hcard,̵ ̵F̵i̵n̵t̵y̵p̵e̵.̵c̵a̵r̵d̵_̵f̵i̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Fintype.card_fin]
      _ = ∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0) := by
        refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun k _ => ?_))
        by_cases hne : i ≠ k
        · rw [pairCollisionProb i k hne hm]
        · simp [hne]
      _ = (n : ℝ) - 1 := by
        have h_inner_sum : ∀ i : Fin n, (∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0)) = ((n : ℝ) - 1) / (n : ℝ) := by
          intro i
          calc
            (∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0))
                = (∑ k : Fin n, (if i ≠ k then (1 : ℝ) else 0)) * (1 / (n : ℝ)) := by
                  simp [Finset.mul_sum, mul_comm]
            _ = ((n : ℝ) - 1) * (1 / (n : ℝ)) := by
              have hsum : (∑ k : Fin n, (if i ≠ k then (1 : ℝ) else 0)) = (n : ℝ) - 1 := by
                calc
                  (∑ k : Fin n, (if i ≠ k then (1 : ℝ) else 0))
                      = (∑ k : Fin n, ((1 : ℝ) - (if i = k then (1 : ℝ) else 0))) := by
                        refine Finset.sum_congr rfl (fun k hk => ?_)
                        by_cases hik : i = k
                        · subst hik; simp
                        · simp [hik]
                  _ = (∑ k : Fin n, (1 : ℝ)) - (∑ k : Fin n, (if i = k then (1 : ℝ) else 0)) := by
                    simp [This simp argument is unused:
  Finset.sum_add_distrib

Hint: Omit it from the simp argument list.
  simp ̵[̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵a̵d̵d̵_̵d̵i̵s̵t̵r̵i̵b̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Finset.sum_add_distrib]
                  _ = (n : ℝ) - 1 := by simp [Fintype.card_fin, Finset.sum_ite_eq, Finset.mem_univ]
              rw [hsum]
            _ = ((n : ℝ) - 1) / (n : ℝ) := by ring
        calc
          (∑ i : Fin n, ∑ k : Fin n, (if i ≠ k then (1 / (n : ℝ)) else 0))
              = ∑ i : Fin n, (((n : ℝ) - 1) / (n : ℝ)) := by
                refine Finset.sum_congr rfl (fun i hi => ?_); rw [h_inner_sum i]
          _ = (n : ℝ) * (((n : ℝ) - 1) / (n : ℝ)) := by
            simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
          _ = (n : ℝ) - 1 := by
            field_simp [show (n : ℝ) ≠ 0 from by exact_mod_cast hn.ne']

  rw [h_cross_expect]
  nlinarith

Construction trials: expected trials to a collision-free secondary hash

A hash assignment a : Fin n → Fin (n^2) of n keys into n² slots is collision-free exactly when it is injective.

abbrev collisionFree {n : ℕ} (a : Fin n → Fin (n^2)) : Prop :=
  ∀ i j : Fin n, a i = a j → i = j

Split a sequence of k + 1 independent trial hashes into the first k trials and the last trial. This witnesses that the prefix coordinates are independent of the last coordinate.


noncomputable def trialsSplitLast {n k : ℕ} :
    (Fin (k + 1) → (Fin n → Fin (n^2))) ≃
      (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) where
  toFun A := ((fun j : Fin k => A (Fin.castSucc j)), A ⟨k, Nat.lt_succ_self k⟩)
  invFun q := fun x : Fin (k + 1) =>
    if hx : x.val < k then q.1 ⟨x.val, hx⟩ else q.2
  left_inv A := by
    funext x
    by_cases hx : x.val < k
    · simp [hx]
    · simp [hx]
      have hx' : x = ⟨k, Nat.lt_succ_self k⟩ := by
        apply Fin.ext
        change x.val = k
        omega
      rw [hx']
  right_inv q := by
    obtain ⟨P, L⟩ := q
    refine Prod.ext ?_ ?_
    · funext j
      simp
    · simp

Split a sequence of t independent trial hashes into the first k trials and the remaining t - k trials, for k ≤ t. This witnesses that the prefix coordinates are independent of the suffix coordinates.


noncomputable def trialsSplitPrefix {n t k : ℕ} (hkt : k ≤ t) :
    (Fin t → (Fin n → Fin (n^2))) ≃
      (Fin k → (Fin n → Fin (n^2))) × (Fin (t - k) → (Fin n → Fin (n^2))) where
  toFun A := ((fun j : Fin k => A (Fin.castLE hkt j)),
              (fun j : Fin (t - k) => A ⟨k + j.val, by omega⟩))
  invFun q := fun x : Fin t =>
    if hx : x.val < k then q.1 ⟨x.val, hx⟩ else q.2 ⟨x.val - k, by omega⟩
  left_inv A := by
    funext x
    by_cases hx : x.val < k
    · simp [hx]
    · simp [hx]
      apply congrArg A
      apply Fin.ext
      change k + (x.val - k) = x.val
      omega
  right_inv q := by
    obtain ⟨P, S⟩ := q
    refine Prod.ext ?_ ?_
    · funext j
      simp
    · funext j
      have hnot : ¬ k + j.val < k := by omega
      simp [hnot]

Independent-trials failure bound. In k independent trials, each of which produces a collision-free hash of n ≥ 2 keys into n² slots with probability at least 1/2 (Theorem 11.9), the probability that all k trials fail is at most (1/2)^k (CLRS §11.5).


theorem perfectHash_prefix_fail_prob_le {n k : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin k → (Fin n → Fin (n^2)) =>
      indicator (∀ j : Fin k, ¬ collisionFree (A j))) ≤ (1/2 : ℝ)^k := by
  induction k with
  | zero =>
      have htrue : ∀ A : Fin 0 → (Fin n → Fin (n^2)),
          (∀ j : Fin 0, ¬ collisionFree (A j)) := by
        intro A j
        exact Fin.elim0 j
      haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by
        have hnpos : 0 < n := by omega
        positivity⟩⟩
      have hcard : Fintype.card (Fin 0 → (Fin n → Fin (n^2))) ≠ 0 := Fintype.card_ne_zero
      calc
        fintypeExpect (fun A : Fin 0 → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin 0, ¬ collisionFree (A j)))
            = fintypeExpect (fun _ : Fin 0 → (Fin n → Fin (n^2)) => (1 : ℝ)) := by
              refine congrArg fintypeExpect (funext fun A => ?_)
              have hP : (∀ j : Fin 0, ¬ collisionFree (A j)) := htrue A
              unfold indicator
              rw [if_pos hP]
        _ = 1 := by
              simp [fintypeExpect_const hcard]
        _ ≤ (1/2 : ℝ)^0 := by
              simp
  | succ k ih =>
      have hnpos : 0 < n := by omega
      haveI : Nonempty (Fin n) := ⟨⟨0, hnpos⟩⟩
      haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by positivity⟩⟩
      have hcardΩ : Fintype.card (Fin n → Fin (n^2)) ≠ 0 := Fintype.card_ne_zero
      -- `∀ j : Fin (k+1), ¬ CF (A j)` splits as the prefix conjunction and the
      -- last trial
      have hsplit : ∀ A : Fin (k + 1) → (Fin n → Fin (n^2)),
          indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j))
            = indicator ((∀ j : Fin k, ¬ collisionFree (A (Fin.castSucc j))) ∧
                ¬ collisionFree (A ⟨k, Nat.lt_succ_self k⟩)) := by
        intro A
        have hiff : (∀ j : Fin (k + 1), ¬ collisionFree (A j)) ↔
            (∀ j : Fin k, ¬ collisionFree (A (Fin.castSucc j))) ∧
              ¬ collisionFree (A ⟨k, Nat.lt_succ_self k⟩) := by
          constructor
          · intro h
            constructor
            · intro j
              exact h (Fin.castSucc j)
            · exact h ⟨k, Nat.lt_succ_self k⟩
          · rintro ⟨hpre, hlast⟩ j
            by_cases hj : j.val < k
            · have hj' : j = Fin.castSucc ⟨j.val, hj⟩ := by
                ext
                rfl
              rw [hj']
              exact hpre ⟨j.val, hj⟩
            · have hj' : j = ⟨k, Nat.lt_succ_self k⟩ := by
                apply Fin.ext
                change j.val = k
                omega
              rw [hj']
              exact hlast
        unfold indicator
        by_cases hP1 : ∀ j : Fin (k + 1), ¬collisionFree (A j)
        · rw [if_pos hP1, if_pos (hiff.mp hP1)]
        · rw [if_neg hP1, if_neg (fun hP2 => hP1 (hiff.mpr hP2))]
      -- reindex the product sample space so the prefix and last trial separate
      have he := fintypeExpect_equiv (trialsSplitLast (n := n) (k := k))
        (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
          indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2)))
      have hLHS : fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j)))
          = fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
              indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2))) := by
        calc
          fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
                indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j)))
              = fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
                  indicator ((∀ j : Fin k, ¬ collisionFree (A (Fin.castSucc j))) ∧
                    ¬ collisionFree (A ⟨k, Nat.lt_succ_self k⟩))) := by
                refine congrArg fintypeExpect (funext fun A => hsplit A)
          _ = fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
                  indicator ((∀ j : Fin k, ¬ collisionFree ((trialsSplitLast (n := n) (k := k) A).1 j)) ∧
                    ¬ collisionFree ((trialsSplitLast (n := n) (k := k) A).2))) := by
                refine congrArg fintypeExpect (funext fun A => ?_)
                simp [trialsSplitLast]
          _ = fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
                  indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2))) := he
      -- the conjunction of the independent prefix event and the last-trial event
      -- factorizes as a product of expectations
      have hprod : fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
              indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2)))
          = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
              indicator (∀ j : Fin k, ¬ collisionFree (B j)))
            * fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) := by
        have hsplit2 : (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
              indicator ((∀ j : Fin k, ¬ collisionFree (p.1 j)) ∧ ¬ collisionFree (p.2)))
            = (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin n → Fin (n^2)) =>
                (fun B : Fin k → (Fin n → Fin (n^2)) => indicator (∀ j : Fin k, ¬ collisionFree (B j))) p.1
                  * (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) p.2) := by
          funext p
          by_cases hpre : ∀ j : Fin k, ¬ collisionFree (p.1 j)
          · by_cases hlast : ¬ collisionFree (p.2)
            · simp [indicator, hpre, hlast]
            · simp [indicator, hpre, hlast]
          · by_cases hlast : ¬ collisionFree (p.2)
            · simp [indicator, This simp argument is unused:
  hpre

Hint: Omit it from the simp argument list.
  simp [indicator, hp̵r̵e̵,̵ ̵h̵last]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hpre, hlast]
            · simp [indicator, This simp argument is unused:
  hpre

Hint: Omit it from the simp argument list.
  simp [indicator, hp̵r̵e̵,̵ ̵h̵last]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hpre, hlast]
        rw [hsplit2]
        exact expect_mul_of_indep (fun B : Fin k → (Fin n → Fin (n^2)) =>
          indicator (∀ j : Fin k, ¬ collisionFree (B j)))
          (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a))
      -- a single trial fails with probability at most 1/2 (Theorem 11.9)
      have hfail : fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) ≤ 1/2 := by
        have hE : fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a))
            = 1 - fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (collisionFree a)) := by
          calc
            fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a))
                = fintypeExpect (fun a : Fin n → Fin (n^2) => (1 : ℝ) - indicator (collisionFree a)) := by
                  refine congrArg fintypeExpect (funext fun a => ?_)
                  by_cases h : collisionFree a
                  · unfold indicator
                    rw [if_neg (fun hna => hna h), if_pos h]
                    simp
                  · unfold indicator
                    rw [if_pos h, if_neg h]
                    simp
            _ = fintypeExpect (fun a : Fin n → Fin (n^2) => (1 : ℝ) + (-indicator (collisionFree a))) := by
                  refine congrArg fintypeExpect (funext fun a => ?_)
                  ring
            _ = fintypeExpect (fun _ : Fin n → Fin (n^2) => (1 : ℝ)) +
                  fintypeExpect (fun a : Fin n → Fin (n^2) => -indicator (collisionFree a)) := fintypeExpect_add _ _
            _ = 1 - fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (collisionFree a)) := by
                  rw [fintypeExpect_const hcardΩ, fintypeExpect_neg]
                  ring
        rw [hE]
        have hcf : 1/2 ≤ fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (collisionFree a)) := by
          simpa [collisionFree] using (perfectHash_collision_free_prob_ge_half (n := n) hn)
        linarith
      -- assemble: E[prefix ∧ last] = E[prefix] · E[last] ≤ (1/2)^k · (1/2)
      calc
        fintypeExpect (fun A : Fin (k + 1) → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin (k + 1), ¬ collisionFree (A j)))
            = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
                indicator (∀ j : Fin k, ¬ collisionFree (B j)))
              * fintypeExpect (fun a : Fin n → Fin (n^2) => indicator (¬ collisionFree a)) := by
              rw [hLHS, hprod]
        _ ≤ (1/2 : ℝ)^k * (1/2) := by
              exact mul_le_mul ih hfail
                (fintypeExpect_nonneg (fun a : Fin n → Fin (n^2) => by
                  unfold indicator
                  split <;> norm_num))
                (by positivity)
        _ = (1/2 : ℝ)^(k + 1) := by
              simp [pow_succ]

The probability that the first k of t independent trials all fail is at most (1/2)^k: the remaining t - k trials are independent of the prefix and marginalise out.


theorem perfectHash_trials_prefix_fail_prob_le {n k t : ℕ} (hn : 2 ≤ n) (hkt : k ≤ t) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
      indicator (∀ j : Fin k, ¬ collisionFree (A (Fin.castLE hkt j)))) ≤ (1/2 : ℝ)^k := by
  haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by
    have hnpos : 0 < n := by omega
    positivity⟩⟩
  have hcard_suffix : Fintype.card (Fin (t - k) → (Fin n → Fin (n^2))) ≠ 0 := Fintype.card_ne_zero
  have hpre : fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
        indicator (∀ j : Fin k, ¬ collisionFree (A (Fin.castLE hkt j))))
      = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
        indicator (∀ j : Fin k, ¬ collisionFree (B j))) := by
    calc
      fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin k, ¬ collisionFree (A (Fin.castLE hkt j))))
          = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
              indicator (∀ j : Fin k, ¬ collisionFree ((trialsSplitPrefix hkt A).1 j))) := by
            refine congrArg fintypeExpect (funext fun A => ?_)
            simp [trialsSplitPrefix]
      _ = fintypeExpect (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin (t - k) → (Fin n → Fin (n^2))) =>
            indicator (∀ j : Fin k, ¬ collisionFree (p.1 j))) := by
            exact fintypeExpect_equiv (trialsSplitPrefix hkt)
              (fun p : (Fin k → (Fin n → Fin (n^2))) × (Fin (t - k) → (Fin n → Fin (n^2))) =>
                indicator (∀ j : Fin k, ¬ collisionFree (p.1 j)))
      _ = fintypeExpect (fun B : Fin k → (Fin n → Fin (n^2)) =>
            indicator (∀ j : Fin k, ¬ collisionFree (B j))) := by
            exact fintypeExpect_fst hcard_suffix
              (fun B : Fin k → (Fin n → Fin (n^2)) => indicator (∀ j : Fin k, ¬ collisionFree (B j)))
  rw [hpre]
  exact perfectHash_prefix_fail_prob_le hn

The number of failed trials before the first collision-free trial in a sequence of t independent trials. Equivalently, the sum over k of the indicators "the first k + 1 trials all fail": each failing trial before the first success contributes exactly one such prefix. If every trial fails, the value is t.

noncomputable def failedTrials {n t : ℕ} (A : Fin t → (Fin n → Fin (n^2))) : ℕ :=
  (Finset.univ.filter (fun k : Fin t =>
    ∀ j : Fin (k.val + 1), ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))).card

failedTrials decomposes as the sum over trial prefixes of the indicator that the first k + 1 trials all fail.

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem failedTrials_eq_sum {n t : ℕ} (A : Fin t → (Fin n → Fin (n^2))) :
    failedTrials A = ∑ k : Fin t, (if (∀ j : Fin (k.val + 1),
      ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j))) then 1 else 0) := by
  unfold failedTrials
  -- (Finset.univ.filter p).card = ∑ k ∈ univ, if p k then 1 else 0
  try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using (Finset.sum_boole (fun k : Fin t => ∀ j : Fin (k.val + 1),
    ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))
    (Finset.univ : Finset (Fin t))).symm

Expected failed trials before a collision-free hash. In the truncated model of t independent trials (each collision-free with probability at least 1/2, Theorem 11.9), the expected number of failed trials before the first collision-free trial is at most 1 — via the tail-sum identity E[F] = Σ_k P[first k trials fail] ≤ Σ_k (1/2)^k = 1 (CLRS §11.5).


theorem perfectHash_expected_failedTrials_le_one {n t : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) ≤ 1 := by
  have hdecomp : (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ))
      = (fun A : Fin t → (Fin n → Fin (n^2)) => ∑ k : Fin t,
          indicator (∀ j : Fin (k.val + 1),
            ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))) := by
    funext A
    rw [failedTrials_eq_sum A]
    simp [indicator, This simp argument is unused:
  Nat.cast_sum

Hint: Omit it from the simp argument list.
  simp [indicator,̵ ̵N̵a̵t̵.̵c̵a̵s̵t̵_̵s̵u̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Nat.cast_sum]
  have hlin : fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ))
      = ∑ k : Fin t, fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
          indicator (∀ j : Fin (k.val + 1),
            ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))) := by
    rw [hdecomp]
    exact fintypeExpect_sum Finset.univ _
  have hterm : ∀ k : Fin t, fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
        indicator (∀ j : Fin (k.val + 1),
          ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j)))) ≤ (1/2 : ℝ)^(k.val + 1) := by
    intro k
    exact perfectHash_trials_prefix_fail_prob_le hn (Nat.succ_le_of_lt k.isLt)
  calc
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ))
        ≤ ∑ k : Fin t, (1/2 : ℝ)^(k.val + 1) := by
          rw [hlin]
          exact Finset.sum_le_sum (fun k _ => hterm k)
    _ ≤ 1 := by
          -- ∑ k : Fin t, (1/2)^(k.val + 1) = (1/2) · ∑ k : Fin t, (1/2)^k.val ≤ (1/2) · 2 = 1
          have hfactor : (∑ k : Fin t, (1/2 : ℝ)^(k.val + 1)) = (1/2) * (∑ k : Fin t, (1/2 : ℝ)^k.val) := by
            calc
              (∑ k : Fin t, (1/2 : ℝ)^(k.val + 1))
                  = (∑ k : Fin t, (1/2 : ℝ)^k.val * (1/2)) := by
                    refine Finset.sum_congr rfl (fun k _ => ?_)
                    rw [pow_succ]
              _ = (1/2) * (∑ k : Fin t, (1/2 : ℝ)^k.val) := by
                    rw [Finset.mul_sum]
                    simp [mul_comm]
          rw [hfactor]
          have hgeom : (∑ k : Fin t, (1/2 : ℝ)^k.val) ≤ 2 := by
            have hrange : (∑ k : Fin t, (1/2 : ℝ)^k.val) = ∑ i ∈ Finset.range t, (1/2 : ℝ)^i := by
              rw [Fin.sum_univ_eq_sum_range (fun i : ℕ => (1/2 : ℝ)^i) t]
            rw [hrange]
            have hgeom_mul := geom_sum_mul_of_le_one (x := (1/2 : ℝ)) (by norm_num) t
            -- (∑ i ∈ range t, (1/2)^i) * (1 - 1/2) = 1 - (1/2)^t, so the product is ≤ 1
            have hmul : (∑ i ∈ Finset.range t, (1/2 : ℝ)^i) * (1/2) ≤ 1 := by
              norm_num at hgeom_mul
              rw [hgeom_mul]
              have hpow : 0 ≤ (1/2 : ℝ)^t := by positivity
              nlinarith
            nlinarith
          nlinarith

The number of trials performed until a collision-free secondary hash is obtained, in a truncated model of t independent trials: the failed trials before the first collision-free trial, plus the successful trial itself. If none of the t trials is collision-free, the value is t + 1. This is a lower truncation of an unbounded waiting time, not an upper estimate. A constructor using a guaranteed terminal fallback may instead interpret the last unit as its successful fallback attempt; that requires a separate bridge.

noncomputable def trialsUntilCollisionFree {n t : ℕ} (A : Fin t → (Fin n → Fin (n^2))) : ℕ :=
  failedTrials A + 1

Expected number of trials to obtain a collision-free secondary hash. In the truncated model of t independent trials — each trial hashes n ≥ 2 keys into n² slots and is collision-free with probability at least 1/2 (Theorem 11.9) — the expected number of trials performed up to and including the first collision-free trial is at most 2 (CLRS §11.5). This theorem bounds each finite truncation. It does not by itself supply an infinite trial process or a limit theorem for its expectation.


theorem perfectHash_expected_trials_le_two {n t : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (trialsUntilCollisionFree A : ℝ)) ≤ 2 := by
  unfold trialsUntilCollisionFree
  calc
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => ((failedTrials A + 1 : ℕ) : ℝ))
        = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ) + 1) := by
          refine congrArg fintypeExpect (funext fun A => ?_)
          simp
    _ = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) + 1 := by
          calc
            fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ) + 1)
                = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) +
                    fintypeExpect (fun _ : Fin t → (Fin n → Fin (n^2)) => (1 : ℝ)) := fintypeExpect_add _ _
            _ = fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) => (failedTrials A : ℝ)) + 1 := by
                  haveI : Nonempty (Fin n → Fin (n^2)) := ⟨fun _ => ⟨0, by
                    have hnpos : 0 < n := by omega
                    positivity⟩⟩
                  have hcard : Fintype.card (Fin t → (Fin n → Fin (n^2))) ≠ 0 := Fintype.card_ne_zero
                  simp [fintypeExpect_const hcard]
    _ ≤ 2 := by
          linarith [perfectHash_expected_failedTrials_le_one (n := n) (t := t) hn]

Existence of a collision-free secondary hash. For n ≥ 2 keys hashed into n² slots, some hash assignment is injective. This follows from Theorem 11.9: the collision-free probability is at least 1/2 > 0, so the event cannot be empty (CLRS §11.5).


theorem exists_collision_free_secondary {n : ℕ} (hn : 2 ≤ n) :
    ∃ a : Fin n → Fin (n^2), ∀ i j : Fin n, a i = a j → i = j := by
  by_contra h
  have hnone : ∀ a : Fin n → Fin (n^2), ¬ (∀ i j : Fin n, a i = a j → i = j) := by
    intro a ha
    exact h ⟨a, ha⟩
  have hzero : fintypeExpect (fun a : Fin n → Fin (n^2) =>
      indicator (∀ i j : Fin n, a i = a j → i = j)) = 0 := by
    unfold fintypeExpect
    rw [show (∑ a : Fin n → Fin (n ^ 2), indicator (∀ i j : Fin n, a i = a j → i = j)) = 0 by
      apply Finset.sum_eq_zero
      intro a ha
      exact if_neg (hnone a)]
    simp
  have hcf := perfectHash_collision_free_prob_ge_half (n := n) hn
  linarith

Abstract construction budget and its finite expectation

Historical abstract two-level budget: primary size plus twice the sum of squared bucket sizes. This is an analysis expression, not measured execution. The companion Construction module supplies a counted constructor and a constant-factor conditional-expectation bridge to this expression.

noncomputable def constructionCost {n : ℕ} (a : Fin n → Fin n) : ℝ :=
  (n : ℝ) + 2 * totalSecondarySpace a

Expected finite trial-count budget times squared bucket size, for at least two keys. The expression charges a supplied square cost per trial; actual collision checking, initialization, and placement are counted in the companion.


theorem perfectHash_expected_bucket_cost_le {n t : ℕ} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
      (trialsUntilCollisionFree A : ℝ) * (n : ℝ)^2) ≤ 2 * (n : ℝ)^2 := by
  have hsq : 0 ≤ (n : ℝ)^2 := by positivity
  calc
    fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
        (trialsUntilCollisionFree A : ℝ) * (n : ℝ)^2)
        = (n : ℝ)^2 * fintypeExpect (fun A : Fin t → (Fin n → Fin (n^2)) =>
            (trialsUntilCollisionFree A : ℝ)) := by
          have hswap : (fun A : Fin t → (Fin n → Fin (n^2)) =>
              (trialsUntilCollisionFree A : ℝ) * (n : ℝ)^2)
              = (fun A : Fin t → (Fin n → Fin (n^2)) => (n : ℝ)^2 * (trialsUntilCollisionFree A : ℝ)) := by
            funext A
            ring
          rw [hswap]
          exact fintypeExpect_const_mul ((n : ℝ)^2) (fun A : Fin t → (Fin n → Fin (n^2)) =>
            (trialsUntilCollisionFree A : ℝ))
    _ ≤ (n : ℝ)^2 * 2 := by
          exact mul_le_mul_of_nonneg_left (perfectHash_expected_trials_le_two hn) hsq
    _ = 2 * (n : ℝ)^2 := by
          ring

The historical abstract construction budget has expectation below 5n under uniform primary assignment. The theorem name is retained for compatibility; executed construction costs require the companion's refinement theorem.


theorem perfectHash_expected_construction_time_le_const_n {n : ℕ} (hn : 0 < n) :
    fintypeExpect (fun a : Fin n → Fin n => constructionCost a) < 5 * (n : ℝ) := by
  have hlin : fintypeExpect (fun a : Fin n → Fin n => constructionCost a)
      = (n : ℝ) + 2 * fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) := by
    unfold constructionCost
    calc
      fintypeExpect (fun a : Fin n → Fin n => (n : ℝ) + 2 * totalSecondarySpace a)
          = fintypeExpect (fun _ : Fin n → Fin n => (n : ℝ)) +
              fintypeExpect (fun a : Fin n → Fin n => 2 * totalSecondarySpace a) :=
            fintypeExpect_add _ _
      _ = (n : ℝ) + 2 * fintypeExpect (fun a : Fin n → Fin n => totalSecondarySpace a) := by
            haveI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩
            have hcard : Fintype.card (Fin n → Fin n) ≠ 0 := Fintype.card_ne_zero
            rw [fintypeExpect_const hcard, fintypeExpect_const_mul]
  rw [hlin]
  have hspace := perfectHash_expected_total_space_lt_2n hn
  nlinarith

end Chapter11end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction.Secondary

Executed finite secondary perfect-hash construction

Every candidate runs a collision check, initializes its secondary slot array, and places its local key indices. The returned ledger counts hash evaluations, equality comparisons, slot initialization, and indexed writes. Supplied finite traces stop on success; exhaustion executes a deterministic injective fallback. Thus the actual attempts equal the existing failedTrials + 1 statistic.

Hashes act on local indices Fin n. Hash-family sampling and representation costs are outside this indexed-operation model. The finite expectation concerns uniform full assignments, and is not a theorem about an unbounded retry process.

namespace CLRS.Chapter11.PerfectConstruction

Hash equality tests, charged for two hash evaluations and one comparison.

def differsFrom (a : α → β) [DecidableEq β] (x : α) : List α → Bool × Nat
  | [] => (true, 0)
  | y :: ys =>
      if a x = a y then (false, 3)
      else let rest := differsFrom a x ys; (rest.1, rest.2 + 3)

theorem differsFrom_correct (a : α → β) [DecidableEq β] (x : α) (xs : List α) :
    (differsFrom a x xs).1 = true ↔ ∀ y ∈ xs, a x ≠ a y := by
  induction xs with
  | nil => simp [differsFrom]
  | cons y ys ih => by_cases h : a x = a y <;> simp [differsFrom, h, ih]

theorem differsFrom_work_le (a : α → β) [DecidableEq β] (x : α) (xs : List α) :
    (differsFrom a x xs).2 ≤ 3 * xs.length := by
  induction xs with
  | nil => simp [differsFrom]
  | cons y ys ih => simp only [differsFrom]; split <;> simp_all; omega

Check all distinct input positions, stopping at the first duplicate hash.

def checkDistinct (a : α → β) [DecidableEq β] : List α → Bool × Nat
  | [] => (true, 0)
  | x :: xs =>
      let head := differsFrom a x xs
      if head.1 then
        let tail := checkDistinct a xs
        (tail.1, head.2 + tail.2)
      else (false, head.2)

              theorem checkDistinct_correct (a : α → β) [DecidableEq β] (xs : List α) :
    (checkDistinct a xs).1 = true ↔ (xs.map a).Nodup := by
  induction xs with
  | nil => simp [checkDistinct]
  | cons x xs ih =>
      simp only [checkDistinct]
      split
      next h =>
        have hh := (differsFrom_correct a x xs).mp h
        simp only [List.map_cons, List.nodup_cons, List.mem_map]
        constructor
        · intro ht
          exact ⟨by rintro ⟨y, hy, he⟩; exact hh y hy he.symm, ih.mp ht⟩
        · intro ht; exact ih.mpr ht.2
      next h =>
        simp only [Bool.false_eq_true, List.map_cons, List.nodup_cons, false_iff]
        intro hn
        apply h
        apply (differsFrom_correct a x xs).mpr
        intro y hy he
        exact hn.1 (List.mem_map.mpr ⟨y, hy, he.symm⟩)theorem checkDistinct_work_le (a : α → β) [DecidableEq β] (xs : List α) :
    (checkDistinct a xs).2 ≤ 3 * xs.length ^ 2 := by
  induction xs with
  | nil => simp [checkDistinct]
  | cons x xs ih =>
      have hh := differsFrom_work_le a x xs
      simp only [checkDistinct]
      split <;> simp only [List.length_cons] <;> nlinarithabbrev Hash (n : Nat) := Fin n → Fin (n ^ 2)

theorem check_hash_correct {n : Nat} (a : Hash n) :
    (checkDistinct a (List.finRange n)).1 = true ↔ collisionFree a := by
  rw [checkDistinct_correct, List.nodup_map_iff_inj_on (List.nodup_finRange n)]
  simp [collisionFree]

Initialize actual empty secondary slots, counting each array push.

def emptySlots (α : Type*) : Nat → Array (Option α) × Nat
  | 0 => (#[], 0)
  | m + 1 => let prev := emptySlots α m; (prev.1.push none, prev.2 + 1)

@[simp] theorem emptySlots_array (α : Type*) (m : Nat) :
    (emptySlots α m).1 = Array.replicate m none := by
  induction m with
  | zero => simp [emptySlots]
  | succ m ih => simp [emptySlots, ih, Array.replicate_succ]

@[simp] theorem emptySlots_work (α : Type*) (m : Nat) : (emptySlots α m).2 = m := by
  induction m with
  | zero => rfl
  | succ m ih => simp [emptySlots, ih]

Place each key in its selected slot. A step charges a hash evaluation and an indexed write; initialization and collision checks are counted separately.

def place {n : Nat} (a : Hash n) : List (Fin n) → Array (Option (Fin n)) →
    Array (Option (Fin n)) × Nat
  | [], out => (out, 0)
  | i :: is, out =>
      let rest := place a is out
      (rest.1.setIfInBounds (a i).val (some i), rest.2 + 2)

@[simp] theorem place_size {n : Nat} (a : Hash n) (xs : List (Fin n)) (out : Array (Option (Fin n))) :
    (place a xs out).1.size = out.size := by
  induction xs with
  | nil => rfl
  | cons i xs ih => simp [place, ih]

@[simp] theorem place_work {n : Nat} (a : Hash n) (xs : List (Fin n)) (out : Array (Option (Fin n))) :
    (place a xs out).2 = 2 * xs.length := by
  induction xs with
  | nil => simp [place]
  | cons i xs ih => simp [place, ih]; omega

Each slot contains the first input key assigned there, or its initial value.


theorem place_get {n : Nat} (a : Hash n) (xs : List (Fin n))
    (out : Array (Option (Fin n))) (s : Nat) (hs : s < out.size) :
    (place a xs out).1[s]'(by simpa using hs) =
      (xs.find? (fun i => (a i).val == s)).orElse (fun _ => out[s]) := by
  induction xs with
  | nil => simp [place]
  | cons i xs ih =>
      simp only [place]
      rw [Array.getElem_setIfInBounds (by simpa using hs)]
      by_cases he : (a i).val = s <;> simp [he, List.find?, ih, Bool.beq_eq_decide_eq]

structure Attempt (n : Nat) where
  hash : Hash n
  slots : Array (Option (Fin n))
  success : Bool
  work : Nat

An actual collision check followed by secondary-array placement.

def attempt {n : Nat} (a : Hash n) : Attempt n :=
  let checked := checkDistinct a (List.finRange n)
  let initial := emptySlots (Fin n) (n ^ 2)
  let filled := place a (List.finRange n) initial.1
  ⟨a, filled.1, checked.1, checked.2 + initial.2 + filled.2⟩

              @[simp] theorem attempt_hash {n : Nat} (a : Hash n) : (attempt a).hash = a := rfl@[simp] theorem attempt_size {n : Nat} (a : Hash n) : (attempt a).slots.size = n ^ 2 := by
  simp [attempt]@[simp] theorem attempt_success {n : Nat} (a : Hash n) :
    (attempt a).success = true ↔ collisionFree a := check_hash_correct a

theorem attempt_work_le {n : Nat} (a : Hash n) : (attempt a).work ≤ 6 * n ^ 2 := by
  have h := checkDistinct_work_le a (List.finRange n)
  have hn : n ≤ n ^ 2 := by nlinarith
  simpa only [attempt, emptySlots_work, place_work, List.length_finRange] using
    (show (checkDistinct a (List.finRange n)).2 + n ^ 2 + 2 * n ≤ 6 * n ^ 2 by
      simp only [List.length_finRange] at h
      nlinarith)

theorem attempt_get {n : Nat} (a : Hash n) (s : Nat) (hs : s < n ^ 2) :
    (attempt a).slots[s]'(by simpa using hs) =
      (List.finRange n).find? (fun i => (a i).val == s) := by
  have h := place_get a (List.finRange n) (emptySlots (Fin n) (n ^ 2)).1 s (by simpa using hs)
  simpa [attempt] using h

theorem attempt_stores {n : Nat} (a : Hash n) (ha : collisionFree a) (i : Fin n) :
    (attempt a).slots[(a i).val]'(by simp) = some i := by
  rw [attempt_get a _ (a i).isLt]
  cases h : (List.finRange n).find? (fun j => (a j).val == (a i).val) with
  | none =>
      have hh := List.find?_eq_none.mp h i (by simp)
      simp at hh
  | some j =>
      have hh := List.find?_some h
      have he : a j = a i := Fin.ext (by simpa using hh)
      rw [ha j i he]

The terminal assignment is explicitly injective, including the empty domain.

def fallback (n : Nat) : Hash n := fun i =>
  ⟨i.val, lt_of_lt_of_le i.isLt (by nlinarith : n ≤ n ^ 2)⟩

theorem fallback_injective (n : Nat) : collisionFree (fallback n) := by
  intro i j hij
  exact Fin.ext (congrArg (fun x : Fin (n ^ 2) => x.val) hij)

structure Build (n : Nat) where
  selected : Attempt n
  attempts : Nat
  work : Nat

Try supplied candidates in order; after their exhaustion execute one explicit injective fallback. Every returned table therefore succeeds.

def build {n : Nat} : List (Hash n) → Build n
  | [] => let final := attempt (fallback n); ⟨final, 1, final.work⟩
  | a :: as =>
      let trial := attempt a
      if trial.success then ⟨trial, 1, trial.work⟩
      else let rest := build as; ⟨rest.selected, rest.attempts + 1, trial.work + rest.work⟩

              theorem build_success {n : Nat} (as : List (Hash n)) : (build as).selected.success = true := by
  induction as with
  | nil => simpa [build] using (attempt_success (fallback n)).mpr (fallback_injective n)
  | cons a as ih =>
      simp only [build]
      split
      · assumption
      · exact ihtheorem build_work_le {n : Nat} (as : List (Hash n)) :
    (build as).work ≤ 6 * n ^ 2 * (build as).attempts := by
  induction as with
  | nil => simpa [build] using attempt_work_le (fallback n)
  | cons a as ih =>
      have h := attempt_work_le a
      simp only [build]
      split <;> simp only <;> nlinarithdef failedPrefix {n : Nat} : List (Hash n) → Nat
  | [] => 0
  | a :: as => if (attempt a).success then 0 else failedPrefix as + 1theorem build_attempts {n : Nat} (as : List (Hash n)) :
    (build as).attempts = failedPrefix as + 1 := by
  induction as with
  | nil => simp [build, failedPrefix]
  | cons a as ih => simp only [build, failedPrefix]; split <;> simp_all


lemma failedTrials_cons {n t : Nat} (A : Fin (t + 1) → Hash n) :
    failedTrials A = if collisionFree (A 0) then 0 else
      failedTrials (fun j : Fin t => A j.succ) + 1 := by
  classical
  rw [failedTrials_eq_sum, Fin.sum_univ_succ]
  have htail (k : Fin t) :
      (∀ j : Fin (k.succ.val + 1),
        ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.succ.isLt) j))) ↔
      (¬ collisionFree (A 0) ∧ ∀ j : Fin (k.val + 1),
        ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt k.isLt) j).succ)) := by
    rw [Fin.forall_fin_succ]
    rfl
  have hzero :
      (∀ j : Fin ((0 : Fin (t + 1)).val + 1),
        ¬ collisionFree (A (Fin.castLE (Nat.succ_le_of_lt (0 : Fin (t + 1)).isLt) j))) ↔
      ¬ collisionFree (A 0) := by
    constructor
    · intro hh
      exact hh 0
    · intro hh j
      have hj : Fin.castLE (Nat.succ_le_of_lt (0 : Fin (t + 1)).isLt) j = 0 := by
        apply Fin.ext
        have h := j.isLt
        change j.val < 1 at h
        change j.val = 0
        omega
      rw [hj]
      exact hh
  simp_rw [htail, hzero]
  by_cases h : collisionFree (A 0)
  · have hh : collisionFree (A 0) ↔ True := iff_true_intro h
    simp only [hh, not_true_eq_false, false_and, ite_false, Finset.sum_const_zero,
      zero_add, ite_true]
  · simp only [h, not_false_eq_true, true_and, ite_true, ite_false]
    rw [failedTrials_eq_sum]
    omega

theorem failedPrefix_ofFn {n t : Nat} (A : Fin t → Hash n) :
    failedPrefix (List.ofFn A) = failedTrials A := by
  classical
  induction t with
  | zero => simp [List.ofFn_zero, failedPrefix, failedTrials]
  | succ t ih =>
      rw [List.ofFn_succ, failedPrefix, failedTrials_cons]
      simp only [attempt_success, ih]def buildTrace {n : Nat} : {t : Nat} → (Fin t → Hash n) → Build n
  | 0, _ => build []
  | _ + 1, A =>
      let current := attempt (A 0)
      if current.success then ⟨current, 1, current.work⟩
      else
        let rest := buildTrace (fun j => A j.succ)
        ⟨rest.selected, rest.attempts + 1, current.work + rest.work⟩theorem buildTrace_eq {n t : Nat} (A : Fin t → Hash n) :
    buildTrace A = build (List.ofFn A) := by
  induction t with
  | zero => simp [buildTrace]
  | succ t ih => simp [buildTrace, List.ofFn_succ, build, ih]

The legacy finite trial random variable is the exact attempt count of finite sampling followed by the terminal injective fallback.


theorem buildTrace_attempts {n t : Nat} (A : Fin t → Hash n) :
    (buildTrace A).attempts = trialsUntilCollisionFree A := by
  rw [buildTrace_eq, build_attempts, failedPrefix_ofFn, trialsUntilCollisionFree]

theorem buildTrace_work_le {n t : Nat} (A : Fin t → Hash n) :
    (buildTrace A).work ≤ 6 * n ^ 2 * trialsUntilCollisionFree A := by
  simpa [← buildTrace_attempts A, buildTrace_eq] using build_work_le (List.ofFn A)

open CLRS.Probability

Expected measured secondary work over the stated finite SUHA trace space.

theorem expected_buildTrace_work_le {n t : Nat} (hn : 2 ≤ n) :
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
      12 * (n : ℝ) ^ 2 := by
  classical
  calc
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
        fintypeExpect (fun A : Fin t → Hash n =>
          6 * (n : ℝ) ^ 2 * (trialsUntilCollisionFree A : ℝ)) := by
      apply fintypeExpect_mono
      intro A
      exact_mod_cast buildTrace_work_le A
    _ = (6 * (n : ℝ) ^ 2) *
        fintypeExpect (fun A : Fin t → Hash n => (trialsUntilCollisionFree A : ℝ)) :=
      fintypeExpect_const_mul _ _
    _ ≤ (6 * (n : ℝ) ^ 2) * 2 :=
      mul_le_mul_of_nonneg_left (perfectHash_expected_trials_le_two hn) (by positivity)
    _ = _ := by ring

Every selected result is a real executed secondary attempt.

theorem build_selected_eq {n : Nat} (as : List (Hash n)) :
    (build as).selected = attempt (build as).selected.hash := by
  induction as with
  | nil => rfl
  | cons a as ih => simp only [build]; split <;> first | rfl | exact ih



theorem build_hash_injective {n : Nat} (as : List (Hash n)) :
    collisionFree (build as).selected.hash := by
  have h := build_success as
  rw [build_selected_eq] at h
  exact attempt_success _ |>.mp h



theorem attempt_only {n : Nat} (a : Hash n) (s : Nat) (i : Fin n)
    (h : (attempt a).slots[s]?.join = some i) : (a i).val = s := by
  by_cases hs : s < n ^ 2
  · have hsize : s < (attempt a).slots.size := by simpa using hs
    rw [Array.getElem?_eq_getElem hsize, Option.join_some, attempt_get a s hs] at h
    have hh := List.find?_some h
    simpa using hh
  · have hsize : ¬ s < (attempt a).slots.size := by simpa using hs
    simp [Array.getElem?_eq_none (Nat.le_of_not_gt hsize)] at h

Package the constructed array as a one-bucket perfect table. All key slots come from the returned placement execution, rather than from a specification search.


def tableOfBuild {n : Nat} (as : List (Hash n)) : PerfectHashTable (Fin n) 1 where
  keys := Finset.univ
  prim := fun _ => 0
  sec := fun _ i => ((build as).selected.hash i).val
  table := fun _ s => (build as).selected.slots[s]?.join
  sec_inj := by
    intro j x y hx hy hpx hpy hs
    exact build_hash_injective as x y (Fin.ext hs)
  table_stores_keys := by
    intro i hi
    rw [build_selected_eq]
    have hs := attempt_stores (build as).selected.hash (build_hash_injective as) i
    simp only [attempt_hash]
    rw [Array.getElem?_eq_getElem (by simp), Option.join_some]
    exact hs
  table_only_keys := by
    intro j s i hi
    refine ⟨by simp, Subsingleton.elim _ _, ?_⟩
    rw [build_selected_eq] at hi
    exact attempt_only _ s i hi

The successful finite builder has a verified membership-query interface.


theorem tableOfBuild_search {n : Nat} (as : List (Hash n)) (i : Fin n) :
    perfectSearch (tableOfBuild as) i := by
  rw [perfectSearch_iff_mem]
  simp [tableOfBuild]




theorem build_work_le_small {n : Nat} (hn : n ≤ 1) (as : List (Hash n)) :
    (build as).work ≤ 6 * n ^ 2 := by
  cases as with
  | nil => simpa [build] using attempt_work_le (fallback n)
  | cons a as =>
      have hc : collisionFree a := by
        intro i j hij
        apply Fin.ext
        have hi := i.isLt
        have hj := j.isLt
        omega
      have hs := (attempt_success a).mpr hc
      simpa only [build, hs, Bool.true_eq, ↓reduceIte] using attempt_work_le a

Empty and singleton buckets are handled directly; the SUHA retry bound is needed only for buckets with at least two keys.


theorem expected_buildTrace_work_le_all (n t : Nat) :
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
      12 * (n : ℝ) ^ 2 := by
  classical
  by_cases hn : 2 ≤ n
  · exact expected_buildTrace_work_le hn
  haveI : Nonempty (Fin t → Hash n) := ⟨fun _ => fallback n⟩
  calc
    fintypeExpect (fun A : Fin t → Hash n => ((buildTrace A).work : ℝ)) ≤
        fintypeExpect (fun _ : Fin t → Hash n => 6 * (n : ℝ) ^ 2) := by
      apply fintypeExpect_mono
      intro A
      rw [buildTrace_eq]
      exact_mod_cast build_work_le_small (by omega : n ≤ 1) (List.ofFn A)
    _ = 6 * (n : ℝ) ^ 2 := fintypeExpect_const Fintype.card_ne_zero _
    _ ≤ _ := by nlinarith [sq_nonneg (n : ℝ)]

end CLRS.Chapter11.PerfectConstruction

CLRSLean.FourthEdition.Chapter_11.Section_11_5_Perfect_Hashing.Construction.TwoLevel

Measured assembly of all secondary tables

The constructor actually distributes original Fin n payloads into primary buckets, caches bucket sizes, and executes and retains every secondary builder. The measured indexed-operation work has conditional expectation at most nine times constructionCost and unconditional expectation below 45 * n.

Secondary tables hash and store local bucket indices. Original payload buckets remain in the result; converting an original query key to its local index is a separate representation boundary. This does not claim constant-time hashing on an arbitrary original key universe or machine runtime for persistent arrays.

namespace CLRS.Chapter11.PerfectConstructionopen CLRS.Probability

Uniform dependent-product sampling has the expected one-coordinate marginal.

theorem expect_pi_apply {ι : Type} [Fintype ι] [DecidableEq ι]
    (Ω : ι → Type) [∀ i, Fintype (Ω i)] [∀ i, DecidableEq (Ω i)]
    [∀ i, Nonempty (Ω i)] (j : ι) (X : Ω j → ℝ) :
    fintypeExpect (fun w : (i : ι) → Ω i => X (w j)) = fintypeExpect X := by
  classical
  calc
    fintypeExpect (fun w : (i : ι) → Ω i => X (w j)) =
        fintypeExpect (fun p : Ω j × ((i : {i : ι // i ≠ j}) → Ω i.val) => X p.1) :=
      fintypeExpect_equiv (Equiv.piSplitAt j Ω) (fun p => X p.1)
    _ = _ := fintypeExpect_fst Fintype.card_ne_zero X

structure Assembly {m : Nat} (sizes : Fin m → Nat) where
  buckets : Array (Σ j : Fin m, Build (sizes j))
  work : Nat

Execute every bucket constructor, storing its returned table in the output array. Each push of a completed bucket record contributes one more operation.

def assemble {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j)) :
    List (Fin m) → Array (Σ j : Fin m, Build (sizes j)) → Assembly sizes
  | [], out => ⟨out, 0⟩
  | j :: js, out =>
      let built := buildTrace (A j)
      let rest := assemble sizes A js (out.push ⟨j, built⟩)
      ⟨rest.buckets, built.work + 1 + rest.work⟩

              theorem assemble_result {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j))
    (js : List (Fin m)) (out : Array (Σ j : Fin m, Build (sizes j))) :
    (assemble sizes A js out).buckets.toList =
      out.toList ++ js.map (fun j => ⟨j, buildTrace (A j)⟩) := by
  induction js generalizing out with
  | nil => simp [assemble]
  | cons j js ih => simp [assemble, ih, List.append_assoc]theorem assemble_work {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j))
    (js : List (Fin m)) (out : Array (Σ j : Fin m, Build (sizes j))) :
    (assemble sizes A js out).work = js.length + (js.map (fun j => (buildTrace (A j)).work)).sum := by
  induction js generalizing out with
  | nil => simp [assemble]
  | cons j js ih => simp [assemble, ih]; omega

theorem assemble_success {m t : Nat} (sizes : Fin m → Nat)
    (A : (j : Fin m) → Fin t → Hash (sizes j)) :
    ∀ entry ∈ (assemble sizes A (List.finRange m) #[]).buckets.toList,
      entry.2.selected.success = true := by
  rw [assemble_result]
  simp only [List.nil_append, List.mem_map]
  rintro entry ⟨j, hj, rfl⟩
  simpa only [buildTrace_eq] using build_success _

Expected work of the actual assembly over independent finite per-bucket trace spaces; no assumption on empty/singleton bucket sizes is needed.


theorem expected_assemble_work_le {m : Nat} (sizes : Fin m → Nat) (t : Nat) :
    fintypeExpect (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
      ((assemble sizes A (List.finRange m) #[]).work : ℝ)) ≤
      (m : ℝ) + 12 * ∑ j : Fin m, (sizes j : ℝ) ^ 2 := by
  classical
  haveI (j : Fin m) : Nonempty (Fin t → Hash (sizes j)) := ⟨fun _ => fallback (sizes j)⟩
  have hex : (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
      ((assemble sizes A (List.finRange m) #[]).work : ℝ)) =
      (fun A => (m : ℝ) + ∑ j : Fin m, ((buildTrace (A j)).work : ℝ)) := by
    funext A
    rw [assemble_work]
    simp [← List.ofFn_id, List.map_ofFn, List.sum_ofFn]
  rw [hex, fintypeExpect_add, fintypeExpect_const Fintype.card_ne_zero,
    fintypeExpect_sum]
  have hmarginal (j : Fin m) :
      fintypeExpect (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
        ((buildTrace (A j)).work : ℝ)) ≤ 12 * (sizes j : ℝ) ^ 2 := by
    rw [expect_pi_apply (fun j : Fin m => Fin t → Hash (sizes j)) j
      (fun B : Fin t → Hash (sizes j) => ((buildTrace B).work : ℝ))]
    exact expected_buildTrace_work_le_all (sizes j) t
  calc
    (m : ℝ) + ∑ j : Fin m,
        fintypeExpect (fun A : (j : Fin m) → Fin t → Hash (sizes j) =>
          ((buildTrace (A j)).work : ℝ)) ≤
        (m : ℝ) + ∑ j : Fin m, 12 * (sizes j : ℝ) ^ 2 := by
      gcongr with j
      exact hmarginal j
    _ = _ := by rw [Finset.mul_sum]

Count a bucket's length by traversing its elements once.

def measureLength : List α → Nat × Nat
  | [] => (0, 0)
  | _ :: xs => let rest := measureLength xs; (rest.1 + 1, rest.2 + 1)

@[simp] theorem measureLength_result (xs : List α) : (measureLength xs).1 = xs.length := by
  induction xs <;> simp_all [measureLength]

@[simp] theorem measureLength_work (xs : List α) : (measureLength xs).2 = xs.length := by
  induction xs <;> simp_all [measureLength]

Cache bucket cardinalities once, counting both visits and cache writes.

def measureBuckets : List (List α) → Array Nat → Array Nat × Nat
  | [], out => (out, 0)
  | b :: bs, out =>
      let measured := measureLength b
      let rest := measureBuckets bs (out.push measured.1)
      (rest.1, measured.2 + 1 + rest.2)

              theorem measureBuckets_result (bs : List (List α)) (out : Array Nat) :
    (measureBuckets bs out).1.toList = out.toList ++ bs.map List.length := by
  induction bs generalizing out with
  | nil => simp [measureBuckets]
  | cons b bs ih => simp [measureBuckets, ih, List.append_assoc]theorem measureBuckets_work (bs : List (List α)) (out : Array Nat) :
    (measureBuckets bs out).2 = bs.length + bs.flatten.length := by
  induction bs generalizing out with
  | nil => simp [measureBuckets]
  | cons b bs ih => simp [measureBuckets, ih]; omegastructure Primary (n : Nat) where
  buckets : Array (List (Fin n))
  sizes : Array Nat
  work : Nat

One primary distribution and one bucket-cardinality traversal. Subsequent secondary attempts read cached sizes instead of recomputing the partition.

def preparePrimary {n : Nat} (a : Fin n → Fin n) : Primary n :=
  let initial := Chapter08.CountingExecution.initializeBuckets (α := Fin n) n
  let distributed := Chapter08.CountingExecution.distribute
    (fun i => (a i).val) (List.finRange n) initial.1
  let measured := measureBuckets distributed.buckets.toList #[]
  ⟨distributed.buckets, measured.1,
    initial.2 + 2 * distributed.inputs + 3 * distributed.updates + measured.2⟩

              @[simp] theorem preparePrimary_bucket_size {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).buckets.size = n := by
  simp [preparePrimary]theorem preparePrimary_buckets {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).buckets.toList =
      (List.range n).map (Chapter08.bucket (fun i => (a i).val) (List.finRange n)) := by
  simp [preparePrimary, Chapter08.CountingExecution.distribute_toList]theorem preparePrimary_sizes {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).sizes.toList =
      (preparePrimary a).buckets.toList.map List.length := by
  simp [preparePrimary, measureBuckets_result]

@[simp] theorem preparePrimary_sizes_size {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).sizes.size = n := by
  rw [← Array.length_toList, preparePrimary_sizes]
  simp

theorem preparePrimary_total_length {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).buckets.toList.flatten.length = n := by
  rw [preparePrimary_buckets]
  cases n with
  | zero => simp
  | succ n =>
      change (Chapter08.countingSortBy n (fun i => (a i).val) (List.finRange (n + 1))).length = n + 1
      have hp := Chapter08.countingSortBy_perm n (fun i => (a i).val) (List.finRange (n + 1))
        (by intro i hi; change (a i).val ≤ n; have h := (a i).isLt; omega)
      simpa using hp.length_eq

theorem preparePrimary_work {n : Nat} (a : Fin n → Fin n) :
    (preparePrimary a).work = 8 * n := by
  have hu : (Chapter08.CountingExecution.distribute
      (fun i : Fin n => (a i).val) (List.finRange n) (Array.replicate n [])).updates = n := by
    simpa using Chapter08.CountingExecution.distribute_updates_eq
      (fun i : Fin n => (a i).val) (List.finRange n) (Array.replicate n [])
      (by intro i hi; simp)
  have hl := preparePrimary_total_length a
  unfold preparePrimary at hl ⊢
  simp only [Chapter08.CountingExecution.initializeBuckets_visits,
    Chapter08.CountingExecution.distribute_inputs, hu, List.length_finRange,
    measureBuckets_work, Array.length_toList, Chapter08.CountingExecution.distribute_size,
    Chapter08.CountingExecution.initializeBuckets_array, Array.size_replicate] at hl ⊢
  rw [hl]
  omega

A stored cached cardinality, not a repeated list-length computation.

def bucketCard {n : Nat} (a : Fin n → Fin n) (j : Fin n) : Nat :=
  (preparePrimary a).sizes[j.val]'(by simp)

              theorem bucketCard_eq {n : Nat} (a : Fin n → Fin n) (j : Fin n) :
    bucketCard a j = (Chapter08.bucket (fun i => (a i).val) (List.finRange n) j.val).length := by
  unfold bucketCard
  simp only [← Array.getElem_toList, preparePrimary_sizes, preparePrimary_buckets,
    List.getElem_map, List.getElem_range]

theorem bucketCard_cast {n : Nat} (a : Fin n → Fin n) (j : Fin n) :
    (bucketCard a j : ℝ) = bucketSize a j := by
  rw [bucketCard_eq, Chapter08.bucket_length_eq_card]
  exact (Chapter08.bucketOccupancy_eq_card a j).symm

theorem bucketCard_sq_sum {n : Nat} (a : Fin n → Fin n) :
    (∑ j : Fin n, (bucketCard a j : ℝ) ^ 2) = totalSecondarySpace a := by
  unfold totalSecondarySpace
  exact Finset.sum_congr rfl (fun j _ => by rw [bucketCard_cast])structure TwoLevel {n : Nat} (a : Fin n → Fin n) where
  primary : Primary n
  secondary : Assembly (bucketCard a)
  work : Nat

Construct every actual secondary array from finite supplied trial traces, retaining the primary payload buckets and all completed secondary arrays.

def buildTwoLevel {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) : TwoLevel a :=
  let primary := preparePrimary a
  let secondary := assemble (fun j => primary.sizes[j.val]'(by simp [primary])) A (List.finRange n) #[]
  ⟨primary, secondary, primary.work + secondary.work⟩

All secondary tables returned by the complete constructor succeeded.

theorem buildTwoLevel_success {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) :
    ∀ entry ∈ (buildTwoLevel a A).secondary.buckets.toList,
      entry.2.selected.success = true :=
  assemble_success (bucketCard a) A

Conditional expected measured work is bounded by the pre-existing analytic budget up to an explicit operation-count constant.


theorem expected_buildTwoLevel_work_le_budget {n : Nat} (a : Fin n → Fin n) (t : Nat) :
    fintypeExpect (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
      ((buildTwoLevel a A).work : ℝ)) ≤ 9 * constructionCost a := by
  classical
  haveI (j : Fin n) : Nonempty (Fin t → Hash (bucketCard a j)) :=
    ⟨fun _ => fallback (bucketCard a j)⟩
  have he := expected_assemble_work_le (bucketCard a) t
  rw [bucketCard_sq_sum] at he
  have hex : (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
      ((buildTwoLevel a A).work : ℝ)) =
      (fun A => (8 * n : ℝ) + ((assemble (bucketCard a) A (List.finRange n) #[]).work : ℝ)) := by
    funext A
    change (((preparePrimary a).work + (assemble (bucketCard a) A (List.finRange n) #[]).work : Nat) : ℝ) = _
    rw [preparePrimary_work]
    push_cast
    rfl
  rw [hex, fintypeExpect_add, fintypeExpect_const Fintype.card_ne_zero]
  have hs : 0 ≤ totalSecondarySpace a := by
    unfold totalSecondarySpace
    exact Finset.sum_nonneg (fun j _ => sq_nonneg _)
  unfold constructionCost
  nlinarith

Average actual finite-with-fallback construction work is linear under the primary SUHA assignment and the conditional independent secondary trace spaces.

theorem expected_buildTwoLevel_work_lt {n : Nat} (hn : 0 < n) (t : Nat) :
    fintypeExpect (fun a : Fin n → Fin n =>
      fintypeExpect (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
        ((buildTwoLevel a A).work : ℝ))) < 45 * (n : ℝ) := by
  classical
  calc
    fintypeExpect (fun a : Fin n → Fin n =>
        fintypeExpect (fun A : (j : Fin n) → Fin t → Hash (bucketCard a j) =>
          ((buildTwoLevel a A).work : ℝ))) ≤
        fintypeExpect (fun a : Fin n → Fin n => 9 * constructionCost a) := by
      apply fintypeExpect_mono
      intro a
      exact expected_buildTwoLevel_work_le_budget a t
    _ = 9 * fintypeExpect (fun a : Fin n → Fin n => constructionCost a) :=
      fintypeExpect_const_mul 9 _
    _ < 9 * (5 * (n : ℝ)) :=
      mul_lt_mul_of_pos_left (perfectHash_expected_construction_time_le_const_n hn) (by norm_num)
    _ = _ := by ring

Each returned secondary array stores every local key index at the slot selected by the hash returned by that same execution.


theorem buildTwoLevel_stores {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) :
    ∀ entry ∈ (buildTwoLevel a A).secondary.buckets.toList,
      ∀ i : Fin (bucketCard a entry.1),
        entry.2.selected.slots[(entry.2.selected.hash i).val]?.join = some i := by
  change ∀ entry ∈ (assemble (bucketCard a) A (List.finRange n) #[]).buckets.toList, _
  rw [assemble_result]
  simp only [List.nil_append, List.mem_map]
  rintro entry ⟨j, hj, rfl⟩ i
  simp only [buildTrace_eq]
  change (build (List.ofFn (A j))).selected.slots[
    ((build (List.ofFn (A j))).selected.hash i).val]?.join = some i
  rw [build_selected_eq]
  simp only [attempt_hash]
  rw [Array.getElem?_eq_getElem (by simp), Option.join_some]
  exact attempt_stores _ (build_hash_injective (List.ofFn (A j))) i




theorem preparePrimary_bucket_length {n : Nat} (a : Fin n → Fin n) (j : Fin n) :
    ((preparePrimary a).buckets[j.val]'(by simp)).length = bucketCard a j := by
  rw [bucketCard_eq]
  simp only [← Array.getElem_toList, preparePrimary_buckets,
    List.getElem_map, List.getElem_range]

Resolve a supplied local index through its selected secondary slot to the original payload. Supplying the local index is an explicit interface requirement.

def recoverPayload {n : Nat} {a : Fin n → Fin n} (built : TwoLevel a)
    (entry : Σ j : Fin n, Build (bucketCard a j)) (i : Fin (bucketCard a entry.1)) :
    Option (Fin n) := do
  let localIndex ← entry.2.selected.slots[(entry.2.selected.hash i).val]?.join
  let payloads ← built.primary.buckets[entry.1.val]?
  payloads[localIndex.val]?



theorem buildTwoLevel_recovers {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j))
    (entry : Σ j : Fin n, Build (bucketCard a j))
    (he : entry ∈ (buildTwoLevel a A).secondary.buckets.toList)
    (i : Fin (bucketCard a entry.1)) :
    recoverPayload (buildTwoLevel a A) entry i =
      some (((preparePrimary a).buckets[entry.1.val]'(by simp))[i.val]'(by
        rw [preparePrimary_bucket_length]; exact i.isLt)) := by
  unfold recoverPayload
  rw [buildTwoLevel_stores a A entry he i]
  change ((preparePrimary a).buckets[entry.1.val]?.bind fun xs => xs[i.val]?) = _
  rw [Array.getElem?_eq_getElem (by simp), Option.bind_some,
    List.getElem?_eq_getElem (by rw [preparePrimary_bucket_length]; exact i.isLt)]




theorem preparePrimary_covers {n : Nat} (a : Fin n → Fin n) (x : Fin n) :
    ∃ i : Fin (bucketCard a (a x)),
      ((preparePrimary a).buckets[(a x).val]'(by simp))[i.val]'(by
        rw [preparePrimary_bucket_length]; exact i.isLt) = x := by
  have hm : x ∈ (preparePrimary a).buckets[(a x).val]'(by simp) := by
    simp only [← Array.getElem_toList, preparePrimary_buckets,
      List.getElem_map, List.getElem_range]
    simp [CLRS.Chapter08.bucket]
  obtain ⟨i, hi, hx⟩ := List.getElem_of_mem hm
  exact ⟨⟨i, by rwa [preparePrimary_bucket_length] at hi⟩, hx⟩

Every original stored payload can be recovered through its actual returned secondary table, given its local index. This does not construct an inverse map from arbitrary original query keys to local indices.


theorem buildTwoLevel_recovers_original {n t : Nat} (a : Fin n → Fin n)
    (A : (j : Fin n) → Fin t → Hash (bucketCard a j)) (x : Fin n) :
    ∃ i : Fin (bucketCard a (a x)),
      recoverPayload (buildTwoLevel a A) ⟨a x, buildTrace (A (a x))⟩ i = some x := by
  obtain ⟨i, hi⟩ := preparePrimary_covers a x
  refine ⟨i, ?_⟩
  rw [buildTwoLevel_recovers, hi]
  change (⟨a x, buildTrace (A (a x))⟩ : Σ j : Fin n, Build (bucketCard a j)) ∈
    (assemble (bucketCard a) A (List.finRange n) #[]).buckets.toList
  rw [assemble_result]
  simp only [List.nil_append, List.mem_map]
  exact ⟨a x, List.mem_finRange _, rfl⟩

end CLRS.Chapter11.PerfectConstruction