Documentation

VCVio.OracleComp.SimSemantics.SimulateQ

Simulation Semantics for Oracles in a Computation #

source
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.

Instances For
    source
    @[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
    source
    @[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)
    source
    @[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.

    Instances For
      source
      @[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
      source
      @[simp]
      theorem simulateQ_spec_query {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (t : spec.Domain) :
      simulateQ impl (liftM (OracleSpec.query t)) = impl t

      Specialized form of simulateQ_query for the canonical spec.query t constructor: simulateQ impl (liftM (spec.query t)) = impl t.

      The general simulateQ_query rewrite leaves an id <$> artifact when applied to spec.query t (because (spec.query t).cont = id). That artifact is harmless when spec.Range t is concrete (it disappears under definitional reduction), but in parametric sum-spec contexts ((E₁ + E₂).Range (Sum.inl t) vs E₁.Range t, both abstract atoms) the type annotations diverge and id_map no longer fires under simp only. This lemma sidesteps the artifact entirely and is the canonical entry point for simplifying simulateQ over an explicit spec.query t.

      source
      @[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))
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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'
      source
      @[simp]
      theorem simulateQ_liftTarget {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {m : Type u → Type v} {n : Type u → Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] (impl : QueryImpl spec m) (comp : OracleComp spec α) :
      simulateQ (QueryImpl.liftTarget n impl) comp = liftM (simulateQ impl comp)
      source
      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
      source
      @[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.

      source
      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.

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

      source
      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.

      source
      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.

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