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.

class SampleableType (β : Type) : Type

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 β
• mem_support_selectElem (x : β) : x ∈ support selectElem
• probOutput_selectElem_eq (x y : β) : Pr[= x | selectElem] = Pr[= y | selectElem]

def uniformSample (β : Type) [h : SampleableType β] : ProbComp β

Select uniformly from the type β using a type-class provided definition. NOTE: naming is somewhat strange now that Fintype isn't explicitly required.

def «term$ᵗ_» : Lean.ParserDescr

@[simp]

theorem probOutput_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] (x : α) : Pr[= x | $ᵗ α] = (↑(Fintype.card α))⁻¹

theorem probOutput_uniformSample_inj (α : Type) [hα : SampleableType α] (x y : α) : Pr[= x | $ᵗ α] = Pr[= y | $ᵗ α]

theorem probOutput_map_bijective_uniformSample (α : Type) [hα : SampleableType α] {f : α → α} (hf : Function.Bijective f) (x : α) : Pr[= x | f <$> ($ᵗ α)] = Pr[= x | $ᵗ α]

theorem probOutput_map_bijective_uniform_cross (α : Type) [hα : SampleableType α] {β : Type} [SampleableType β] [Finite α] (f : α → β) (hf : Function.Bijective f) (y : β) : Pr[= y | f <$> ($ᵗ α)] = Pr[= y | $ᵗ β]

Pushing forward uniform sampling along a bijection preserves output probabilities.

theorem probOutput_bind_bijective_uniform_cross (α : Type) [hα : SampleableType α] {β γ : Type} [SampleableType β] [Finite α] (f : α → β) (hf : Function.Bijective f) (g : β → ProbComp γ) (z : γ) : Pr[= z | do let x ← $ᵗ α g (f x)] = Pr[= z | do let y ← $ᵗ β g y]

Binding after pushing forward uniform sampling along a bijection preserves output probabilities.

theorem probOutput_add_left_uniform (α : Type) [hα : SampleableType α] [AddGroup α] (m x : α) : Pr[= x | (fun (x : α) => m + x) <$> ($ᵗ α)] = Pr[= x | $ᵗ α]

theorem probOutput_bind_add_left_uniform (α : Type) [hα : SampleableType α] [AddGroup α] {β : Type} (m : α) (f : α → ProbComp β) (z : β) : Pr[= z | do let y ← $ᵗ α f (m + y)] = Pr[= z | do let y ← $ᵗ α f y]

theorem probOutput_add_right_uniform (α : Type) [hα : SampleableType α] [AddGroup α] (m x : α) : Pr[= x | (fun (x : α) => x + m) <$> ($ᵗ α)] = Pr[= x | $ᵗ α]

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)).

theorem probOutput_bind_add_right_uniform (α : Type) [hα : SampleableType α] [AddGroup α] {β : Type} (m : α) (f : α → ProbComp β) (z : β) : Pr[= z | do let y ← $ᵗ α f (y + m)] = Pr[= z | do let y ← $ᵗ α f y]

@[simp]

theorem evalDist_add_left_uniform (α : Type) [hα : SampleableType α] [AddGroup α] (m : α) : evalDist ((fun (x : α) => m + x) <$> ($ᵗ α)) = evalDist ($ᵗ α)

Translating a uniform additive sample preserves the full evaluation distribution.

theorem evalDist_add_left_uniform_eq (α : Type) [hα : SampleableType α] [AddGroup α] (m₁ m₂ : α) : evalDist ((fun (x : α) => m₁ + x) <$> ($ᵗ α)) = evalDist ((fun (x : α) => m₂ + x) <$> ($ᵗ α))

Two additive translations of a uniform sample have the same evaluation distribution.

@[simp]

theorem evalDist_add_right_uniform (α : Type) [hα : SampleableType α] [AddGroup α] (m : α) : evalDist ((fun (x : α) => x + m) <$> ($ᵗ α)) = evalDist ($ᵗ α)

Right-translation analogue of evalDist_add_left_uniform: right-adding a constant to a uniform sample in AddGroup α preserves the full evaluation distribution.

theorem evalDist_add_right_uniform_eq (α : Type) [hα : SampleableType α] [AddGroup α] (m₁ m₂ : α) : evalDist ((fun (x : α) => x + m₁) <$> ($ᵗ α)) = evalDist ((fun (x : α) => x + m₂) <$> ($ᵗ α))

Two right-translations of a uniform sample have the same evaluation distribution.

theorem evalDist_map_bijective_uniform_cross (α : Type) [hα : SampleableType α] {β : Type} [SampleableType β] [Finite α] (f : α → β) (hf : Function.Bijective f) : evalDist (f <$> ($ᵗ α)) = evalDist ($ᵗ β)

Pushing forward uniform sampling via a bijection preserves the full evaluation distribution.

theorem evalDist_bind_bijective_add_right_uniform (α : Type) [hα : SampleableType α] {β γ : Type} [AddGroup β] [SampleableType β] [Finite α] (f : α → β) (hf : Function.Bijective f) (m : β) (cont : β → ProbComp γ) : (evalDist do let x ← $ᵗ α cont (f x + m)) = evalDist do let y ← $ᵗ β cont y

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.

theorem evalDist_bind_bijective_add_right_eq (α : Type) [hα : SampleableType α] {β γ : Type} [AddGroup β] [SampleableType β] [Finite α] (f : α → β) (hf : Function.Bijective f) (m₁ m₂ : β) (cont : β → ProbComp γ) : (evalDist do let x ← $ᵗ α cont (f x + m₁)) = evalDist do let x ← $ᵗ α cont (f x + m₂)

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.

theorem probFailure_uniformSample (α : Type) [hα : SampleableType α] : Pr[⊥ | $ᵗ α] = 0

@[simp]

instance instNeverFailProbCompUniformSample (α : Type) [hα : SampleableType α] : NeverFail ($ᵗ α)

@[simp]

theorem evalDist_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] [Nonempty α] : evalDist ($ᵗ α) = liftM (PMF.uniformOfFintype α)

@[simp]

theorem support_uniformSample (α : Type) [hα : SampleableType α] : support ($ᵗ α) = Set.univ

theorem mem_support_uniformSample (α : Type) [hα : SampleableType α] {x : α} : x ∈ support ($ᵗ α)

@[simp]

theorem finSupport_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] [DecidableEq α] : finSupport ($ᵗ α) = Finset.univ

@[simp]

theorem probEvent_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] (p : α → Prop) [DecidablePred p] : probEvent ($ᵗ α) p = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card α)

@[reducible]

def SampleableType.Fin (n : ℕ) : SampleableType (_root_.Fin (n + 1))

@[implicit_reducible]

instance instSampleableTypeFinOfNeZeroNat (n : ℕ) [hn : NeZero n] : SampleableType (Fin n)

@[implicit_reducible]

instance instSampleableTypeOfUnique (α : Type) [Unique α] : SampleableType α

@[implicit_reducible]

instance instSampleableTypeBool : SampleableType Bool

@[implicit_reducible]

instance instSampleableTypeRangeSumHAddOracleSpec {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} [h : (t : ι) → SampleableType (spec.Range t)] [h' : (t : ι') → SampleableType (spec'.Range t)] (t : ι ⊕ ι') : SampleableType ((spec + spec').Range t)

A sum of oracle specs with sampleable ranges again has sampleable ranges.

@[implicit_reducible]

instance instSampleableTypeProdOfFintypeOfInhabited (α β : Type) [Fintype α] [Fintype β] [Inhabited α] [Inhabited β] [SampleableType α] [SampleableType β] : SampleableType (α × β)

Select a uniform element from α × β by independently selecting from α and β.

@[reducible]

def SampleableType.ofEquiv {α β : Type} [SampleableType α] (e : α ≃ β) : SampleableType β

A type equivalent to a SampleableType is also SampleableType.

@[implicit_reducible]

instance FinEnum.SampleableType (α : Type) [h : FinEnum α] [Nonempty α] : _root_.SampleableType α

Any finitely enumerable type can be sampled uniformly using the underlying equivalence.

@[implicit_reducible]

instance instFinEnumZModOfNeZeroNat_vCVio (n : ℕ) [NeZero n] : FinEnum (ZMod n)

@[implicit_reducible]

instance instFinEnumBitVec_vCVio (n : ℕ) : FinEnum (BitVec n)

@[implicit_reducible]

instance instFinEnumUInt8_vCVio : FinEnum UInt8

@[implicit_reducible]

instance instFinEnumUInt16_vCVio : FinEnum UInt16

@[implicit_reducible]

instance instFinEnumUInt32_vCVio : FinEnum UInt32

@[implicit_reducible]

instance instFinEnumUInt64_vCVio : FinEnum UInt64

@[implicit_reducible]

instance instFinEnumUSize_vCVio : FinEnum USize

@[implicit_reducible]

instance instFinEnumInt8_vCVio : FinEnum Int8

@[implicit_reducible]

instance instFinEnumInt16_vCVio : FinEnum Int16

@[implicit_reducible]

instance instFinEnumInt32_vCVio : FinEnum Int32

@[implicit_reducible]

instance instFinEnumInt64_vCVio : FinEnum Int64

@[implicit_reducible]

instance instFinEnumISize_vCVio : FinEnum ISize

@[implicit_reducible]

instance instSampleableTypeVector (α : Type) (n : ℕ) [SampleableType α] : SampleableType (Vector α n)

Select a uniform element from Vector α n by independently selecting α at each index.

@[implicit_reducible]

instance instFintypeVector (α : Type u) (n : ℕ) [Fintype α] : Fintype (Vector α n)

Vector α n is finite when α is finite, via the equivalence with Fin n → α.

@[implicit_reducible]

instance instSampleableTypeFinFunc {n : ℕ} {α : Type} [SampleableType α] : SampleableType (Fin n → α)

A function from Fin n to a SampleableType is also SampleableType.

@[implicit_reducible]

instance instSampleableTypeMatrixFin (α : Type) (n m : ℕ) [SampleableType α] : SampleableType (Matrix (Fin n) (Fin m) α)

Select a uniform element from Matrix α n by selecting each row independently.

theorem probOutput_uniformBool_not_decide_eq_decide {ob : ProbComp Bool} : Pr[= true | do let b ← $ᵗ Bool let b' ← ob pure !decide (b = b')] = Pr[= true | do let b ← $ᵗ Bool let b' ← ob pure (decide (b = b'))]

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.

theorem probOutput_bind_uniformBool {α : Type} (f : Bool → ProbComp α) (x : α) : Pr[= x | do let b ← $ᵗ Bool f b] = (Pr[= x | f true] + Pr[= x | f false]) / 2

Conditioning on a uniform boolean averages the two branch probabilities.

theorem probOutput_uniformBool_branch_toReal_sub_half (real rand : ProbComp Bool) : Pr[= true | do let b ← $ᵗ Bool have __do_jp : Bool → ProbComp Bool := fun (z : Bool) => pure (b == z) if b = true then do let y ← real __do_jp y else do let y ← rand __do_jp y].toReal - 1 / 2 = (Pr[= true | real].toReal - Pr[= true | rand].toReal) / 2

Guessing a uniformly random bit after branching between real and rand decomposes into the difference of the branch success probabilities.

theorem probOutput_decide_eq_uniformBool_half (f : Bool → ProbComp Bool) (heq : evalDist (f true) = evalDist (f false)) : Pr[= true | do let b ← $ᵗ Bool let b' ← f b pure (decide (b = b'))] = 1 / 2

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.