Library probsa.probability.pred

From probsa Require Export util.notation util.stdpp.

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.
Proof.
  unfold "∩", pred_intersection ⇒ ? ? ? ? ?.
  by rewrite -andb_assoc.
Qed.

Lemma pred_cap_and :
  ∀ (X : Type) (A B : pred X) (x : X), (A ∩ B ) x → A x ∧ B x.
Proof.
  by unfold "∩", pred_intersection ⇒ ? ? ? ? /andP [].
Qed.