Simulation Semantics for Oracles in a Computation

def simulateQ {ι : Type u_1} {spec : OracleSpec ι} {r : Type u → Type u_2} [Monad r] (impl : QueryImpl spec r) {α : Type u} (mx : OracleComp spec α) : r α

Given an implementation of spec in the monad r, convert an OracleComp spec α to a implementation in r α by substituting impl t for query t throughout.

@[simp]

theorem simulateQ_pure {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (x : α) : simulateQ impl (pure x) = pure x

@[simp]

theorem simulateQ_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : α → OracleComp spec β) : simulateQ impl (mx >>= my) = do let x ← simulateQ impl mx simulateQ impl (my x)

@[reducible]

def simulateQ' {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] [LawfulMonad r] (impl : QueryImpl spec r) : OracleComp spec →ᵐ r

Version of simulateQ that bundles into a monad hom.

@[simp]

theorem simulateQ_query {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (q : OracleQuery spec α) : simulateQ impl (liftM q) = q.cont <$> impl q.input

@[simp]

theorem simulateQ_query_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (q : OracleQuery spec α) (ou : α → OracleComp spec β) : simulateQ impl (liftM q >>= ou) = do let u ← liftM (impl q.input) simulateQ impl (ou (q.cont u))

@[simp]

theorem simulateQ_map {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (f : α → β) : simulateQ impl (f <$> mx) = f <$> simulateQ impl mx

@[simp]

theorem simulateQ_seq {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (og : OracleComp spec (α → β)) (mx : OracleComp spec α) : simulateQ impl (og <*> mx) = simulateQ impl og <*> simulateQ impl mx

@[simp]

theorem simulateQ_seqLeft {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : OracleComp spec β) : simulateQ impl (mx <* my) = simulateQ impl mx <* simulateQ impl my

@[simp]

theorem simulateQ_seqRight {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : OracleComp spec β) : simulateQ impl (mx *> my) = simulateQ impl mx *> simulateQ impl my

@[simp]

theorem simulateQ_ite {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (p : Prop) [Decidable p] (mx mx' : OracleComp spec α) : simulateQ impl (if p then mx else mx') = if p then simulateQ impl mx else simulateQ impl mx'

theorem simulateQ_def {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OracleComp spec α) : simulateQ impl mx = (fun {α : Type u} (x : spec.toPFunctor.FreeM α) => (PFunctor.FreeM.mapMHom impl).toFun α x) mx

@[simp]

theorem simulateQ_id' {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} (mx : OracleComp spec α) : simulateQ (QueryImpl.id' spec) mx = mx

QueryImpl.id' is an identity for simulateQ with implementaiton in OracleComp spec.

theorem simulateQ_ofLift_eq_self {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (mx : OracleComp spec α) : simulateQ (QueryImpl.ofLift spec (OracleComp spec)) mx = mx

Lifting queries to their original implementation has no effect on a computation.

@[simp]

theorem simulateQ_option_elim {α β : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] (impl : QueryImpl spec n) (x : Option α) (my : OracleComp spec β) (my' : α → OracleComp spec β) : simulateQ impl (x.elim my my') = x.elim (simulateQ impl my) fun (x : α) => simulateQ impl (my' x)

@[simp]

theorem simulateQ_option_elimM {α β : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OracleComp spec (Option α)) (my : OracleComp spec β) (my' : α → OracleComp spec β) : simulateQ impl (Option.elimM mx my my') = Option.elimM (simulateQ impl mx) (simulateQ impl my) fun (x : α) => simulateQ impl (my' x)

theorem simulateQ_optionT_bind' {α β : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OptionT (OracleComp spec) α) (f : α → OptionT (OracleComp spec) β) : simulateQ impl (mx >>= f).run = do let a ← simulateQ impl mx.run simulateQ impl (f a).run

simulateQ distributes through OptionT.bind, stated via OptionT.run.

theorem simulateQ_optionT_bind'' {α β : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OptionT (OracleComp spec) α) (f : α → OptionT (OracleComp spec) β) : simulateQ impl (mx >>= f).run = Option.elimM (simulateQ impl mx.run) (pure none) fun (a : α) => simulateQ impl (f a).run

simulateQ distributes through OptionT.bind, stated via Option.elimM.

theorem simulateQ_optionT_bind {α β : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OptionT (OracleComp spec) α) (f : α → OptionT (OracleComp spec) β) : simulateQ impl (mx >>= f) = do let a ← simulateQ impl mx simulateQ impl (f a)

simulateQ distributes through OptionT.bind: the simulated OptionT-bind is the OptionT-bind of the simulated pieces.

@[simp]

theorem simulateQ_optionT_lift {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (comp : OracleComp spec α) : simulateQ impl (OptionT.lift comp) = OptionT.lift (simulateQ impl comp)

simulateQ commutes with OptionT.lift.