Evaluation Distributions on Boolean-Valued Computations

Specialization lemmas for MonadLiftT m SPMF computations returning Bool.

@[simp]

theorem probOutput_true_add_false {m : Type → Type u_1} [MonadLiftT m SPMF] (mx : m Bool) : Pr[= true | mx] + Pr[= false | mx] = 1 - Pr[⊥ | mx]

@[simp]

theorem probOutput_false_add_true {m : Type → Type u_1} [MonadLiftT m SPMF] (mx : m Bool) : Pr[= false | mx] + Pr[= true | mx] = 1 - Pr[⊥ | mx]

theorem probOutput_true_eq_sub {m : Type → Type u_1} [MonadLiftT m SPMF] (mx : m Bool) : Pr[= true | mx] = 1 - Pr[⊥ | mx] - Pr[= false | mx]

theorem probOutput_false_eq_sub {m : Type → Type u_1} [MonadLiftT m SPMF] (mx : m Bool) : Pr[= false | mx] = 1 - Pr[⊥ | mx] - Pr[= true | mx]

@[simp]

theorem probOutput_not_map {m : Type → Type u_1} [Monad m] [MonadLiftT m SPMF] [LawfulMonad m] [LawfulMonadLiftT m SPMF] (mx : m Bool) : Pr[= true | (fun (x : Bool) => !x) <$> mx] = Pr[= false | mx]

@[simp]

theorem probOutput_not_map' {m : Type → Type u_1} [Monad m] [MonadLiftT m SPMF] [LawfulMonad m] [LawfulMonadLiftT m SPMF] (mx : m Bool) : Pr[= false | (fun (x : Bool) => !x) <$> mx] = Pr[= true | mx]

theorem probOutput_true_add_false_of_neverFail {m : Type → Type u_1} [Monad m] [MonadLiftT m SPMF] {mx : m Bool} [NeverFail mx] : Pr[= true | mx] + Pr[= false | mx] = 1

@[simp]

theorem probEvent_true_eq_probOutput {m : Type → Type u_1} [MonadLiftT m SPMF] (mx : m Bool) : (probEvent mx fun (x : Bool) => x = true) = Pr[= true | mx]

@[simp]

theorem probEvent_not_eq_probOutput {m : Type → Type u_1} [MonadLiftT m SPMF] (mx : m Bool) : (probEvent mx fun (x : Bool) => x = false) = Pr[= false | mx]

theorem probOutput_true_bind_map_eq_probEvent {m : Type → Type u_1} [Monad m] [MonadLiftT m SPMF] {α β : Type} [LawfulMonad m] [LawfulMonadLiftT m SPMF] (mx : m α) (my : α → m β) (p : α → β → Bool) : Pr[= true | do let x ← mx p x <$> my x] = probEvent (do let x ← mx let __do_lift ← my x pure (x, __do_lift)) fun (x : α × β) => match x with | (x, y) => p x y = true