Specifications of Available Oracles

An OracleSpec ι specifies a collection of oracles indexed by ι, given as the map sending each index to the output type of that oracle. It is the same data as a PFunctor, and the bridge toPFunctor / ofPFunctor exposes that algebra: oracle specifications can be combined with + (a disjoint sum of oracle sets), *, OracleSpec.sigma, and OracleSpec.pi. The empty specification []ₒ provides no oracles.

This file also defines the standard sampling specifications coinSpec, unifSpec, and probSpec.

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

An OracleSpec ι specifies 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)

• fintypeB (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)

• inhabitedB (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)

• decidableEqA : DecidableEq spec.toPFunctor.A
• decidableEqB (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)

@[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, specify 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, specify access to an oracle that given an input to the oracle for each index returns an index and an output 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 (ℕ × ℕ)

Select uniformly from Fin (m + 1) for a pair (n, m) : ℕ × ℕ, where the first component is unused.