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 α

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

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.

theorem OracleComp.liftComp_def {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLift (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 : MonadLift (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 : MonadLift (OracleQuery spec) (OracleQuery superSpec)] (q : OracleQuery spec α) : (liftM q).liftComp superSpec = liftM q

@[simp]

theorem OracleComp.liftComp_bind {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLift (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 : MonadLift (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 : MonadLift (OracleQuery spec) (OracleQuery superSpec)] (og : OracleComp spec (α → β)) (mx : OracleComp spec α) : (og <*> mx).liftComp superSpec = og.liftComp superSpec <*> mx.liftComp superSpec

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

Extend a lifting on OracleQuery to a lifting on OracleComp.

@[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.instLawfulMonadLift {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : LawfulMonadLift (OracleComp spec) (OracleComp superSpec)

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

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

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

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