Coercions Between Computations With Additional Oracles

This file defines a isSubSpec relation for pairs of oracleSpec where one can be thought of as an extension of the other with additional oracles. The definition consists is a thin wrapper around a MonadLift instance on OracleQuery, which extends to a lifting operation on OracleComp.

We use the notation spec ⊂ₒ spec' to represent that one set of oracles is a subset of another, where the non-inclusive subset symbol reflects that we avoid defining this instance reflexively.

class OracleSpec.SubSpec {ι : Type u} {τ : Type v} (spec : OracleSpec ι) (superSpec : OracleSpec τ) extends MonadLift (OracleQuery spec) (OracleQuery superSpec) : Type (max (max (max u (u_1 + 1)) v) w)

Relation defining an inclusion of one set of oracles into another, where the mapping doesn't affect the underlying probability distribution of the computation. Informally, spec ⊂ₒ superSpec means that for any query to an oracle of sub_spec, it can be perfectly simulated by a computation using the oracles of superSpec.

We avoid implementing this via the built-in subset notation as we care about the actual data of the mapping rather than just its existence, which is needed when defining type coercions.

• monadLift {α : Type u_1} : OracleQuery spec α → OracleQuery superSpec α
• liftM_map {α β : Type u_1} (q : OracleQuery spec α) (f : α → β) : liftM (f <$> q) = f <$> liftM q

def OracleSpec.«term_⊂ₒ_» : Lean.TrailingParserDescr

@[reducible]

def OracleSpec.SubSpec.trans {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {κ : Type w'} {spec₃ : OracleSpec κ} (h₁ : spec ⊂ₒ superSpec) (h₂ : superSpec ⊂ₒ spec₃) : spec ⊂ₒ spec₃

Transitivity for SubSpec: if spec₁ ⊂ₒ spec₂ and spec₂ ⊂ₒ spec₃, then spec₁ ⊂ₒ spec₃.

class OracleSpec.LawfulSubSpec {ι : Type u} {τ : Type v} (spec : OracleSpec ι) (superSpec : OracleSpec τ) [h : spec ⊂ₒ superSpec] : Prop

LawfulSubSpec extends SubSpec with the requirement that lifting preserves distributions. The axiom requires that the continuation of each lifted query is a bijection from the super-range to the sub-range, which guarantees that the uniform distribution is preserved under the mapping.

• cont_bijective (t : spec.Domain) : Function.Bijective (MonadLift.monadLift (OracleQuery.query t)).snd

theorem OracleSpec.LawfulSubSpec.evalDist_liftM_query {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] [superSpec.Fintype] [superSpec.Inhabited] [spec.Fintype] [spec.Inhabited] (t : spec.Domain) : PMF.map (MonadLift.monadLift (OracleQuery.query t)).snd (PMF.uniformOfFintype (superSpec.Range (MonadLift.monadLift (OracleQuery.query t)).fst)) = PMF.uniformOfFintype (spec.Range t)

def OracleComp.liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (mx : OracleComp spec α) (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] : OracleComp superSpec α

Lift a computation from spec to superSpec using a SubSpec instance on queries. Usually liftM should be preferred but this can allow more explicit annotation.

theorem OracleComp.liftComp_def {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (mx : OracleComp spec α) : mx.liftComp superSpec = simulateQ (fun (t : spec.Domain) => liftM (query t)) mx

@[simp]

theorem OracleComp.liftComp_pure {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (x : α) : (pure x).liftComp superSpec = pure x

@[simp]

theorem OracleComp.liftComp_query {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (q : OracleQuery spec α) : (liftM q).liftComp superSpec = q.cont <$> liftM (query q.input)

@[simp]

theorem OracleComp.liftComp_bind {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (mx : OracleComp spec α) (ob : α → OracleComp spec β) : (mx >>= ob).liftComp superSpec = do let x ← mx.liftComp superSpec (ob x).liftComp superSpec

@[simp]

theorem OracleComp.liftComp_map {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (mx : OracleComp spec α) (f : α → β) : (f <$> mx).liftComp superSpec = f <$> mx.liftComp superSpec

@[simp]

theorem OracleComp.liftComp_seq {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {α β : Type w} (superSpec : OracleSpec τ) [h : MonadLiftT (OracleQuery spec) (OracleQuery superSpec)] (og : OracleComp spec (α → β)) (mx : OracleComp spec α) : (og <*> mx).liftComp superSpec = og.liftComp superSpec <*> mx.liftComp superSpec

@[simp]

theorem OracleComp.evalDist_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [spec.Fintype] [spec.Inhabited] [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) : evalDist (mx.liftComp superSpec) = evalDist mx

@[simp]

theorem OracleComp.probOutput_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [spec.Fintype] [spec.Inhabited] [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) (x : α) : Pr[= x | mx.liftComp superSpec] = Pr[= x | mx]

@[simp]

theorem OracleComp.probEvent_liftComp {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [spec.Fintype] [spec.Inhabited] [superSpec.Fintype] [superSpec.Inhabited] [h : spec ⊂ₒ superSpec] [spec.LawfulSubSpec superSpec] (mx : OracleComp spec α) (p : α → Prop) : probEvent (mx.liftComp superSpec) p = probEvent mx p

@[implicit_reducible, instance 100]

instance OracleComp.instMonadLiftOfOracleQuery {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : MonadLift (OracleComp spec) (OracleComp superSpec)

Extend a lifting on OracleQuery to a lifting on OracleComp.

Registered as a low-priority MonadLift (not MonadLiftT) so that:

• For spec = superSpec, Lean's built-in MonadLiftT.refl (which is definitionally id) wins typeclass resolution. This is what Std.Do.Spec.UnfoldLift.monadLift_refl (a rfl-based lemma) needs in order to peel off spurious self-lifts inside mvcgen-elaborated terms.

• For MonadLiftT (OracleQuery spec) (OracleComp superSpec), the built-in high-priority MonadLift (OracleQuery superSpec) (OracleComp superSpec) is tried first by monadLiftTrans and succeeds via the SubSpec chain on OracleQuery, never reaching this instance. Single-query lifts therefore go through the standard "lift query then embed" path with no spurious walk through liftComp.

• For MonadLiftT (OracleComp spec) (OracleComp superSpec) with spec ≠ superSpec, the high-priority built-in fails (no MonadLiftT (OracleComp _) (OracleQuery _)), Lean backtracks to this low-priority instance, and the recursive subgoal collapses via MonadLiftT.refl. The result is a single liftComp mx superSpec.

@[simp]

theorem OracleComp.liftComp_eq_liftM {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] (mx : OracleComp spec α) : mx.liftComp superSpec = liftM mx

We choose to actively rewrite liftComp as liftM to enable LawfulMonadLift lemmas.

instance OracleComp.instLawfulMonadLift {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : LawfulMonadLift (OracleComp spec) (OracleComp superSpec)

@[simp]

theorem OracleComp.monadLift_eq_self {ι : Type u} {spec : OracleSpec ι} {α : Type u_1} (mx : OracleComp spec α) : monadLift mx = mx

Self-lift on OracleComp is definitionally id, supplied by Lean's built-in MonadLiftT.refl thanks to the low-priority MonadLift instance above (which causes the parametric path to lose typeclass resolution to MonadLiftT.refl when spec = superSpec).

Regression smoke-tests for the instance-priority invariants above. The rfl proofs are the load-bearing signal: if priority drifts so that the parametric MonadLift beats MonadLiftT.refl, the self-lift stops being definitionally id and the rfl below breaks. Similarly, the MonadLiftT synthesis check guards against future refactors that would remove the transitive lift chain.

@[implicit_reducible]

instance OracleComp.instMonadLiftOptionTOfOracleQuery {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : MonadLift (OptionT (OracleComp spec)) (OptionT (OracleComp superSpec))

@[simp]

theorem OracleComp.liftM_OptionT_eq {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] (mx : OptionT (OracleComp spec) α) : liftM mx = have impl := fun (t : spec.Domain) => liftM (query t); simulateQ impl mx

@[simp]

theorem OracleComp.liftM_failure {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : liftM failure = failure

instance OracleComp.instLawfulMonadLiftOptionT {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : LawfulMonadLift (OptionT (OracleComp spec)) (OptionT (OracleComp superSpec))

@[simp]

theorem OracleComp.monadLift_liftM_OptionT {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] (mx : OracleComp spec α) : monadLift (liftM mx) = liftM mx

Coherence: lifting an OracleComp to a superspec and then into OptionT via the standard MonadLift equals lifting directly through the transitive MonadLiftT chain (which goes through the simulateQ-based OptionT MonadLift instance).

@[implicit_reducible]

instance OracleComp.instMonadLiftStateTOfOracleQuery {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {σ : Type u_1} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] : MonadLift (StateT σ (OracleComp spec)) (StateT σ (OracleComp superSpec))

@[simp]

theorem OracleComp.liftM_StateT_eq {ι : Type u} {τ : Type v} {spec : OracleSpec ι} {superSpec : OracleSpec τ} {α σ : Type w} [MonadLift (OracleQuery spec) (OracleQuery superSpec)] (mx : StateT σ (OracleComp spec) α) : liftM mx = StateT.mk fun (s : σ) => liftM (mx.run s)