Documentation

VCVio.OracleComp.SimSemantics.Append

Append/Add Operation for Simulation Oracles #

source
def QueryImpl.add {ι₁ : Type u_4} {ι₂ : Type u_5} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_1} (impl₁ : QueryImpl spec₁ m) (impl₂ : QueryImpl spec₂ m) :
QueryImpl (spec₁ + spec₂) m

Simplest version of adding queries when all implementations are in the same monad. The actual add notation for QueryImpl uses QueryImpl.addLift which adds monad lifting to this definition for greater flexibility.

Instances For
    source
    @[implicit_reducible]
    instance QueryImpl.instHAddSumHAddOracleSpec {ι₁ : Type u_4} {ι₂ : Type u_5} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_1} :
    HAdd (QueryImpl spec₁ m) (QueryImpl spec₂ m) (QueryImpl (spec₁ + spec₂) m)

    Add two QueryImpl to get an implementation on the sum of the two OracleSpec.

    source
    theorem QueryImpl.add_apply {ι₁ : Type u_4} {ι₂ : Type u_5} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_1} (impl₁ : QueryImpl spec₁ m) (impl₂ : QueryImpl spec₂ m) (t : (spec₁ + spec₂).Domain) :
    (impl₁ + impl₂) t = match t with | Sum.inl t => impl₁ t | Sum.inr t => impl₂ t
    source
    @[simp]
    theorem QueryImpl.add_apply_inl {ι₁ : Type u_4} {ι₂ : Type u_5} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_1} (impl₁ : QueryImpl spec₁ m) (impl₂ : QueryImpl spec₂ m) (t : spec₁.Domain) :
    (impl₁ + impl₂) (Sum.inl t) = impl₁ t
    source
    @[simp]
    theorem QueryImpl.add_apply_inr {ι₁ : Type u_4} {ι₂ : Type u_5} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_1} (impl₁ : QueryImpl spec₁ m) (impl₂ : QueryImpl spec₂ m) (t : spec₂.Domain) :
    (impl₁ + impl₂) (Sum.inr t) = impl₂ t
    source
    def QueryImpl.addLift {ι₁ : Type u_7} {ι₂ : Type u_8} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_4} {n : Type u → Type u_5} {r : Type u → Type u_6} [MonadLiftT m r] [MonadLiftT n r] (impl₁ : QueryImpl spec₁ m) (impl₂ : QueryImpl spec₂ n) :
    QueryImpl (spec₁ + spec₂) r

    Version of QueryImpl.add that also lifts the two implementations to a shared lift monad.

    Instances For
      source
      @[simp]
      theorem QueryImpl.addLift_def {ι₁ : Type u_7} {ι₂ : Type u_8} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type u → Type u_4} {n : Type u → Type u_5} {r : Type u → Type u_6} [MonadLiftT m r] [MonadLiftT n r] (impl₁ : QueryImpl spec₁ m) (impl₂ : QueryImpl spec₂ n) :
      impl₁.addLift impl₂ = liftTarget r impl₁ + liftTarget r impl₂
      source
      @[simp]
      theorem QueryImpl.simulateQ_add_liftComp_left {ι₁' ι₂' : Type} {spec₁' : OracleSpec ι₁'} {spec₂' : OracleSpec ι₂'} {α : Type} {m' : Type → Type v} [Monad m'] [LawfulMonad m'] (impl₁' : QueryImpl spec₁' m') (impl₂' : QueryImpl spec₂' m') (oa : OracleComp spec₁' α) :
      simulateQ (impl₁' + impl₂') (oa.liftComp (spec₁' + spec₂')) = simulateQ impl₁' oa
      source
      @[simp]
      theorem QueryImpl.simulateQ_add_liftComp_right {ι₁' ι₂' : Type} {spec₁' : OracleSpec ι₁'} {spec₂' : OracleSpec ι₂'} {α : Type} {m' : Type → Type v} [Monad m'] [LawfulMonad m'] (impl₁' : QueryImpl spec₁' m') (impl₂' : QueryImpl spec₂' m') (ob : OracleComp spec₂' α) :
      simulateQ (impl₁' + impl₂') (ob.liftComp (spec₁' + spec₂')) = simulateQ impl₂' ob
      source
      theorem QueryImpl.simulateQ_liftComp_left_eq_of_apply {ι₁' ι₂' : Type} {spec₁' : OracleSpec ι₁'} {spec₂' : OracleSpec ι₂'} {α : Type} {m' : Type → Type v} [Monad m'] [LawfulMonad m'] (impl : QueryImpl (spec₁' + spec₂') m') (impl₁ : QueryImpl spec₁' m') (h : ∀ (t : ι₁'), impl (Sum.inl t) = impl₁ t) (oa : OracleComp spec₁' α) :
      simulateQ impl (oa.liftComp (spec₁' + spec₂')) = simulateQ impl₁ oa
      source
      theorem QueryImpl.simulateQ_liftComp_right_eq_of_apply {ι₁' ι₂' : Type} {spec₁' : OracleSpec ι₁'} {spec₂' : OracleSpec ι₂'} {α : Type} {m' : Type → Type v} [Monad m'] [LawfulMonad m'] (impl : QueryImpl (spec₁' + spec₂') m') (impl₂ : QueryImpl spec₂' m') (h : ∀ (t : ι₂'), impl (Sum.inr t) = impl₂ t) (oa : OracleComp spec₂' α) :
      simulateQ impl (oa.liftComp (spec₁' + spec₂')) = simulateQ impl₂ oa
      source
      theorem QueryImpl.simulateQ_liftM_eq_of_query {ι₁' ι₂' : Type} {spec₁' : OracleSpec ι₁'} {spec₂' : OracleSpec ι₂'} {α : Type} {m' : Type → Type v} [Monad m'] [LawfulMonad m'] [MonadLiftT (OracleComp spec₁') (OracleComp spec₂')] [LawfulMonadLiftT (OracleComp spec₁') (OracleComp spec₂')] (impl : QueryImpl spec₂' m') (impl₁ : QueryImpl spec₁' m') (h : ∀ (t : ι₁'), simulateQ impl (liftM (liftM (OracleSpec.query t))) = impl₁ t) (oa : OracleComp spec₁' α) :
      simulateQ impl (liftM oa) = simulateQ impl₁ oa