Selecting Uniformly From a Collection

This file defines some computations for selecting uniformly at random from a number of different collections, using unifSpec to make the random choices.

TODO: A lot of lemmas here could exist at the PMF level instead. Probably even a lot of the uniform constructions themselves (like uniformOfList)

class OracleComp.HasUniformSelect (cont : Type u) (β : outParam Type) : Type (max 1 u)

Typeclass to implement the notation $ xs for selecting an object uniformly from a collection. The container type is given by cont with the resulting type given by β. NOTE: This current implementation doesn't impose any "correctness" conditions, it purely exists to provide the notation, could revisit that in the future.

• uniformSelect : cont → ProbComp β

def OracleComp.uniformSelect {cont : Type} (β : Type) [h : HasUniformSelect cont β] (xs : cont) : ProbComp β

Given a selectable object, we can get a random element by indexing into the element vector.

def OracleComp.«term$_» : Lean.ParserDescr

instance OracleComp.hasUniformSelectList (α : Type) : HasUniformSelect (List α) α

Select a random element from a list by indexing into it with a uniform value. If the list is empty we instead just fail rather than choose a default value. This means selecting from a vector is often preferable, as we can prove at the type level that there is an element in the list, avoiding the defualt case of empty lists.

@[simp]

theorem OracleComp.uniformSelectList_nil {α : Type} : uniformSelect α [] = failure

theorem OracleComp.uniformSelectList_cons {α : Type} (x : α) (xs : List α) : uniformSelect α (x :: xs) = (fun (x_1 : Fin (xs.length + 1)) => (x :: xs)[x_1]) <$> $[0..xs.length]

@[simp]

theorem OracleComp.evalDist_uniformSelectList {α : Type} (xs : List α) : evalDist (uniformSelect α xs) = match xs with | [] => PMF.pure none | x :: xs => PMF.map (fun (x_1 : Fin xs.length.succ) => some (x :: xs)[x_1]) (PMF.uniformOfFintype (Fin xs.length.succ))

@[simp]

theorem OracleComp.support_uniformSelectList {α : Type} (xs : List α) : support (uniformSelect α xs) = if xs.isEmpty = true then ∅ else {y : α | y ∈ xs}

@[simp]

theorem OracleComp.finSupport_uniformSelectList {α : Type} [DecidableEq α] (xs : List α) : finSupport (uniformSelect α xs) = if xs.isEmpty = true then ∅ else xs.toFinset

@[simp]

theorem OracleComp.probOutput_uniformSelectList {α : Type} [DecidableEq α] (xs : List α) (x : α) : [=x|uniformSelect α xs] = if xs.isEmpty = true then 0 else ↑(List.count x xs) / ↑xs.length

@[simp]

theorem OracleComp.probFailure_uniformSelectList {α : Type} (xs : List α) : [⊥|uniformSelect α xs] = if xs.isEmpty = true then 1 else 0

@[simp]

theorem OracleComp.probEvent_uniformSelectList {α : Type} (xs : List α) (p : α → Prop) [DecidablePred p] : [p|uniformSelect α xs] = if xs.isEmpty = true then 0 else ↑(List.countP (fun (b : α) => decide (p b)) xs) / ↑xs.length

instance OracleComp.hasUniformSelectVector (α : Type) (n : ℕ) : HasUniformSelect (Vector α (n + 1)) α

Select a random element from a vector by indexing into it with a uniform value. TODO: different types of vectors in mathlib now

theorem OracleComp.uniformSelectVector_def {α : Type} {n : ℕ} (xs : Vector α (n + 1)) : uniformSelect α xs = uniformSelect α xs.toList

noncomputable instance OracleComp.hasUniformSelectFinset (α : Type) [DecidableEq α] : HasUniformSelect (Finset α) α

Choose a random element from a finite set, by converting to a list and choosing from that. This is noncomputable as we don't have a canoncial ordering for the resulting list, so generally this should be avoided when possible.

theorem OracleComp.uniformSelectFinset_def {α : Type} [DecidableEq α] (s : Finset α) : uniformSelect α s = uniformSelect α s.toList

@[simp]

theorem OracleComp.support_uniformSelectFinset {α : Type} [DecidableEq α] (s : Finset α) : support (uniformSelect α s) = if s.Nonempty then ↑s else ∅

@[simp]

theorem OracleComp.finSupport_uniformSelectFinset {α : Type} [DecidableEq α] (s : Finset α) : finSupport (uniformSelect α s) = if s.Nonempty then s else ∅

@[simp]

theorem OracleComp.probOutput_uniformSelectFinset {α : Type} [DecidableEq α] (s : Finset α) (x : α) : [=x|uniformSelect α s] = if x ∈ s then (↑s.card)⁻¹ else 0

@[simp]

theorem OracleComp.probFailure_uniformSelectFinset {α : Type} [DecidableEq α] (s : Finset α) : [⊥|uniformSelect α s] = if s.Nonempty then 0 else 1

@[simp]

theorem OracleComp.evalDist_uniformSelectFinset {α : Type} [DecidableEq α] (s : Finset α) : evalDist (uniformSelect α s) = if hs : s.Nonempty then OptionT.lift (PMF.uniformOfFinset s hs) else failure

class OracleComp.SelectableType (β : Type) : Type 1

A SelectableType β 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 SelectableType.probOutput_selectElem for the reduction when α has a fintype instance. NOTE: universe polymorphism of β is hard.

• selectElem : ProbComp β
• mem_support_selectElem (x : β) : x ∈ support selectElem
• probOutput_selectElem_eq (x y : β) : [=x|selectElem] = [=y|selectElem]
• probFailure_selectElem : [⊥|selectElem] = 0

def OracleComp.uniformOfFintype (β : Type) [h : SelectableType β] : 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 OracleComp.«term$ᵗ_» : Lean.ParserDescr

@[simp]

theorem OracleComp.probOutput_uniformOfFintype (α : Type) [hα : SelectableType α] [Fintype α] (x : α) : [=x|$ᵗα] = (↑(Fintype.card α))⁻¹

@[simp]

theorem OracleComp.probFailure_uniformOfFintype (α : Type) [hα : SelectableType α] : [⊥|$ᵗα] = 0

@[simp]

theorem OracleComp.neverFails_uniformOfFintype (α : Type) [hα : SelectableType α] : neverFails ($ᵗα)

@[simp]

theorem OracleComp.evalDist_uniformOfFintype (α : Type) [hα : SelectableType α] [Fintype α] [Inhabited α] : evalDist ($ᵗα) = OptionT.lift (PMF.uniformOfFintype α)

@[simp]

theorem OracleComp.support_uniformOfFintype (α : Type) [hα : SelectableType α] : support ($ᵗα) = Set.univ

@[simp]

theorem OracleComp.finSupport_uniformOfFintype (α : Type) [hα : SelectableType α] [Fintype α] [DecidableEq α] : finSupport ($ᵗα) = Finset.univ

@[simp]

theorem OracleComp.probEvent_uniformOfFintype (α : Type) [hα : SelectableType α] [Fintype α] (p : α → Prop) [DecidablePred p] : [p|$ᵗα] = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card α)

instance OracleComp.instSelectableTypeOfUnique (α : Type) [Unique α] : SelectableType α

instance OracleComp.instSelectableTypeBool : SelectableType Bool

instance OracleComp.instSelectableTypeProdOfFintypeOfInhabited (α β : Type) [Fintype α] [Fintype β] [Inhabited α] [Inhabited β] [SelectableType α] [SelectableType β] : SelectableType (α × β)

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

instance OracleComp.instSelectableTypeFinHAddNatOfNat (n : ℕ) : SelectableType (Fin (n + 1))

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

instance OracleComp.instSelectableTypeFinOfNeZeroNat (n : ℕ) [hn : NeZero n] : SelectableType (Fin n)

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

instance OracleComp.instSelectableTypeVector (α : Type) (n : ℕ) [SelectableType α] : SelectableType (Vector α n)

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

instance OracleComp.instSelectableTypeMatrixFin (α : Type) (n m : ℕ) [SelectableType α] : SelectableType (Matrix (Fin n) (Fin m) α)

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

theorem OracleComp.probOutput_uniformBool_not_decide_eq_decide {ob : ProbComp Bool} : [=true|do let b ← $ᵗBool let b' ← ob pure !decide (b = b')] = [=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.