Computations with Uniform Selection Oracles

This file defines a type ProbComp α for the case of OracleComp with access to a uniform selection oracle, specified by unifSpec, as well as common operations for this type.

We define $[0..n] as uniform selection starting from zero for any n : ℕ (uniformFin) as well as a version $[n⋯m] that tries to synthesize an instance of n < m (uniformRange). This allows us to avoid needing an OptionT wrapper to handle empty ranges.

We also define typeclasses HasUniformSelect β cont and HasUniformSelect! β cont to allow for $ xs and $! xs notation for uniform sampling from a container. These don't really enforce any semantics, so any new definition will need to prove lemmas about the behavior of the operation. TODO: we could introduce a mixin typeclass at least to handle this?

SampleableType α on the other hand allows for $ᵗ α notation for uniform type sampleing, and does enforce the uniformity of outputs. Encapsulating the thing you want to select in a SampleableType can therefore give more useful lemmas out of the box, in particular when using subtypes.

TODO: Some lemmas here don't exist at the PMF/SPMF levels.

@[reducible, inline]

abbrev ProbComp : Type → Type

Simplified notation for computations with no oracles besides random inputs. This specific case can be used with #eval to run a random program, see OracleComp.runIO. NOTE: Need to decide if this should be more opaque than abbrev, seems like no as of now..

def ProbComp.sampleIID {α : Type} (k : ℕ) (samp : ProbComp α) : ProbComp (Fin k → α)

Independently sample k values from samp, returning them as a Fin k → α.

def ProbComp.uniformFin (n : ℕ) : ProbComp (Fin (n + 1))

$[0..n] is the computation choosing a random value in the given range, inclusively. By making this range inclusive we avoid the case of choosing from the empty range.

def ProbComp.«term$[0.._]» : Lean.ParserDescr

theorem ProbComp.uniformFin_def (n : ℕ) : $[0..n] = liftM (OracleQuery.query n)

@[simp]

theorem ProbComp.support_uniformFin (n : ℕ) : support $[0..n] = Set.univ

@[simp]

theorem ProbComp.finSupport_uniformFin (n : ℕ) : finSupport $[0..n] = Finset.univ

theorem ProbComp.probOutput_uniformFin_eq_div (n : ℕ) (m : Fin (n + 1)) : Pr[= m | $[0..n]] = 1 / (↑n + 1)

@[simp]

theorem ProbComp.probOutput_uniformFin (n : ℕ) (m : Fin (n + 1)) : Pr[= m | $[0..n]] = (↑n + 1)⁻¹

@[simp]

theorem ProbComp.probEvent_uniformFin (n : ℕ) (p : Fin (n + 1) → Prop) [DecidablePred p] : probEvent $[0..n] p = ↑(Fin.countP fun (i : Fin (n + 1)) => decide (p i)) / ↑(n + 1)

theorem ProbComp.probFailure_uniformFin (n : ℕ) : Pr[⊥ | $[0..n]] = 0

def ProbComp.inductionOn {α : Type} {C : ProbComp α → Prop} (pure : ∀ (a : α), C (pure a)) (query_bind : ∀ (n : ℕ) (mx : Fin (n + 1) → ProbComp α), (∀ (m : Fin (n + 1)), C (mx m)) → C ($[0..n] >>= mx)) (oa : ProbComp α) : C oa

Nicer induction rule for ProbComp that uses monad notation. Allows inductive definitions on computations by considering the two cases:

• return x / pure x for any x
• do let u ← $[0..n]; oa u (with inductive results for oa u) See oracleComp_emptySpec_equiv for an example of using this in a proof. If the final result needs to be a Type and not a Prop, see OracleComp.construct.

def ProbComp.uniformRange (n m : ℕ) (h : n < m) : ProbComp (Fin (m + 1))

Select uniformly from a non-empty range. The notation attempts to derive h automatically.

def ProbComp.tacticUniform_range_tactic : Lean.ParserDescr

Tactic to attempt to prove uniformRange decreasing bound, similar to array indexing.

def ProbComp.tacticUniform_range_tactic_1 : Lean.ParserDescr

def ProbComp.tacticUniform_range_tactic_2 : Lean.ParserDescr

def ProbComp.«term$[_⋯_]» : Lean.ParserDescr

Select uniformly from a range of numbers. Attempts to use `get

theorem ProbComp.uniformRange_def (n m : ℕ) (h : n < m) : uniformRange n m h = uniformRange n m h

@[simp]

theorem ProbComp.uniformRange_eq_uniformFin (n : ℕ) (hn : 0 < n) : uniformRange 0 n hn = $[0..n]

@[simp]

theorem ProbComp.probOutput_uniformRange (n m : ℕ) (k : Fin (m + 1)) (h : n < m) : Pr[= k | uniformRange n m h] = if n ≤ ↑k then (↑m - ↑n + 1)⁻¹ else 0

@[simp]

theorem ProbComp.support_uniformRange (n m : ℕ) (h : n < m) : support (uniformRange n m h) = Set.Icc (Fin.ofNat (m + 1) n) (Fin.ofNat (m + 1) m)

@[simp]

theorem ProbComp.finSupport_uniformRange (n m : ℕ) (h : n < m) : finSupport (uniformRange n m h) = Finset.Icc (Fin.ofNat (m + 1) n) (Fin.ofNat (m + 1) m)

@[simp]

theorem ProbComp.probEvent_uniformRange (n m : ℕ) (p : Fin (m + 1) → Prop) [DecidablePred p] (h : n < m) : probEvent (uniformRange n m h) p = ↑{x : Fin (m + 1) | n ≤ ↑x ∧ p x}.card / (↑m - ↑n + 1)

theorem ProbComp.probFailure_uniformRange (n m : ℕ) (h : n < m) : Pr[⊥ | uniformRange n m h] = 0

class ProbComp.HasUniformSelect (cont : Type u) (β : outParam Type) : Type 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 β. β is marked as an outParam so that Lean will first pick the output type before synthesizing. 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 → OptionT ProbComp β

class ProbComp.HasUniformSelect! (cont : Type u) (β : outParam Type) : Type u

Version of HasUniformSelect that doesn't allow for failure. Useful for things like Vector that can be shown nonempty at the type level.

• uniformSelect! : cont → ProbComp β

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

def ProbComp.«term$!_» : Lean.ParserDescr

@[implicit_reducible]

instance ProbComp.hasUniformSelect_of_hasUniformSelect! {cont : Type u} {β : Type} [h : HasUniformSelect! cont β] : HasUniformSelect cont β

Given a non-failing uniform selection operation we also have a potentially failing one, using OptionT.lift

@[simp]

theorem ProbComp.liftM_uniformSelect! {cont : Type u} {β : Type} [HasUniformSelect! cont β] (xs : cont) : liftM ($!xs) = $xs

Compatibility of the $! xs operation with $ xs given the inferred instance. TODO: I think we probably want to simp in the other direction when possible?

theorem ProbComp.uniformSelect_eq_liftM_uniformSelect! {cont : Type u} {β : Type} [HasUniformSelect! cont β] (xs : cont) : $xs = liftM ($!xs)

@[implicit_reducible]

instance ProbComp.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.

theorem ProbComp.uniformSelectList_def {α : Type} (xs : List α) : $xs = match xs with | [] => failure | x :: xs => (fun (x_1 : Fin (xs.length + 1)) => (x :: xs)[x_1]) <$> liftM $[0..xs.length]

@[simp]

theorem ProbComp.uniformSelectList_nil {α : Type} : $ [] = failure

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

@[simp]

theorem ProbComp.support_uniformSelectList {α : Type} (xs : List α) : support ($xs) = {x : α | x ∈ xs}

@[simp]

theorem ProbComp.finSupport_uniformSelectList {α : Type} [DecidableEq α] (xs : List α) : finSupport ($xs) = xs.toFinset

@[simp]

theorem ProbComp.probOutput_uniformSelectList {α : Type} [DecidableEq α] (xs : List α) (x : α) : Pr[= x | $xs] = ↑(List.count x xs) / ↑xs.length

@[simp]

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

@[simp]

theorem ProbComp.probEvent_uniformSelectList {α : Type} (xs : List α) (p : α → Prop) [DecidablePred p] : probEvent ($xs) p = ↑(List.countP (fun (b : α) => decide (p b)) xs) / ↑xs.length

@[implicit_reducible]

instance ProbComp.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 ProbComp.uniformSelectVector_def {α : Type} {n : ℕ} (xs : Vector α (n + 1)) : $!xs = (fun (x : Fin (n + 1)) => xs[x]) <$> $[0..n]

@[simp]

theorem ProbComp.support_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) : support ($!xs) = {x : α | x ∈ xs.toList}

@[simp]

theorem ProbComp.finSupport_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) [DecidableEq α] : finSupport ($xs) = xs.toList.toFinset

@[simp]

theorem ProbComp.probOutput_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) [DecidableEq α] (x : α) : Pr[= x | $!xs] = ↑(Vector.count x xs) / (↑n + 1)

@[simp]

theorem ProbComp.probEvent_uniformSelectVector {α : Type} {n : ℕ} (xs : Vector α (n + 1)) (p : α → Prop) [DecidablePred p] : probEvent ($xs) p = ↑(List.countP (fun (b : α) => decide (p b)) xs.toList) / (↑n + 1)

@[implicit_reducible]

instance ProbComp.hasUniformSelectListVector (α : Type) (n : ℕ) : HasUniformSelect! (List.Vector α (n + 1)) α

theorem ProbComp.uniformSelectListVector_def {α : Type} {n : ℕ} (xs : List.Vector α (n + 1)) : $!xs = (fun (x : Fin (n + 1)) => xs[x]) <$> $[0..n]

@[simp]

theorem ProbComp.probOutput_uniformSelectListVector {α : Type} {n : ℕ} (xs : List.Vector α (n + 1)) [DecidableEq α] (x : α) : Pr[= x | $!xs] = ↑(List.count x xs.toList) / (↑n + 1)

@[simp]

theorem ProbComp.probEvent_uniformSelectListVector {α : Type} {n : ℕ} (xs : List.Vector α (n + 1)) (p : α → Prop) [DecidablePred p] : probEvent ($!xs) p = ↑(List.countP (fun (b : α) => decide (p b)) xs.toList) / (↑n + 1)

@[implicit_reducible]

noncomputable instance ProbComp.hasUniformSelectFinset (α : Type) : 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 ProbComp.uniformSelectFinset_def {α : Type} (s : Finset α) : $s = $s.toList

@[simp]

theorem ProbComp.support_uniformSelectFinset {α : Type} (s : Finset α) : support ($s) = if s.Nonempty then ↑s else ∅

@[simp]

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

@[simp]

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

@[simp]

theorem ProbComp.probEvent_uniformSelectFinset {α : Type} (s : Finset α) (p : α → Prop) [DecidablePred p] : probEvent ($s) p = ↑{x ∈ s | p x}.card / ↑s.card

@[simp]

theorem ProbComp.probFailure_uniformSelectFinset {α : Type} (s : Finset α) : Pr[⊥ | $s] = if s.Nonempty then 0 else 1

@[implicit_reducible]

instance ProbComp.instHasUniformSelectArray {α : Type} : HasUniformSelect (Array α) α

@[simp]

theorem support_coin : support OracleComp.coin = {true, false}

@[simp]

theorem finSupport_coin : finSupport OracleComp.coin = {true, false}

@[simp]

theorem probOutput_coin (b : Bool) : Pr[= b | OracleComp.coin] = 2⁻¹

@[simp]

theorem probEvent_coin (p : Bool → Prop) [DecidablePred p] : probEvent OracleComp.coin p = if p true then if p false then 1 else 2⁻¹ else if p false then 2⁻¹ else 0

@[simp]

theorem probFailure_coin : Pr[⊥ | OracleComp.coin] = 0