Inverting a support membership

A proof about a probabilistic program often starts from a hypothesis h : x ∈ m.support and needs the intermediate results that produced x: for m = p >>= f, some a ∈ p.support with x ∈ (f a).support, and so on through every bind, map and pure of the program. Written by hand, each layer is one obtain ⟨a, ha, h⟩ := (PMF.mem_support_bind_iff _ _ _).mp h, or its OracleComp.supportWith counterpart, and each returned value one more cases on an equation.

The simp set supp_norm does the rewriting, and supp_cases h does it and destructures the result. The set covers PMF and the possible results OracleComp.supportWith of oracle programs, including OracleComp.support and ProbComp. Membership in the support of

• p >>= f, PMF.bind p f: ∃ a, a ∈ p.support ∧ x ∈ (f a).support;
• f <$> p, PMF.map f p: ∃ a, a ∈ p.support ∧ f a = x;
• pure a, PMF.pure a: x = a;
• if c then p else q: c ∧ x ∈ p.support ∨ ¬c ∧ x ∈ q.support;
• a uniform draw (ProbComp.unifFin, ProbComp.uniform, PMF.uniformOfFintype) or a query answered from Set.univ: True, so the drawn value has no membership hypothesis;
• the law ProbComp.eval m of a program: as for m, through PMF.bind, PMF.map and PMF.pure.

The set then substitutes a returned value into the rest of a sequence (exists_eq_left) and splits an equation of pairs into equations of their components (Prod.mk.injEq). The order of the existentials is the order of the program, so rcases patterns follow its binds.

Main definitions

• supp_cases h: rewrite h with supp_norm and destructure the result completely, substituting every equation one of whose sides is a local variable.
• supp_cases h with pat: rewrite h with supp_norm and destructure it with the rcases pattern pat.

Main results

• Cslib.Probability.PMF.mem_support_ite_iff, Cslib.OracleComp.mem_supportWith_ite_iff: membership in the support of a conditional, as a disjunction over the condition.

theorem Cslib.Probability.PMF.mem_support_ite_iff {α : Type u_1} (c : Prop) [Decidable c] (p q : PMF α) (x : α) : x ∈ (if c then p else q).support ↔ c ∧ x ∈ p.support ∨ ¬c ∧ x ∈ q.support

A value is in the support of a conditional distribution iff it is in the support of the branch the condition selects.

theorem Cslib.OracleComp.mem_supportWith_ite_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type u_2} {possible : (q : ι) → Set (spec q)} (c : Prop) [Decidable c] (p q : OracleComp spec α) (x : α) : x ∈ supportWith possible (if c then p else q) ↔ c ∧ x ∈ supportWith possible p ∨ ¬c ∧ x ∈ supportWith possible q

A possible result of a conditional program is a possible result of the branch the condition selects.

def Cslib.Tactic.SuppCases.suppCases : Lean.ParserDescr

supp_cases h inverts a hypothesis h : x ∈ m.support, where m is a PMF or an OracleComp program (OracleComp.supportWith, OracleComp.support, ProbComp) built from bind, map, pure, if and uniform draws. It rewrites h with the simp set supp_norm into existentials over the supports of the parts of m and equations for its returned values, in the order of the program, then destructures it:

• supp_cases h destructures completely: each intermediate result and each support hypothesis is introduced with an inaccessible name, conditionals split into one goal per branch, and every equation one of whose sides is a local variable is substituted. Use it when the rest of the proof needs no names, or refers to hypotheses by type (‹_›, assumption, omega).
• supp_cases h with ⟨a, ha, b, hb, rfl⟩ destructures with an rcases pattern instead.
• supp_cases h [foo_def, hc] first adds the given simp lemmas to the rewriting, to unfold a named program or decide a condition.

It fails when h does not state a membership in a support, and when the simp set does not apply to it, for instance because the program is a definition that must be unfolded first.