Simulation Semantics for Oracles in a Computation

This file defines a type SimOracle spec specₜ σ to represent a way to simulate oracles in spec using the oracles in specₜ, maintaining some state of type σ. We then define a function simulate so oa s to simulate the computation oa using so to answer oracle queries, with initial state s.

We mark lemmas regarding simulating specific computations as @[simp low], so that lemmas specific to certain simulation oracles get applied firts. For example idOracle has no effect upon simulation, and we should apply that fact first.

structure QueryImpl {ι : Type w} (spec : OracleSpec ι) (m : Type u → Type v) : Type (max (max (u + 1) v) w)

Specifies a way to simulate a set of oracles using another set of oracles. e.g. using uniform selection oracles with a query cache to simulate a random oracle. simulateQ gives a method for applying a simulation oracle to a specific computation.

• impl {α : Type u} (q : spec.OracleQuery α) : m α

theorem QueryImpl.ext {ι : Type w} {spec : OracleSpec ι} {m : Type u → Type v} {x y : QueryImpl spec m} (impl : @impl ι spec m x = @impl ι spec m y) : x = y

theorem QueryImpl.ext_iff {ι : Type w} {spec : OracleSpec ι} {m : Type u → Type v} {x y : QueryImpl spec m} : x = y ↔ @impl ι spec m x = @impl ι spec m y

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

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

def OracleComp.simulateQ {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [AlternativeMonad m] (so : QueryImpl spec m) (oa : OracleComp spec α) : m α

Canonical lifting of a function OracleQuery spec α → m α to a new function OracleComp spec α by preserving bind, pure, and failure. NOTE: could change the output type to OracleComp spec →ᵐ m, makes some stuff below free

@[simp]

theorem OracleComp.simulateQ_ite {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [AlternativeMonad m] (so : QueryImpl spec m) (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) : simulateQ so (if p then oa else oa') = if p then simulateQ so oa else simulateQ so oa'

@[simp]

theorem OracleComp.simulateQ_failure {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] : simulateQ so failure = failure

@[simp]

theorem OracleComp.simulateQ_query {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] (q : spec.OracleQuery α) : simulateQ so (liftM q) = so.impl q

@[simp]

theorem OracleComp.simulateQ_pure {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] (x : α) : simulateQ so (pure x) = pure x

@[simp]

theorem OracleComp.simulateQ_comp_pure_comp {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] (f : α → β) : simulateQ so ∘ pure ∘ f = pure ∘ f

@[simp]

theorem OracleComp.simulateQ_query_bind {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] (q : spec.OracleQuery α) (ob : α → OracleComp spec β) : simulateQ so (liftM q >>= ob) = so.impl q >>= simulateQ so ∘ ob

@[simp]

theorem OracleComp.simulateQ_bind {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] [LawfulAlternative m] (oa : OracleComp spec α) (ob : α → OracleComp spec β) : simulateQ so (oa >>= ob) = simulateQ so oa >>= simulateQ so ∘ ob

@[simp]

theorem OracleComp.simulateQ_map {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] [LawfulAlternative m] (oa : OracleComp spec α) (f : α → β) : simulateQ so (f <$> oa) = f <$> simulateQ so oa

@[simp]

theorem OracleComp.simulateQ_seq {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] [LawfulAlternative m] (og : OracleComp spec (α → β)) (oa : OracleComp spec α) : simulateQ so (og <*> oa) = simulateQ so og <*> simulateQ so oa

@[simp]

theorem OracleComp.simulateQ_seqLeft {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] [LawfulAlternative m] (oa : OracleComp spec α) (ob : OracleComp spec β) : simulateQ so (oa <* ob) = simulateQ so oa <* simulateQ so ob

@[simp]

theorem OracleComp.simulateQ_seqRight {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} {α β : Type u} [AlternativeMonad m] (so : QueryImpl spec m) [LawfulMonad m] [LawfulAlternative m] (oa : OracleComp spec α) (ob : OracleComp spec β) : simulateQ so (oa *> ob) = simulateQ so oa *> simulateQ so ob

def idOracle {ι : Type u_1} {spec : OracleSpec ι} : QueryImpl spec (OracleComp spec)

Simulate a computation using the original oracles by "replacing" queries with queries. This operates as an actual identity for simulate', in that we get an exact equality between the new and original computation. This can be useful especially with SimOracle.append, in order to simulate a single oracle in a larger set of oracles, leaving the behavior of other oracles unchanged. The relevant spec can usually be inferred automatically, so we leave it implicit.

@[simp]

theorem idOracle.apply_eq {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (q : spec.OracleQuery α) : idOracle.impl q = liftM q

@[simp]

theorem idOracle.simulateQ_eq_id {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} : OracleComp.simulateQ idOracle = id

theorem idOracle.simulateQ_eq {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) : OracleComp.simulateQ idOracle oa = oa

def defaultOracle {ι : Type u_1} {spec : OracleSpec ι} [spec.FiniteRange] : QueryImpl spec Option

Simulate a computation by having each oracle return the default value of the query output type for all queries. This gives a way to run arbitrary computations to get some output. Mostly useful in some existence proofs, not usually used in an actual implementation.

@[simp]

theorem defaultOracle.apply_eq {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} [spec.FiniteRange] (q : spec.OracleQuery α) : defaultOracle.impl q = pure q.defaultOutput

@[simp]

theorem defaultOracle.simulateQ_eq_getM_defaultResult {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} [spec.FiniteRange] : OracleComp.simulateQ defaultOracle = Option.getM ∘ OracleComp.defaultResult

theorem defaultOracle.simulateQ_eq {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} [spec.FiniteRange] (oa : OracleComp spec α) : OracleComp.simulateQ defaultOracle oa = oa.defaultResult.getM