Composition and instrumentation of oracle handlers

preInsert and postInsert attach per-query effects before answering or after successful answers. Projections that preserve monadic composition transfer the resulting executions, supports, and finite supports.

@[reducible, inline]

abbrev QueryImpl.preInsert {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (so : QueryImpl spec m) (nx : spec.Domain → n α) : QueryImpl spec n

Oracle-facing compatibility alias for PFunctor.Handler.preInsert.

theorem QueryImpl.preInsert_apply {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} [LawfulMonad n] (so : QueryImpl spec m) (nx : spec.Domain → n α) (t : spec.Domain) : so.preInsert nx t = do let _ ← nx t liftM (so t)

theorem QueryImpl.simulateQ_preInsert_query {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} [LawfulMonad n] (so : QueryImpl spec m) (nx : spec.Domain → n α) (t : spec.Domain) : simulateQ (so.preInsert nx) (query t) = do let _ ← nx t liftM (so t)

One-step characterisation of simulateQ (preInsert so nx) on a single query.

theorem QueryImpl.simulateQ_preInsert.induct {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [Monad m] [LawfulMonad m] [LawfulMonad n] (so : QueryImpl spec m) (nx : spec.Domain → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.preInsert nx t) = so t) {motive : OracleComp spec β → m β → Prop} (h_pure : ∀ (x : β), motive (pure x) (pure x)) (h_query_bind : ∀ (t : spec.Domain) (k : spec.Range t → OracleComp spec β) (k' : spec.Range t → m β), (∀ (u : spec.Range t), motive (k u) (k' u)) → motive (query t >>= k) (so t >>= k')) (oa : OracleComp spec β) : motive oa (proj (simulateQ (so.preInsert nx) oa))

Induction principle for proj (simulateQ (so.preInsert nx) oa) parametric in a motive OracleComp spec β → m β → Prop. The recursion structure of proj_simulateQ_preInsert is exposed as two cases mirroring OracleComp.inductionOn: in pure x the projected term reduces to pure x, and in query t >>= k it reduces to so t >>= k' for some continuation k' u = proj (simulateQ (so.preInsert nx) (k u)). Tagged @[elab_as_elim] so it is usable as induction oa using simulateQ_preInsert.induct.

theorem QueryImpl.proj_simulateQ_preInsert {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [Monad m] [LawfulMonad m] [LawfulMonad n] (so : QueryImpl spec m) (nx : spec.Domain → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.preInsert nx t) = so t) (oa : OracleComp spec β) : proj (simulateQ (so.preInsert nx) oa) = simulateQ so oa

Generic strip lemma: given a monad-morphism-style projection proj : ∀ {γ}, n γ → m γ that preserves pure and bind and discards the inserted side effect on each query, simulating with preInsert so nx and projecting back recovers simulateQ so. The proof is the canonical use of simulateQ_preInsert.induct: the parametric motive is instantiated to the equality with simulateQ so oa, leaving trivial cases.

theorem QueryImpl.simulateQ_preInsert_const_pure {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [Monad m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] (so : QueryImpl spec m) (x : α) (oa : OracleComp spec β) : simulateQ (so.preInsert fun (x_1 : spec.Domain) => pure x) oa = liftM (simulateQ so oa)

When nx is constantly pure x, preInsert so nx is the lift of so and the resulting simulation equals the lifted underlying simulation. Generic analogue of the run_simulateQ_withTraceBefore_const_one no-op identity.

theorem QueryImpl.support_proj_simulateQ_preInsert {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [Monad m] [LawfulMonad m] [LawfulMonad n] [MonadAttach m] (so : QueryImpl spec m) (nx : spec.Domain → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.preInsert nx t) = so t) (oa : OracleComp spec β) : support (proj (simulateQ (so.preInsert nx) oa)) = support (simulateQ so oa)

theorem QueryImpl.finSupport_proj_simulateQ_preInsert {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [Monad m] [LawfulMonad m] [LawfulMonad n] [MonadAttach m] [HasEvalFinset m] [DecidableEq β] (so : QueryImpl spec m) (nx : spec.Domain → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.preInsert nx t) = so t) (oa : OracleComp spec β) : finSupport (proj (simulateQ (so.preInsert nx) oa)) = finSupport (simulateQ so oa)

@[reducible, inline]

abbrev QueryImpl.postInsert {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} (so : QueryImpl spec m) {α : Type u} (nx : (t : spec.Domain) → spec.Range t → n α) : QueryImpl spec n

Oracle-facing compatibility alias for PFunctor.Handler.postInsert.

theorem QueryImpl.postInsert_apply {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (so : QueryImpl spec m) (nx : (t : spec.Domain) → spec.Range t → n α) (t : spec.Domain) : so.postInsert nx t = do let u ← liftM (so t) let _ ← nx t u pure u

theorem QueryImpl.simulateQ_postInsert_query {m : Type u → Type v} {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} [LawfulMonad n] (so : QueryImpl spec m) (nx : (t : spec.Domain) → spec.Range t → n α) (t : spec.Domain) : simulateQ (so.postInsert nx) (query t) = do let u ← liftM (so t) let _ ← nx t u pure u

One-step characterisation of simulateQ (postInsert so nx) on a single query.

theorem QueryImpl.simulateQ_postInsert.induct {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [LawfulMonad m] [LawfulMonad n] (so : QueryImpl spec m) (nx : (t : spec.Domain) → spec.Range t → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.postInsert nx t) = so t) {motive : OracleComp spec β → m β → Prop} (h_pure : ∀ (x : β), motive (pure x) (pure x)) (h_query_bind : ∀ (t : spec.Domain) (k : spec.Range t → OracleComp spec β) (k' : spec.Range t → m β), (∀ (u : spec.Range t), motive (k u) (k' u)) → motive (query t >>= k) (so t >>= k')) (oa : OracleComp spec β) : motive oa (proj (simulateQ (so.postInsert nx) oa))

Induction principle for proj (simulateQ (so.postInsert nx) oa) parametric in a motive OracleComp spec β → m β → Prop. The recursion structure of proj_simulateQ_postInsert is exposed as two cases mirroring OracleComp.inductionOn: in pure x the projected term reduces to pure x, and in query t >>= k it reduces to so t >>= k' for some continuation k' u = proj (simulateQ (so.postInsert nx) (k u)). Tagged @[elab_as_elim] so it is usable as induction oa using simulateQ_postInsert.induct.

theorem QueryImpl.proj_simulateQ_postInsert {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [LawfulMonad m] [LawfulMonad n] (so : QueryImpl spec m) (nx : (t : spec.Domain) → spec.Range t → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.postInsert nx t) = so t) (oa : OracleComp spec β) : proj (simulateQ (so.postInsert nx) oa) = simulateQ so oa

Generic strip lemma: given a monad-morphism-style projection proj : ∀ {γ}, n γ → m γ that preserves pure and bind and discards the inserted side effect on each query, simulating with postInsert so nx and projecting back recovers simulateQ so. The proof is the canonical use of simulateQ_postInsert.induct: the parametric motive is instantiated to the equality with simulateQ so oa, leaving trivial cases.

theorem QueryImpl.simulateQ_postInsert_const_pure {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] (so : QueryImpl spec m) (x : α) (oa : OracleComp spec β) : simulateQ (so.postInsert fun (x_1 : spec.Domain) (x_2 : spec.Range x_1) => pure x) oa = liftM (simulateQ so oa)

When nx is constantly pure x, postInsert so nx is the lift of so and the resulting simulation equals the lifted underlying simulation. Generic analogue of the run_simulateQ_withTrace_const_one no-op identity.

theorem QueryImpl.support_proj_simulateQ_postInsert {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [MonadAttach m] (so : QueryImpl spec m) (nx : (t : spec.Domain) → spec.Range t → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.postInsert nx t) = so t) (oa : OracleComp spec β) : support (proj (simulateQ (so.postInsert nx) oa)) = support (simulateQ so oa)

theorem QueryImpl.finSupport_proj_simulateQ_postInsert {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] {ι : Type u_1} {spec : OracleSpec ι} {α β : Type u} [LawfulMonad m] [LawfulMonad n] [MonadAttach m] [HasEvalFinset m] [DecidableEq β] (so : QueryImpl spec m) (nx : (t : spec.Domain) → spec.Range t → n α) (proj : {γ : Type u} → n γ → m γ) (hproj_pure : ∀ {γ : Type u} (x : γ), proj (pure x) = pure x) (hproj_bind : ∀ {γ δ : Type u} (b : n γ) (f : γ → n δ), proj (b >>= f) = do let x ← proj b proj (f x)) (hproj_apply : ∀ (t : spec.Domain), proj (so.postInsert nx t) = so t) (oa : OracleComp spec β) : finSupport (proj (simulateQ (so.postInsert nx) oa)) = finSupport (simulateQ so oa)