Specifications of Available Oracles

This file defines a type OracleSpec to represent a set of available oracles. The available oracles are all indexed by some (potentially infinite) indexing set ι, and for each index i a pair of types domain i and range i.

We also define a number of basic oracle constructions:

• ∅: Access to no oracles
• T →ₒ U: Access to a single oracle with given input and output
• coinSpec: A single oracle for flipping a coin
• unifSpec: A family of oracles for selecting from [0..n] for any n

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

A structure to represents a specification of oracles available to a computation. The available oracles are all indexed by some (potentially infinite) indexing set ι. Represented as a map from indices i to the domain and codomain of the corresponding oracle.

Equations

• OracleSpec ι = (ι → Type ?u.12 × Type ?u.12)

instance OracleSpec.instInhabited {ι : Type u} : Inhabited (OracleSpec ι)

Equations

• OracleSpec.instInhabited = { default := fun (x : ι) => (PUnit.{?u.12 + 1}, PUnit.{?u.12 + 1}) }

@[reducible, inline]

def OracleSpec.domain {ι : Type u} (spec : OracleSpec ι) (i : ι) : Type v

Type of the domain for calls to the oracle corresponding to i.

Equations

• spec.domain i = (spec i).1

@[reducible, inline]

def OracleSpec.range {ι : Type u} (spec : OracleSpec ι) (i : ι) : Type w

Type of the range for calls to the oracle corresponding to i.

Equations

• spec.range i = (spec i).2

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

Typeclass to capture decidable equality of the oracle input and outputs. Needed for things like finSupport to be well defined.

• domain_decidableEq' (i : ι) : DecidableEq (spec.domain i)
• range_decidableEq' (i : ι) : DecidableEq (spec.range i)

instance OracleSpec.domain_decidableEq {ι : Type u} {spec : OracleSpec ι} {i : ι} [h : spec.DecidableEq] : DecidableEq (spec.domain i)

Equations

• OracleSpec.domain_decidableEq = OracleSpec.DecidableEq.domain_decidableEq' i

instance OracleSpec.range_decidableEq {ι : Type u} {spec : OracleSpec ι} {i : ι} [h : spec.DecidableEq] : DecidableEq (spec.range i)

Equations

• OracleSpec.range_decidableEq = OracleSpec.DecidableEq.range_decidableEq' i

class OracleSpec.FiniteRange {ι : Type u} (spec : OracleSpec ι) : Type (max u u_1)

Typeclass for specs where each oracle has a finite and non-empty output type. Needed for things like evalDist and probOutput.

• range_inhabited' (i : ι) : Inhabited (spec.range i)
• range_fintype' (i : ι) : Fintype (spec.range i)

instance OracleSpec.range_inhabited {ι : Type u} {spec : OracleSpec ι} {i : ι} [h : spec.FiniteRange] : Inhabited (spec.range i)

Equations

• OracleSpec.range_inhabited = OracleSpec.FiniteRange.range_inhabited' i

instance OracleSpec.range_fintype {ι : Type u} {spec : OracleSpec ι} {i : ι} [h : spec.FiniteRange] : Fintype (spec.range i)

Equations

• OracleSpec.range_fintype = OracleSpec.FiniteRange.range_fintype' i

def OracleSpec.append {ι₁ : Type u} {ι₂ : Type u'} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) : OracleSpec (ι₁ ⊕ ι₂)

spec₁ ++ spec₂ combines the two sets of oracles disjointly using Sum for the indexing set. inl i is a query to oracle i of spec, and inr i for oracle i of spec'.

Equations

• (spec₁ ++ₒ spec₂) (Sum.inl i) = spec₁ i
• (spec₁ ++ₒ spec₂) (Sum.inr i) = spec₂ i

def OracleSpec.«term_++ₒ_» : Lean.TrailingParserDescr

Equations

• OracleSpec.«term_++ₒ_» = Lean.ParserDescr.trailingNode `OracleSpec.«term_++ₒ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ₒ ") (Lean.ParserDescr.cat `term 66))

instance OracleSpec.instDecidableEqSumAppend {ι₁ : Type u} {ι₂ : Type u'} (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.instFiniteRangeSumAppend {ι₁ : Type u} {ι₂ : Type u'} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) [h₁ : spec₁.FiniteRange] [h₂ : spec₂.FiniteRange] : (spec₁ ++ₒ spec₂).FiniteRange

Equations

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

@[reducible, inline]

def OracleSpec.rename {ι : Type u} {τ : Type u'} (spec : OracleSpec ι) (f : τ → ι) : OracleSpec τ

Reduce the indexing set by pulling back along some map f.

Equations

• spec.rename f = spec ∘ f

@[reducible, inline]

def emptySpec : OracleSpec PEmpty.{u_1 + 1}

Access to no oracles, represented by an empty indexing set. We take the domain and range to be PUnit (rather than e.g. empty.elim i), which often gives better behavior for proofs even though the oracle is never called.

Equations

• []ₒ x✝ = (PUnit.{?u.10 + 1}, PUnit.{?u.10 + 1})

def «term[]ₒ» : Lean.ParserDescr

Equations

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

instance instUniqueDomainPEmptyEmptySpec (i : PEmpty.{u_1 + 1}) : Unique ([]ₒ.domain i)

Equations

• instUniqueDomainPEmptyEmptySpec i = PUnit.instUnique

instance instUniqueRangePEmptyEmptySpec (i : PEmpty.{u_1 + 1}) : Unique ([]ₒ.range i)

Equations

• instUniqueRangePEmptyEmptySpec i = PUnit.instUnique

instance instDecidableEqPEmptyEmptySpec : []ₒ.DecidableEq

Equations

• instDecidableEqPEmptyEmptySpec = { domain_decidableEq' := inferInstance, range_decidableEq' := inferInstance }

instance instFiniteRangePEmptyEmptySpec : []ₒ.FiniteRange

Equations

• instFiniteRangePEmptyEmptySpec = { range_inhabited' := inferInstance, range_fintype' := inferInstance }

@[reducible, inline]

def singletonSpec (T U : Type v) : OracleSpec PUnit.{u + 1}

T →ₒ U represents a single oracle, with domain T and range U. Uses the singleton type PUnit as the indexing set.

Equations

• (T →ₒ U) x✝ = (T, U)

def «term_→ₒ_» : Lean.TrailingParserDescr

Equations

• «term_→ₒ_» = Lean.ParserDescr.trailingNode `«term_→ₒ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₒ ") (Lean.ParserDescr.cat `term 26))

instance instDecidableEqPUnitSingletonSpecOfDecidableEq {T U : Type v} [DecidableEq T] [DecidableEq U] : (T →ₒ U).DecidableEq

Equations

• instDecidableEqPUnitSingletonSpecOfDecidableEq = { domain_decidableEq' := inferInstance, range_decidableEq' := inferInstance }

instance instFiniteRangePUnitSingletonSpecOfInhabitedOfFintype {T U : Type v} [Inhabited U] [Fintype U] : (T →ₒ U).FiniteRange

Equations

• instFiniteRangePUnitSingletonSpecOfInhabitedOfFintype = { range_inhabited' := inferInstance, range_fintype' := inferInstance }

@[reducible, inline]

def coinSpec : OracleSpec Unit

A coin flipping oracle produces a random Bool with no meaningful input.

Equations

• coinSpec = (Unit →ₒ Bool)

instance instDecidableEqUnitCoinSpec : coinSpec.DecidableEq

Equations

• instDecidableEqUnitCoinSpec = { domain_decidableEq' := inferInstance, range_decidableEq' := inferInstance }

instance instFiniteRangeUnitCoinSpec : coinSpec.FiniteRange

Equations

• instFiniteRangeUnitCoinSpec = { range_inhabited' := inferInstance, range_fintype' := inferInstance }

def unifSpec' : OracleSpec (Type u)

Equations

• unifSpec' α = (PUnit.{?u.10 + 1}, α)

@[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 n = (Unit, Fin (n + 1))

def probSpec : OracleSpec ℕ

Equations

• probSpec n = (ℕ, Fin (n + 1))

instance instDecidableEqNatUnifSpec : unifSpec.DecidableEq

Equations

• instDecidableEqNatUnifSpec = { domain_decidableEq' := inferInstance, range_decidableEq' := inferInstance }

instance instFiniteRangeNatUnifSpec : unifSpec.FiniteRange

Equations

• instFiniteRangeNatUnifSpec = { range_inhabited' := inferInstance, range_fintype' := inferInstance }