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.

Equations

• OracleSpec ι = (ι → Type ?u.7)

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

Equations

• spec.toPFunctor = { A := ι, B := spec }

@[reducible, inline]

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

Equations

• OracleSpec.ofPFunctor P = P.B

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

Equations

• _spec.Domain = ι

@[reducible, inline]

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

Equations

• spec.Range t = spec t

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)

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

Equations

• OracleSpec.instFintypeRangeOfFintype t = PFunctor.Fintype.fintype_B 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)

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

Equations

• OracleSpec.instInhabitedRangeOfInhabited t = PFunctor.Inhabited.inhabited_B 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)

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

Equations

• OracleSpec.instDecidableEqDomainOfDecidableEq = PFunctor.DecidableEq.decidableEq_A

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

Equations

• OracleSpec.instDecidableEqRangeOfDecidableEq t = PFunctor.DecidableEq.decidableEq_B 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. dtumad: we should examine if this should be used more strictly in evalDist stuff. We could require computations without this tag to provide their own PMF embedding, even if it can be inferred implicitly.

@[reducible, always_inline]

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

Equations

• OracleSpec.ofFn F = F

def OracleSpec.singletonSpec : Lean.TrailingParserDescr

Equations

• OracleSpec.singletonSpec = Lean.ParserDescr.trailingNode `OracleSpec.singletonSpec 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₒ ") (Lean.ParserDescr.cat `term 26))

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

Equations

• OracleSpec.instFintypeOfFnOfFintype F = { fintype_B := h }

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

Equations

• OracleSpec.instDecidableEqOfFnOfDecidableEq F = { decidableEq_A := h, decidableEq_B := h' }

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

Equations

• OracleSpec.instInhabitedOfFnOfInhabited F = { inhabited_B := h }

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.

Equations

• OracleSpec.instHAddSum = { hAdd := fun (spec : OracleSpec ι) (spec' : OracleSpec ι') => Sum.elim spec spec' }

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'

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• OracleSpec.sigma specs t = specs t.fst t.snd

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

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.

Equations

• OracleSpec.instHMulProd = { hMul := fun (spec : OracleSpec ι) (spec' : OracleSpec ι') (t : ι × ι') => spec.Range t.1 ⊕ spec'.Range t.2 }

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

Equations

• OracleSpec.pi specs t = ((i : ι) × specs i (t i))

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

Equations

• []ₒ = OracleSpec.ofFn fun (x : PEmpty.{?u.4 + 1}) => PEmpty.{?u.3 + 1}

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

Equations

• OracleSpec.«term[]ₒ» = Lean.ParserDescr.node `OracleSpec.«term[]ₒ» 1024 (Lean.ParserDescr.symbol "[]ₒ")

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

Equations

• coinSpec = OracleSpec.ofFn fun (x : Unit) => Bool

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

Equations

• unifSpec = OracleSpec.ofFn fun (n : ℕ) => Fin (n + 1)

@[reducible, inline]

def probSpec : OracleSpec (ℕ × ℕ)

dt: should or shouldn't we switch to this. Compare to (· + m) <$> $[0..n]. One question is that we may have empty selection Select uniformly from a range (not starting from zero).

Equations

• probSpec = OracleSpec.ofFn fun (x : ℕ × ℕ) => match x with | (_n, m) => Fin (m + 1)