Append Operation for Simulation Oracles

This file defines an operation SimOracle.append that takes two simulation oracles so and so' from spec₁ and spec₂ respectively to a shared target spec specₜ, and constructs a new simulation oracle from spec₁ ++ spec₂ to specₜ.

This operation is also compatible with the SubSpec instances involving OracleSpec.append. For example if oa : OracleComp spec₁ α is coerced to ↑oa : OracleComp (spec₁ ++ spec₂) α, then we have simulate' (so ++ₛₒ so') ↑oa s = simulate' so oa s.1, as the additional oracles from the coercion will never actually be called.

TODO: simp lemmas are not always applied properly, seemingly due to the free n variable.

def SimOracle.append {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m₁ m₂ n : Type u → Type v} [MonadLiftT m₁ n] [MonadLiftT m₂ n] (so : QueryImpl spec₁ m₁) (so' : QueryImpl spec₂ m₂) : QueryImpl (spec₁ ++ₒ spec₂) n

Given simulation oracles so and so' with source oracles spec₁ and spec₂ respectively, with the same target oracles specₜ, construct a new simulation oracle from specₜ, answering queries to either oracle set with queries to the corresponding simulation oracle. NOTE: n can't be inferred from the explicit parameters, the use case needs to give context

Equations

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

def SimOracle.«term_++ₛₒ_» : Lean.TrailingParserDescr

Equations

• SimOracle.«term_++ₛₒ_» = Lean.ParserDescr.trailingNode `SimOracle.«term_++ₛₒ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ₛₒ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem SimOracle.append_apply_inl {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m₁ m₂ n : Type u → Type v} [MonadLift m₁ n] [MonadLift m₂ n] (so : QueryImpl spec₁ m₁) (so' : QueryImpl spec₂ m₂) (i : ι₁) (t : spec₁.domain i) : (so ++ₛₒ so').impl (OracleSpec.query (Sum.inl i) t) = liftM (so.impl (OracleSpec.query i t))

@[simp]

theorem SimOracle.append_apply_inr {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m₁ m₂ n : Type u → Type v} [MonadLift m₁ n] [MonadLift m₂ n] (so : QueryImpl spec₁ m₁) (so' : QueryImpl spec₂ m₂) (i : ι₂) (t : spec₂.domain i) : (so ++ₛₒ so').impl (OracleSpec.query (Sum.inr i) t) = liftM (so'.impl (OracleSpec.query i t))

@[simp]

theorem SimOracle.simulate_coe_append_left {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type u} {m₁ m₂ n : Type u → Type v} [MonadLift m₁ n] [MonadLift m₂ n] (so : QueryImpl spec₁ m₁) (so' : QueryImpl spec₂ m₂) [AlternativeMonad n] [LawfulAlternative n] [LawfulMonad n] [AlternativeMonad m₁] [LawfulMonad m₁] [LawfulAlternative m₁] [LawfulMonadLift m₁ n] [LawfulAlternativeLift m₁ n] (oa : OracleComp spec₁ α) : OracleComp.simulateQ (so ++ₛₒ so') (liftM oa) = liftM (OracleComp.simulateQ so oa)

@[simp]

theorem SimOracle.simulate_coe_append_right {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type u} {m₁ m₂ n : Type u → Type v} [MonadLift m₁ n] [MonadLift m₂ n] (so : QueryImpl spec₁ m₁) (so' : QueryImpl spec₂ m₂) [AlternativeMonad n] [LawfulAlternative n] [LawfulMonad n] [AlternativeMonad m₂] [LawfulMonad m₂] [LawfulAlternative m₂] [LawfulMonadLift m₂ n] [LawfulAlternativeLift m₂ n] (oa : OracleComp spec₂ α) : OracleComp.simulateQ (so ++ₛₒ so') (liftM oa) = liftM (OracleComp.simulateQ so' oa)