Computations with Oracle Access

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

OracleComp spec α represents computations with oracle access to oracles in spec, where the final return value has type α, represented as a free monad over the PFunctor corresponding to spec.

@[reducible, match_pattern]

def OracleComp.queryBind {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (t : spec.Domain) (k : spec.Range t → OracleComp spec α) : OracleComp spec α

Make one oracle query at input t, then continue with k on the response.

This is the PFunctor.FreeM.roll constructor specialized to OracleComp; the @[match_pattern] attribute makes it usable both as a term and as a match pattern.

@[implicit_reducible]

instance OracleComp.instMonad {ι : Type u} (spec : OracleSpec ι) : Monad (OracleComp spec)

instance OracleComp.instLawfulMonad {ι : Type u} (spec : OracleSpec ι) : LawfulMonad (OracleComp spec)

@[implicit_reducible]

instance OracleComp.instMonadLiftOracleQuery {ι : Type u} {spec : OracleSpec ι} : MonadLift (OracleQuery spec) (OracleComp spec)

@[reducible]

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

Manually lift an OracleQuery to an OracleComp.

theorem OracleComp.liftM_def {α : Type v} {ι : Type u} {spec : OracleSpec ι} (q : OracleQuery spec α) : liftM q = PFunctor.FreeM.lift q

@[simp]

theorem OracleComp.liftM_ne_pure {α : Type v} {ι : Type u} {spec : OracleSpec ι} (q : OracleQuery spec α) (x : α) : liftM q ≠ pure x

@[simp]

theorem OracleComp.pure_ne_liftM {α : Type v} {ι : Type u} {spec : OracleSpec ι} (x : α) (q : OracleQuery spec α) : pure x ≠ liftM q

@[simp]

theorem OracleComp.liftM_map {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (q : OracleQuery spec α) (f : α → β) : liftM (f <$> q) = f <$> liftM q

@[inline]

def OracleComp.coin : OracleComp coinSpec Bool

coin is the computation representing a coin flip, given a coin flipping oracle.

theorem OracleComp.coin_def : coin = liftM (OracleSpec.query ())

theorem OracleComp.pure_def {α : Type v} {ι : Type u} {spec : OracleSpec ι} (x : α) : pure x = PFunctor.FreeM.pure x

theorem OracleComp.bind_def {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (oa : OracleComp spec α) (ob : α → OracleComp spec β) : oa >>= ob = PFunctor.FreeM.bind oa ob

def OracleComp.casesOn {ι : Type u} {spec : OracleSpec ι} {α : Type u_2} {motive : OracleComp spec α → Sort u_1} (oa : OracleComp spec α) (pure : (x : α) → motive (PFunctor.FreeM.pure x)) (queryBind : (t : spec.Domain) → (k : spec.Range t → OracleComp spec α) → motive (queryBind t k)) : motive oa

Cases eliminator on OracleComp exposing the high-level pure / queryBind alternatives. Registered as the default cases eliminator so that cases oa with | pure x => ... | queryBind t k => ... works transparently on top of the free-monad substrate.

def OracleComp.recOn {ι : Type u} {spec : OracleSpec ι} {α : Type u_2} {motive : OracleComp spec α → Sort u_1} (oa : OracleComp spec α) (pure : (x : α) → motive (PFunctor.FreeM.pure x)) (queryBind : (t : spec.Domain) → (k : spec.Range t → OracleComp spec α) → ((u : spec.Range t) → motive (k u)) → motive (queryBind t k)) : motive oa

Structural recursion eliminator on OracleComp exposing the high-level pure / queryBind alternatives, with an induction hypothesis on every continuation in the queryBind case. Registered as the default induction eliminator so that induction oa with | pure x => ... | queryBind t k ih => ... works transparently on top of the free-monad substrate.

theorem OracleComp.failure_def {α : Type v} {ι : Type u} {spec : OracleSpec ι} : failure = OptionT.fail

theorem OracleComp.orElse_def {α : Type v} {ι : Type u} {spec : OracleSpec ι} (oa oa' : OptionT (OracleComp spec) α) : (oa <|> oa') = OptionT.mk do let __do_lift ← oa.run match __do_lift with | some a => pure (some a) | x => oa'.run

theorem OracleComp.bind_congr' {α β : Type v} {ι : Type u} {spec : OracleSpec ι} {oa oa' : OracleComp spec α} {ob ob' : α → OracleComp spec β} (h : oa = oa') (h' : ∀ (x : α), ob x = ob' x) : oa >>= ob = oa' >>= ob'

@[simp]

theorem OracleComp.guard_eq {ι : Type u} {spec : OracleSpec ι} (p : Prop) [Decidable p] : guard p = if p then pure () else failure

theorem OracleComp.ite_bind {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) (ob : α → OracleComp spec β) : (if p then oa else oa') >>= ob = if p then oa >>= ob else oa' >>= ob

def OracleComp.inductionOn {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Prop} (pure : ∀ (a : α), C (pure a)) (query_bind : ∀ (t : spec.Domain) (oa : spec.Range t → OracleComp spec α), (∀ (u : spec.Range t), C (oa u)) → C (liftM (OracleSpec.query t) >>= oa)) (oa : OracleComp spec α) : C oa

Nicer induction rule for OracleComp that uses monad notation. Allows inductive definitions on computations by considering the two cases:

• return x / pure x for any x
• do let u ← query i t; oa u (with inductive results for oa u) See oracleComp_emptySpec_equiv for an example of using this in a proof. If the final result needs to be a Type and not a Prop, see OracleComp.construct.

def OracleComp.inductionOnOptional {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OptionT (OracleComp spec) α → Prop} (pure : ∀ (a : α), C (pure a)) (query_bind : ∀ (t : spec.Domain) (oa : spec.Range t → OptionT (OracleComp spec) α), (∀ (u : spec.Range t), C (oa u)) → C (liftM (OracleSpec.query t) >>= oa)) (failure : C failure) (oa : OptionT (OracleComp spec) α) : C oa

Version of OracleComp.inductionOn that includes an OptionT in the monad stack and requires an explicit case to handle failure.

def OracleComp.induction {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Prop} (oa : OracleComp spec α) (pure : ∀ (a : α), C (pure a)) (query_bind : ∀ (t : spec.Domain) (oa : spec.Range t → OracleComp spec α), (∀ (u : spec.Range t), C (oa u)) → C (liftM (OracleSpec.query t) >>= oa)) : C oa

Version of OracleComp.inductionOn with the computation at the start.

def OracleComp.inductionOptional {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OptionT (OracleComp spec) α → Prop} (oa : OptionT (OracleComp spec) α) (pure : ∀ (a : α), C (pure a)) (query_bind : ∀ (t : spec.Domain) (oa : spec.Range t → OptionT (OracleComp spec) α), (∀ (u : spec.Range t), C (oa u)) → C (liftM (OracleSpec.query t) >>= oa)) (failure : C failure) : C oa

Version of OracleComp.inductionOnOptional with the computation at the start.

def OracleComp.construct {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type u_1} (pure : (a : α) → C (pure a)) (query_bind : (t : spec.Domain) → (oa : spec.Range t → OracleComp spec α) → ((u : spec.Range t) → C (oa u)) → C (liftM (OracleSpec.query t) >>= oa)) (oa : OracleComp spec α) : C oa

Version of construct with automatic induction on the query in when defining the query_bind case. Can be useful with spec.DecidableEq and spec.FiniteRange. mapM/simulateQ is usually preferable to this if the object being constructed is a monad.

@[simp]

theorem OracleComp.construct_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) {C : OracleComp spec α → Type u_1} (h_pure : (a : α) → C (pure a)) (h_query_bind : (t : spec.Domain) → (oa : spec.Range t → OracleComp spec α) → ((u : spec.Range t) → C (oa u)) → C (liftM (OracleSpec.query t) >>= oa)) : OracleComp.construct h_pure h_query_bind (pure x) = h_pure x

@[simp]

theorem OracleComp.construct_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) {C : OracleComp spec (spec.Range t) → Type u_1} (h_pure : (u : spec.Range t) → C (pure u)) (h_query_bind : (t' : spec.Domain) → (oa : spec.Range t' → OracleComp spec (spec.Range t)) → ((u : spec.Range t') → C (oa u)) → C (liftM (OracleSpec.query t') >>= oa)) : OracleComp.construct h_pure h_query_bind (liftM (OracleSpec.query t)) = h_query_bind t pure h_pure

@[simp]

theorem OracleComp.construct_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} (t : spec.Domain) (mx : spec.Range t → OracleComp spec α) {C : OracleComp spec α → Type u_1} (h_pure : (a : α) → C (pure a)) (h_query_bind : (t : spec.Domain) → (mx : spec.Range t → OracleComp spec α) → ((u : spec.Range t) → C (mx u)) → C (liftM (OracleSpec.query t) >>= mx)) : OracleComp.construct h_pure h_query_bind (liftM (OracleSpec.query t) >>= mx) = h_query_bind t mx fun (u : spec.Range t) => OracleComp.construct h_pure h_query_bind (mx u)

def OracleComp.isPure {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} : OracleComp spec α → Bool

Returns true for computations that don't query any oracles or fail, else false.

@[simp]

theorem OracleComp.isPure_pure {α : Type v} {ι : Type u} {spec : OracleSpec ι} (x : α) : (pure x).isPure = true

@[simp]

theorem OracleComp.isPure_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) : (liftM (OracleSpec.query t)).isPure = false

@[simp]

theorem OracleComp.isPure_query_bind {α : Type v} {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (ou : spec.Range t → OracleComp spec α) : (liftM (OracleSpec.query t) >>= ou).isPure = false

@[simp]

theorem OracleComp.pure_ne_query {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : pure u ≠ liftM (OracleSpec.query t)

@[simp]

theorem OracleComp.query_ne_pure {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : liftM (OracleSpec.query t) ≠ pure u

theorem OracleComp.pure_eq_query_iff_false {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : pure u = liftM (OracleSpec.query t) ↔ False

theorem OracleComp.query_eq_pure_iff_false {ι : Type u} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : liftM (OracleSpec.query t) = pure u ↔ False

def OracleComp.defaultResult {α : Type v} {ι : Type u} {spec : OracleSpec ι} [spec.Inhabited] (oa : OracleComp spec α) : α

Given a computation oa : OracleComp spec α, construct a value x : α, by assuming each query returns the default value given by the Inhabited instance.

def OracleComp.totalQueries {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] {α : Type v} (oa : OracleComp spec α) : ℕ

Total number of queries in a computation across all possible execution paths. Can be a helpful alternative to sizeOf when proving recursive calls terminate.

@[simp]

theorem OracleComp.pure_inj {α : Type v} {ι : Type u} {spec : OracleSpec ι} (x y : α) : pure x = pure y ↔ x = y

Two pure computations are equal iff they return the same value.

@[simp]

theorem OracleComp.bind_eq_pure_iff {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : oa >>= ob = pure y ↔ ∃ (x : α), oa = pure x ∧ ob x = pure y

Binding two computations gives a pure operation iff the first computation is pure and the second computation does something pure with the result.

@[simp]

theorem OracleComp.pure_eq_bind_iff {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : pure y = oa >>= ob ↔ ∃ (x : α), oa = pure x ∧ ob x = pure y

Binding two computations gives a pure operation iff the first computation is pure and the second computation does something pure with the result.

theorem OracleComp.bind_eq_pure {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : (∃ (x : α), oa = pure x ∧ ob x = pure y) → oa >>= ob = pure y

Alias of the reverse direction of OracleComp.bind_eq_pure_iff.

---

Binding two computations gives a pure operation iff the first computation is pure and the second computation does something pure with the result.

theorem OracleComp.pure_eq_bind {α β : Type v} {ι : Type u} {spec : OracleSpec ι} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : (∃ (x : α), oa = pure x ∧ ob x = pure y) → pure y = oa >>= ob

Alias of the reverse direction of OracleComp.pure_eq_bind_iff.

---

Binding two computations gives a pure operation iff the first computation is pure and the second computation does something pure with the result.