Computations with Oracle Access

A value oa : OracleComp spec α represents a computation with return type α, with access to any of the oracles specified by spec : OracleSpec. Returning a value x corresponds to the computation pure' α x. The computation queryBind' i t α ou represents querying the oracle corresponding to index i on input t, getting a result u : spec.range i, and then running ou u. We also allow for a failure' operation for quitting out. These operations induce Monad and Alternative instances on OracleComp spec.

pure' α a gives a monadic pure operation, while a more general >>= operator is derived by induction on the first computation (see OracleComp.bind). This importantly allows us to define a LawfulMonad instance on OracleComp spec, which isn't possible if a general bind operator is included in the main syntax.

We also define simple operations like coin : OracleComp coinSpec Bool for flipping a fair coin, and $[0..n] : ProbComp (Fin (n + 1)) for selecting from an inclusive range.

Note that the monadic structure on OracleComp exists only for a fixed OracleSpec, so it isn't possible to combine computations where one has a superset of oracles of the other. We later introduce a set of type coercions that mitigate this for most common cases, such as calling a computation with spec as part of a computation with spec ++ spec'.

inductive OracleSpec.OracleQuery {ι : Type u} (spec : OracleSpec ι) : Type v → Type (max u v)

An OracleQuery to one of the oracles in spec, bundling an index and the input to use for querying that oracle, implemented as a dependent pair. Implemented as a functor with the oracle output type as the constructor result.

• query {ι : Type u} {spec : OracleSpec ι} (i : ι) (t : spec.domain i) : spec.OracleQuery (spec.range i)

def OracleSpec.OracleQuery.defaultOutput {ι : Type u} {spec : OracleSpec ι} {α : Type v} [(i : ι) → Inhabited (spec.range i)] (q : spec.OracleQuery α) : α

Equations

• (OracleSpec.query i t).defaultOutput = default

def OracleSpec.OracleQuery.index {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : ι

Equations

• (OracleSpec.query i t).index = i

@[simp]

theorem OracleSpec.OracleQuery.index_query {ι : Type u} {spec : OracleSpec ι} (i : ι) (t : spec.domain i) : (query i t).index = i

def OracleSpec.OracleQuery.input {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : spec.domain q.index

Equations

• (OracleSpec.query i t).input = t

@[simp]

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

@[simp]

theorem OracleSpec.OracleQuery.range_index {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : spec.range q.index = α

theorem OracleSpec.OracleQuery.eq_query_index_input {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : q = ⋯ ▸ query q.index q.input

def OracleSpec.OracleQuery.rangeDecidableEq {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.DecidableEq] : spec.OracleQuery α → DecidableEq α

Equations

• (OracleSpec.query i t).rangeDecidableEq = inferInstance

def OracleSpec.OracleQuery.rangeFintype {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] : spec.OracleQuery α → Fintype α

Equations

• (OracleSpec.query i t).rangeFintype = inferInstance

def OracleSpec.OracleQuery.rangeInhabited {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] : spec.OracleQuery α → Inhabited α

Equations

• (OracleSpec.query i t).rangeInhabited = inferInstance

instance OracleSpec.OracleQuery.isEmpty {α : Type v} : IsEmpty ([]ₒ.OracleQuery α)

instance OracleSpec.OracleQuery.instDecidableEqOfDomain {ι : Type u} {spec : OracleSpec ι} [hι : DecidableEq ι] [hd : (i : ι) → DecidableEq (spec.domain i)] {α : Type u} : DecidableEq (spec.OracleQuery α)

Equations

• One or more equations did not get rendered due to their size.

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

OracleComp spec α represents computations with oracle access to oracles in spec, where the final return value has type α. The basic computation is just an OracleQuery, augmented with pure and bind by FreeMonad, and failure is also added after by the OptionT transformer.

In practive computations in OracleComp spec α have have one of three forms:

• return x to succeed with some x : α as the result.
• do u ← query i t; oa u where oa is a continutation to run with the query result
• failure which terminates the computation early See OracleComp.inductionOn for an explicit induction principle.

Equations

• OracleComp spec = OptionT (FreeMonad spec.OracleQuery)

@[reducible, inline]

abbrev ProbComp : Type z → Type (max z 1)

Simplified notation for computations with no oracles besides random inputs.

Equations

• ProbComp = OracleComp unifSpec

instance OracleComp.instAlternativeMonad {ι : Type u} {spec : OracleSpec ι} : AlternativeMonad (OracleComp spec)

Equations

• OracleComp.instAlternativeMonad = inferInstanceAs (AlternativeMonad (OptionT (FreeMonad spec.OracleQuery)))

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

instance OracleComp.instLawfulAlternative {ι : Type u} {spec : OracleSpec ι} : LawfulAlternative (OracleComp spec)

instance OracleComp.instInhabited {ι : Type u} {spec : OracleSpec ι} {α : Type v} : Inhabited (OracleComp spec α)

Equations

• OracleComp.instInhabited = { default := failure }

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

Lift a query by first lifting to the free moand and then to the option.

Equations

• OracleComp.lift q = OptionT.lift (FreeMonad.lift q)

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

Automatically coerce an OracleQuery spec α to an OracleComp spec α.

Equations

• OracleComp.instMonadLiftOracleQuery = { monadLift := fun {α : Type ?u.15} => OracleComp.lift }

instance OracleComp.instMonadFunctorOracleQuery {ι : Type u} {spec : OracleSpec ι} : MonadFunctor spec.OracleQuery (OracleComp spec)

Lift a function on oracle queries to one on oracle computations.

Equations

• One or more equations did not get rendered due to their size.

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

theorem OracleComp.lift_query_def {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q : spec.OracleQuery α) : liftM q = OptionT.lift (FreeMonad.lift q)

Alias of OracleComp.liftM_def.

theorem OracleComp.liftM_query_eq_liftM_liftM {ι : Type u} {spec : OracleSpec ι} {m : Type v → Type z} [MonadLift (OracleComp spec) m] {α : Type v} (q : spec.OracleQuery α) : liftM q = liftM (liftM q)

@[simp]

theorem OracleComp.liftM_query_stateT {ι : Type u} {spec : OracleSpec ι} {σ α : Type v} (q : spec.OracleQuery α) : liftM q = liftM (liftM q)

@[simp]

theorem OracleComp.liftM_query_writerT {ι : Type u} {spec : OracleSpec ι} {ω : Type v} [Monoid ω] {α : Type v} (q : spec.OracleQuery α) : liftM q = liftM (liftM q)

@[simp]

theorem OracleComp.liftM_query_readerT {ι : Type u} {spec : OracleSpec ι} {ρ α : Type v} (q : spec.OracleQuery α) : liftM q = liftM (liftM q)

theorem OracleComp.query_bind_eq_roll {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : liftM q >>= ob = OptionT.mk (FreeMonad.roll q ob)

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

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

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

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

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

@[reducible, inline]

def OracleComp.coin : OracleComp coinSpec Bool

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

Equations

• OracleComp.coin = liftM (OracleSpec.query () ())

@[reducible, inline]

def OracleComp.uniformFin (n : ℕ) : ProbComp (Fin (n + 1))

$[0..n] is the computation choosing a random value in the given range, inclusively. By making this range inclusive we avoid the case of choosing from the empty range.

Equations

• $[0..n] = liftM (OracleSpec.query n ())

@[reducible, inline]

def OracleComp.uniformFin' (n m : ℕ) : OracleComp probSpec (Fin (m + 1))

Equations

• ($[n⋯m]) = liftM (OracleSpec.query m n)

def OracleComp.«term$[0.._]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def OracleComp.«term$[_⋯_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

theorem OracleComp.ite_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (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 : ∀ (i : ι) (t : spec.domain i) (oa : spec.range i → OracleComp spec α), (∀ (u : spec.range i), C (oa u)) → C (liftM (OracleSpec.query i t) >>= oa)) (failure : C failure) (oa : OracleComp spec α) : C oa

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

• return x / pure x for any x
• do let u ← query i t; oa u (with inductive results for oa u)
• failure 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.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def OracleComp.construct {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type u_1} (pure : (a : α) → C (pure a)) (query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (failure : C failure) (oa : OracleComp spec α) : C oa

NOTE: if inductionOn could work with Sort u instead of Prop we wouldn't need this, not clear to me why lean doesn't like unifying the Prop and Type cases.

If the output type of C is a monad then OracleComp.mapM is usually preferable.

Equations

• OracleComp.construct pure query_bind failure oa = FreeMonad.construct (fun (t : Option α) => Option.rec failure pure t) (fun {β : Type ?u.72} => query_bind) oa

def OracleComp.construct' {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type u_1} (pure : (a : α) → C (pure a)) (query_bind : (i : ι) → (t : spec.domain i) → (oa : spec.range i → OracleComp spec α) → ((u : spec.range i) → C (oa u)) → C (liftM (OracleSpec.query i t) >>= oa)) (failure : C failure) (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. NOTE: may be better to just use this universally in all cases? avoids duplicating lemmas below.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OracleComp.construct_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type w} (h_pure : (a : α) → C (pure a)) (h_query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (h_failure : C failure) (x : α) : OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (pure x) = h_pure x

@[simp]

theorem OracleComp.construct_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type w} (h_pure : (a : α) → C (pure a)) (h_query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (h_failure : C failure) : OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure failure = h_failure

@[simp]

theorem OracleComp.construct_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type w} (h_pure : (a : α) → C (pure a)) (h_query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (h_failure : C failure) (q : spec.OracleQuery α) : OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (liftM q) = h_query_bind q pure h_pure

theorem OracleComp.construct_liftM {ι : Type u} {spec : OracleSpec ι} {α : Type v} {C : OracleComp spec α → Type w} (h_pure : (a : α) → C (pure a)) (h_query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (h_failure : C failure) (q : spec.OracleQuery α) : OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (liftM q) = h_query_bind q pure h_pure

Alias of OracleComp.construct_query.

@[simp]

theorem OracleComp.construct_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {C : OracleComp spec α → Type w} (h_pure : (a : α) → C (pure a)) (h_query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (h_failure : C failure) (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (liftM q >>= oa) = h_query_bind q oa fun (u : β) => OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (oa u)

@[simp]

theorem OracleComp.construct_roll {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {C : OracleComp spec α → Type w} (h_pure : (a : α) → C (pure a)) (h_query_bind : {β : Type v} → (q : spec.OracleQuery β) → (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (liftM q >>= oa)) (h_failure : C failure) (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (OptionT.mk (FreeMonad.roll q oa)) = h_query_bind q oa fun (u : β) => OracleComp.construct h_pure (fun {β : Type v} => h_query_bind) h_failure (oa u)

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

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

Equations

• OracleComp.isPure (FreeMonad.pure x_1) = x_1.isSome
• x✝.isPure = false

def OracleComp.isFailure {ι : Type u} {spec : OracleSpec ι} {α : Type v} : OracleComp spec α → Bool

Returns true for computations that fail else false.

Equations

• OracleComp.isFailure (FreeMonad.pure x_1) = x_1.isNone
• x✝.isFailure = false

@[simp]

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

@[simp]

theorem OracleComp.isPure_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : (liftM q >>= oa).isPure = false

@[simp]

theorem OracleComp.isPure_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} : failure.isPure = false

@[simp]

theorem OracleComp.isFailure_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) : (pure x).isFailure = false

@[simp]

theorem OracleComp.isFailure_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : (liftM q >>= oa).isFailure = false

@[simp]

theorem OracleComp.isFailure_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} : failure.isFailure = true

theorem OracleComp.exists_eq_of_isPure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {oa : OracleComp spec α} (h : oa.isPure = true) : ∃ (x : α), oa = pure x

theorem OracleComp.eq_failure_of_isFailure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {oa : OracleComp spec α} (h : oa.isFailure = true) : oa = failure

@[simp]

theorem OracleComp.pure_ne_query {ι : Type u} {spec : OracleSpec ι} {β : Type v} (y : β) (q : spec.OracleQuery β) : pure y ≠ liftM q

@[simp]

theorem OracleComp.query_ne_pure {ι : Type u} {spec : OracleSpec ι} {β : Type v} (y : β) (q : spec.OracleQuery β) : liftM q ≠ pure y

@[simp]

theorem OracleComp.pure_ne_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (x : α) (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : pure x ≠ liftM q >>= oa

@[simp]

theorem OracleComp.query_bind_ne_pure {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (x : α) (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : liftM q >>= oa ≠ pure x

@[simp]

theorem OracleComp.pure_ne_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) : pure x ≠ failure

@[simp]

theorem OracleComp.failure_ne_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (x : α) : failure ≠ pure x

@[simp]

theorem OracleComp.failure_ne_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : failure ≠ liftM q >>= oa

@[simp]

theorem OracleComp.query_bind_ne_failure {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q : spec.OracleQuery β) (oa : β → OracleComp spec α) : liftM q >>= oa ≠ failure

@[simp]

theorem OracleComp.query_ne_failure {ι : Type u} {spec : OracleSpec ι} {β : Type v} (q : spec.OracleQuery β) : liftM q ≠ failure

@[simp]

theorem OracleComp.failure_ne_query {ι : Type u} {spec : OracleSpec ι} {β : Type v} (q : spec.OracleQuery β) : failure ≠ liftM q

theorem OracleComp.pure_eq_query_iff_false {ι : Type u} {spec : OracleSpec ι} {β : Type v} (y : β) (q : spec.OracleQuery β) : pure y = liftM q ↔ False

theorem OracleComp.query_eq_pure_iff_false {ι : Type u} {spec : OracleSpec ι} {β : Type v} (y : β) (q : spec.OracleQuery β) : liftM q = pure y ↔ False

def OracleComp.mapM {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (query_map : {α : Type v} → spec.OracleQuery α → m α) (oa : OracleComp spec α) : m α

Implement all queries in a computation using some other monad m, preserving the pure and bind operations, giving a computation in the new monad. The function qm specifies how to replace the queries in the computation, and fail is used whenever failure is encountered. If the final output type has an Alternative instance then simulate is usually preffered.

Equations

• OracleComp.mapM fail query_map oa = OracleComp.construct pure (fun {β : Type ?u.30} (q : spec.OracleQuery β) (x : β → OracleComp spec α) (r : β → m α) => query_map q >>= r) fail oa

@[simp]

theorem OracleComp.mapM_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) (x : α) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (pure x) = pure x

@[simp]

theorem OracleComp.mapM_failure {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) failure = fail

@[simp]

theorem OracleComp.mapM_query {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) [LawfulMonad m] (q : spec.OracleQuery α) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (liftM q) = qm q

@[simp]

theorem OracleComp.mapM_query_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (liftM q >>= ob) = do let x ← qm q OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (ob x)

theorem OracleComp.mapM_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) [LawfulMonad m] (oa : OracleComp spec α) (ob : α → OracleComp spec β) (hfail : ∀ (f : α → m β), fail >>= f = fail) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (oa >>= ob) = do let x ← OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) oa OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (ob x)

@[simp]

theorem OracleComp.mapM_bind' {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [AlternativeMonad m] [LawfulMonad m] [LawfulAlternative m] (qm : {α : Type v} → spec.OracleQuery α → m α) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : OracleComp.mapM (fun {α : Type v} => failure) (fun {α : Type v} => qm) (oa >>= ob) = do let x ← OracleComp.mapM (fun {α : Type v} => failure) (fun {α : Type v} => qm) oa OracleComp.mapM (fun {α : Type v} => failure) (fun {α : Type v} => qm) (ob x)

theorem OracleComp.mapM_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) [LawfulMonad m] (oa : OracleComp spec α) (f : α → β) (hfail : ∀ (f : α → β), f <$> fail = fail) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (f <$> oa) = f <$> OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) oa

@[simp]

theorem OracleComp.mapM_map' {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] (qm : {α : Type v} → spec.OracleQuery α → m α) (oa : OracleComp spec α) (f : α → β) : OracleComp.mapM (fun {α : Type v} => failure) (fun {α : Type v} => qm) (f <$> oa) = f <$> OracleComp.mapM (fun {α : Type v} => failure) (fun {α : Type v} => qm) oa

theorem OracleComp.mapM_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) [LawfulMonad m] (og : OracleComp spec (α → β)) (oa : OracleComp spec α) (hfail : ∀ (f : (α → β) → m β), fail >>= f = fail) (hfail' : ∀ (f : α → β), f <$> fail = fail) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (og <*> oa) = OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) og <*> OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) oa

@[simp]

theorem OracleComp.mapM_ite {ι : Type u} {spec : OracleSpec ι} {α : Type v} {m : Type v → Type w} [Monad m] (fail : {α : Type v} → m α) (qm : {α : Type v} → spec.OracleQuery α → m α) (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) : OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) (if p then oa else oa') = if p then OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) oa else OracleComp.mapM (fun {α : Type v} => fail) (fun {α : Type v} => qm) oa'

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

Given a computation oa : OracleComp spec α, construct a value x : α, by assuming each query returns the default value given by the Inhabited instance. Returns none if the default path would lead to failure.

Equations

• oa.defaultResult = OracleComp.mapM (fun {α : Type ?u.27} => none) (fun {α : Type ?u.27} => some ∘ OracleSpec.OracleQuery.defaultOutput) oa

def OracleComp.totalQueries {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] {α : 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem OracleComp.liftM_inj {ι : Type u} {spec : OracleSpec ι} {α : Type v} (q q' : spec.OracleQuery α) : liftM q = liftM q' ↔ q = q'

@[simp]

theorem OracleComp.query_inj {ι : Type u} {spec : OracleSpec ι} (i : ι) (t t' : spec.domain i) : liftM (OracleSpec.query i t) = liftM (OracleSpec.query i t') ↔ t = t'

@[simp]

theorem OracleComp.queryBind_inj {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (q q' : spec.OracleQuery α) (ob ob' : α → OracleComp spec β) : liftM q >>= ob = liftM q' >>= ob' ↔ q = q' ∧ ob = ob'

@[simp]

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

@[simp]

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

theorem OracleComp.bind_eq_pure {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (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.

theorem OracleComp.pure_eq_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (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.

instance OracleComp.instDecidableEq {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [hd : (i : ι) → DecidableEq (spec.domain i)] [hι : DecidableEq ι] [h : DecidableEq α] : DecidableEq (OracleComp spec α)

If the oracle indexing-type ι, output type α, and domains of all oracles have DecidableEq then OracleComp spec α also has DecidableEq.

Equations

• One or more equations did not get rendered due to their size.
• OracleComp.instDecidableEq (FreeMonad.pure (some x_2)) (FreeMonad.pure (some y)) = match y, h x_2 y with | .(x_2), isTrue ⋯ => isTrue ⋯ | y, isFalse h => isFalse ⋯
• OracleComp.instDecidableEq (FreeMonad.pure none) (FreeMonad.pure (some y)) = isFalse ⋯
• OracleComp.instDecidableEq (FreeMonad.pure (some x_2)) (FreeMonad.pure none) = isFalse ⋯
• OracleComp.instDecidableEq (FreeMonad.pure none) (FreeMonad.pure none) = isTrue ⋯
• OracleComp.instDecidableEq (FreeMonad.pure x_2) (FreeMonad.roll q r) = isFalse ⋯
• OracleComp.instDecidableEq (FreeMonad.roll q r) (FreeMonad.pure x_2) = isFalse ⋯