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.

All lemmas are generic over any monad m with [HasEvalSPMF m].

theorem cons_mem_support_seq_map_cons_iff {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m (List α)) (x : α) (xs : List α) : x :: xs ∈ support (List.cons <$> mx <*> my) ↔ x ∈ support mx ∧ xs ∈ support my

theorem cons_mem_finSupport_seq_map_cons_iff {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (my : m (List α)) (x : α) (xs : List α) : x :: xs ∈ finSupport (List.cons <$> mx <*> my) ↔ x ∈ finSupport mx ∧ xs ∈ finSupport my

theorem probOutput_cons_seq_map_cons_eq_mul {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m (List α)) (x : α) (xs : List α) : Pr[= x :: xs | List.cons <$> mx <*> my] = Pr[= x | mx] * Pr[= xs | my]

theorem probOutput_cons_seq_map_cons_eq_mul' {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m (List α)) (x : α) (xs : List α) : Pr[= x :: xs | (fun (xs : List α) (x : α) => x :: xs) <$> my <*> mx] = Pr[= x | mx] * Pr[= xs | my]

@[simp]

theorem probOutput_map_append_left {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] [DecidableEq α] (xs : List α) (mx : m (List α)) (ys : List α) : Pr[= ys | (fun (x : List α) => xs ++ x) <$> mx] = if List.take xs.length ys = xs then Pr[= List.drop xs.length ys | mx] else 0

theorem 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 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 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 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 probOutput_cons_map {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (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 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 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 support_seq_map_vector_cons {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] {n : ℕ} (mx : m α) (my : m (List.Vector α n)) [LawfulMonad m] : support ((fun (x1 : α) (x2 : List.Vector α n) => x1 ::ᵥ x2) <$> mx <*> my) = {xs : List.Vector α n.succ | xs.head ∈ support mx ∧ xs.tail ∈ support my}

@[simp]

theorem probOutput_seq_map_vector_cons_eq_mul {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] {n : ℕ} (mx : m α) (my : m (List.Vector α n)) [LawfulMonad m] (xs : List.Vector α (n + 1)) : Pr[= xs | (fun (x1 : α) (x2 : List.Vector α n) => x1 ::ᵥ x2) <$> mx <*> my] = Pr[= xs.head | mx] * Pr[= xs.tail | my]

@[simp]

theorem probOutput_seq_map_vector_cons_eq_mul' {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] {n : ℕ} (mx : m α) (my : m (List.Vector α n)) [LawfulMonad m] (xs : List.Vector α (n + 1)) : Pr[= xs | (fun (xs : List.Vector α n) (x : α) => x ::ᵥ xs) <$> my <*> mx] = Pr[= xs.head | mx] * Pr[= xs.tail | my]

@[simp]

theorem probOutput_vector_toList {α : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] {n : ℕ} [LawfulMonad m] (mx' : m (List.Vector α n)) (xs : List α) : Pr[= xs | List.Vector.toList <$> mx'] = if h : xs.length = n then Pr[= ⟨xs, h⟩ | mx'] else 0

@[simp]

theorem neverFail_list_vector_mmap {α β : Type v} {m : Type v → Type u_1} [Monad m] [HasEvalSPMF m] {n : ℕ} {f : α → m β} {as : List.Vector α n} (h : ∀ x ∈ as.toList, NeverFail (f x)) : NeverFail (List.Vector.mmap f as)

NeverFail lemmas for list monadic operations

@[simp]

theorem neverFail_list_mapM {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {f : α → m β} {as : List α} (h : ∀ x ∈ as, NeverFail (f x)) : NeverFail (List.mapM f as)

@[simp]

theorem neverFail_list_mapM' {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] [HasEvalSPMF m] {f : α → m β} {as : List α} (h : ∀ x ∈ as, NeverFail (f x)) : NeverFail (List.mapM' f as)

@[simp]

theorem neverFail_list_flatMapM {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {f : α → m (List β)} {as : List α} (h : ∀ x ∈ as, NeverFail (f x)) : NeverFail (List.flatMapM f as)

@[simp]

theorem neverFail_list_filterMapM {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {f : α → m (Option β)} {as : List α} (h : ∀ x ∈ as, NeverFail (f x)) : NeverFail (List.filterMapM f as)

@[simp]

theorem neverFail_list_foldlM {α : Type u_1} {m : Type u_3 → Type u_4} [Monad m] [HasEvalSPMF m] {s : Type u_3} {f : s → α → m s} {init : s} {as : List α} (h : ∀ (i : s), ∀ x ∈ as, NeverFail (f i x)) : NeverFail (List.foldlM f init as)

@[simp]

theorem neverFail_list_foldrM {α : Type u_1} {m : Type u_3 → Type u_4} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {s : Type u_3} {f : α → s → m s} {init : s} {as : List α} (h : ∀ (i : s), ∀ x ∈ as, NeverFail (f x i)) : NeverFail (List.foldrM f init as)