Implementing Oracle Queries in Other Monads

This file defines a type QueryImpl spec m to represent implementations of queries to spec in terms of the monad m.

@[reducible]

def QueryImpl {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) : Type (max v u_1)

Specifies a way to implement queries to oracles in spec using the monad m. This is defined in terms of a mapping of input elements to oracle outputs, which extends to a mapping on OracleQuery spec by copying over the continuation, and then further to OracleComp spec by preserving the pure and bind operations. See QueryImpl.map_query and HasSimulateQ for these two operations.

Equations

• QueryImpl spec m = ((x : spec.Domain) → m (spec.Range x))

instance QueryImpl.instInhabitedOfInhabitedOfPure {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [spec.Inhabited] [Pure m] : Inhabited (QueryImpl spec m)

Equations

• QueryImpl.instInhabitedOfInhabitedOfPure = { default := fun (x : spec.Domain) => pure default }

theorem QueryImpl.ext {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {so so' : QueryImpl spec m} (h : ∀ (x : spec.Domain), so x = so' x) : so = so'

Two query implementations are the same if they are the same on all query inputs.

theorem QueryImpl.ext_iff {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {so so' : QueryImpl spec m} : so = so' ↔ ∀ (x : spec.Domain), so x = so' x

def QueryImpl.mapQuery {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [Functor m] (impl : QueryImpl spec m) (q : OracleQuery spec α) : m α

Embed an oracle query into a new functor by applying the implementation to the input value before applying the continuation of the element.

Equations

• impl.mapQuery q = q.cont <$> impl q.input

@[simp]

theorem QueryImpl.mapQuery_query {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} [Functor m] [LawfulFunctor m] (impl : QueryImpl spec m) (t : spec.Domain) : impl.mapQuery (OracleQuery.query t) = impl t

def QueryImpl.liftTarget {ι : Type u_2} {spec : OracleSpec ι} {m : Type u → Type v} (n : Type u → Type u_1) [MonadLiftT m n] (impl : QueryImpl spec m) : QueryImpl spec n

Gadget for auto-adding a lift to the end of a query implementation.

Equations

• QueryImpl.liftTarget n impl t = liftM (impl t)

@[simp]

theorem QueryImpl.liftTarget_apply {ι : Type u_2} {spec : OracleSpec ι} {m : Type u → Type v} (n : Type u → Type u_1) [MonadLiftT m n] (impl : QueryImpl spec m) (t : spec.Domain) : liftTarget n impl t = liftM (impl t)

@[simp]

theorem QueryImpl.liftTarget_self {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} (impl : QueryImpl spec m) : liftTarget m impl = impl

Lifting an implementation to the original monad has no effect.

@[simp]

theorem QueryImpl.mapQuery_liftTarget {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} (n : Type u → Type w) [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] (impl : QueryImpl spec m) (q : OracleQuery spec α) : (liftTarget n impl).mapQuery q = liftM (impl.mapQuery q)

def QueryImpl.id {ι : Type u_1} (spec : OracleSpec ι) : QueryImpl spec (OracleQuery spec)

Identity implementation for queries, sending q : OracleQuery spec α to itself.

Equations

• QueryImpl.id spec = OracleQuery.query

@[simp]

theorem QueryImpl.id_apply {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : QueryImpl.id spec t = OracleQuery.query t

@[simp]

theorem QueryImpl.mapQuery_id {ι : Type u_2} {α : Type u_1} {spec : OracleSpec ι} (q : OracleQuery spec α) : (QueryImpl.id spec).mapQuery q = q

def QueryImpl.id' {ι : Type u_1} (spec : OracleSpec ι) : QueryImpl spec (OracleComp spec)

Version of QueryImpl.id that automatically lifts into OracleComp spec rather than just implementing queries in the lower level OracleQuery spec monad

Equations

• QueryImpl.id' spec = QueryImpl.liftTarget (OracleComp spec) (QueryImpl.id spec)

@[simp]

theorem QueryImpl.id'_apply {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : QueryImpl.id' spec t = liftM (OracleQuery.query t)

@[simp]

theorem QueryImpl.mapQuery_id' {ι : Type u_2} {α : Type u_1} {spec : OracleSpec ι} (q : OracleQuery spec α) : (QueryImpl.id' spec).mapQuery q = liftM q

def QueryImpl.ofLift {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) [MonadLiftT (OracleQuery spec) m] : QueryImpl spec m

Given that queries in spec lift to the monad m we get an implementation via lifting.

Equations

• QueryImpl.ofLift spec m t = liftM (OracleQuery.query t)

@[simp]

theorem QueryImpl.ofLift_apply {ι : Type u_1} (spec : OracleSpec ι) (m : Type u → Type v) [MonadLiftT (OracleQuery spec) m] (t : spec.Domain) : ofLift spec m t = liftM (OracleQuery.query t)

@[simp]

theorem QueryImpl.mapQuery_ofLift {ι : Type u_1} {α : Type u} (spec : OracleSpec ι) (m : Type u → Type v) [Functor m] [MonadLiftT (OracleQuery spec) m] (q : OracleQuery spec α) : (ofLift spec m).mapQuery q = q.cont <$> liftM (OracleQuery.query q.input)

@[simp]

theorem QueryImpl.ofLift_eq_id {ι : Type u_1} {spec : OracleSpec ι} : ofLift spec (OracleQuery spec) = QueryImpl.id spec

@[simp]

theorem QueryImpl.ofLift_eq_id' {ι : Type u_1} {spec : OracleSpec ι} : ofLift spec (OracleComp spec) = QueryImpl.id' spec

def QueryImpl.ofFn {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → spec.Range t) : QueryImpl spec Id

View a function from oracle inputs to outputs as an implementation in the Id monad. Can be used to run a computation to get a specific value.

Equations

• QueryImpl.ofFn f = f

@[simp]

theorem QueryImpl.ofFn_apply {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → spec.Range t) (t : spec.Domain) : ofFn f t = f t

@[simp]

theorem QueryImpl.mapQuery_ofFn {ι : Type u_2} {spec : OracleSpec ι} {α : Type u_1} (f : (t : spec.Domain) → spec.Range t) (q : OracleQuery spec α) : (ofFn f).mapQuery q = q.cont (f q.input)

def QueryImpl.ofFn? {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) : QueryImpl spec Option

Version of ofFn that allows queries to fail to return a value.

Equations

• QueryImpl.ofFn? f = f

@[simp]

theorem QueryImpl.ofFn?_apply {ι : Type u_1} {spec : OracleSpec ι} (f : (t : spec.Domain) → Option (spec.Range t)) (t : spec.Domain) : ofFn? f t = f t

@[simp]

theorem QueryImpl.mapQuery_ofFn? {ι : Type u_2} {spec : OracleSpec ι} {α : Type u_1} (f : (t : spec.Domain) → Option (spec.Range t)) (q : OracleQuery spec α) : (ofFn? f).mapQuery q = Option.map q.cont (f q.input)

@[reducible]

def QueryImpl.ofPolynomial {R : Type u_1} [Semiring R] (p : Polynomial R) : QueryImpl (OracleSpec.ofFn fun (x : R) => R) Id

Implement a single oracle as evaluation of a Polynomial.

Equations

• QueryImpl.ofPolynomial p = QueryImpl.ofFn fun (t : R) => Polynomial.eval t p

@[reducible]

def QueryImpl.ofMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) : QueryImpl (OracleSpec.ofFn fun (x : σ → R) => R) Id

Implement a single oracle as the evaluation of an `MvPolynomial.

Equations

• QueryImpl.ofMvPolynomial p = QueryImpl.ofFn fun (t : σ → R) => (MvPolynomial.eval t) p

@[reducible]

def QueryImpl.ofVector {α : Type u_1} {n : ℕ} (v : Vector α n) : QueryImpl (OracleSpec.ofFn fun (x : Fin n) => α) Id

Implement a single oracle as indexing into a Vector.

Equations

• QueryImpl.ofVector v = QueryImpl.ofFn fun (t : Fin n) => v[t]

@[reducible]

def QueryImpl.ofListVector {α : Type u_1} {n : ℕ} (v : List.Vector α n) : QueryImpl (OracleSpec.ofFn fun (x : Fin n) => α) Id

Oracle context for ability to query elements of a vector v.

Equations

• QueryImpl.ofListVector v = QueryImpl.ofFn fun (t : Fin n) => v[t]