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 : ∀ {α : Type u} (q : spec.OracleQuery α), Prod.fst <$> (so.impl q).run = liftM q) (oa : OracleComp spec α) : Prod.fst <$> (simulateQ so oa).run = oa

theorem OracleComp.probFailure_writerT_run_simulateQ {ι : Type u} {spec : OracleSpec ι} {α ω : Type u} [Monoid ω] [spec.FiniteRange] {so : QueryImpl spec (WriterT ω (OracleComp spec))} (hso : ∀ {α : Type u} (q : spec.OracleQuery α), Prod.fst <$> (so.impl q).run = liftM q) (hso' : ∀ {α : Type u} (q : spec.OracleQuery α), [⊥|(so.impl q).run] = 0) (oa : OracleComp spec α) : [⊥|(simulateQ so oa).run] = [⊥|oa]

theorem OracleComp.neverFails_writerT_run_simulateQ_iff {ι : Type u} {spec : OracleSpec ι} {α ω : Type u} [Monoid ω] {so : QueryImpl spec (WriterT ω (OracleComp spec))} (hso : ∀ {α : Type u} (q : spec.OracleQuery α), (Prod.fst <$> (so.impl q).run).support = ⊤) (hso' : ∀ {α : Type u} (q : spec.OracleQuery α), (so.impl q).run.neverFails) (oa : OracleComp spec α) : (simulateQ so oa).run.neverFails ↔ oa.neverFails