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.

Equations
    Instances For
      source
      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.

      Equations
        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.

        Equations
          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₂