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 (OracleQuery spec) (OracleQuery superSpec) : Type (max (max (max u (u_1 + 1)) v) w)

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} : OracleQuery spec α → OracleQuery superSpec α
• liftM_map {α β : Type u_1} (q : OracleQuery spec α) (f : α → β) : liftM (f <$> q) = f <$> liftM q

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))

def OracleSpec.SubSpec.trans {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {κ : Type w'} {spec₃ : OracleSpec κ} (h₁ : spec ⊂ₒ superSpec) (h₂ : superSpec ⊂ₒ spec₃) : spec ⊂ₒ spec₃

Transitivity for SubSpec: if spec₁ ⊂ₒ spec₂ and spec₂ ⊂ₒ spec₃, then spec₁ ⊂ₒ spec₃.

Equations

• h₁.trans h₂ = { monadLift := fun {α : Type ?u.48} (q : OracleQuery spec α) => MonadLift.monadLift (MonadLift.monadLift q), liftM_map := ⋯ }

class OracleSpec.LawfulSubSpec {ι : Type u} {τ : Type v} (spec : OracleSpec ι) (superSpec : OracleSpec τ) [h : spec ⊂ₒ superSpec] : Prop

LawfulSubSpec extends SubSpec with the requirement that lifting preserves distributions. The axiom requires that the continuation of each lifted query is a bijection from the super-range to the sub-range, which guarantees that the uniform distribution is preserved under the mapping.

• cont_bijective (t : spec.Domain) : Function.Bijective (MonadLift.monadLift (OracleQuery.query t)).snd

theorem OracleSpec.LawfulSubSpec.evalDist_liftM_query {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] [superSpec.Fintype] [superSpec.Inhabited] [spec.Fintype] [spec.Inhabited] (t : spec.Domain) : PMF.map (MonadLift.monadLift (OracleQuery.query t)).snd (PMF.uniformOfFintype (superSpec.Range (MonadLift.monadLift (OracleQuery.query t)).fst)) = PMF.uniformOfFintype (spec.Range t)

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

Lift a computation from spec to superSpec using a SubSpec instance on queries. Usually liftM should be preferred but this can allow more explicit annotation.

Equations

• mx.liftComp superSpec = simulateQ (fun (t : spec.Domain) => liftM (OracleQuery.query t)) mx

theorem OracleComp.liftComp_def {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (mx : OracleComp spec α) : mx.liftComp superSpec = simulateQ (fun (t : spec.Domain) => liftM (query t)) mx

@[simp]

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

@[simp]

theorem OracleComp.liftComp_query {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (q : OracleQuery spec α) : (liftM q).liftComp superSpec = q.cont <$> liftM (query q.input)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem OracleComp.evalDist_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [spec.Fintype] [spec.Inhabited] [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) : evalDist (mx.liftComp superSpec) = evalDist mx

@[simp]

theorem OracleComp.probOutput_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [spec.Fintype] [spec.Inhabited] [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) (x : α) : Pr[=x | mx.liftComp superSpec] = Pr[=x | mx]

@[simp]

theorem OracleComp.probEvent_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [spec.Fintype] [spec.Inhabited] [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) (p : α → Prop) : Pr[p | mx.liftComp superSpec] = Pr[p | mx]

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

Extend a lifting on OracleQuery to a lifting on OracleComp.

Equations

• OracleComp.instMonadLiftTOfOracleQuery = { monadLift := fun {α : Type ?u.29} (mx : OracleComp spec α) => mx.liftComp superSpec }

@[simp]

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

We choose to actively rewrite liftComp as liftM to enable LawfulMonadLift lemmas.

instance OracleComp.instLawfulMonadLiftT {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] : LawfulMonadLiftT (OracleComp spec) (OracleComp superSpec)

@[simp]

theorem OracleComp.monadLift_eq_self {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (mx : OracleComp spec α) : monadLift mx = mx

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

Equations

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

@[simp]

theorem OracleComp.liftM_OptionT_eq {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] (mx : OptionT (OracleComp spec) α) : liftM mx = have impl := fun (t : spec.Domain) => liftM (query t); simulateQ impl mx

@[simp]

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

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

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

Equations

• OracleComp.instMonadLiftStateTOfOracleQuery = { monadLift := fun {α : Type ?u.36} (mx : StateT σ (OracleComp spec) α) => StateT.mk fun (s : σ) => (mx.run s).liftComp superSpec }

@[simp]

theorem OracleComp.liftM_StateT_eq {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α σ : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] (mx : StateT σ (OracleComp spec) α) : liftM mx = StateT.mk fun (s : σ) => liftM (mx.run s)