Library Bernouilli

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.

This page has been generated by coqdoc