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 OracleQuery.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 α

@[implicit_reducible]

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

OracleQuery spec inherets the functorial structure from PFunctor.Obj.

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

@[reducible, inline]

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

The oracle input used in an oracle query.

@[simp]

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

@[simp]

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

@[simp]

theorem OracleQuery.input_map' {ι : Type u_3} {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_1} {spec : OracleSpec ι} {α : Type u_3} (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_2} {spec : OracleSpec ι} {α : Type u_1} (t : spec.Domain) (f : spec.Range t → α) : cont ⟨t, f⟩ = f

@[simp]

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

@[simp]

theorem OracleQuery.cont_map' {ι : Type u_3} {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_2} {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_2} {spec : OracleSpec ι} {α : Type u_1} {q q' : OracleQuery spec α} : q = q' ↔ q.input = q'.input ∧ q.cont ≍ q'.cont

theorem OracleQuery.ext' {ι : Type u_2} {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_1} {spec : OracleSpec ι} {α : Type u_3} [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_2} {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_2} {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.

def OracleQuery.query {ι : Type u_1} {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. Note: could consider putting this in the OracleQuery monad, type inference struggles tho.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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