Documentation

VCVio.EvalDist.Bool

Evaluation Distributions on Boolean-Valued Computations #

Specialization lemmas for HasEvalSPMF computations returning Bool.

source
@[simp]
theorem probOutput_true_add_false {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[= true | mx] + Pr[= false | mx] = 1 - Pr[⊥ | mx]
source
@[simp]
theorem probOutput_false_add_true {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[= false | mx] + Pr[= true | mx] = 1 - Pr[⊥ | mx]
source
theorem probOutput_true_eq_sub {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[= true | mx] = 1 - Pr[⊥ | mx] - Pr[= false | mx]
source
theorem probOutput_false_eq_sub {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
Pr[= false | mx] = 1 - Pr[⊥ | mx] - Pr[= true | mx]
source
@[simp]
theorem probOutput_not_map {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m Bool) :
Pr[= true | (fun (x : Bool) => !x) <$> mx] = Pr[= false | mx]
source
@[simp]
theorem probOutput_not_map' {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m Bool) :
Pr[= false | (fun (x : Bool) => !x) <$> mx] = Pr[= true | mx]
source
theorem probOutput_true_add_false_of_neverFail {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] {mx : m Bool} [NeverFail mx] :
Pr[= true | mx] + Pr[= false | mx] = 1
source
@[simp]
theorem probEvent_true_eq_probOutput {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
(probEvent mx fun (x : Bool) => x = true) = Pr[= true | mx]
source
@[simp]
theorem probEvent_not_eq_probOutput {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] (mx : m Bool) :
(probEvent mx fun (x : Bool) => x = false) = Pr[= false | mx]
source
theorem probOutput_true_bind_map_eq_probEvent {m : Type → Type u_1} [Monad m] [HasEvalSPMF m] {α β : Type} [LawfulMonad m] (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