probUntil Properties

This file proves evaluation and normalization results about probUntil.

Implementation Notes

Many lemmas in this file deal are stated for truncations of the probUntil program to a finite number of attempts. Because this term is not used outside this file, we will not factor out an explicit probUntilCut term.

@[simp]

theorem SLang.probUntilCut_zero {T : Type} (st : T) (body : SLang T) (cond : T → Bool) (x : T) : SLang.probWhileCut (fun (v : T) => decide (cond v = false)) (fun (x : T) => body) 0 st x = 0

Truncation of probUntil program to zero unrollings is identically zero.

@[simp]

theorem SLang.probUntilCut_apply_unsat {T : Type} (body : SLang T) (cond : T → Bool) (fuel : ℕ) (i : T) (x : T) (h : ¬cond x = true) : SLang.probWhileCut (fun (v : T) => decide (cond v = false)) (fun (x : T) => body) fuel i x = 0

Truncation of probUntil program to any number of unrollings will evaluate to zero, for values which do not satisfy cond.

@[simp]

theorem SLang.probUntil_apply_unsat {T : Type} (body : SLang T) (cond : T → Bool) (x : T) (h : ¬cond x = true) : body.probUntil cond x = 0

probUntil evaluates to zero at all values which do not satisfy cond.

theorem SLang.if_simpl {T : Type} (body : SLang T) (cond : T → Bool) (x_1 : T) (x : T) : (if x_1 = x then 0 else if cond x_1 = true then if x = x_1 then body x_1 else 0 else 0) = 0

theorem SLang.repeat_1 {T : Type} (body : SLang T) (cond : T → Bool) (x : T) (h : cond x = true) : ∑' (i : T), body i * SLang.probWhileCut (fun (v : T) => decide (cond v = false)) (fun (x : T) => body) 1 i x = body x

theorem SLang.tsum_split_ite_exp {T : Type} (cond : T → Bool) (f : T → ENNReal) (g : T → ENNReal) : (∑' (i : T), if cond i = false then f i else g i) = (∑' (i : T), if cond i = false then f i else 0) + ∑' (i : T), if cond i = true then g i else 0

theorem SLang.probUntilCut_closed_form {T : Type} (body : SLang T) (cond : T → Bool) (fuel : ℕ) (x : T) (h1 : cond x = true) : ∑' (i : T), body i * SLang.probWhileCut (fun (v : T) => decide (cond v = false)) (fun (x : T) => body) fuel i x = ∑ i ∈ Finset.range fuel, body x * (∑' (x : T), if cond x = true then 0 else body x) ^ i

theorem SLang.probUntilCut_convergence {T : Type} (body : SLang T) (cond : T → Bool) (x : T) : ⨆ (fuel : ℕ), ∑ i ∈ Finset.range fuel, body x * (∑' (x : T), if cond x = true then 0 else body x) ^ i = body x * (1 - ∑' (x : T), if cond x = true then 0 else body x)⁻¹

Expression for the limit of the closed form of truncated until

theorem SLang.probUntilCut_monotone {T : Type} (body : SLang T) (cond : T → Bool) (x : T) (a : T) : Monotone fun (i : ℕ) => body a * SLang.probWhileCut (fun (v : T) => decide (cond v = false)) (fun (x : T) => body) i a x

Truncated until term is monotone in the maximum number of steps.

@[simp]

theorem SLang.probUntil_apply_sat {T : Type} (body : SLang T) (cond : T → Bool) (x : T) (h : cond x = true) : body.probUntil cond x = body x * (1 - ∑' (x : T), if cond x = true then 0 else body x)⁻¹

until term evaluates to body, normalizing by the total mass of elements which satisfy cond.

@[simp]

theorem SLang.probUntil_apply {T : Type} (body : SLang T) (cond : T → Bool) (x : T) : body.probUntil cond x = (if cond x = true then body x else 0) * (1 - ∑' (x : T), if cond x = true then 0 else body x)⁻¹

Closed form for evaluation of until. until is:

• zero outside support of cond
• body inside the support of cond rescaled by the total mass outside the support of cond.

@[simp]

theorem SLang.probUntil_apply_norm {T : Type} (body : SLang T) (cond : T → Bool) (x : T) (norm : ∑' (x : T), body x = 1) : body.probUntil cond x = (if cond x = true then body x else 0) * (∑' (x : T), if cond x = true then body x else 0)⁻¹

When body is a proper PMF, until is

• zero outside the support of cond
• body inside the support of cond normalized into a PMF.