Computations that Never Fail

This file defines a predicate-as-typeclass stating that a probabilistic computation never produces failure mass, together with lemmas for how the property behaves under common monadic combinators.

Given a HasEvalSPMF m instance and a computation mx : m α in that monad, NeverFail mx means that Pr[⊥ | mx] = 0, i.e. that the computation never fails.

Defined as a typeclass to allow it to be synthesized automatically in certain cases. However we don't include any instances for bind as this blows up the search space. Instances involving bind should be added manually as needed.

The existence of a HasEvalPMF m instance implies that NeverFail mx holds for any computaiton in the monad, since the PMF doesn't allow any probability of failing.

class NeverFail {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) : Prop

NeverFail mx states that the computation mx : m α has zero probability of failure, equivalently the mass of (evalDist mx) at none is 0.

Formally: NeverFail mx iff Pr[⊥ | mx] = 0.

Remarks:

• This class is a predicate (Prop-valued). It does not add data.
• Use the lemmas in this file (e.g. bind_of_mem_support) to transport the property through monadic structure. We intentionally avoid a bind instance, as the natural condition depends on the support of the left-hand side.

• probFailure_eq_zero : Pr[⊥ | mx] = 0

theorem probFailure_eq_zero' {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} (h : NeverFail mx) : Pr[⊥ | mx] = 0

Version of probFailure_eq_zero that avoids typeclass search.

instance HasEvalPMF.instNeverFail {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] (mx : m α) : NeverFail mx

A computation in a monad with HasEvalPMF can't fail as outputs sum to probability 1.

theorem HasEvalSPMF.neverFail_iff {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) : NeverFail mx ↔ Pr[⊥ | mx] = 0

@[simp]

instance HasEvalSPMF.neverFail_pure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (x : α) : NeverFail (pure x)

@[simp]

theorem HasEvalSPMF.neverFail_bind_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (my : α → m β) : NeverFail (mx >>= my) ↔ NeverFail mx ∧ ∀ x ∈ support mx, NeverFail (my x)

@[simp]

theorem HasEvalSPMF.neverFail_map_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (f : α → β) : NeverFail (f <$> mx) ↔ NeverFail mx

@[simp]

theorem HasEvalSet.not_neverFail_failure {α : Type u} {m : Type u → Type v} [AlternativeMonad m] [HasEvalSPMF m] [HasEvalSet.LawfulFailure m] : ¬NeverFail failure

theorem NeverFail.of_probFailure_eq_zero {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (h : Pr[⊥ | mx] = 0) : NeverFail mx

@[simp]

instance NeverFail.instPure {α : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {x : α} : NeverFail (pure x)

If mx is a pure return, it never fails. This follows since evalDist (pure x) is the Dirac distribution on some x.

theorem NeverFail.bind_of_mem_support {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} [hx : NeverFail mx] (hy : ∀ x ∈ support mx, NeverFail (my x)) : NeverFail (mx >>= my)

Precise bind lemma: if mx never fails and for all x in the support of mx the continuation my x never fails, then the whole bind never fails.

Sketch: using evalDist_bind and the identity

Pr[⊥ | mx >>= my] = Pr[⊥ | mx] + ∑ x, Pr[= x | mx] * Pr[⊥ | my x],

the first term vanishes by NeverFail mx, while for x ∉ support mx the coefficient Pr[= x | mx] is 0, and for x ∈ support mx the second factor vanishes by hypothesis. Hence the sum is 0.

theorem NeverFail.bind_of_forall {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} [hx : NeverFail mx] [hy : ∀ (x : α), NeverFail (my x)] : NeverFail (mx >>= my)

Weak bind lemma: if the right-hand side never fails for every possible input (∀ x), then the bind never fails.

This is a convenience corollary of bind_of_mem_support; it is often easy to apply when my is uniform in its input (e.g. ignores it) or is known to be never-failing globally.

@[simp]

instance NeverFail.instMap {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {mx : m α} [h : NeverFail mx] (f : α → β) : NeverFail (f <$> mx)

Mapping a value through a total function preserves NeverFail.

@[simp]

instance NeverFail.instSeq {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {mf : m (α → β)} {mx : m α} [hf : NeverFail mf] [hx : NeverFail mx] : NeverFail (mf <*> mx)

If both the function computation and the argument computation never fail, then their applicative sequencing also never fails.

@[simp]

instance NeverFail.instSeqLeft {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {mx : m α} {my : m β} [hx : NeverFail mx] [hy : NeverFail my] : NeverFail (mx <* my)

If mx and my never fail, then mx <* my never fails.

@[simp]

instance NeverFail.instSeqRight {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] {mx : m α} {my : m β} [hx : NeverFail mx] [hy : NeverFail my] : NeverFail (mx *> my)

If mx and my never fail, then mx *> my never fails.