Distribution Semantics for Computations with Lists and Vectors

This file contains lemmas for probEvent and probOutput of computations involving List. We also include Vector as a related case.

theorem OracleComp.probFailure_list_mapM_loop {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] (xs : List α) (f : α → m β) (ys : List β) : Pr[⊥ | List.mapM.loop f xs ys] = 1 - (List.map (fun (x : α) => 1 - Pr[⊥ | f x]) xs).prod

@[simp]

theorem OracleComp.probFailure_list_mapM {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] (xs : List α) (f : α → m β) : Pr[⊥ | List.mapM f xs] = 1 - (List.map (fun (x : α) => 1 - Pr[⊥ | f x]) xs).prod

@[simp]

theorem OracleComp.probOutput_list_mapM_loop {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [DecidableEq β] (xs : List α) (f : α → m β) (ys zs : List β) : Pr[=zs | List.mapM.loop f xs ys] = if zs.length = xs.length + ys.length ∧ List.take ys.length zs = ys.reverse then (List.zipWith (fun (x : α) (z : β) => Pr[=z | f x]) xs (List.drop ys.length zs)).prod else 0

theorem OracleComp.probOutput_bind_eq_mul {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] {mx : m α} {my : α → m β} {y : β} (x : α) (h : ∀ x' ∈ support mx, y ∈ support (my x') → x' = x) : Pr[=y | mx >>= my] = Pr[=x | mx] * Pr[=y | my x]

@[simp]

theorem OracleComp.probOutput_cons_map {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [DecidableEq α] (mx : m (List α)) (x : α) (xs : List α) : Pr[=xs | List.cons x <$> mx] = if hxs : xs = [] then 0 else Pr[=xs.head hxs | pure x] * Pr[=xs.tail | mx]

@[simp]

theorem OracleComp.probOutput_list_mapM {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (xs : List α) (f : α → m β) (ys : List β) : Pr[=ys | List.mapM f xs] = if ys.length = xs.length then (List.zipWith (fun (x1 : β) (x2 : α) => Pr[=x1 | f x2]) ys xs).prod else 0

@[simp]

theorem OracleComp.probOutput_list_mapM' {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (xs : List α) (f : α → m β) (ys : List β) : Pr[=ys | List.mapM' f xs] = if ys.length = xs.length then (List.zipWith (fun (x1 : β) (x2 : α) => Pr[=x1 | f x2]) ys xs).prod else 0