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 100]

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₂

Congruence on the left summand: an inclusion spec₁ ⊂ₒ spec₃ extends to spec₁ + spec₂ ⊂ₒ spec₃ + spec₂.

Low priority so that searches whose source spec is a metavariable (notably the MonadLiftT (OracleComp spec) (OracleComp superSpec) chain behind whole-computation coercions) prefer the direct embeddings subSpec_add_left / subSpec_add_right. This keeps such coercions a single liftComp, definitionally, instead of a stack of lifts through an intermediate 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 100]

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₃

Congruence on the right summand: an inclusion spec₂ ⊂ₒ spec₃ extends to spec₁ + spec₂ ⊂ₒ spec₁ + spec₃.

Low priority for the same reason as subSpec_left_add_left_add_of_subSpec: the direct embeddings must win metavariable-headed searches so that whole-computation coercions stay a single liftComp.

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