Coercing Computations to Larger Oracle Sets

This file defines SubSpec instances for oracle specs constructed with either OracleSpec.add or OracleSpec.sigma. Each instance spells out the monadLift action explicitly (rather than letting it default from onQuery / onResponse) so that the lifted query reduces fully under isDefEq. This is load-bearing for rw / simp lemmas like probEvent_liftComp to find their pattern through the synthesized MonadLiftT instance chain.

@[implicit_reducible, instance 100]

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

We need Inhabited to prevent infinite type-class searching.

@[instance 100]

instance OracleQuery.instLawfulSubSpecPEmptyEmptySpec {τ : Type u} [Inhabited τ] {spec : OracleSpec τ} : []ₒ.LawfulSubSpec spec

@[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.

@[simp]

theorem OracleQuery.liftM_add_left_def {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type u} (q : OracleQuery spec₁ α) : liftM q = OracleQuery.mk (Sum.inl q.input) q.cont

@[simp]

theorem OracleQuery.liftM_add_left_query {ι₁ : Type u_1} {ι₂ : Type u_3} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (t : spec₁.Domain) : liftM (OracleSpec.query t) = OracleSpec.query (Sum.inl t)

instance OracleQuery.lawfulSubSpec_add_left {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : spec₁.LawfulSubSpec (spec₁ + spec₂)

@[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.

@[simp]

theorem OracleQuery.liftM_add_right_def {ι₁ : Type u_2} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type u} (q : OracleQuery spec₂ α) : liftM q = OracleQuery.mk (Sum.inr q.input) q.cont

@[simp]

theorem OracleQuery.liftM_add_right_query {ι₁ : Type u_3} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (t : spec₂.Domain) : liftM (OracleSpec.query t) = OracleSpec.query (Sum.inr t)

instance OracleQuery.lawfulSubSpec_add_right {ι₁ : Type u_2} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : spec₂.LawfulSubSpec (spec₁ + spec₂)

instance OracleQuery.disjointSubSpec_add_left_right {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : spec₁.DisjointSubSpec spec₂ (spec₁ + spec₂)

instance OracleQuery.disjointSubSpec_add_right_left {ι₁ : Type u_2} {ι₂ : Type u_1} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} : spec₂.DisjointSubSpec spec₁ (spec₁ + spec₂)

@[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₂

@[simp]

theorem OracleQuery.liftM_left_add_left_add_def {ι₁ : Type u_1} {ι₂ : Type u_3} {ι₃ : 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

@[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 (OracleSpec.query t) = match t with | Sum.inl t => liftM (liftM (OracleSpec.query t)) | Sum.inr t => OracleSpec.query (Sum.inr t)

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

@[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₃

@[simp]

theorem OracleQuery.liftM_right_add_right_add_def {ι₁ : Type u_3} {ι₂ : 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))

@[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 (OracleSpec.query t) = match t with | Sum.inl t => OracleSpec.query (Sum.inl t) | Sum.inr t => liftM (liftM (OracleSpec.query t))

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₃)

@[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₃

@[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⟩

@[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 (OracleSpec.query t) = match t with | Sum.inl t => OracleSpec.query (Sum.inl (Sum.inl t)) | Sum.inr (Sum.inl t) => OracleSpec.query (Sum.inl (Sum.inr t)) | Sum.inr (Sum.inr t) => OracleSpec.query (Sum.inr t)

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₃)

@[implicit_reducible]

instance OracleQuery.subSpec_sigma {σ : Type u_1} {ι : Type u_2} (specs : σ → OracleSpec ι) (j : σ) : specs j ⊂ₒ OracleSpec.sigma specs

@[simp]

theorem OracleQuery.liftM_sigma_def {α : Type u} {σ : Type u_2} {ι : Type u_1} (specs : σ → OracleSpec ι) (j : σ) (q : OracleQuery (specs j) α) : liftM q = OracleQuery.mk ⟨j, q.input⟩ q.cont

@[simp]

theorem OracleQuery.liftM_sigma_query {σ : Type u_3} {ι : Type u_1} (specs : σ → OracleSpec ι) (j : σ) (t : (specs j).Domain) : liftM (OracleSpec.query t) = OracleSpec.query ⟨j, t⟩

instance OracleQuery.lawfulSubSpec_sigma {σ : Type u_2} {ι : Type u_1} (specs : σ → OracleSpec ι) (j : σ) : (specs j).LawfulSubSpec (OracleSpec.sigma specs)

@[simp]

theorem OracleQuery.liftM_eq_liftM_liftM {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_4} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} {α : Type u} [spec₁ ⊂ₒ spec₂] [MonadLift (OracleQuery spec₂) (OracleQuery spec₃)] (q : OracleQuery spec₁ α) : liftM q = liftM (liftM q)