Library probsa.probability.nrvar

Require Export prosa.behavior.time.

From probsa.probability Require Export brvar.
Local Open Scope nat_scope.

Natural Random Variable

For the sake of clarity, we define a random variable nrvar over a countable set Ω with measure μ, whose values are in the natural numbers nrvar. The random variable is defined using the general random variable notion rvar, which takes a set Ω, a measure μ, and a type eqType of nat as arguments.

Definition nrvar {Ω} (μ : measure Ω) :=
@rvar Ω μ [eqType of nat].

We define a mapping from rvar (option nat) to nrvar.

Definition odflt0 {Ω} {μ : measure Ω} (O : rvar μ [eqType of option instant]) : nrvar μ :=
mkRvar μ (fun ω ⇒ odflt 0%nat (O ω)).

Definition nrvar_addop_id {Ω} {μ : measure Ω} :=
mkRvar μ (fun _ ⇒ 0%nat).

Notation Instances

Next, we define notation-related typeclass instances for nrvar.

Instance nrvar_nrvar_pred_leqop {Ω} {μ : measure Ω} : LeqOp (nrvar μ) (nrvar μ) (pred Ω) :=
  { leq_op A B := fun ω ⇒ A ω ≤ B ω }.

Instance nrvar_nrvar_brvar_leqop {Ω} {μ : measure Ω} : LeqOp (nrvar μ) (nrvar μ) (brvar μ) :=
  { leq_op A B := mkRvar μ (fun ω ⇒ A ω ≤ B ω) }.

Instance rvar_nat_pred_leqop {Ω} {μ : measure Ω} : LeqOp (nrvar μ) nat (pred Ω) :=
  { leq_op A c := fun ω ⇒ A ω ≤ c }.

Instance nrvar_addop {Ω} {μ : measure Ω} : AddOp (nrvar μ) :=
  { add_op A B := mkRvar μ (fun ω ⇒ A ω + B ω) }.

Instance nrvar_subop {Ω} {μ : measure Ω} : SubOp (nrvar μ) :=
  { sub_op A B := mkRvar μ (fun ω ⇒ A ω - B ω) }.

Instance nrvar_nat_pred_eqop {Ω} {μ : measure Ω} : EqOp (nrvar μ) nat (pred Ω) :=
  { eq_op X x := mkRvar μ (fun ω ⇒ X ω == x) }.

Instance onrvar_onat_pred_eqop {Ω} {μ : measure Ω} :
  EqOp (rvar μ [eqType of option duration]) (option duration) (pred Ω) :=
  { eq_op X x := mkRvar μ (fun ω ⇒ X ω == x) }.

Instance onrvar_nrvar_brvar_leqop {Ω} {μ : measure Ω} :
  LeqOp (rvar μ [eqType of option instant]) (nrvar μ) (brvar μ) :=
  { leq_op := fun X Y ⇒ mkRvar μ (fun ω ⇒ X ω ⟨<=⟩ Y ω) }.

Instance onrvar_onat_pred_leqop {Ω} {μ : measure Ω} :
  LeqOp (rvar μ [eqType of option instant]) (option nat) (pred Ω) :=
  { leq_op rv ow := fun ω ⇒ rv ω ⟨<=⟩ ow }.

Notation "∑[rv]_{ x <- xs | P } F" :=
  (\big[nrvar_addop/nrvar_addop_id]_( x <- xs | P ) F)
    (at level 41, F at level 41, x, xs at level 50,
      format "'[' ∑[rv]_{ x <- xs | P } '/ ' F ']'") : probability_scope.

Notation "∑[rv]_{ x <- xs } F" :=
  (\big[nrvar_addop/nrvar_addop_id]_( x <- xs ) F)
    (at level 41, F at level 41, x, xs at level 50,
      format "'[' ∑[rv]_{ x <- xs } '/ ' F ']'") : probability_scope.

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

Lemma sum_nrvar_sum_nat :
  ∀ {T : eqType} {Ω} {μ : measure Ω} (X : T → nrvar μ) (xs : seq T) (ω : Ω),
    (∑[rv ]_{i <- xs } X i ) ω = \sum_(i <- xs) X i ω.
Proof.
  induction xs ⇒ ω; first by rewrite !big_nil.
  by rewrite !big_cons -IHxs.
Qed.