Library probsa.probability.pred
(* --------------------------------- ProBsa --------------------------------- *)
From probsa Require Export util.notation util.stdpp.
(* --------------------------------- Main ----------------------------------- *)
From probsa Require Export util.notation util.stdpp.
(* --------------------------------- Main ----------------------------------- *)
To enable the set-theoretic notation (such as ∩ and ∪) over
predicates, we introduce type-class instances for NegOp,
Union, Intersection.
Instance neg_pred {Ω} : NegOp (pred Ω) :=
{ neg_op A := fun ω ⇒ ~~ A ω }.
Instance pred_union {Ω} : Union (pred Ω) :=
{ union A B := fun ω ⇒ A ω || B ω }.
Instance pred_intersection {Ω} : Intersection (pred Ω) :=
{ intersection A B := fun ω ⇒ A ω && B ω }.
Lemma pred_cap_assoc :
∀ (X : Type) (A B C : pred X) (x : X), ((A ∩ B) ∩ C) x = (A ∩ (B ∩ C)) x.
Lemma pred_cap_and :
∀ (X : Type) (A B : pred X) (x : X), (A ∩ B) x → A x ∧ B x.
{ neg_op A := fun ω ⇒ ~~ A ω }.
Instance pred_union {Ω} : Union (pred Ω) :=
{ union A B := fun ω ⇒ A ω || B ω }.
Instance pred_intersection {Ω} : Intersection (pred Ω) :=
{ intersection A B := fun ω ⇒ A ω && B ω }.
Lemma pred_cap_assoc :
∀ (X : Type) (A B C : pred X) (x : X), ((A ∩ B) ∩ C) x = (A ∩ (B ∩ C)) x.
Lemma pred_cap_and :
∀ (X : Type) (A B : pred X) (x : X), (A ∩ B) x → A x ∧ B x.