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.

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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)

instance OracleSpec.range_decidableEq {ι : Type u} {spec : OracleSpec ι} {i : ι} [h : spec.DecidableEq] : DecidableEq (spec.range 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)

instance OracleSpec.range_fintype {ι : Type u} {spec : OracleSpec ι} {i : ι} [h : spec.FiniteRange] : Fintype (spec.range 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'.

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

instance OracleSpec.instDecidableEqSumAppend {ι₁ : Type u} {ι₂ : Type u'} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) [h₁ : spec₁.DecidableEq] [h₂ : spec₂.DecidableEq] : (spec₁ ++ₒ spec₂).DecidableEq

instance OracleSpec.instFiniteRangeSumAppend {ι₁ : Type u} {ι₂ : Type u'} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) [h₁ : spec₁.FiniteRange] [h₂ : spec₂.FiniteRange] : (spec₁ ++ₒ spec₂).FiniteRange

@[reducible, inline]

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

Reduce the indexing set by pulling back along some map 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.

def «term[]ₒ» : Lean.ParserDescr

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

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

instance instDecidableEqPEmptyEmptySpec : []ₒ.DecidableEq

instance instFiniteRangePEmptyEmptySpec : []ₒ.FiniteRange

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

def «term_→ₒ_» : Lean.TrailingParserDescr

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

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

@[reducible, inline]

def coinSpec : OracleSpec Unit

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

instance instDecidableEqUnitCoinSpec : coinSpec.DecidableEq

instance instFiniteRangeUnitCoinSpec : coinSpec.FiniteRange

def unifSpec' : OracleSpec (Type u)

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

def probSpec : OracleSpec ℕ

instance instDecidableEqNatUnifSpec : unifSpec.DecidableEq

instance instFiniteRangeNatUnifSpec : unifSpec.FiniteRange