Morphisms of HasQuery Monads

This module contains the heavier HasQuery naturality layer. It imports ProbComp and monad homomorphisms, so files that only need the basic query capability should import VCVio.OracleComp.HasQuery.Basic instead.

Use this module for proofs that a monad morphism preserves oracle queries, or that it commutes with the canonical lift of public randomness.

structure HasQuery.QueryHom {ι : Type u} (spec : OracleSpec ι) (m : Type v → Type w) [Monad m] [HasQuery spec m] (n : Type v → Type x) [Monad n] [HasQuery spec n] extends m →ᵐ n : Type (max (max (v + 1) w) x)

A QueryHom spec m n is a monad morphism m →ᵐ n that also preserves the distinguished oracle-query capability for spec. This is the right notion of morphism for proving that a construction generic over HasQuery spec is natural in the chosen oracle semantics.

• toFun (α : Type v) : m α → n α
• toFun_pure' {α : Type v} (x : α) : self.toFun α (pure x) = pure x
• toFun_bind' {α β : Type v} (x : m α) (y : α → m β) : self.toFun β (x >>= y) = do let x ← self.toFun α x self.toFun β (y x)
• map_query' (t : spec.Domain) : self.toFun (spec.Range t) (query t) = query t

def HasQuery.PreservesProbCompLift {m : Type → Type w} [Monad m] [MonadLiftT ProbComp m] {n : Type → Type x} [Monad n] [MonadLiftT ProbComp n] (F : m →ᵐ n) : Prop

A monad morphism preserves public randomness when it commutes with the distinguished lifting of plain probabilistic computations into the ambient monad.

@[simp]

theorem HasQuery.map_query {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} [Monad m] [HasQuery spec m] {n : Type v → Type x} [Monad n] [HasQuery spec n] (F : QueryHom spec m n) (t : spec.Domain) : (fun {α : Type v} (x : m α) => F.toFun α x) (query t) = query t