Executable uniform oracle programs

ProbComp programs draw finite-range uniform inputs. The sampling operations and container notation in this module are executable; their possible outputs use native attachment semantics.

@[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 (OracleSpec.query n)

@[simp]

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

theorem 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.uniformRangeTactic : Lean.ParserDescr

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

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

Select uniformly from [n, m], proving the bound with uniform_range_tactic.

@[simp]

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

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

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

@[instance_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)

@[instance_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}

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

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}

@[instance_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]

@[instance_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 ∅

@[instance_reducible]

instance ProbComp.hasUniformSelectArray (α : Type) : HasUniformSelect (Array α) α

theorem ProbComp.uniformSelectArray_def {α : Type} (xs : Array α) : $xs = if h : xs.size = 0 then failure else do let u ← liftM $[0..xs.size - 1] pure xs[u]

@[simp]

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

@[simp]

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

@[instance_reducible]

noncomputable instance ProbComp.hasUniformSelectMultiset (α : Type) : HasUniformSelect (Multiset α) α

Choose a random element from a multiset, by converting to a list and choosing from that. This is noncomputable as the underlying list is only canonical up to permutation; for any fixed Multiset.toList representative each element is sampled with weight equal to its multiplicity.

theorem ProbComp.uniformSelectMultiset_def {α : Type} (s : Multiset α) : $s = $s.toList

@[simp]

theorem ProbComp.support_uniformSelectMultiset {α : Type} (s : Multiset α) : support ($s) = {x : α | x ∈ s}

@[simp]

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