Support Analysis for Sub-Distributions

This file provides key lemmas for extracting support information from sub-distribution operations, particularly SDistr.bind.

Main results

• SDistr.bind_support_witness - If (d.bind f)(some b) ≠ 0, then there exists an intermediate value a with d(some a) ≠ 0 and (f a)(some b) ≠ 0.
• tsum_option_split - Split a sum over Option α into the none term plus the sum over some terms.
• tsum_some_eq_mass - The sum over some outcomes equals the mass.

Motivation

These lemmas are the foundation for the unary probabilistic Hoare logic (pHL) proof rules, particularly pHoare_bind and pHoare_sample. They extract existential witnesses from nonzero probability observations.

References

• EasyCrypt: support analysis in pRHL rnd tactic
• CertiCrypt (Barthe et al.): coupling and support reasoning in Coq

Splitting sums over Option

theorem CatCrypt.Prob.tsum_option_split {α : Type u_1} (f : Option α → ENNReal) : ∑' (x : Option α), f x = f none + ∑' (a : α), f (some a)

Sum over Option α splits into the none term plus sum over some terms. This is a fundamental decomposition for reasoning about sub-distributions.

theorem CatCrypt.Prob.tsum_some_eq_mass {α : Type u_1} (d : SDistr α) : ∑' (a : α), d (some a) = d.mass

The sum over some outcomes equals the mass of the distribution.

theorem CatCrypt.Prob.tsum_some_of_mass_one {α : Type u_1} (d : SDistr α) (h : d.mass = 1) : ∑' (a : α), d (some a) = 1

If mass = 1, the sum over some outcomes equals 1.

theorem CatCrypt.Prob.mass_one_implies_none_zero {α : Type u_1} (d : SDistr α) (h : d.mass = 1) : d none = 0

If mass = 1, then d(none) = 0 (no failure).

Bind support witness

theorem CatCrypt.Prob.SDistr.bind_support_witness {α : Type u_1} {β : Type u_2} {d : SDistr α} {f : α → SDistr β} {b : β} (h : (d.bind f) (some b) ≠ 0) : ∃ (a : α), d (some a) ≠ 0 ∧ (f a) (some b) ≠ 0

Key lemma: If (d.bind f)(some b) ≠ 0, then there exists an intermediate value a such that d(some a) ≠ 0 and (f a)(some b) ≠ 0.

This extracts a witness from the nonzero probability of a bind result. The proof uses the contrapositive of ENNReal.tsum_eq_zero: if the sum ∑ oa, d(oa) * (cont oa)(some b) is nonzero, at least one term must be nonzero.

Proof sketch:

1. SDistr.bind is PMF.bind with failure propagation
2. PMF.bind_apply gives (d.bind f)(some b) = ∑' oa, d(oa) * (cont oa)(some b)
3. If this sum ≠ 0, by contrapositive of tsum_eq_zero, ∃ oa with term ≠ 0
4. That term is d(oa) * (cont oa)(some b) ≠ 0, so both factors ≠ 0
5. oa cannot be none (since cont of none is fail, giving 0)
6. So oa = some a for some a, giving our witness

theorem CatCrypt.Prob.SDistr.bind_support_witness_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {d : SDistr (α × β)} {f : α × β → SDistr γ} {c : γ} (h : (d.bind f) (some c) ≠ 0) : ∃ (a : α) (b : β), d (some (a, b)) ≠ 0 ∧ (f (a, b)) (some c) ≠ 0

Variant: if the bind result with a continuation on pairs has nonzero probability, extract the intermediate pair.

Pointwise reasoning helpers

theorem CatCrypt.Prob.ENNReal_tsum_le_of_pointwise {α : Type u_1} {f g : α → ENNReal} (h : ∀ (a : α), f a ≤ g a) : ∑' (a : α), f a ≤ ∑' (a : α), g a

In ENNReal, if the sum of f is ≤ sum of g pointwise, then tsum f ≤ tsum g.

theorem CatCrypt.Prob.tsum_ite_le {α : Type u_1} (P : α → Prop) [DecidablePred P] (f : α → ENNReal) : (∑' (a : α), if P a then f a else 0) ≤ ∑' (a : α), f a

Conditional sum is bounded by unconditional sum.

theorem CatCrypt.Prob.tsum_ite_add_compl {α : Type u_1} (P : α → Prop) [DecidablePred P] (f : α → ENNReal) : ((∑' (a : α), if P a then f a else 0) + ∑' (a : α), if ¬P a then f a else 0) = ∑' (a : α), f a

Conditional sums partition the unconditional sum when terms are nonneg.

Product type tsum splitting

theorem CatCrypt.Prob.tsum_prod_eq {α : Type u_1} {β : Type u_2} {f : α × β → ENNReal} : ∑' (p : α × β), f p = ∑' (a : α) (b : β), f (a, b)

Split a tsum over α × β into nested tsums.

theorem CatCrypt.Prob.tsum_bool_prod_eq {β : Type u_2} {f : Bool × β → ENNReal} : ∑' (p : Bool × β), f p = ∑' (b : β), f (true, b) + ∑' (b : β), f (false, b)

Split a tsum over Bool × β into true and false parts.