Simulation using WriterT Monad Transformers #
Lemmas about simulateQ with output monad WriterT ω (OracleComp spec) for some ω
Note we only handle monoid version of WriterT, append should be added eventually.
theorem
OracleComp.fst_map_writerT_run_simulateQ
{ι : Type u}
{spec : OracleSpec ι}
{α ω : Type u}
[Monoid ω]
{so : QueryImpl spec (WriterT ω (OracleComp spec))}
(hso : ∀ (t : spec.Domain), Prod.fst <$> (so t).run = liftM (query t))
(oa : OracleComp spec α)
:
Taking the first component of the WriterT output recovers the original computation, when the query implementation preserves the underlying oracle behavior (hso).
theorem
OracleComp.NeverFail_writerT_run_simulateQ_iff
{ι : Type u}
{spec : OracleSpec ι}
{α ω : Type u}
[Monoid ω]
[spec.Fintype]
[spec.Inhabited]
{so : QueryImpl spec (WriterT ω (OracleComp spec))}
(oa : OracleComp spec α)
: