Coercions Between Computations With Additional Oracles #
This file defines the SubSpec relation between pairs of OracleSpecs. An
instance spec ⊂ₒ superSpec packages the data of a polynomial-functor lens
PFunctor.Lens spec.toPFunctor superSpec.toPFunctor between the underlying
PFunctors, given by
onQuery : spec.Domain → superSpec.Domain--- forward translation on query inputs (oracle indices), andonResponse : (t : spec.Domain) → superSpec.Range (onQuery t) → spec.Range t--- fiberwise backward translation on query responses.
By the Yoneda lemma this lens data is in bijection with natural transformations
OracleQuery spec → OracleQuery superSpec. The class therefore extends MonadLift (OracleQuery spec) (OracleQuery superSpec). Concrete instances
spell monadLift out alongside the lens data and discharge the
propositional coherence liftM_eq_lift (typically rfl); see the class
docstring for why the monadLift field is not defaulted.
We use the notation spec ⊂ₒ spec' to represent this inclusion. The
non-inclusive subset symbol reflects that we avoid defining SubSpec
reflexively, since MonadLiftT.refl already handles the identity case.
LawfulSubSpec refines SubSpec with the requirement that onResponse is
bijective on every fiber, i.e. that the underlying lens is cartesian in
the sense of PFunctor.Lens.IsCartesian. This is strictly weaker than
PFunctor.Lens.Equiv (which would also require onQuery to be a bijection,
ruling out the basic case spec ⊂ₒ (spec + spec') where onQuery = Sum.inl).
Cartesianness is exactly the condition needed to preserve the uniform
distribution under lifting (evalDist_liftComp); see
LawfulSubSpec.toLens_isCartesian for the bridge to the lens-level
predicate.
Inclusion of one set of oracles into another, packaged as a polynomial-functor
lens between the underlying OracleSpecs. Carries the forward translation
onQuery on query inputs and the fiberwise backward translation onResponse
on query responses, plus the resulting MonadLift action.
We extends MonadLift (OracleQuery spec) (OracleQuery superSpec) so that
typeclass synthesis can derive MonadLift (and therefore MonadLiftT)
through the structure projection SubSpec.toMonadLift. The monadLift
field is not defaulted: each concrete SubSpec instance must spell it
out, alongside onQuery / onResponse, and discharge the propositional
coherence liftM_eq_lift (typically by rfl).
Spelling monadLift out explicitly (rather than defaulting it from the
lens data) is what makes the lifted query fully reduce during rw / simp
pattern matching against lemmas like probEvent_liftComp. A defaulted
monadLift field becomes opaque to isDefEq once it travels through the
MonadLiftT instance chain, which silently breaks rewriting.
Informally, spec ⊂ₒ superSpec says that any query to an oracle of spec
can be perfectly simulated by a query to an oracle of superSpec. We avoid
the built-in Subset notation because we care about the actual data of the
mapping (it is needed when defining type coercions), not just its existence.
Forward translation on query inputs (oracle indices).
Fiberwise backward translation on query responses.
- liftM_eq_lift {β : Type w} (q : OracleQuery spec β) : MonadLift.monadLift q = ⟨onQuery q.input, q.cont ∘ onResponse q.input⟩
Instances
Inclusion of one set of oracles into another, packaged as a polynomial-functor
lens between the underlying OracleSpecs. Carries the forward translation
onQuery on query inputs and the fiberwise backward translation onResponse
on query responses, plus the resulting MonadLift action.
We extends MonadLift (OracleQuery spec) (OracleQuery superSpec) so that
typeclass synthesis can derive MonadLift (and therefore MonadLiftT)
through the structure projection SubSpec.toMonadLift. The monadLift
field is not defaulted: each concrete SubSpec instance must spell it
out, alongside onQuery / onResponse, and discharge the propositional
coherence liftM_eq_lift (typically by rfl).
Spelling monadLift out explicitly (rather than defaulting it from the
lens data) is what makes the lifted query fully reduce during rw / simp
pattern matching against lemmas like probEvent_liftComp. A defaulted
monadLift field becomes opaque to isDefEq once it travels through the
MonadLiftT instance chain, which silently breaks rewriting.
Informally, spec ⊂ₒ superSpec says that any query to an oracle of spec
can be perfectly simulated by a query to an oracle of superSpec. We avoid
the built-in Subset notation because we care about the actual data of the
mapping (it is needed when defining type coercions), not just its existence.
Instances For
The lens action on a single query: forward on the input, post-compose the
backward fiber on the continuation. Used as the canonical reduced form of
liftM q for proofs that need to inspect the resulting query.
Instances For
The polynomial-functor lens between the underlying PFunctors carried by
a SubSpec instance. This is the lens-level view of the data; concrete
properties (like cartesianness via LawfulSubSpec) are stated on this lens.
The other half of the data, monadLift, is fixed by liftM_eq_lift to be
the standard action of this lens on OracleQuery.
Instances For
Transitivity of SubSpec: lens composition.
Instances For
LawfulSubSpec extends SubSpec with the requirement that the backward
translation onResponse is bijective on every fiber. Equivalently: the
underlying lens SubSpec.toLens is cartesian in the sense of
PFunctor.Lens.IsCartesian, i.e. it is a fiberwise isomorphism over an
arbitrary forward map on positions.
This is strictly weaker than PFunctor.Lens.Equiv, which would also force
onQuery to be a bijection. We intentionally only require fiberwise
bijectivity because the canonical SubSpec instances embed a small spec
into a larger one (e.g. spec₁ ⊂ₒ (spec₁ + spec₂) with onQuery = Sum.inl),
and these embeddings are essential to the API.
Cartesianness is exactly what is needed to preserve the uniform distribution
under the lift: see evalDist_liftM_query and the bridge
LawfulSubSpec.toLens_isCartesian.
- onResponse_bijective (t : spec.Domain) : Function.Bijective (SubSpec.onResponse t)
The backward translation is bijective on every fiber.
Instances
Lawful oracle-spec inclusion: a SubSpec whose response translation is
bijective on every fiber.
Instances For
The lens-level statement of LawfulSubSpec: the underlying
PFunctor.Lens is cartesian. This makes the dictionary between the
oracle-spec layer and the polynomial-functor lens layer explicit.
Pushing the uniform distribution on superSpec.Range through the lens's
backward fiber recovers the uniform distribution on spec.Range. Load-bearing
for evalDist_liftComp below.
Two oracle-spec inclusions into the same ambient spec have disjoint query images.
This is stronger than LawfulSubSpec: lawfulness preserves the distribution of
responses under lifting, while disjointness says the two lifted query namespaces
do not overlap inside the ambient interface.
The two forward query maps have disjoint images.
Instances
Oracle-spec inclusions with disjoint query images in an ambient interface.
Instances For
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.
Instances For
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-inMonadLiftT.refl(which is definitionallyid) wins typeclass resolution. This is whatStd.Do.Spec.UnfoldLift.monadLift_refl(arfl-based lemma) needs in order to peel off spurious self-lifts insidemvcgen-elaborated terms.For
MonadLiftT (OracleQuery spec) (OracleComp superSpec), the built-in high-priorityMonadLift (OracleQuery superSpec) (OracleComp superSpec)is tried first bymonadLiftTransand succeeds via theSubSpecchain onOracleQuery, never reaching this instance. Single-query lifts therefore go through the standard "lift query then embed" path with no spurious walk throughliftComp.For
MonadLiftT (OracleComp spec) (OracleComp superSpec)withspec ≠ superSpec, the high-priority built-in fails (noMonadLiftT (OracleComp _) (OracleQuery _)), Lean backtracks to this low-priority instance, and the recursive subgoal collapses viaMonadLiftT.refl. The result is a singleliftComp mx superSpec.
We choose to actively rewrite liftComp as liftM to enable LawfulMonadLift lemmas.
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.
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).