Documentation

VCVio.OracleComp.Coercions.Add

Coercing Computations to Larger Oracle Sets #

This file defines SubSpec instances for oracle specs constructed with either OracleSpec.add or OracleSpec.sigma.

TODO: document the "canonical forms" that work well with this

source
@[instance 100]
instance OracleQuery.instSubSpecPEmptyEmptySpecOfInhabited {τ : Type u} [Inhabited τ] {spec : OracleSpec τ} :
[]ₒ ⊂ₒ spec

We need Inhabited to prevent infinite type-class searching.

Equations
    source
    instance OracleQuery.subSpec_add_left {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} :
    spec₁ ⊂ₒ spec₁ + spec₂

    Add additional oracles to the right side of the existing ones.

    Equations
      source
      @[simp]
      theorem OracleQuery.liftM_add_left_def {ι₁ : Type u_1} {ι₂ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type u} (q : OracleQuery spec₁ α) :
      liftM q = OracleQuery.mk (Sum.inl q.input) q.cont
      source
      @[simp]
      theorem OracleQuery.liftM_add_left_query {ι₁ : Type u_1} {ι₂ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (t : spec₁.Domain) :
      liftM (query t) = query (Sum.inl t)
      source
      instance OracleQuery.subSpec_add_right {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} :
      spec₂ ⊂ₒ spec₁ + spec₂

      Add additional oracles to the left side of the exiting ones

      Equations
        source
        @[simp]
        theorem OracleQuery.liftM_add_right_def {ι₁ : Type u_3} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type u} (q : OracleQuery spec₂ α) :
        liftM q = OracleQuery.mk (Sum.inr q.input) q.cont
        source
        @[simp]
        theorem OracleQuery.liftM_add_right_query {ι₁ : Type u_3} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (t : spec₂.Domain) :
        liftM (query t) = query (Sum.inr t)
        source
        instance OracleQuery.subSpec_left_add_left_add_of_subSpec {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} [h : spec₁ ⊂ₒ spec₃] :
        spec₁ + spec₂ ⊂ₒ spec₃ + spec₂
        Equations
          source
          @[simp]
          theorem OracleQuery.liftM_left_add_left_add_def {ι₁ : Type u_1} {ι₂ : Type u_4} {ι₃ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} {α : Type u} [h : spec₁ ⊂ₒ spec₃] (q : OracleQuery (spec₁ + spec₂) α) :
          liftM q = match q with | ⟨Sum.inl q, f⟩ => liftM (liftM (OracleQuery.mk q f)) | ⟨Sum.inr q, f⟩ => OracleQuery.mk (Sum.inr q) f
          source
          @[simp]
          theorem OracleQuery.liftM_left_add_left_add_query {ι₁ : Type u_1} {ι₂ : Type u_4} {ι₃ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} [h : spec₁ ⊂ₒ spec₃] (t : (spec₁ + spec₂).Domain) :
          liftM (query t) = match t with | Sum.inl t => liftM (liftM (query t)) | Sum.inr t => query (Sum.inr t)
          source
          instance OracleQuery.subSpec_right_add_right_add_of_subSpec {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} [h : spec₂ ⊂ₒ spec₃] :
          spec₁ + spec₂ ⊂ₒ spec₁ + spec₃
          Equations
            source
            @[simp]
            theorem OracleQuery.liftM_right_add_right_add_def {ι₁ : Type u_4} {ι₂ : Type u_1} {ι₃ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} {α : Type u} [h : spec₂ ⊂ₒ spec₃] (q : OracleQuery (spec₁ + spec₂) α) :
            liftM q = match q with | ⟨Sum.inl q, f⟩ => OracleQuery.mk (Sum.inl q) f | ⟨Sum.inr q, f⟩ => liftM (liftM (OracleQuery.mk q f))
            source
            @[simp]
            theorem OracleQuery.liftM_right_add_right_add_query {ι₁ : Type u_4} {ι₂ : Type u_1} {ι₃ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} [h : spec₂ ⊂ₒ spec₃] (t : (spec₁ + spec₂).Domain) :
            liftM (query t) = match t with | Sum.inl t => query (Sum.inl t) | Sum.inr t => liftM (liftM (query t))
            source
            instance OracleQuery.subSpec_add_assoc {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} :
            spec₁ + (spec₂ + spec₃) ⊂ₒ spec₁ + spec₂ + spec₃
            Equations
              source
              @[simp]
              theorem OracleQuery.liftM_add_assoc_def {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} {α : Type u} (q : OracleQuery (spec₁ + (spec₂ + spec₃)) α) :
              liftM q = match q with | ⟨Sum.inl t, f⟩ => ⟨Sum.inl (Sum.inl t), f⟩ | ⟨Sum.inr (Sum.inl t), f⟩ => ⟨Sum.inl (Sum.inr t), f⟩ | ⟨Sum.inr (Sum.inr t), f⟩ => ⟨Sum.inr t, f⟩
              source
              @[simp]
              theorem OracleQuery.liftM_add_assoc_query {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} (t : (spec₁ + (spec₂ + spec₃)).Domain) :
              liftM (query t) = match t with | Sum.inl t => query (Sum.inl (Sum.inl t)) | Sum.inr (Sum.inl t) => query (Sum.inl (Sum.inr t)) | Sum.inr (Sum.inr t) => query (Sum.inr t)
              source
              instance OracleQuery.subSpec_sigma {σ : Type u_1} {ι : Type u_2} (specs : σ → OracleSpec ι) (j : σ) :
              specs j ⊂ₒ OracleSpec.sigma specs
              Equations
                source
                @[simp]
                theorem OracleQuery.liftM_sigma_def {α : Type u} {σ : Type u_3} {ι : Type u_1} (specs : σ → OracleSpec ι) (j : σ) (q : OracleQuery (specs j) α) :
                liftM q = OracleQuery.mk ⟨j, q.input⟩ q.cont
                source
                @[simp]
                theorem OracleQuery.liftM_sigma_query {σ : Type u_3} {ι : Type u_1} (specs : σ → OracleSpec ι) (j : σ) (t : (specs j).Domain) :
                liftM (query t) = query ⟨j, t⟩
                source
                @[simp]
                theorem OracleQuery.liftM_eq_liftM_liftM {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_5} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} {α : Type u} [spec₁ ⊂ₒ spec₂] [MonadLift (OracleQuery spec₂) (OracleQuery spec₃)] (q : OracleQuery spec₁ α) :
                liftM q = liftM (liftM q)