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.
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.