Output Distribution of Computations #
This file defines the MonadLiftT-based probability and support semantics for OracleComp.
A per-query distribution on an OracleSpec. Each query index t : ι is
assigned a PMF (spec t) for its responses. This is the abstract data needed
to lift OracleComp spec into PMF; uniformity is not assumed — see
IsUniformSpec for the uniform-sampling specialization.
Specs that should opt into uniform sampling are best registered via
IsUniformSpec, which extends this class and additionally carries
Fintype / Inhabited on each range plus a propositional witness that
toPMF is the canonical uniform distribution.
- toPMF (t : ι) : PMF (spec t)
The distribution of responses to query
t.
Instances
An OracleSpec whose responses are uniformly sampled from finite, inhabited
ranges. Bundles spec.Fintype, spec.Inhabited, and IsProbabilitySpec spec
together with a Prop witness that the per-query distribution agrees with
PMF.uniformOfFintype. Use this as the canonical input to lemmas that
mention Fintype.card (spec.Range _) or PMF.uniformOfFintype in their
statements.
- fintype : spec.Fintype
Every response set is finite.
- inhabited : spec.Inhabited
Every response set is inhabited.
The per-query distribution is the uniform distribution on the response set.
Instances
Bridge from [spec.Fintype] [spec.Inhabited] to IsUniformSpec spec.
Deliberately not an instance — IsUniformSpec must be opted into per
spec so that uniform-sampling semantics never attach silently to a spec
whose author didn't intend a probabilistic interpretation. Use this
helper when declaring IsUniformSpec for a concrete spec.
Instances For
Propagate IsUniformSpec through +: each summand's uniformity is
preserved on its branch. IsProbabilitySpec (spec + spec') is derived via
the extends chain.
Successor to the legacy empty marker OracleSpec.IsProbSpec. The replacement
IsUniformSpec bundles Fintype, Inhabited, IsProbabilitySpec, and a uniformity
witness.
Instances For
Embed OracleComp into PMF by interpreting each query via the per-query
distribution provided by IsProbabilitySpec.
Direct MonadLiftT (OracleComp spec) SetM: the syntactic / operational
support of mx, computed by folding queries to Set.univ. Independent of any
probability structure on spec — works for arbitrary specs without Fintype
or Inhabited. The bridge to the probability side is EvalDistCompatible
below, supplied only when [IsUniformSpec spec].
Note: This is the only MonadLiftT (OracleComp spec) SetM instance Lean will
find. The generic MonadLiftT SPMF SetM is declared as MonadLiftT (not
MonadLift), so monadLiftTrans cannot chain OracleComp → SPMF → SetM.
Abstract distribution of a single lifted query under IsProbabilitySpec:
the per-query distribution toPMF is pushed forward through the query's
continuation. Uniform-content sibling: evalDist_liftM.
liftM (query t) : OracleComp spec _ evaluates to the per-query distribution
IsProbabilitySpec.toPMF t, lifted to SPMF.
Alias of OracleComp.support_query.
Support-aware bind congruence: if two continuations agree on all elements in the support
of mx, the resulting bind computations are equal.
Finite version of support for when oracles have a finite set of possible outputs.
NOTE: we can't use simulateQ because Finset lacks a Monad instance.
OracleComp spec admits the bridge between its direct support semantics and the
SPMF.support of its evalDist.
An output has non-zero probability in evalDist iff it is in computation support.
Alias of the forward direction of OracleComp.mem_support_evalDist_iff.
An output has non-zero probability in evalDist iff it is in computation support.
Alias of the reverse direction of OracleComp.mem_support_evalDist_iff.
An output has non-zero probability in evalDist iff it is in computation support.
Finite-support variant of mem_support_evalDist_iff.
Alias of the reverse direction of OracleComp.mem_support_evalDist_iff'.
Finite-support variant of mem_support_evalDist_iff.
Alias of the forward direction of OracleComp.mem_support_evalDist_iff'.
Finite-support variant of mem_support_evalDist_iff.
Two events have equal probabilities when their predicates agree on the support of the first computation and the two computations share an evaluation distribution.
Probabilities of orElse (<|>) #
oa <|> oa' runs oa, falling back to oa' only when oa returns none. The base OracleComp
never fails, so the two failure events are independent: oa <|> oa' fails exactly when both do, and
an output comes either from oa or — on oa's failure mass — from oa'. (support_orElse is left
as a future addition; it follows from probOutput_orElse via the support↔probability bridge.)
If an oracle implementation preserves the distribution of each source query, then
simulateQ preserves the distribution of every source computation.
The possible outputs of mx when queries can output values in the specified sets.
NOTE: currently proofs using this should reduce to simulateQ. A full API would be better
Instances For
Reachable outputs of a bind are the reachable outputs of the continuation over reachable outputs of the first computation.
Membership form of [OracleComp.supportWhen_bind].
Enlarging the set of possible oracle outputs only enlarges the reachable output set.
The output distribution of mx when queries follow the specified distribution.
Instances For
obtain-friendly bind support peeler at the bare OracleComp level. Unlike rw [mem_support_bind_iff], applying this lemma to a hypothesis uses definitional unification to
match mx >>= f, so it engages through the Monad/MonadLift instance-tree mismatches that block
the syntactic rw (the elaborated OracleComp.instMonad/Bind.bind spelling produced by
unfolding nested protocol definitions differs syntactically from the canonical >>=).
obtain-friendly pure support resolver at the bare OracleComp level: y ∈ support (pure a) forces y = a, matched by definitional unification (so it engages on the
PFunctor.FreeM.pure spelling that the syntactic support_pure rw rejects).
obtain-friendly <$> (map) support peeler at the bare OracleComp level: y ∈ support (g <$> mx) yields a preimage a ∈ support mx with y = g a, matched by definitional unification
(so it engages on the elaborated Functor.map/OracleComp.instMonad spelling that the syntactic
support_map rw rejects).
Support-level peeler for an OptionT-monadic bind, stated at the underlying
OracleComp-level .run: every element y of the support of the run of mx >>= f factors
through an intermediate some a in mx's run support and a y in the run support of f a,
unless mx's run can produce none (in which case y may be that none). Companion to
OptionT.mem_support_bind_mk for the case where the OptionT.run has already been stripped to
the bare underlying computation.
Applies to a hypothesis y ∈ support oa whenever oa is definitionally (mx >>= f).run
(the OptionT.run is identity), so callers need not respell the full bind term.
OptionT.lift-headed specialization of mem_support_run_bind: a lifted (hence
never-failing) first computation oa peels cleanly, with the intermediate value living in
support oa directly (no none branch).