Query Implementations with State Monads #
This file gives lemmas about QueryImpl spec m when m is something like StateT σ n.
TODO: should generalize things to MonadState once laws for it exist.
def
QueryImpl.prodStateT
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{spec₁ : OracleSpec ι₁}
{spec₂ : OracleSpec ι₂}
{m : Type (max u_3 u_4) → Type u_5}
[Functor m]
{σ₁ σ₂ : Type (max u_3 u_4)}
(impl₁ : QueryImpl spec₁ (StateT σ₁ m))
(impl₂ : QueryImpl spec₂ (StateT σ₂ m))
:
Given implementations for oracles in spec₁ and spec₂ in terms of state monads for
two different contexts σ₁ and σ₂, implement the combined set spec₁ + spec₂ in terms
of a combined σ₁ × σ₂ state.
Equations
Instances For
def
QueryImpl.piStateT
{τ : Type}
[DecidableEq τ]
{ι : τ → Type u_1}
{spec : (t : τ) → OracleSpec (ι t)}
{m : Type (max u_2 u_3) → Type u_4}
[Monad m]
{σ : τ → Type (max u_2 u_3)}
(impl : (t : τ) → QueryImpl (spec t) (StateT (σ t) m))
:
QueryImpl (OracleSpec.sigma spec) (StateT ((t : τ) → σ t) m)
Indexed version of QueryImpl.prodStateT. Note that m cannot vary with t.
dtumad: The Function.update thing is nice but forces DecidableEq.
Equations
Instances For
theorem
OracleComp.StateT_run_simulateQ_eq_map_run'_simulateQ
{ι : Type u_1}
{spec : OracleSpec ι}
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
{σ : Type u}
(so : QueryImpl spec (StateT σ m))
{α : Type u}
[Subsingleton σ]
(oa : OracleComp spec α)
(s s' : σ)
:
If the state type is Subsingleton, then we can represent simulation in terms of simulate',
adding back any state at the end of the computation.
theorem
OracleComp.StateT_run'_simulateQ_eq_self
{ι : Type u_1}
{spec : OracleSpec ι}
{σ α : Type u}
(so : QueryImpl spec (StateT σ (OracleComp spec)))
(h : ∀ (t : spec.Domain) (s : σ), (so t).run' s = liftM (query t))
(oa : OracleComp spec α)
(s : σ)
: