Specifications of Available Oracles

def OracleSpec (ι : Type u) : Type (max u (v + 1))

An OracleSpec ι is specieifes a set of oracles indexed by ι. Defined as a map from each input to the type of the oracle's output.

def OracleSpec.toPFunctor {ι : Type u} (spec : OracleSpec ι) : PFunctor.{u, u_1}

@[reducible, inline]

def OracleSpec.ofPFunctor (P : PFunctor.{u_1, u_2}) : OracleSpec P.A

@[simp]

theorem OracleSpec.toPFunctor_ofPFunctor (P : PFunctor.{u_1, u_2}) : (ofPFunctor P).toPFunctor = P

@[simp]

theorem OracleSpec.ofPFunctor_toPFunctor {ι : Type u} (spec : OracleSpec ι) : ofPFunctor spec.toPFunctor = spec

@[reducible, inline]

abbrev OracleSpec.Domain {ι : Type u} (_spec : OracleSpec ι) : Type u

@[reducible, inline]

abbrev OracleSpec.Range {ι : Type u} (spec : OracleSpec ι) (t : ι) : Type u_1

class OracleSpec.Fintype {ι : Type u} (spec : OracleSpec ι) extends spec.toPFunctor.Fintype : Type (max u u_1)

• fintype_B (a : spec.toPFunctor.A) : Fintype (spec.toPFunctor.B a)

@[implicit_reducible]

instance OracleSpec.instFintypeRangeOfFintype {ι : Type u} {spec : OracleSpec ι} [h : spec.Fintype] (t : spec.Domain) : Fintype (spec.Range t)

class OracleSpec.Inhabited {ι : Type u} (spec : OracleSpec ι) extends spec.toPFunctor.Inhabited : Type (max u u_1)

• inhabited_B (a : spec.toPFunctor.A) : Inhabited (spec.toPFunctor.B a)

@[implicit_reducible]

instance OracleSpec.instInhabitedRangeOfInhabited {ι : Type u} {spec : OracleSpec ι} [h : spec.Inhabited] (t : spec.Domain) : Inhabited (spec.Range t)

class OracleSpec.DecidableEq {ι : Type u} (spec : OracleSpec ι) extends spec.toPFunctor.DecidableEq : Type (max u u_1)

• decidableEq_A : DecidableEq spec.toPFunctor.A
• decidableEq_B (a : spec.toPFunctor.A) : DecidableEq (spec.toPFunctor.B a)

@[implicit_reducible]

instance OracleSpec.instDecidableEqDomainOfDecidableEq {ι : Type u} {spec : OracleSpec ι} [h : spec.DecidableEq] : DecidableEq spec.Domain

@[implicit_reducible]

instance OracleSpec.instDecidableEqRangeOfDecidableEq {ι : Type u} {spec : OracleSpec ι} [h : spec.DecidableEq] (t : spec.Domain) : DecidableEq (spec.Range t)

class OracleSpec.IsProbSpec {ι : Type u} (spec : OracleSpec ι) [spec.Inhabited] [spec.Fintype] : Type

Type-class gadget to enable probability notation for computation over an OracleSpec. Can be defined for any spec with spec.Range finite and inhabited, but generally should only be instantied for things like coinSpec or unifSpec. TODO: Examine if this should be used as a requirement in evalDist instances. Just forces more explicit differentiation of when the semantics should apply.

@[reducible, always_inline]

def OracleSpec.ofFn {ι : Type u} (F : ι → Type v) : OracleSpec ι

def OracleSpec.singletonSpec : Lean.TrailingParserDescr

@[implicit_reducible]

instance OracleSpec.instFintypeOfFnOfFintype {ι : Type u} (F : ι → Type v) [h : (i : ι) → Fintype (F i)] : (ofFn F).Fintype

@[implicit_reducible]

instance OracleSpec.instDecidableEqOfFnOfDecidableEq {ι : Type u} (F : ι → Type v) [h : DecidableEq ι] [h' : (i : ι) → DecidableEq (F i)] : (ofFn F).DecidableEq

@[implicit_reducible]

instance OracleSpec.instInhabitedOfFnOfInhabited {ι : Type u} (F : ι → Type v) [h : (i : ι) → Inhabited (F i)] : (ofFn F).Inhabited

@[implicit_reducible]

instance OracleSpec.instHAddSum {ι : Type u_1} {ι' : Type u_2} : HAdd (OracleSpec ι) (OracleSpec ι') (OracleSpec (ι ⊕ ι'))

spec₁ + spec₂ specifies access to oracles in both spec₁ and spec₂. The input is split as a sum type of the two original input sets. This corresponds exactly to addition of the corresponding PFunctor.

theorem OracleSpec.add_def {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') : spec + spec' = Sum.elim spec spec'

@[simp]

theorem OracleSpec.add_apply_inl {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') (t : ι) : (spec + spec') (Sum.inl t) = spec t

@[simp]

theorem OracleSpec.add_apply_inr {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') (t : ι') : (spec + spec') (Sum.inr t) = spec' t

@[simp]

theorem OracleSpec.toPFunctor_add {ι ι' : Type (max u_1 u_2)} (spec : OracleSpec ι) (spec' : OracleSpec ι') : (spec + spec').toPFunctor = spec.toPFunctor + spec'.toPFunctor

@[simp]

theorem OracleSpec.ofPFunctor_add (P P' : PFunctor.{u_1, u_2}) : ofPFunctor (P + P') = ofPFunctor P + ofPFunctor P'

@[implicit_reducible]

instance OracleSpec.instFintypeSumHAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [h : spec.Fintype] [h' : spec'.Fintype] : (spec + spec').Fintype

@[implicit_reducible]

instance OracleSpec.instDecidableEqSumHAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [h : spec.DecidableEq] [h' : spec'.DecidableEq] : (spec + spec').DecidableEq

@[implicit_reducible]

instance OracleSpec.instInhabitedSumHAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [h : spec.Inhabited] [h' : spec'.Inhabited] : (spec + spec').Inhabited

def OracleSpec.sigma {ι : Type u_1} {τ : ι → Type u_2} (specs : (i : ι) → OracleSpec (τ i)) : OracleSpec ((i : ι) × (specs i).Domain)

Given an indexed set of OracleSpec, specifiy access to all of the oracles, by requiring an index into the corresponding oracle in the input.

@[simp]

theorem OracleSpec.sigma_apply {ι : Type u_1} {τ : ι → Type u_2} (specs : (i : ι) → OracleSpec (τ i)) (t : (i : ι) × (specs i).Domain) : OracleSpec.sigma specs t = specs t.fst t.snd

@[simp]

theorem OracleSpec.toPFunctor_sigma {ι : Type u_1} {τ : ι → Type u_2} (specs : (i : ι) → OracleSpec (τ i)) : (OracleSpec.sigma specs).toPFunctor = PFunctor.sigma fun (i : ι) => (specs i).toPFunctor

@[simp]

theorem OracleSpec.ofPFunctor_sigma {ι : Type u_1} (P : ι → PFunctor.{u_2, u_3}) : ofPFunctor (PFunctor.sigma P) = OracleSpec.sigma fun (i : ι) => ofPFunctor (P i)

@[implicit_reducible]

instance OracleSpec.instHMulProd {ι : Type u_1} {ι' : Type u_2} : HMul (OracleSpec ι) (OracleSpec ι') (OracleSpec (ι × ι'))

spec₁ * spec₂ represents an oracle that takes in a pair of inputs for each set, and returns an element in the output of one oracle or the other. The corresponds exactly to multiplication in PFunctor.

@[simp]

theorem OracleSpec.mul_apply {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') (t : ι × ι') : (spec * spec').Range t = (spec.Range t.1 ⊕ spec'.Range t.2)

@[simp]

theorem OracleSpec.toPFunctor_mul {ι ι' : Type (max u_1 u_2)} (spec : OracleSpec ι) (spec' : OracleSpec ι') : (spec * spec').toPFunctor = spec.toPFunctor * spec'.toPFunctor

@[simp]

theorem OracleSpec.ofPFunctor_mul (P P' : PFunctor.{u_1, u_2}) : ofPFunctor (P * P') = ofPFunctor P * ofPFunctor P'

def OracleSpec.pi {ι : Type u_1} {τ : ι → Type u_2} (specs : (i : ι) → OracleSpec (τ i)) : OracleSpec ((i : ι) → (specs i).Domain)

Given an indexed set of OracleSpec, specifiy access to an oracle that given an input to the oracle for each index returns an index and an ouptut for that index.

@[simp]

theorem OracleSpec.pi_apply {ι : Type u_1} {τ : ι → Type u_2} (specs : (i : ι) → OracleSpec (τ i)) (t : (i : ι) → (specs i).Domain) : OracleSpec.pi specs t = ((i : ι) × specs i (t i))

@[simp]

theorem OracleSpec.toPFunctor_pi {ι : Type u_1} {τ : ι → Type u_2} (specs : (i : ι) → OracleSpec (τ i)) : (OracleSpec.pi specs).toPFunctor = PFunctor.pi fun (i : ι) => (specs i).toPFunctor

@[simp]

theorem OracleSpec.ofPFunctor_pi {ι : Type u_1} (P : ι → PFunctor.{u_2, u_3}) : ofPFunctor (PFunctor.pi P) = OracleSpec.pi fun (i : ι) => ofPFunctor (P i)

@[reducible]

def OracleSpec.emptySpec : OracleSpec PEmpty.{u_1 + 1}

Specifies access to no oracles, using the empty type as the indexing type.

def OracleSpec.«term[]ₒ» : Lean.ParserDescr

@[simp]

theorem OracleSpec.toPFunctor_emptySpec : []ₒ.toPFunctor = 0

@[simp]

theorem OracleSpec.ofPFunctor_zero : ofPFunctor 0 = []ₒ

@[reducible]

def coinSpec : OracleSpec Unit

Access to a coin flipping oracle. Because of termination rules in Lean this is slightly weaker than unifSpec, as we have only finitely many coin flips.

@[reducible, inline]

def unifSpec : OracleSpec ℕ

Access to oracles for uniformly selecting from Fin (n + 1) for arbitrary n : ℕ. By adding 1 to the index we avoid selection from the empty type Fin 0 ≃ empty.

@[reducible, inline]

def probSpec : OracleSpec (ℕ × ℕ)

NOTE: There isn't really any built in Select uniformly from a range (not starting from zero).