Coercions Between Computations With Additional Oracles

This file defines a isSubSpec relation for pairs of oracleSpec where one can be thought of as an extension of the other with additional oracles. The definition consists is a thin wrapper around a MonadLift instance on OracleQuery, which extends to a lifting operation on OracleComp.

We use the notation spec ⊂ₒ spec' to represent that one set of oracles is a subset of another, where the non-inclusive subset symbol reflects that we avoid defining this instance reflexively.

class OracleSpec.SubSpec {ι : Type u} {τ : Type v} (spec : OracleSpec ι) (superSpec : OracleSpec τ) extends MonadLift spec.OracleQuery superSpec.OracleQuery : Type (max (max u (u_1 + 1)) v)

Relation defining an inclusion of one set of oracles into another, where the mapping doesn't affect the underlying probability distribution of the computation. Informally, spec ⊂ₒ superSpec means that for any query to an oracle of sub_spec, it can be perfectly simulated by a computation using the oracles of superSpec.

We avoid implementing this via the built-in subset notation as we care about the actual data of the mapping rather than just its existence, which is needed when defining type coercions.

• monadLift {α : Type u_1} : spec.OracleQuery α → superSpec.OracleQuery α

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

Equations

• OracleSpec.«term_⊂ₒ_» = Lean.ParserDescr.trailingNode `OracleSpec.«term_⊂ₒ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊂ₒ ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem OracleSpec.SubSpec.liftM_query_eq_liftM_liftM {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (q : spec.OracleQuery α) : liftM q = liftM (liftM q)

theorem OracleSpec.SubSpec.evalDist_lift_query {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [superSpec.FiniteRange] [Fintype α] [Nonempty α] (q : spec.OracleQuery α) : (liftM (liftM q)).evalDist = OptionT.lift (PMF.uniformOfFintype α)

@[simp]

theorem OracleSpec.SubSpec.evalDist_liftM {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [superSpec.FiniteRange] [Fintype α] [Nonempty α] (q : spec.OracleQuery α) : (liftM q).evalDist = OptionT.lift (PMF.uniformOfFintype α)

@[simp]

theorem OracleSpec.SubSpec.supportWhen_monadLift {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (q : spec.OracleQuery α) (poss : {α : Type w} → superSpec.OracleQuery α → Set α) : ((liftM q).supportWhen fun {α : Type w} => poss) = poss (liftM q)

@[simp]

theorem OracleSpec.SubSpec.support_toFun {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (q : spec.OracleQuery α) : (liftM (MonadLift.monadLift q)).support = Set.univ

@[simp]

theorem OracleSpec.SubSpec.finSupport_toFun {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [spec.DecidableEq] [superSpec.DecidableEq] [superSpec.FiniteRange] [DecidableEq α] [Fintype α] (q : spec.OracleQuery α) : (liftM (MonadLift.monadLift q)).finSupport = Finset.univ

@[simp]

theorem OracleSpec.SubSpec.probOutput_toFun {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [superSpec.FiniteRange] [Fintype α] (q : spec.OracleQuery α) (u : α) : [=u|liftM (MonadLift.monadLift q)] = (↑(Fintype.card α))⁻¹

@[simp]

theorem OracleSpec.SubSpec.probEvent_toFun {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [superSpec.FiniteRange] [Fintype α] (q : spec.OracleQuery α) (p : α → Prop) [DecidablePred p] : [p|liftM (MonadLift.monadLift q)] = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card α)

def OracleComp.liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (oa : OracleComp spec α) (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] : OracleComp superSpec α

Lift a computation from spec to superSpec using a SubSpec instance on queries.

Equations

• oa.liftComp superSpec = OracleComp.simulateQ { impl := fun {α : Type ?u.14} => liftM } oa

theorem OracleComp.liftComp_def {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (oa : OracleComp spec α) : oa.liftComp superSpec = simulateQ { impl := fun {α : Type w} => liftM } oa

@[simp]

theorem OracleComp.liftComp_pure {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (x : α) : (pure x).liftComp superSpec = pure x

@[simp]

theorem OracleComp.liftComp_query {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (q : spec.OracleQuery α) : (liftM q).liftComp superSpec = liftM q

@[simp]

theorem OracleComp.liftComp_bind {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (oa : OracleComp spec α) (ob : α → OracleComp spec β) : (oa >>= ob).liftComp superSpec = do let x ← oa.liftComp superSpec (ob x).liftComp superSpec

@[simp]

theorem OracleComp.liftComp_failure {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] : failure.liftComp superSpec = failure

@[simp]

theorem OracleComp.liftComp_map {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (oa : OracleComp spec α) (f : α → β) : (f <$> oa).liftComp superSpec = f <$> oa.liftComp superSpec

@[simp]

theorem OracleComp.liftComp_seq {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (og : OracleComp spec (α → β)) (oa : OracleComp spec α) : (og <*> oa).liftComp superSpec = og.liftComp superSpec <*> oa.liftComp superSpec

@[simp]

theorem OracleComp.evalDist_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [spec.FiniteRange] [superSpec.FiniteRange] (oa : OracleComp spec α) : (oa.liftComp superSpec).evalDist = oa.evalDist

Lifting a computation to a different set of oracles doesn't change the output distribution, since evalDist assumes uniformly random queries.

@[simp]

theorem OracleComp.support_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [spec.FiniteRange] [superSpec.FiniteRange] (oa : OracleComp spec α) : (oa.liftComp superSpec).support = oa.support

@[simp]

theorem OracleComp.finSupport_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [spec.DecidableEq] [superSpec.DecidableEq] [DecidableEq α] [spec.FiniteRange] [superSpec.FiniteRange] (oa : OracleComp spec α) : (oa.liftComp superSpec).finSupport = oa.finSupport

@[simp]

theorem OracleComp.probOutput_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [spec.FiniteRange] [superSpec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|oa.liftComp superSpec] = [=x|oa]

@[simp]

theorem OracleComp.probEvent_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] [spec.FiniteRange] [superSpec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : [p|oa.liftComp superSpec] = [p|oa]

@[simp]

theorem OracleComp.neverFails_lift_comp_iff {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift spec.OracleQuery superSpec.OracleQuery] (oa : OracleComp spec α) : (oa.liftComp superSpec).neverFails ↔ oa.neverFails

instance OracleComp.instMonadLiftOfOracleQuery {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLift spec.OracleQuery superSpec.OracleQuery] : MonadLift (OracleComp spec) (OracleComp superSpec)

Extend a lifting on OracleQuery to a lifting on OracleComp.

Equations

• OracleComp.instMonadLiftOfOracleQuery = { monadLift := fun {α : Type ?u.45} (oa : OracleComp spec α) => oa.liftComp superSpec }

@[simp]

theorem OracleComp.liftM_eq_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [MonadLift spec.OracleQuery superSpec.OracleQuery] (oa : OracleComp spec α) : liftM oa = oa.liftComp superSpec