# SProbas.v: Definition of the monad for sub-distributions

Require Export Probas.

## Definition of (sub)distribution

Subdistributions are measure functions such that
• mu (1-f) <= 1 - mu f
• f <= 1-g -> mu f + mu g <= mu (f+g)
• mu f & mu g <= mu (f & g) - [ mu (f+k) <= mu f + k ] - [ mu (k * f) = k * mu (f) ] - [ mu (lub f_n) <= lub mu (f_n) ]

## Properties of sub-measures

Lemma smu_monotonic : forall (A : Type)(m: sdistr A), monotonic (smu m).
Hint Resolve smu_monotonic.
Implicit Arguments smu_monotonic [A].

Lemma smu_stable : forall (A : Type)(m: sdistr A), stable (smu m).
Hint Resolve smu_stable.
Implicit Arguments smu_stable [A].

Lemma smu_zero : forall (A : Type)(m: sdistr A), smu m (fzero A) == 0.
Hint Resolve smu_zero.

Lemma smu_stable_mult_right : forall (A : Type)(m:(sdistr A)) (c:U) (f : A -> U),
smu m (fun x => (f x) * c) == (smu m f) * c.

Lemma smu_le_minus_left : forall (A : Type)(m:sdistr A) (f g:A -> U),
smu m (fminus f g) <= smu m f.
Hint Resolve smu_le_minus_left.

Lemma smu_le_minus : forall (A:Type) (m:sdistr A)(f g: A -> U),
g <= f -> smu m (fminus f g) <= smu m f - smu m g.
Hint Resolve smu_le_minus.

Lemma smu_cte : forall (A : Type)(m:(sdistr A)) (c:U),
smu m (fcte A c) == c * smu m (fone A).
Hint Resolve smu_cte.

Lemma smu_cte_le : forall (A : Type)(m:(sdistr A)) (c:U),
smu m (fcte A c) <= c.

Lemma smu_cte_eq : forall (A : Type)(m:(sdistr A)) (c:U),
smu m (fone A) == 1 -> smu m (fcte A c) == c.

Hint Resolve smu_cte_le smu_cte_eq.

Lemma smu_le_minus_cte : forall (A:Type) (m:sdistr A)(f: A -> U) (k:U),
smu m f - k <= smu m (fminus f (fcte A k)).

Lemma smu_inv_le_minus :
forall (A:Type) (m:sdistr A)(f: A -> U), smu m (finv f) <= smu m (fone A) - smu m f.

Lemma smu_inv_minus_inv : forall (A:Type) (m:sdistr A)(f: A -> U),
smu m (finv f) + [1-](smu m (fone A)) <= [1-](smu m f).

Definition stable_plus_sdistr : forall A (m:M A),
stable_plus m -> stable_inv m -> stable_mult m -> continuous m -> sdistr A.
Defined.

Definition distr_sdistr : forall A, distr A -> sdistr A.
Defined.

Definition Sunit A (x:A) : sdistr A := distr_sdistr (Munit x).

Lemma Sunit_unit : forall A (x:A), smu (Sunit x) = unit x.

Lemma Sunit_simpl : forall A (x:A) (f : MF A), smu (Sunit x) f = f x.

Definition Slet : forall A B:Type, (sdistr A) -> (A -> sdistr B) -> sdistr B.
Defined.

Lemma Slet_star : forall (A B:Type) (m:sdistr A) (M : A -> sdistr B),
smu (Slet m M) = star (smu m) (fun x => smu (M x)).

Lemma Slet_simpl : forall A B (m:sdistr A) (M : A -> sdistr B) (f:MF B),
smu (Slet m M) f = smu m (fun x => smu (M x) f).

Non deterministic choice

Definition Smin (A:Type)(m1 m2 : sdistr A) : sdistr A.
Save.

## Operations on sub-distributions

Instance Osdistr (A : Type) : ord (sdistr A) :=
{ Ole := fun f g => smu f <= smu g;
Oeq := fun f g => smu f == smu g}.
Defined.

Lemma Sunit_compat : forall A (x y : A), x = y -> Sunit x == Sunit y.

Lemma Slet_compat : forall (A B : Type) (m1 m2:sdistr A) (M1 M2 : A-> sdistr B),
m1 == m2 -> M1 == M2 -> Slet m1 M1 == Slet m2 M2.

Lemma le_sdistr_gen : forall (A:Type) (m1 m2:sdistr A),
m1 <= m2 -> forall f g, f <= g -> smu m1 f <= smu m2 g.

Lemma Slet_unit : forall (A B:Type) (x:A) (m:A -> sdistr B), Slet (Sunit x) m == m x.

Lemma M_ext : forall (A:Type) (m:sdistr A), Slet m (fun x => Sunit x) == m.

Lemma Mcomp : forall (A B C:Type) (m1:(sdistr A)) (m2:A -> sdistr B) (m3:B -> sdistr C),
Slet (Slet m1 m2) m3 == Slet m1 (fun x:A => (Slet (m2 x) m3)).

Lemma Slet_le_compat : forall (A B:Type) (m1 m2: sdistr A) (f1 f2 : A -> sdistr B),
m1 <= m2 -> f1 <= f2 -> Slet m1 f1 <= Slet m2 f2.

## A specific subdistribution

Definition sdistr_null : forall A : Type, sdistr A.
Defined.

Lemma le_sdistr_null : forall (A:Type) (m : sdistr A), sdistr_null A <= m.
Hint Resolve le_sdistr_null.

## Least upper bound of increasing sequences of sdistributions

Section Lubs.
Variable A : Type.

Definition Smu : sdistr A -m> M A.
Defined.

Lemma Smu_simpl : forall d f, Smu d f = smu d f.

Variable smuf : nat -m> sdistr A.

Definition smu_lub: sdistr A.

Defined.

Lemma smu_lub_simpl : smu smu_lub = lub (Smu @ smuf).

Lemma smu_lub_le : forall n:nat, smuf n <= smu_lub.

Lemma smu_lub_sup : forall m:sdistr A, (forall n:nat, smuf n <= m) -> smu_lub <= m.

End Lubs.

## Sub-distribution for flip

The distribution associated to flip () is
Definition Sflip : sdistr bool := distr_sdistr Flip.

Lemma Sflip_simpl : smu Sflip = flip.

## Uniform sub-distribution beween 0 and n

Require Arith.

### Distribution for Srandomn

The sdistribution associated to Srandom n is we cannot factorize because of possible overflow

Definition Srandom (n:nat): sdistr nat:= distr_sdistr (Random n).

Lemma Srandom_simpl : forall n, smu (Srandom n) = random n.