Simulation Semantics through OptionT Handlers

Distributivity lemmas for simulateQ over OptionT-shaped operations (Option.elim, Option.elimM, OptionT.bind, OptionT.lift).

These lemmas appeal to the central simulateQ theory in VCVio.OracleComp.SimSemantics.SimulateQ; the file is grouped under SimSemantics/OptionT/ to mirror the per-transformer organization used for StateT, WriterT, and ReaderT.

@[simp]

theorem simulateQ_option_elim {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [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)

@[simp]

theorem simulateQ_option_elimM {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [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)

theorem simulateQ_optionT_bind' {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [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.

theorem simulateQ_optionT_bind'' {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [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.

theorem simulateQ_optionT_bind {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [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.

@[simp]

theorem simulateQ_optionT_lift {α : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [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.

mapM over OptionT

When every step of a mapM resolves to pure (some _) under simulateQ, the whole mapM resolves to pure (some _) of the pointwise mapped collection. These are the List and Vector companions to simulateQ_optionT_bind' / simulateQ_optionT_lift.

theorem simulateQ_optionT_list_mapM_pure {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (f : α → OptionT (OracleComp spec) β) (g : α → β) (l : List α) (hfg : ∀ (x : α), simulateQ impl (f x) = pure (some (g x))) : simulateQ impl (List.mapM f l) = pure (some (List.map g l))

simulateQ over List.mapM in OptionT: when each step is pure (some (g x)) under simulateQ, the whole mapM is pure (some (l.map g)).

theorem simulateQ_optionT_mapM_pure {α β : Type u} {ι : Type u_3} {spec : OracleSpec ι} {n : Type u → Type u_2} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) {k : ℕ} (f : α → OptionT (OracleComp spec) β) (g : α → β) (xs : Vector α k) (hfg : ∀ (x : α), simulateQ impl (f x) = pure (some (g x))) : simulateQ impl (Vector.mapM f xs) = pure (some (Vector.map g xs))

simulateQ over Vector.mapM in OptionT: when each step is pure (some (g x)) under simulateQ, the whole mapM is pure (some (xs.map g)).