Inclusions for combined oracle signatures

Sum and dependent-sum signatures have canonical response-preserving inclusions. The public query equations expose their action for rewriting without unfolding instance implementation details.

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

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

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

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

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

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

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

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