Basic Constructions of Simulation Oracles

This file defines a number of basic simulation oracles, as well as operations to combine them.

def QueryImpl.compose {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {m : Type u → Type v} [AlternativeMonad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) : QueryImpl spec m

Given an implementation of spec in terms of a new set of oracles spec', and an implementation of spec' in terms of arbitrary m, implement spec in terms of m.

Equations

• so'∘ₛso = { impl := fun {α : Type ?u.60} (q : spec.OracleQuery α) => OracleComp.simulateQ so' (so.impl q) }

def QueryImpl.«term_∘ₛ_» : Lean.TrailingParserDescr

Equations

• QueryImpl.«term_∘ₛ_» = Lean.ParserDescr.trailingNode `QueryImpl.«term_∘ₛ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∘ₛ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem QueryImpl.apply_compose {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type u} {m : Type u → Type v} [AlternativeMonad m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (q : spec.OracleQuery α) : (so'∘ₛso).impl q = OracleComp.simulateQ so' (so.impl q)

@[simp]

theorem QueryImpl.simulateQ_compose {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α : Type u} {m : Type u → Type v} [AlternativeMonad m] [LawfulMonad m] [LawfulAlternative m] (so' : QueryImpl spec' m) (so : QueryImpl spec (OracleComp spec')) (oa : OracleComp spec α) : OracleComp.simulateQ (so'∘ₛso) oa = OracleComp.simulateQ so' (OracleComp.simulateQ so oa)

def QueryImpl.equivState {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) : QueryImpl spec (StateT τ (OracleComp spec'))

Substitute an equivalent type for the state of a simulation oracle, by using the equivalence to move back and forth between the states as needed. This can be useful when operations such like simOracle.append add on a state of type Unit. TODO: this should really exist on the StateT level probably instead.

Equations

• so.equivState e = { impl := fun {α : Type ?u.64} (q : spec.OracleQuery α) (s : τ) => Prod.map id ⇑e <$> so.impl q (e.symm s) }

@[simp]

theorem QueryImpl.equivState_apply {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) (q : spec.OracleQuery α) : (so.equivState e).impl q = fun (s : τ) => Prod.map id ⇑e <$> so.impl q (e.symm s)

@[simp]

theorem QueryImpl.equivState_subsingleton {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) [Subsingleton σ] (e : σ ≃ σ) : so.equivState e = so

Masking a Subsingleton state has no effect, since the new state elements look the same.

@[simp]

theorem QueryImpl.equivState_equivState {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec'))) (e : σ ≃ τ) : (so.equivState e).equivState e.symm = so

def unifOracle {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] : QueryImpl spec ProbComp

Simulation oracle for replacing queries with uniform random selection, using unifSpec. The resulting computation is still identical under evalDist. The relevant OracleSpec can usually be inferred automatically, so we leave it implicit.

Equations

• unifOracle = { impl := fun {α : Type} (x : spec.OracleQuery α) => match α, x with | .(spec.range i), OracleSpec.query i t => $ᵗspec.range i }

@[simp]

theorem unifOracle.apply_eq {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} (q : spec.OracleQuery α) : unifOracle.impl q = match α, q with | .(spec.range i), OracleSpec.query i t => $ᵗspec.range i

@[simp]

theorem unifOracle.evalDist_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] (oa : OracleComp spec α) : (OracleComp.simulateQ unifOracle oa).evalDist = oa.evalDist

@[simp]

theorem unifOracle.support_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} (oa : OracleComp spec α) : OracleComp.support (OracleComp.simulateQ unifOracle oa) = oa.support

@[simp]

theorem unifOracle.finSupport_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (oa : OracleComp spec α) : OracleComp.finSupport (OracleComp.simulateQ unifOracle oa) = oa.finSupport

@[simp]

theorem unifOracle.probOutput_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|OracleComp.simulateQ unifOracle oa] = [=x|oa]

@[simp]

theorem unifOracle.probEvent_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → OracleComp.SelectableType (spec.range i)] {α : Type} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : [p|OracleComp.simulateQ unifOracle oa] = [p|oa]