Documentation

VCVio.OracleComp.HasQuery.Basic

Basic HasQuery Capability #

This is the lightweight dependency boundary for the query capability. It defines HasQuery spec m, exports the bare identifier query, and provides only the foundational instances for primitive query syntax and monad lifts.

Core syntax modules, especially VCVio.OracleComp.OracleComp, should import this file when they need the class or the bare query export. Do not add QueryImpl, ProbComp, or monad-morphism APIs here; those live in downstream modules with explicit imports.

source
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.

Instances
    source
    @[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.

    source
    @[simp]
    theorem HasQuery.instOracleQuery_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) :
    query t = OracleSpec.query t
    source
    @[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.

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