Typeclasses for Denotational Monad Semantics #
This file builds atop MonadLiftT m SPMF / MonadLiftT m PMF for assigning denotational
probability semantics to monadic computations. We also introduce functions
probOutput, probEvent, and probFailure with associated notation.
-- dtumad: document various probability notation definitions here
MonadLiftT m SetM and MonadLiftT m SPMF #
The SetM / SPMF lifts exposed by this layer are declared as MonadLiftT,
not MonadLift. Total semantic sources may still expose a plain MonadLift
into PMF; the important point here is that support is never obtained by a
transitive m → SPMF → SetM path, and parameterized/typeclass-gated
probability lifts avoid MonadLift instance search. There are two independent
reasons.
No transitive SPMF → SetM lift. The MonadLiftT SPMF SetM instance below
exists so support and friends work on raw SPMF α. Crucially it is declared
as MonadLiftT rather than MonadLift, which means Lean's monadLiftTrans
(which requires MonadLift n o for the outer hop) cannot chain it: a monad
m with MonadLiftT m SPMF does not automatically gain MonadLiftT m SetM
via transitivity. Each monad declares its MonadLiftT m SetM directly — e.g.
OracleComp uses the syntactic simulateQ into SetM (which doesn't require
[spec.Fintype]), and EvalDistCompatible records the propositional coherence
between that syntactic support and SPMF.support ∘ evalDist.
Resolution fragility for parameterized + typeclass-gated lifts. Lifts whose
source is parameterized (OracleComp spec, OptionT m, StateT σ m, …) and
which are gated by a typeclass on the parameter ([IsProbabilitySpec spec],
[MonadLiftT m SPMF], …) must also be MonadLiftT, not MonadLift. Demoting
to MonadLift forces Lean to find the instance through its transitive
instance, whose outer hop is MonadLift n o with n a semiOutParam. When
the recursion lands on a parameterized head like MonadLift (OracleComp ?spec) PMF,
Lean has to simultaneously unify ?spec through the semiOutParam, discharge
the typeclass premise on ?spec, and pin down ?spec from the inner reflexive
premise — a combination Lean's instance search refuses to chase. The direct
MonadLiftT declaration sidesteps this with a single-step head match.
Direct MonadLiftT SPMF SetM (only on SPMF itself — not the transitive
MonadLift that would create a diamond).
Coherence between support (via MonadLiftT m SetM) and evalDist
(via MonadLiftT m SPMF): x ∈ support mx iff Pr[= x | mx] ≠ 0.
This typeclass is exported by every monad that admits both lifts and they
agree on outputs — i.e. support mx = SPMF.support (evalDist mx).
Instances
SPMF is trivially compatible: both lifts coincide on the nose.
Evaluation distribution notation for any monad lifting into SPMF.
Instances For
Probability that a computation mx returns the value x.
Instances For
Probability that a computation mx will fail to return a value.
Instances For
Probability that a computation returns a particular output.
Instances For
Probability that a computation returns a value satisfying a predicate.
Instances For
Probability that a computation fails to return a value.
Instances For
Alias of the forward direction of probOutput_eq_zero_iff.
Alias of the reverse direction of probOutput_eq_zero_iff.
Alias of the reverse direction of zero_eq_probOutput_iff.
Alias of the reverse direction of probOutput_eq_zero_iff'.
Alias of the forward direction of probOutput_eq_zero_iff'.
Alias of the reverse direction of zero_eq_probOutput_iff'.
Alias of the reverse direction of probOutput_pos_iff.
Alias of the forward direction of probOutput_pos_iff.
Alias of the reverse direction of probOutput_pos_iff'.
Alias of the forward direction of probOutput_pos_iff'.
Alias of the reverse direction of probEvent_eq_zero_iff.
Alias of the reverse direction of probEvent_eq_zero_iff'.
Alias of the reverse direction of probEvent_ne_zero_iff.
Alias of the reverse direction of probEvent_ne_zero_iff'.
Alias of the reverse direction of probEvent_pos_iff.
Alias of the reverse direction of probEvent_pos_iff'.
Set.Nonempty companion to the simp-only probEvent_ne_zero_iff: the event has positive
probability iff some reachable output satisfies p. The Set.Nonempty witness stays atomic under
grind (unlike the saturating ∃ x ∈ support mx, p x form). Mirrors
probFailure_eq_one_iff_not_nonempty.
Deliberately NOT in the default grind set: together with probEvent_eq_zero_iff_not_nonempty
and probFailure_eq_one_iff_not_nonempty it re-forms a saturation cycle in the generic-monad
context (grind times out on the probEvent_eq_one_iff statement shape with all three tagged;
dropping any one of the trio restores fail-fast, and dropping this one is free: grind recovers
≠ 0 ↔ Nonempty from the kept = 0 ↔ ¬ Nonempty sibling by classical negation). Gated by
VCVioTest/GrindFailFast.lean.
grind-friendly companion to the simp-only probEvent_eq_zero_iff: the event has probability
zero iff no reachable output satisfies p, phrased via Set.Nonempty rather than the saturating
∀ x ∈ support mx, ¬ p x. The negation of probEvent_ne_zero_iff_nonempty.
If two events are equivalent on the support of mx then they have the same output chance.
Probability that a computation returns a value satisfying a predicate.
Instances For
Probability that a computation returns a value satisfying a predicate.
See probOutput_true_eq_probEvent for relation to the above definitions.
Instances For
Probability bounds and total-probability sums #
Alias of the reverse direction of probOutput_eq_one_iff.
Alias of the reverse direction of one_eq_probOutput_iff.
Alias of the reverse direction of probOutput_eq_one_iff'.
Alias of the reverse direction of one_eq_probOutput_iff'.
If a non-failing computation can only return x, then it returns x with probability one.
grind-friendly companion to probFailure_eq_one_iff: phrasing "fails with probability one"
via Set.Nonempty — which grind keeps atomic — avoids the support quantifier that makes the
support = ∅ form saturate, so this stays in the default grind set.
Lemmas for monads with a total PMF denotation #
These lemmas hold when m lifts into PMF (so computations never fail). They expose the
absence of failure mass and total normalization of the resulting distribution.
First-moment / Markov bound. The probability of p is at most the expectation of any
ℝ≥0∞-valued cost c that is ≥ 1 wherever p holds. This is the elementary core of a
first-moment (union) argument: a monotone "bad" event whose occurrence forces a unit of some
nonnegative cost has probability bounded by the expected cost.
First-moment / Markov bound (support-restricted cost). Variant of
probEvent_le_tsum_probOutput_mul_cost whose c ≥ 1 hypothesis need only hold on the
support of mx.
If p implies q on the support of a computation then it is more likely to happen.
If p implies q on the finSupport of a computation then it is more likely to happen.
If p implies q everywhere then p is less likely than q. Convenience
specialisation of probEvent_mono that drops the support hypothesis.
Alias of the reverse direction of probEvent_eq_one_iff.
Pointwise variant of probOutput_eq_one_iff: Pr[= x | mx] = 1 iff the support is
a subset of {x} (phrased as a forall over the support) and the computation never fails.
More usable than probOutput_eq_one_iff when the caller wants to iterate over arbitrary
support elements rather than prove a set equality.
Alias of the reverse direction of one_eq_probEvent_iff.
Alias of the reverse direction of probEvent_eq_one_iff'.
Alias of the reverse direction of one_eq_probEvent_iff'.