``` ```

# Probas.v: The monad for distributions

``` Require Export Monads. Set Implicit Arguments. Module Proba (Univ:Universe). Module MP := (Monad Univ). ```

## Definition of distribution

Distributions are monotonic measure functions such that
``` Record distr (A:Type) : Type :=   {mu : M A;    mu_stable_inv : stable_inv mu;    mu_stable_plus : stable_plus mu;    mu_stable_mult : stable_mult mu;    mu_continuous : continuous mu}. Hint Resolve mu_stable_plus mu_stable_inv mu_stable_mult mu_continuous. ```

## Properties of measures

``` Lemma mu_monotonic : forall (A : Type)(m: distr A), monotonic (mu m). intros; apply fmonotonic; auto. Save. Hint Resolve mu_monotonic. Implicit Arguments mu_monotonic [A]. Lemma mu_stable_eq : forall (A : Type)(m: distr A), stable (mu m). intros; apply fmon_stable; auto. Save. Hint Resolve mu_stable_eq. Implicit Arguments mu_stable_eq [A]. Lemma mu_zero : forall (A : Type)(m: distr A), mu m (fzero A) == 0. intros. apply Oeq_trans with (mu m (fmult 0 (fzero A))); auto. apply mu_stable_eq; unfold fmult; simpl; auto. apply Oeq_trans with (0 * (mu m (fzero A))); auto. apply mu_stable_mult; auto. Save. Hint Resolve mu_zero. Lemma mu_one_inv : forall (A : Type)(m:distr A),    mu m (fone A) == 1 -> forall f, mu m (finv f) == [1-] (mu m f). intros; apply Ole_antisym. apply (mu_stable_inv m f). apply Uplus_le_simpl_left with (mu m f); auto. setoid_rewrite (Uinv_opp_right (mu m f)). apply Ole_trans with (mu m (fun x => (f x) + [1-] (f x))). setoid_rewrite <- H; apply (mu_monotonic m); auto. assert (H1 : fplusok f (finv f)). red; unfold finv; intro x; auto. setoid_rewrite <- (mu_stable_plus m H1); auto. Save. Hint Resolve mu_one_inv. Lemma mu_fplusok : forall (A : Type)(m:distr A) f g, fplusok f g ->             mu m f <= [1-] mu m g. intros; apply Ole_trans with (mu m (finv g)); auto. apply (mu_stable_inv m g). Save. Hint Resolve mu_fplusok. Lemma mu_le_minus : forall (A : Type)(m:distr A) (f g:MF A),      mu m (fminus f g) <= mu m f. intros; apply mu_monotonic; unfold fminus; auto. Save. Hint Resolve mu_le_minus. Lemma mu_le_plus : forall (A : Type)(m:distr A) (f g:MF A),      mu m (fplus f g) <= mu m f + mu m g. intros; apply Ole_trans with (mu m (fplus (fminus f (fesp f g)) g)). apply mu_monotonic. unfold fle,fplus,fminus,fesp; intros; auto. rewrite (mu_stable_plus m (f:=fminus f (fesp f g)) (g:=g)). red; unfold fminus,fesp,finv; intro x; auto. Usimpl; auto. Save. Hint Resolve mu_le_plus. Lemma mu_cte : forall (A : Type)(m:(distr A)) (c:U),    mu m (fcte A c) == c * mu m (fone A). intros. apply Oeq_trans with (mu m (fun x => c * 1)). apply (mu_stable_eq m); simpl; auto. unfold fone; rewrite <- (mu_stable_mult m c (fun x => 1)); auto. Save. Hint Resolve mu_cte. Lemma mu_cte_le : forall (A : Type)(m:distr A) (c:U), mu m (fcte A c) <= c. intros; apply Ole_trans with (c * mu m (fone A)); auto. Save. Lemma mu_cte_eq : forall (A : Type)(m:distr A) (c:U),    mu m (fone A) == 1 -> mu m (fcte A c) == c. intros; apply Oeq_trans with (c * mu m (fone A)); auto. setoid_rewrite H; auto. Save. Hint Resolve mu_cte_le mu_cte_eq. Lemma mu_stable_mult_right : forall (A : Type)(m:distr A) (c:U) (f : MF A),    mu m (fun x => (f x) * c) == (mu m f) * c. intros; apply Oeq_trans with    (mu m (fun x => c * (f x))). apply mu_stable_eq; simpl; auto. apply Oeq_trans with (c * mu m f); auto. exact (mu_stable_mult m c f). Save. Lemma mu_stable_minus : forall (A:Type) (m:distr A)(f g : MF A),  fle g f -> mu m (fun x => f x - g x) == mu m f - mu m g. intros; change (mu m (fminus f g) == mu m f - mu m g). apply (stable_minus_distr (m:=mu m)); auto. Save. Lemma mu_inv_minus : forall (A:Type) (m:distr A)(f: MF A), mu m (finv f) == mu m (fone A) - mu m f. intros; apply Oeq_trans with (mu m (fun x => fone A x - f x)). apply (mu_stable_eq m); repeat red; unfold finv,fone; intros; auto. apply mu_stable_minus; auto. Save. Lemma mu_inv_minus_inv : forall (A:Type) (m:distr A)(f: MF A),      mu m (finv f) + [1-](mu m (fone A)) == [1-](mu m f). intros; apply Uminus_eq_perm_right. apply Uinv_le_compat. apply (mu_monotonic m); unfold fone; auto. unfold Uminus. rewrite mu_inv_minus; repeat Usimpl. unfold Uminus. apply Uinv_eq_compat; auto. Save. Lemma mu_le_esp_inv : forall (A:Type) (m:distr A)(f g : MF A),  ([1-]mu m (finv f)) & mu m g <= mu m (fesp f g). intros; rewrite Uesp_sym. apply Uplus_inv_le_esp; Usimpl. apply Ole_trans with (mu m (fplus (fesp f g) (finv f))); auto. apply (mu_monotonic m); unfold fplus, fesp,finv; simpl; intros. rewrite Uesp_sym; auto. Save. Hint Resolve mu_le_esp_inv. Lemma mu_stable_inv_inv : forall (A:Type) (m:distr A)(f : MF A),              mu m f <= [1-] mu m (finv f). intros; apply Ole_trans with (mu m (finv (finv f))). apply (mu_monotonic m); auto. intro x; unfold finv; auto. apply (mu_stable_inv m); auto. Save. Hint Resolve mu_stable_inv_inv. Lemma mu_le_esp : forall (A:Type) (m:distr A)(f g : MF A),  mu m f & mu m g <= mu m (fesp f g). intros; apply Ole_trans with (([1-]mu m (finv f)) & mu m g); auto. Save. Hint Resolve mu_le_esp. Definition Distr (A:Type) : ord. intro A; exists (distr A) (fun (f g : distr A) => mu f <= mu g); auto. intros; apply Ole_trans with (mu y); auto. Defined. Lemma eq_distr_intro :         forall A (m1 m2:Distr A), (forall f, mu m1 f == mu m2 f) -> m1==m2. intros; split; auto. Save. Lemma eq_distr_elim : forall A (m1 m2:Distr A), m1==m2 -> forall f, mu m1 f == mu m2 f. auto. Save. Hint Resolve eq_distr_intro eq_distr_elim. ```

## Monadic operators for distributions

``` Definition Munit : forall A:Type, A -> Distr A. intros A x. exists (unit x). apply unit_stable_inv. apply unit_stable_plus. apply unit_stable_mult. apply unit_continuous. Defined. Definition Mlet : forall A B:Type, Distr A -> (A -> Distr B) -> Distr B. intros A B mA mB. exists (star (mu mA) (fun x => (mu (mB x)))). apply star_stable_inv; auto. apply star_stable_plus; auto. apply star_stable_mult; auto. apply star_continuous; auto. Defined. Lemma Mlet_simpl : forall (A B:Type) (m:Distr A) (M:A -> Distr B) (f:B->U),      mu (Mlet m M) f = mu m (fun x => (mu (M x) f)). trivial. Save. ```

## Operations on distributions

``` Lemma Munit_compat : forall A (x y : A), x=y -> Munit x == Munit y. intros; subst; auto. Save. Lemma Mlet_le_compat : forall (A B : Type) (m1 m2:Distr A) (M1 M2 : A-o> Distr B),   m1 <= m2 -> M1<=M2 -> Mlet m1 M1 <= Mlet m2 M2. unfold Mlet,star; simpl; intros A B m1 m2 M1 M2 Hm HM f. apply Ole_trans with (mu m2 (fun x : A => mu (M1 x) f)); auto. Save. Hint Resolve Mlet_le_compat. Definition MLet (A B : Type) : Distr A -m> (A-o>Distr B) -m> Distr B                := le_stable2_mon (Mlet_le_compat (A:=A) (B:=B)). Lemma MLet_simpl : forall (A B:Type) (m:Distr A) (M:A -> Distr B)(f:B->U),      mu (MLet A B m M) f =mu m (fun x => mu (M x) f). trivial. Save. Lemma Mlet_eq_compat : forall (A B : Type) (m1 m2:Distr A) (M1 M2 : A-o> Distr B),   m1 == m2 -> M1==M2 -> Mlet m1 M1 == Mlet m2 M2. intros; apply Ole_antisym; auto. Save. Lemma Munit_eq : forall (A:Type) (q:A->U) x, mu (Munit x) q == q x. trivial. Save. Lemma mu_le_compat : forall (A:Type) (m1 m2:Distr A),   m1 <= m2 -> forall f g : A -o>U, f <= g -> mu m1 f <= mu m2 g. intros; apply Ole_trans with (mu m2 f); auto. Save. ```

## Properties of monadic operators

``` Lemma Mlet_unit : forall (A B:Type) (x:A) (m:A -> Distr B), Mlet (Munit x) m == m x. auto. Save. Lemma Mext : forall (A:Type) (m:Distr A), Mlet m (fun x => Munit x) == m. intros; apply eq_distr_intro; simpl; intros. apply (mu_stable_eq m); simpl; apply ford_eq_intro; auto. Save. Lemma Mcomp : forall (A B C:Type) (m1: Distr A) (m2:A -> Distr B) (m3:B -> Distr C),      Mlet (Mlet m1 m2) m3 == Mlet m1 (fun x:A => Mlet (m2 x) m3). intros; apply eq_distr_intro; intros; simpl; trivial. Save. ```

## A specific distribution

``` Definition distr_null : forall A : Type, Distr A. intro A; exists (fmon_cte (A -o> U) (0:U)); try red; auto. Defined. Lemma le_distr_null : forall (A:Type) (m : Distr A), distr_null A <= m. red; intros. unfold distr_null; simpl; auto. Save. Hint Resolve le_distr_null. ```

## Least upper bound of increasing sequences of distributions

``` Section Lubs. Variable A : Type. Definition Mu : Distr A -m> M A. exists (mu (A:=A)); auto. Defined. Variable muf : natO -m> Distr A. Definition mu_lub: Distr A. exists (lub (Mu @ muf)). red; intros; simpl; apply lub_inv; intros; simpl. apply (mu_stable_inv (muf n)). red; intros; simpl. apply Oeq_trans with (lub ((UPlus @2 ((Mu @ muf) <_> f)) ((Mu @ muf) <_> g))); auto. apply lub_eq_stable; auto. simpl; apply fmon_eq_intro; intro; exact (mu_stable_plus (muf n) H); auto. red; intros; simpl. apply Oeq_trans with (lub (UMult k @ ((Mu @ muf) <_> f))); auto. apply lub_eq_stable; auto. simpl; apply fmon_eq_intro; intro; exact (mu_stable_mult (muf n) k f); auto. unfold M; apply cont_lub; intros. apply (mu_continuous (muf n)). Defined. Lemma mu_lub_le : forall n:nat, muf n <= mu_lub. simpl; intros. apply le_lub with (f:=(Mu @ muf) <_> x) (n:=n). Save. Lemma mu_lub_sup : forall m: distr A, (forall n:nat, muf n <= m) -> mu_lub <= m. simpl; intros. apply lub_le; simpl; intros; auto. Save. End Lubs. Hint Resolve mu_lub_le mu_lub_sup. ```

### Distributions seen as a Cpo

``` Definition cDistr : forall (A:Type), cpo. intros; exists (Distr A) (distr_null A) (mu_lub (A:=A)); auto. Defined. ```

## Distribution for `flip`

The distribution associated to `flip ()` is
``` Definition flip : M bool. exists (fun (f : bool -> U) => [1/2] * (f true) + [1/2] * (f false)). red; intros; simpl. apply Ole_trans with ([1/2]* y true +[1/2]* x false ); auto. Defined. Lemma flip_stable_inv : stable_inv flip. unfold flip, stable_inv, finv; auto. Save. Lemma flip_stable_plus : stable_plus flip. unfold flip, stable_plus, fplus; intros; simpl. rewrite (Udistr_plus_left [1/2] _ _ (H true)). rewrite (Udistr_plus_left [1/2] _ _ (H false)). repeat norm_assoc_right. apply Uplus_eq_compat_right. repeat norm_assoc_left; apply Uplus_eq_compat_left; auto. Save. Lemma flip_stable_mult : stable_mult flip. unfold flip, stable_mult, fmult; intros; simpl. assert (H:([1/2]* f true) <= ([1-] ([1/2]* f false))); auto. rewrite (Udistr_plus_left k _ _ H); auto. Save. Lemma flip_continuous : continuous flip. unfold continuous; intros; simpl. do 2 rewrite <- lub_eq_mult. rewrite <- lub_eq_plus; auto. Save. Definition ctrue : MF bool := fun (b:bool) => if b then 1 else 0. Definition cfalse : MF bool := fun (b:bool) => if b then 0 else 1. Lemma flip_ctrue : flip ctrue == [1/2]. unfold flip, ctrue; simpl; auto. setoid_rewrite (Umult_one_right [1/2]). setoid_rewrite (Umult_zero_right [1/2]); auto. Save. Lemma flip_cfalse : flip cfalse == [1/2]. unfold flip, cfalse; simpl; auto. setoid_rewrite (Umult_one_right [1/2]). setoid_rewrite (Umult_zero_right [1/2]); auto. Save. Hint Resolve flip_ctrue flip_cfalse. Definition Flip : Distr bool. exists flip. apply flip_stable_inv. apply flip_stable_plus. apply flip_stable_mult. apply flip_continuous. Defined. ```

## Uniform distribution beween 0 and n

``` Require Arith. ```

### Definition of `fnth`

`fnth n k` is defined as
``` Definition fnth (n:nat) : nat -> U := fun k => [1/]1+n. ```

### Basic properties of `fnth`

``` Lemma Unth_eq : forall n, Unth n == [1-] (sigma (fnth n) n). intro; exact (Unth_prop n). Save. Hint Resolve Unth_eq. Lemma sigma_fnth_one : forall n, sigma (fnth n) (S n) == 1. intros; rewrite sigma_S. unfold fnth at 1. rewrite (Unth_eq n); auto. Save. Hint Resolve sigma_fnth_one. Lemma Unth_inv_eq : forall n, [1-] ([1/]1+n) == sigma (fnth n) n. intro; setoid_rewrite (Unth_eq n); auto. Save. Lemma sigma_fnth_sup : forall n m, (m > n) -> sigma (fnth n) m == sigma (fnth n) (S n). intros. assert ((S n) <= m)%nat; auto with arith. elim H0; intros; auto. rewrite sigma_S; auto. setoid_rewrite H2. assert (m0 > n); auto with arith. setoid_rewrite (sigma_fnth_one n); auto. Save. Lemma sigma_fnth_le : forall n m, (sigma (fnth n) m) <= (sigma (fnth n) (S n)). intros; setoid_rewrite (sigma_fnth_one n); auto. Save. Hint Resolve sigma_fnth_le. ```
`fnth` is a retract
``` Lemma fnth_retract : forall n:nat,(retract (fnth n) (S n)). red; intros. unfold fnth at 1. apply Ole_trans with ([1-] (sigma (fnth n) n)); auto with arith. Save. Implicit Arguments fnth_retract []. ```

### Distribution for `random n`

The distribution associated to `random n` is we cannot factorize because of possible overflow
``` Definition random (n:nat):M nat. intro n; exists (fun (f:nat->U) => sigma (fun k => Unth n * f k) (S n)). red; intros; auto. Defined. Lemma random_simpl : forall n (f : nat->U),            random n f = sigma (fun k => Unth n * f k) (S n). trivial. Save. ```

### Properties of `random`

``` Lemma random_stable_inv : forall n, stable_inv (random n). unfold random, stable_inv, finv; intros; simpl. rewrite (sigma_inv f (fnth_retract n)); auto. Save. Lemma random_stable_plus : forall n, stable_plus (random n). unfold stable_plus, fplus; intros. repeat (rewrite random_simpl). unfold fplusok, fle, finv in H. apply Oeq_trans with  (sigma (fun k : nat => ([1/]1+n * f k) + ([1/]1+n * g k)) (S n)). apply sigma_eq_compat; intros. assert (f k <= [1-] (g k)); auto. apply sigma_plus with (f:=fun k : nat => Unth n * f k)                       (g:=fun k : nat => Unth n * g k); auto. Save. Lemma random_stable_mult : forall n, stable_mult (random n). unfold stable_mult, fmult; intros; repeat (rewrite random_simpl). apply Oeq_trans with  (sigma (fun l : nat => k * ([1/]1+n * f l)) (S n)). apply sigma_eq_compat; intros; auto. apply sigma_mult with (f:=fun k : nat => Unth n * f k). red; intros. apply Ole_trans with ([1/]1+n); auto. apply Ole_trans with ([1-] (sigma (fun k1 => Unth n) k0)); auto. apply (fnth_retract n k0); auto. Save. Lemma random_continuous : forall n, continuous (random n). unfold continuous; intros; rewrite random_simpl. apply Ole_trans with     (sigma (fun k : nat => lub (c:=U) (UMult ([1/]1+n) @ (h <o> k))) (S n)). apply sigma_le_compat; intros; simpl. rewrite (lub_eq_mult ([1/]1+n) (h <o> k)); auto. apply Ole_trans with (sigma (lub (c:=nat-d>U) (ford_shift (fun k : nat => (UMult ([1/]1+n) @ (h <o> k))))) (S n)); auto. rewrite sigma_lub1; auto. Save. Definition Random (n:nat) : Distr nat. intro n; exists (random n). apply random_stable_inv. apply random_stable_plus. apply random_stable_mult. apply random_continuous. Defined. Lemma Random_simpl : forall (n:nat), mu (Random n) = random n. trivial. Save. Lemma Random_total : forall n : nat, mu (Random n) (fone nat) == 1. intros; simpl mu;unfold fone; rewrite random_simpl. apply Oeq_trans with (sigma (fnth n) (S n)). apply sigma_eq_compat. intros; repeat Usimpl; auto. auto. Save. Hint Resolve Random_total. Lemma Random_inv : forall f n, mu (Random n) (finv f) == [1-] (mu (Random n) f). intros; apply mu_one_inv; auto. Save. Hint Resolve Random_inv. End Proba. ```
 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (70 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (52 entries) Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (15 entries) Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

This page has been generated by coqdoc