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.

@[implicit_reducible]

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.

@[reducible]

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

Typeclass data on indices and answer types

Domain and Range are reducible, so a global instance concluding C spec.Domain or C (spec.Range t) for a generic spec is indexed as C ι, respectively C (?spec ?t): a candidate for every C _ goal, with spec undetermined. Instance search then invents a specification through ofFn, and either times out (VCVio#772) or answers an ordinary DecidableEq, Fintype, or Inhabited goal through oracle-specification data. The only such instances left are the fintype and inhabited projections of the retiring IsUniformSpec. Index equality is an ordinary [DecidableEq ι] hypothesis, and data on answer types are ordinary [DecidableEq (spec.Range t)], [Fintype (spec.Range t)], or [Inhabited (spec.Range t)] hypotheses, quantified over t when a statement ranges over arbitrary queries. Specifications built with ofFn reduce to their answer types, so unifSpec, coinSpec, and A →ₒ B need no instances of their own; + combines the per-branch instances of its summands.

@[reducible, always_inline]

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

def OracleSpec.singletonSpec : Lean.TrailingParserDescr

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

The ordinary instance reducibility assigned by the instance command lets its HAdd.hAdd projection reduce while checking dependent implicit types such as (spec₁ + spec₂).Range (.inl t), without unfolding combined specifications during ordinary reducible-transparency tactic matching.

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

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

Deliberately not @[simp]: toPFunctor occurs inside the (instance-carrying) type of an OracleComp, so rewriting with this under a simulateQ/liftM strands the goal in a form the simulateQ_query family can no longer match.

@[simp]

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

The answer types of a sum specification inherit the per-branch instances of its summands. These are indexed on the HAdd.hAdd head of the combined specification, so they apply only to goals about a sum.

@[instance_reducible]

instance OracleSpec.instFintypeRangeSumHAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [h : (t : ι) → Fintype (spec.Range t)] [h' : (t : ι') → Fintype (spec'.Range t)] (t : ι ⊕ ι') : Fintype ((spec + spec').Range t)

@[instance_reducible]

instance OracleSpec.instDecidableEqRangeSumHAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [h : (t : ι) → DecidableEq (spec.Range t)] [h' : (t : ι') → DecidableEq (spec'.Range t)] (t : ι ⊕ ι') : DecidableEq ((spec + spec').Range t)

@[instance_reducible]

instance OracleSpec.instInhabitedRangeSumHAdd {ι : Type u_1} {ι' : Type u_2} (spec : OracleSpec ι) (spec' : OracleSpec ι') [h : (t : ι) → Inhabited (spec.Range t)] [h' : (t : ι') → Inhabited (spec'.Range t)] (t : ι ⊕ ι') : Inhabited ((spec + spec').Range t)

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)

@[instance_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 u} {ι' : Type u'} (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.