Fisher–Yates shuffle

DefinitionFisher–Yates shuffle with supplied draws#✓fully proved

Given a vector \(x = (x_0, \dots, x_{n-1})\) and a draw history \(d\), which assigns to each position \(i < n\) a number \(d_i\) with \(0 \le d_i < n - i\), the Fisher–Yates computation processes the positions \(i = 0, 1, \dots, n - 1\) in increasing order and at position \(i\) swaps the entries at positions \(i\) and \(i + d_i\) of the current vector. It returns the final vector together with a cost pair in \(\mathbb{N} \times \mathbb{N}\): each retrieved draw adds \((1, 0)\) and each swap adds \((0, 1)\).

public def randomlyPermute {α : Type u} {n : Nat} (xs : Vector α n)
    (draws : (i : Fin n) → Fin (n - i.val)) :
    Cslib.Algorithms.Lean.TimeM (Nat × Nat) (Vector α n) :=
  scan draws 0 xs

Used by 8

Used byOutput distribution of the Fisher–Yates shuffle · Probability of a Fisher–Yates outcome · Fisher–Yates produces a uniformly random permutation · Fisher–Yates on the empty vector · Fisher–Yates output is a rearrangement of its input · Prefix probabilities of the Fisher–Yates shuffle · Fisher–Yates on a one-element vector · Cost of the Fisher–Yates shuffle

TheoremCost of the Fisher–Yates shuffle#✓fully proved

For every vector \(x\) of length \(n\) and every draw history \(d\), which assigns to each position \(i < n\) a number \(d_i\) with \(0 \le d_i < n - i\), the Fisher–Yates computation on \(x\) and \(d\) has cost pair \((n, n)\): it retrieves exactly \(n\) draws and performs exactly \(n\) swaps.

When \(n \ge 1\), this count includes the final draw \(d_{n-1} = 0\) and the self-swap at position \(n - 1\).

public theorem randomlyPermute_time {α : Type u} {n : Nat} (xs : Vector α n)
    (draws : (i : Fin n) → Fin (n - i.val)) :
    (randomlyPermute xs draws).time = (n, n)

Uses 1 · Used by 3

Statement usesFisher–Yates shuffle with supplied draws

Used byFisher–Yates produces a uniformly random permutation · Prefix probabilities of the Fisher–Yates shuffle · Fisher–Yates on a one-element vector

TheoremFisher–Yates output is a rearrangement of its input#✓fully proved

For every vector \(x\) of length \(n\) and every draw history \(d\), which assigns to each position \(i < n\) a number \(d_i\) with \(0 \le d_i < n - i\), the list of entries of the vector returned by the Fisher–Yates computation on \(x\) and \(d\) is a permutation of the list of entries of \(x\). In particular every value occurs equally often in both, even when values of \(x\) repeat.

public theorem randomlyPermute_perm {α : Type u} {n : Nat} (xs : Vector α n)
    (draws : (i : Fin n) → Fin (n - i.val)) :
    (randomlyPermute xs draws).ret.toList.Perm xs.toList

Uses 1

Statement usesFisher–Yates shuffle with supplied draws

TheoremFisher–Yates on the empty vector#✓fully proved

For the empty vector \(x\) (of length \(0\)) and its empty draw history, the Fisher–Yates computation returns \(x\) with cost pair \((0, 0)\): it retrieves no draws and performs no swaps.

public theorem randomlyPermute_empty {α : Type u} (xs : Vector α 0)
    (draws : (i : Fin 0) → Fin (0 - i.val)) :
    randomlyPermute xs draws = ⟨xs, (0, 0)⟩

Uses 1

Statement usesFisher–Yates shuffle with supplied draws

TheoremFisher–Yates on a one-element vector#✓fully proved

For every vector \(x\) of length \(1\) and every draw history \(d\), the Fisher–Yates computation returns \(x\) unchanged with cost pair \((1, 1)\): it still retrieves the single draw \(d_0 = 0\) and performs the self-swap at position \(0\).

public theorem randomlyPermute_singleton {α : Type u} (xs : Vector α 1)
    (draws : (i : Fin 1) → Fin (1 - i.val)) :
    randomlyPermute xs draws = ⟨xs, (1, 1)⟩

Uses 2

Statement usesFisher–Yates shuffle with supplied draws

Proof usesCost of the Fisher–Yates shuffle

DefinitionOutput distribution of the Fisher–Yates shuffle#✓fully proved

For a vector \(x\) of length \(n\), this is the probability distribution on outcomes (a vector of length \(n\) together with a cost pair in \(\mathbb{N} \times \mathbb{N}\)) obtained by choosing a draw history \(d\) uniformly at random among all assignments of a number \(d_i\) with \(0 \le d_i < n - i\) to each position \(i < n\), and returning the result of the Fisher–Yates computation on \(x\) and \(d\).

This models an ideal source of random draws, not an executable pseudorandom generator, and does not assume that the output permutation is uniform.

public def randomlyPermuteDistribution {α : Type u} {n : Nat}
    (xs : Vector α n) : PMF (Cslib.Algorithms.Lean.TimeM (Nat × Nat) (Vector α n)) := by
  letI : Nonempty ((i : Fin n) → Fin (n - i.val)) := ⟨fun i => ⟨0, by omega⟩⟩
  exact (Cslib.Probability.PMF.uniformOfFintype ((i : Fin n) → Fin (n - i.val))).map
    (randomlyPermute xs)

Uses 1 · Used by 2

Statement usesFisher–Yates shuffle with supplied draws

Used byProbability of a Fisher–Yates outcome · Fisher–Yates produces a uniformly random permutation

TheoremProbability of a Fisher–Yates outcome#✓fully proved

Let \(x\) be a vector of length \(n\), and consider the draw histories \(d\), which assign to each position \(i < n\) a number \(d_i\) with \(0 \le d_i < n - i\). For every outcome \(o\) (a vector of length \(n\) together with a cost pair), the probability that the Fisher–Yates output distribution of \(x\) assigns to \(o\) equals the sum, over all draw histories \(d\) for which the Fisher–Yates computation on \(x\) and \(d\) yields exactly \(o\), of \(\prod_{i=0}^{n-1} \frac{1}{n - i}\).

Distinct histories that yield the same outcome (for example when values of \(x\) repeat) add up, and an outcome that no history yields has probability \(0\).

public theorem randomlyPermuteDistribution_apply {α : Type u} {n : Nat} (xs : Vector α n)
    (out : Cslib.Algorithms.Lean.TimeM (Nat × Nat) (Vector α n)) :
    randomlyPermuteDistribution xs out =
      ∑ draws : (i : Fin n) → Fin (n - i.val),
        if out = randomlyPermute xs draws
        then ∏ i : Fin n, ((n - i.val : Nat) : ENNReal)⁻¹ else 0

Uses 2

Statement usesFisher–Yates shuffle with supplied draws · Output distribution of the Fisher–Yates shuffle

TheoremFisher–Yates produces a uniformly random permutation#✓fully proved

Let \(x = (x_0, \dots, x_{n-1})\) be a vector and let \(\sigma\) be a permutation of \(\{0, \dots, n - 1\}\) chosen uniformly at random. Then the Fisher–Yates output distribution of \(x\) equals the distribution of the outcome consisting of the vector \((x_{\sigma(0)}, \dots, x_{\sigma(n-1)})\) with cost pair \((n, n)\).

public theorem randomlyPermuteDistribution_eq_map_uniform {α : Type u} {n : Nat}
    (xs : Vector α n) :
    randomlyPermuteDistribution xs =
      (Cslib.Probability.PMF.uniformOfFintype (Equiv.Perm (Fin n))).map
        (fun σ => (⟨Vector.ofFn (fun p => xs[(σ p).val]), (n, n)⟩ :
          Cslib.Algorithms.Lean.TimeM (Nat × Nat) (Vector α n)))

Uses 3

Statement usesOutput distribution of the Fisher–Yates shuffle

Proof usesFisher–Yates shuffle with supplied draws · Cost of the Fisher–Yates shuffle

TheoremPrefix probabilities of the Fisher–Yates shuffle#✓fully proved

Let \(k \le n\) and let \(a_0, \dots, a_{k-1}\) be distinct elements of \(\{0, \dots, n - 1\}\). Run the Fisher–Yates computation on the vector \((0, 1, \dots, n - 1)\) with every draw history \(d\), which assigns to each position \(i < n\) a number \(d_i\) with \(0 \le d_i < n - i\), and give each history weight \(1/n!\). Then the total weight of the histories whose output vector has entry \(a_p\) at position \(p\) for every \(p < k\) equals \((n - k)!/n!\).

There are exactly \(n!\) draw histories, so this is the probability of the prefix under a uniformly random history. The cases \(k = 0\) and \(k = n\) are included.

public theorem randomlyPermute_prefix_probability {n k : Nat} (hkn : k ≤ n)
    (a : Fin k → Fin n) (hinj : Function.Injective a) :
    (∑ draws : (i : Fin n) → Fin (n - i.val),
      if ∀ p : Fin k,
        (randomlyPermute (Vector.ofFn fun q : Fin n => q) draws).ret[(Fin.castLE hkn p).val] = a p
      then (n.factorial : ENNReal)⁻¹ else 0) =
        ((n - k).factorial : ENNReal) / n.factorial

Uses 2

Statement usesFisher–Yates shuffle with supplied draws

Proof usesCost of the Fisher–Yates shuffle

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.