Uniform Selection Over a Type #
This file defines a typeclass SampleableType β for types β with a canonical uniform selection
operation, using the ProbComp monad.
As compared to HasUniformSelect this provides much more structure on the behavior,
enforcing that every possible output has the same output probability never fails.
A SampleableType β instance means that β is a finite inhabited type,
with a computation selectElem that selects uniformly at random from the type.
This generally requires choosing some "canonical" ordering for the type,
so we include this to get a computable version of selection.
We also require that each element has the same probability of being chosen from by selectElem,
see SampleableType.probOutput_uniformSample for the reduction when α has a fintype instance
involving the explicit cardinality of the type.
- selectElem : ProbComp β
Instances
Select uniformly from the type β using a type-class provided definition.
NOTE: naming is somewhat strange now that Fintype isn't explicitly required.
Instances For
Every element of a uniform sample over a Fintype has output probability card⁻¹.
Pushing a uniform sample through a bijection of α preserves each output probability.
Pushing forward uniform sampling along a bijection preserves output probabilities.
Binding after pushing forward uniform sampling along a bijection preserves output probabilities.
Left-translation by a constant in AddGroup α preserves the uniform output distribution,
since (m + ·) is a bijection on α with inverse (-m + ·).
Left-translating the bound variable of a uniform sample by a constant in AddGroup α
preserves the output distribution of the subsequent computation.
Right-translation analogue of probOutput_add_left_uniform: right-adding a constant to a
uniform sample in AddGroup α preserves the output distribution, since (· + m) is a bijection
on α with inverse (· + (-m)).
Right-translating the bound variable of a uniform sample by a constant in AddGroup α
preserves the output distribution of the subsequent computation.
Right-translation analogue of evalDist_add_left_uniform: right-adding a constant to a
uniform sample in AddGroup α preserves the full evaluation distribution.
Pushing forward uniform sampling via a bijection preserves the full evaluation distribution.
Bijective uniform + right-translation gives uniform. Sampling x ← $ᵗ α, transporting
through a bijection f : α → β, and right-adding any fixed m : β yields the same distribution
as sampling y ← $ᵗ β directly, as observed by any continuation cont : β → ProbComp γ.
This is the "one-time pad" fact underlying many cryptographic reductions: bijective transport
makes f x uniform on β, and in any AddGroup β right-translation (· + m) is a bijection
on the uniform measure, so the sum is again uniform.
Constant-irrelevance form of evalDist_bind_bijective_add_right_uniform: sampling through a
bijection and right-adding a constant has a distribution independent of the constant. Any two
offsets produce the same evaluation distribution.
Uniform sampling never fails, so its support is nonempty (which in turn witnesses Nonempty α).
Tagged @[grind] rather than @[simp] because simp rewrites support ($ᵗ α) to Set.univ
first, after which it would need a separate Nonempty α fact.
A sum of oracle specs with sampleable ranges again has sampleable ranges.
Select a uniform element from α × β by independently selecting from α and β.
Any finitely enumerable type can be sampled uniformly using the underlying equivalence.
Noncomputable bridge from a nonempty Fintype with decidable equality to SampleableType,
via Fintype.equivFin. Used by downstream instances (e.g. Sym α n, Equiv.Perm α, β ↪ α)
whose Mathlib Fintype instances are not paired with a FinEnum. Provided as a def rather
than an instance to avoid overlap with FinEnum.SampleableType.
Instances For
This typeclass shouldn't cause diamonds since Nonempty is propositional.
This typeclass shouldn't cause diamonds since Finite is propositional.
We avoid making this an instance globally as many types already have a Fintype instance
that would not be definitionally equal to this one.
Instances For
Select a uniform element from Vector α n by independently selecting α at each index.
A function from Fin n to a SampleableType is also SampleableType. This is the base
case used by the general FinEnum-indexed instSampleableTypeFunc below.
A function β → α for β finitely enumerable and α sampleable is itself sampleable.
This generalizes the Fin n → α instance above: the FinEnum.fin instance recovers it.
Select a uniform element from List.Vector α n by independently selecting α at each
index. The construction goes through the equivalence with Fin n → α.
Select a uniform element from Matrix ι κ α by independently selecting an entry for each
(i, j). Both index types only need to be FinEnum; the previous Fin n × Fin m-indexed
instance is recovered through FinEnum.fin.
Discoverability wrapper: SampleableType (α ⊕ β) follows from FinEnum on each side
plus nonemptiness of the sum, via Mathlib's FinEnum.sum instance and
FinEnum.SampleableType. Listed explicitly so users can see it in the instance set rather
than relying on a multi-step search.
Discoverability wrapper: SampleableType (Finset α) for FinEnum α. Uniform sampling
draws every subset of α with the same probability (2^|α| outcomes). Finset α is always
inhabited by ∅, so no Nonempty hypothesis is needed.
Uniform sampling of size-n multisets over a FinEnum type. Sym α n is the correct finite
analogue of Multiset α: a plain Multiset α is unbounded in multiplicity and thus not finite,
while Sym α n is finite whenever α is. We obtain a computable uniform sampler from the
canonical enumeration Sym.finEnum; for a base type with only a Fintype instance use
SampleableType.ofFintype instead.
Note this is genuinely uniform on multisets: mapping a uniform List.Vector α n through
Sym.ofVector is not (it weights each multiset by its number of orderings), so we enumerate
Sym α n canonically rather than pushing forward from vectors.
Uniform sampling of permutations of a FinEnum type. Equiv.Perm α has n! elements when
Fintype.card α = n. We obtain a computable uniform sampler from the canonical enumeration
Equiv.Perm.finEnum. Useful for shuffle-based protocols and oblivious-permutation games.
Uniform sampling of injections β ↪ α for FinEnum types. The number of such embeddings is
α.card! / (α.card - β.card)! when β.card ≤ α.card, else 0; the Nonempty (β ↪ α)
hypothesis rules out the latter case. We obtain a computable uniform sampler from the canonical
enumeration Function.Embedding.finEnum (itself computable, unlike Mathlib's Fintype (β ↪ α)).
A function from a finite type D with Fintype + DecidableEq (not necessarily FinEnum)
to a SampleableType is itself SampleableType, transporting the Fin (Fintype.card D) → α
sampler across the canonical equivalence (D → α) ≃ (Fin (Fintype.card D) → α).
This is the noncomputable counterpart to the computable FinEnum-domain instance
instSampleableTypeFunc, and is given lower priority so that for a FinEnum domain the
computable instance is preferred; it is the fallback for Fintype + DecidableEq-only domains.
Overwriting one coordinate of a uniform function table is measure-preserving.
Drawing a value u uniformly from R, then a full function table g : D → R uniformly, and
returning Function.update g t u yields the same distribution as drawing the table directly.
This is the t-marginal independence of the uniform (product) distribution on D → R: the value
at coordinate t is uniform and independent of the others, so replacing it with a fresh
independent uniform draw leaves the joint distribution unchanged. It is the marginalization step
behind eager-sampling reformulations of oracle responses.
The first coordinate of a uniform pair is uniform.
Mapping the uniform distribution on α × β through Prod.fst yields the uniform distribution on
α: the Prod.fst-marginal of a uniform (product) distribution is uniform.
Restricting a uniform function table to a subdomain along an injection is uniform.
For an injection e : A → B between finite types, drawing a uniform table g : B → R and
restricting it along e (i.e. g ∘ e) yields the uniform distribution on A → R.
This is the marginalization of the uniform (product) distribution on B → R onto the block of
coordinates indexed by Set.range e: those coordinates are jointly uniform and independent of
the rest, and e reindexes the block by A. It underlies eager-sampling reformulations that
project a fine-grained random-oracle table onto a coarser one.
Patch a uniform function table at every point of a list l, drawing one fresh uniform value
per list entry. With l = [] the table is returned unchanged; with l = d :: ds the tail is
patched first and the head point d is then overwritten with a fresh uniform draw.
This is the iterated form of Function.update used by evalDist_uniformSample_patchList: the
outermost update is at the head, so the list is consumed head-first.
Instances For
Patching a uniform function table at finitely many points preserves uniformity.
Drawing a uniform table g : D → R and then patchTable l g — overwriting g at every point of
l with independent fresh uniform draws — yields the same distribution as drawing the table
directly. The points of l need not be distinct: each Function.update is the outermost
operation of its recursion step, so evalDist_uniformSample_bind_update applies regardless of
overlap. This is the marginalization step behind trace-conditioned eager-table reformulations,
where the patched points are determined only after the table is sampled.
Given an independent probabilistic computation ob : ProbComp Bool, the probability that its
output b' differs from a uniformly chosen boolean b is the same as the probability that they
are equal. In other words, P(b ≠ b') = P(b = b') where b is uniform.
Guessing a uniformly random bit after branching between real and rand decomposes into
the difference of the branch success probabilities.
If the distribution of f b is independent of b, then guessing a uniformly random
bit by running f has success probability exactly 1/2.
This is the core lemma behind "all-random hybrid has probability 1/2" arguments.
Given that the output type of all oracles has a SampleableType instance, replace all queries
with uniformly random responses by calling the corresponding uniformSample at each query.