Oracle Queries

This file defines OracleQuery, the single-query functor induced by an OracleSpec.

def OracleQuery {ι : Type u} (spec : OracleSpec ι) : Type w → Type (max u v w)

Functor to represent queries to oracles specified by an OracleSpec ι, defined to be the object type of the corresponding PFunctor. In particular an element of OracleQuery spec α consists of an input value t : spec.Domain, and a continuation f : spec.Range t → α specifying what to do with the result. See OracleSpec.query for the case when the continuation f just returns the query result.

@[reducible]

def OracleQuery.mk {ι : Type u_1} {α : Type u_2} {spec : OracleSpec ι} (t : spec.Domain) (f : spec.Range t → α) : OracleQuery spec α

def OracleSpec.query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : OracleQuery spec (spec.Range t)

Query an oracle on in input t to get a result in the corresponding range t.

Marked protected: the bare identifier query resolves to HasQuery.query (exported in VCVio.OracleComp.HasQuery.Basic), which yields a value in the ambient monad and lets Lean recover spec from the expected type without an ascription. Use spec.query t or OracleSpec.query t when you specifically want the primitive single-query syntax OracleQuery spec (spec.Range t).

theorem OracleSpec.query_def {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : OracleSpec.query t = ⟨t, id⟩

Primitive query notation

OracleSpec.query is protected so the bare identifier query resolves to HasQuery.query (exported in VCVio.OracleComp.HasQuery.Basic) for ergonomic monadic use. Files that work structurally on the primitive single-query syntax OracleQuery spec _ (e.g. liftM (query t), (query t).cont, induction on query_bind) can opt back into the primitive interpretation of bare query with a single line:

open scoped OracleSpec.PrimitiveQuery

The notation is scoped to this namespace, so it never leaks past a file boundary; you must explicitly opt in.

def OracleSpec.PrimitiveQuery.termQuery : Lean.ParserDescr

Inside open scoped OracleSpec.PrimitiveQuery, the bare identifier query aliases the primitive single-query syntax OracleSpec.query.

@[implicit_reducible]

instance OracleQuery.instFunctor {ι : Type u} {spec : OracleSpec ι} : Functor (OracleQuery spec)

OracleQuery spec inherets the functorial structure from PFunctor.Obj.

instance OracleQuery.instLawfulFunctor {ι : Type u} {spec : OracleSpec ι} : LawfulFunctor (OracleQuery spec)

@[reducible, inline]

def OracleQuery.input {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (q : OracleQuery spec α) : spec.Domain

The oracle input used in an oracle query.

@[simp]

theorem OracleQuery.input_apply {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (t : spec.Domain) (f : spec.Range t → α) : input ⟨t, f⟩ = t

@[simp]

theorem OracleQuery.input_map {ι : Type u} {spec : OracleSpec ι} {α β : Type u_1} (q : OracleQuery spec α) (f : α → β) : (f <$> q).input = q.input

@[simp]

theorem OracleQuery.input_map' {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} (q : OracleQuery spec α) (f : α → β) : input (spec.toPFunctor.map f q) = q.input

@[reducible, inline]

def OracleQuery.cont {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (q : OracleQuery spec α) (f : spec.Range q.input) : α

The continutation used for the result of an oracle query.

@[simp]

theorem OracleQuery.cont_apply {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (t : spec.Domain) (f : spec.Range t → α) : cont ⟨t, f⟩ = f

@[simp]

theorem OracleQuery.cont_map {ι : Type u} {spec : OracleSpec ι} {α β : Type u_1} (q : OracleQuery spec α) (f : α → β) : (f <$> q).cont = f ∘ q.cont

@[simp]

theorem OracleQuery.cont_map' {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {β : Type u_2} (q : OracleQuery spec α) (f : α → β) : cont (spec.toPFunctor.map f q) = f ∘ q.cont

theorem OracleQuery.ext {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {q q' : OracleQuery spec α} (h : q.input = q'.input) (h' : q.cont ≍ q'.cont) : q = q'

Two oracles queries are equal if they query for the same input and run extensionally equal continuation on the results of the query.

theorem OracleQuery.ext_iff {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} {q q' : OracleQuery spec α} : q = q' ↔ q.input = q'.input ∧ q.cont ≍ q'.cont

theorem OracleQuery.ext' {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (t : spec.Domain) {cont cont' : spec.Range t → α} (h : cont = cont') : ⟨t, cont⟩ = ⟨t, cont'⟩

Version of OracleQuery.ext that avoids using HEq when the inputs are the same.

@[implicit_reducible]

instance OracleQuery.instInhabited {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} [Inhabited ι] [Inhabited α] : Inhabited (OracleQuery spec α)

If an oracle exists and the output type is non-empty then the type of queries is non-empty.

instance OracleQuery.instIsEmpty {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} [h : IsEmpty ι] : IsEmpty (OracleQuery spec α)

If there are no oracles available then the type of queries is empty.

instance OracleQuery.instSubsingleton {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} [h : Subsingleton ι] [h' : Subsingleton α] : Subsingleton (OracleQuery spec α)

If there is a at most one oracle and output, then ther is at most one query.

@[simp]

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

@[simp]

theorem OracleQuery.cont_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : (OracleSpec.query t).cont = id

@[simp]

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

@[simp]

theorem OracleQuery.snd_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : (OracleSpec.query t).snd = id

@[simp]

theorem OracleQuery.cont_map_query_input {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : OracleQuery spec α) : q.cont <$> OracleSpec.query q.input = q

@[simp]

theorem OracleQuery.cont_map_query_input' {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (q : OracleQuery spec α) : spec.toPFunctor.map q.cont (OracleSpec.query q.input) = q

@[simp]

theorem OracleQuery.query_eq_mk_iff {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (cont : spec.Range t → spec.Range t) : OracleSpec.query t = OracleQuery.mk t cont ↔ cont = id

@[simp]

theorem OracleQuery.mk_eq_query_iff {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (cont : spec.Range t → spec.Range t) : OracleQuery.mk t cont = OracleSpec.query t ↔ cont = id