Generic Oracle Query Capability

This file defines HasQuery spec m, a thin capability interface for monads that can issue queries to an oracle family spec.

OracleComp spec remains the canonical free syntax for explicit oracle computations, structural induction, and query-bound reasoning. HasQuery is the lighter interface used when a construction only needs to ask oracle queries, without reifying or analyzing the query syntax.

The key design choice is that HasQuery is just a facade over the existing lifting story: the primitive single-query syntax OracleQuery spec is itself a HasQuery spec instance, and any monad that supports MonadLiftT (OracleQuery spec) m automatically gets a HasQuery spec m instance as well. As a result, the capability composes with the existing SubSpec coercions and with standard transformer lifts such as StateT, ReaderT, ExceptT, and WriterT.

class HasQuery {ι : Type u} (spec : OracleSpec ι) (m : Type v → Type w) : Type (max u w)

Capability to issue queries to the oracle family spec inside the ambient monad m.

• query (t : spec.Domain) : m (spec.Range t)

  Issue a single oracle query.

@[reducible, inline]

abbrev QueryImpl.toHasQuery {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} (impl : QueryImpl spec m) : HasQuery spec m

View a concrete query implementation as query capability in the same monad. This is useful when instantiating a generic HasQuery construction directly inside an analysis monad such as StateT σ ProbComp or WriterT ω (OracleComp spec).

@[simp]

theorem QueryImpl.toHasQuery_query {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} (impl : QueryImpl spec m) (t : spec.Domain) : HasQuery.query t = impl t

@[implicit_reducible]

instance HasQuery.instOracleQuery {ι : Type u} {spec : OracleSpec ι} : HasQuery spec (OracleQuery spec)

The primitive single-query syntax OracleQuery spec has the obvious query capability.

@[simp]

theorem HasQuery.instOracleQuery_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : query t = OracleQuery.query t

def HasQuery.toQueryImpl {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} [HasQuery spec m] : QueryImpl spec m

Repackage HasQuery as a QueryImpl, for APIs that still consume explicit oracle implementations.

@[simp]

theorem HasQuery.toQueryImpl_apply {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} [HasQuery spec m] (t : spec.Domain) : toQueryImpl t = query t

@[implicit_reducible, instance 100]

instance HasQuery.instOfMonadLift {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} [MonadLiftT (OracleQuery spec) m] : HasQuery spec m

Any lawful lift of OracleQuery spec into m gives query capability in m. This is the main bridge that makes HasQuery compose with SubSpec lifts and standard transformer lifts.

@[simp]

theorem HasQuery.instOfMonadLift_query {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type w} [MonadLiftT (OracleQuery spec) m] (t : spec.Domain) : query t = liftM (OracleQuery.query t)

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