Library probsa.util.notation

(* -------------------------------- Coq-Proba ------------------------------- *)
From discprob.prob Require Export prob countable.

(* --------------------------- Reals and SSReflect -------------------------- *)
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool ssrfun seq eqtype fintype bigop choice.

(* ---------------------------------- Main ---------------------------------- *)
Global Open Scope probability_scope.

(* --------------------------- Coq-Proba notation --------------------------- *)
Definition measure := distrib.
Notation "'ℙ<' μ '>{[' E ']}'" := (pr μ E)
  (at level 10, format "ℙ< μ >{[ E ]}") : probability_scope.

(* --------------- stdpp-like notation for random variables --------------- *)
Class EqOp A B C := eq_op: A → B → C.
Global Instance: Params (@eq_op) 2 := {}.
Infix "⟨=⟩" := eq_op (at level 90, left associativity) : stdpp_scope.

Instance nat_nat_bool_eqop : EqOp nat_countType [countType of nat] bool :=
  { eq_op a b := a == b }.

Class LeqOp A B C := leq_op: A → B → C.
Global Instance: Params (@leq_op) 2 := {}.
Infix "⟨<=⟩" := leq_op (at level 50, left associativity) : stdpp_scope.

Instance onat_onat_bool_leqop : LeqOp (option nat) (option nat) bool :=
  { leq_op a b := (odflt 0 a ≤ odflt 0 b)%nat }.

Instance onat_nat_bool_leqop : LeqOp (option nat) nat bool :=
  { leq_op := fun a b ⇒ (odflt 0 a ≤ b)%nat }.

Class LtOp A B C := lt_op: A → B → C.
Global Instance: Params (@lt_op) 2 := {}.
Infix "⟨<⟩" := lt_op (at level 50, left associativity) : stdpp_scope.

Instance onat_onat_bool_ltop : LtOp (option nat) (option nat) bool :=
  { lt_op a b := (odflt 0 a < odflt 0 b)%nat }.

Class NegOp A := neg_op: A → A.
Global Instance: Params (@neg_op) 1 := {}.
Notation "! x" := (neg_op x) (at level 100) : stdpp_scope.

Class AddOp A := add_op: A → A → A.
Global Instance: Params (@add_op) 2 := {}.
Infix "⟨+⟩" := add_op (at level 50, left associativity) : stdpp_scope.

Class SubOp A := sub_op: A → A → A.
Global Instance: Params (@sub_op) 2 := {}.
Infix "⟨-⟩" := sub_op (at level 50, left associativity) : stdpp_scope.

(* ---------------------------- BigOp notation ---------------------------- *)
Notation "∑_{ m <= i < n } F" :=
  (\big[Rplus/0%R]_(i <- index_iota m n ) F%R)
    (at level 41, F at level 41, i, m, n at level 50,
      format "'[' ∑_{ m <= i < n } '/ ' F ']'") : probability_scope.

Notation "∑_{ m <= i <= n } F" :=
  (\big[Rplus/0%R]_(i <- index_iota m n.+1 ) F%R)
    (at level 41, F at level 41, i, m, n at level 50,
      format "'[' ∑_{ m <= i <= n } '/ ' F ']'") : probability_scope.

Notation "∑[∞]_{ i <- I } F" :=
  (Series (countable_sum (λ ( i : I ), F)))
    (at level 41, F at level 41, i, I at level 50,
      format "'[' ∑[∞]_{ i <- I } '/ ' F ']'") : probability_scope.