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.

theorem OracleComp.StateT_run_simulateQ_eq_map_run'_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [AlternativeMonad m] [LawfulAlternative m] {σ : Type u} [Subsingleton σ] (so : QueryImpl spec (StateT σ m)) {α : Type u} (oa : OracleComp spec α) (s s' : σ) : (simulateQ so oa).run s = (fun (x : α) => (x, s')) <$> (simulateQ so oa).run' 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} [Subsingleton σ] {α : Type u} (so : QueryImpl spec (StateT σ (OracleComp spec))) (h : ∀ (α : Type u) (q : spec.OracleQuery α) (s : σ), (so.impl q).run' s = liftM q) (oa : OracleComp spec α) (s : σ) : (simulateQ so oa).run' s = oa