``` ```

# Simulating Bernouilli distribution

``` Require Export Prog. Set Implicit Arguments. Set Strict Implicit. Module Bernouilli (Univ:Universe). Import Univ. Module RP := (Rules Univ). Import RP. Import RP.PP. Import RP.PP.MP. Import RP.PP.MP.UP. ```

## Program for computing a Bernouilli distribution

bernouilli p gives true with probability p and false with probability (1-p)
```let rec bernouilli x = if flip then
if x < 1/2 then false else bernouilli (2 p - 1)
else if x < 1/2 then bernouilli (2 p) else true
```

``` Hypothesis dec_demi : forall x : U, {x < Unth 1}+{Unth 1 <= x}. Definition Fbern (f: U -> (distr bool)) (p:U) :=     Mif Flip        (if dec_demi p then (Munit false) else (f (p & p)))        (if dec_demi p then (f (p + p)) else (Munit true)). Lemma Fbern_mon :    forall f g : U -> distr bool, (forall n, le_distr (f n) (g n))    -> forall n, le_distr (Fbern f n) (Fbern g n). Definition bernouilli : U -> (distr bool) :=    Mfix Fbern Fbern_mon. ```

### Definition of the invariant

``` Definition q (p:U) (n:nat) :=     p - (Uexp (Unth 1) n). Add Morphism q : q_eq_compat. ```

### Properties of the invariant

``` Lemma q_esp_S : forall p n, q (p & p) n == q p (S n) & q p (S n). Lemma q_esp_le : forall p n,     (q p (S n)) <= (Unth 1) * (q (p & p) n) + (Unth 1). Lemma q_plus_eq :   forall p n, (p <= Unth 1) -> (q p (S n)) == (Unth 1) * (q (p + p) n). Lemma q_0 : forall p:U, q p 0 == U0. Lemma p_le : forall (p:U) (n:nat), p - (Unth n) <= q p n. Hint Resolve p_le. Lemma lim_q_p : forall p, p <= lub (q p). Hint Resolve lim_q_p.      ```

### Properties of the bernouilli program

``` Definition q1 (b:bool) := if b then U1 else U0. Lemma bernouilli_true :    okfun (fun p => p) bernouilli q1. Definition q2 (b:bool) := if b then U0 else U1. Lemma bernouilli_false :    okfun (fun p => Uinv p) bernouilli q2. Lemma q1_q2_inv : forall b:bool, q1 b == Uinv (q2 b). Lemma bernouilli_eq :       forall p, mu (bernouilli p) q1 == p. End Bernouilli. ```