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
@[implicit_reducible, instance 100]
instance OracleQuery.instSubSpecPEmptyEmptySpecOfInhabited {τ : Type u} [Inhabited τ] {spec : OracleSpec τ} :
[]ₒ ⊂ₒ spec

We need Inhabited to prevent infinite type-class searching.

source
@[instance 100]
instance OracleQuery.instLawfulSubSpecPEmptyEmptySpec {τ : Type u} [Inhabited τ] {spec : OracleSpec τ} :
[]ₒ.LawfulSubSpec spec
source
@[implicit_reducible]
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.

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.lawfulSubSpec_add_left {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} :
spec₁.LawfulSubSpec (spec₁ + spec₂)
source
@[implicit_reducible]
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.

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.lawfulSubSpec_add_right {ι₁ : Type u_2} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} :
spec₂.LawfulSubSpec (spec₁ + spec₂)
source
@[implicit_reducible]
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₂
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.lawfulSubSpec_left_add_left_add {ι₁ : Type u_1} {ι₂ : Type u_4} {ι₃ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} [spec₁ ⊂ₒ spec₃] [spec₁.LawfulSubSpec spec₃] :
(spec₁ + spec₂).LawfulSubSpec (spec₃ + spec₂)
source
@[implicit_reducible]
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₃
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.lawfulSubSpec_right_add_right_add {ι₁ : Type u_4} {ι₂ : Type u_1} {ι₃ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} [spec₂ ⊂ₒ spec₃] [spec₂.LawfulSubSpec spec₃] :
(spec₁ + spec₂).LawfulSubSpec (spec₁ + spec₃)
source
@[implicit_reducible]
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₃
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.lawfulSubSpec_add_assoc {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} :
(spec₁ + (spec₂ + spec₃)).LawfulSubSpec (spec₁ + spec₂ + spec₃)
source
@[implicit_reducible]
instance OracleQuery.subSpec_sigma {σ : Type u_1} {ι : Type u_2} (specs : σ → OracleSpec ι) (j : σ) :
specs j ⊂ₒ OracleSpec.sigma specs
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
instance OracleQuery.lawfulSubSpec_sigma {σ : Type u_2} {ι : Type u_1} (specs : σ → OracleSpec ι) (j : σ) :
(specs j).LawfulSubSpec (OracleSpec.sigma specs)
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)