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.

Equations

• $ᵗβ = SampleableType.selectElem

def «term$ᵗ_» : Lean.ParserDescr

Equations

• «term$ᵗ_» = Lean.ParserDescr.node `«term$ᵗ_» 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "$ᵗ") (Lean.ParserDescr.cat `term 90))

@[simp]

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

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

theorem probOutput_map_bijective_uniform_cross (α : Type) [hα : SampleableType α] {β : Type} [SampleableType β] [Fintype α] [Fintype β] (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 β] [Fintype α] (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]

@[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.

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

Pushing forward uniform sampling along a bijection preserves the full 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] : Pr[p | $ᵗα] = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card α)

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

Equations

• instSampleableTypeOfUnique α = { selectElem := pure default, mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

instance instSampleableTypeBool : SampleableType Bool

Equations

• instSampleableTypeBool = { selectElem := $!#v[true, false], mem_support_selectElem := instSampleableTypeBool._proof_2, probOutput_selectElem_eq := instSampleableTypeBool._proof_3 }

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

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

Equations

• instSampleableTypeProdOfFintypeOfInhabited α β = { selectElem := (fun (x1 : α) (x2 : β) => (x1, x2)) <$> ($ᵗα) <*> $ᵗβ, mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

instance instSampleableTypeFinHAddNatOfNat (n : ℕ) : SampleableType (Fin (n + 1))

Nonempty Fin types can be selected from, using implicit casting of Fin (n - 1 + 1).

Equations

• instSampleableTypeFinHAddNatOfNat n = { selectElem := $[0..n], mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

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

Version of Fin selection using the NeZero typeclass, avoiding the need for n + 1.

Equations

• instSampleableTypeFinOfNeZeroNat n = { selectElem := Fin.cast ⋯ <$> ($ᵗFin (n - 1 + 1)), mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

instance instSampleableTypeZModOfNeZeroNat (n : ℕ) [hn : NeZero n] : SampleableType (ZMod n)

Version of ZMod selection using the NeZero typeclass, matching Fin n.

Equations

• instSampleableTypeZModOfNeZeroNat n = { selectElem := ⇑(ZMod.finEquiv n) <$> ($ᵗFin n), mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

instance instSampleableTypeBitVec (n : ℕ) : SampleableType (BitVec n)

Choose a random bit-vector by converting a random number between 0 and 2 ^ n.

Equations

• instSampleableTypeBitVec n = { selectElem := BitVec.ofFin <$> ($ᵗFin (2 ^ n)), mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

A type equivalent to a SampleableType is also SampleableType.

Equations

• SampleableType.ofEquiv e = { selectElem := ⇑e <$> ($ᵗα), mem_support_selectElem := ⋯, probOutput_selectElem_eq := ⋯ }

instance instSampleableTypeUInt8 : SampleableType UInt8

Unsigned machine words inherit uniform sampling from the corresponding fixed-width bitvectors.

Equations

• One or more equations did not get rendered due to their size.

instance instSampleableTypeUInt16 : SampleableType UInt16

Equations

• One or more equations did not get rendered due to their size.

instance instSampleableTypeUInt32 : SampleableType UInt32

Equations

• One or more equations did not get rendered due to their size.

instance instSampleableTypeUInt64 : SampleableType UInt64

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• instSampleableTypeFinFunc = SampleableType.ofEquiv { toFun := fun (v : Vector α n) (i : Fin n) => v.get i, invFun := Vector.ofFn, left_inv := ⋯, right_inv := ⋯ }

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

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

Equations

• instSampleableTypeMatrixFinOfDecidableEq α n m = id inferInstance

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.