Library ALEA.IterFlip
Definition of a random walk
We interpret the probabilistic programlet rec iter x = if flip() then iter (x+1) else x
Require Import ZArith.
Instance Fiter_mon :
monotonic (fun (f:Z -> distr Z) (x:Z) => Mif Flip (f (Zsucc x)) (Munit x)).
Save.
Definition Fiter : (Z -> distr Z) -m> (Z -> distr Z)
:= mon (fun f (x:Z) => Mif Flip (f (Zsucc x)) (Munit x)).
Lemma Fiter_simpl : forall f x, Fiter f x = Mif Flip (f (Zsucc x)) (Munit x).
Definition iterflip : Z -> distr Z := Mfix Fiter.
Instance Fiter_mon :
monotonic (fun (f:Z -> distr Z) (x:Z) => Mif Flip (f (Zsucc x)) (Munit x)).
Save.
Definition Fiter : (Z -> distr Z) -m> (Z -> distr Z)
:= mon (fun f (x:Z) => Mif Flip (f (Zsucc x)) (Munit x)).
Lemma Fiter_simpl : forall f x, Fiter f x = Mif Flip (f (Zsucc x)) (Munit x).
Definition iterflip : Z -> distr Z := Mfix Fiter.
Main result
Probability for iter to terminate is 1Auxiliary function p
Definition p_n = 1 - [1/2] ^ nFixpoint p_ (n : nat) : U := match n with O => 0 | (S n) => [1/2] * p_ n + [1/2] end.
Lemma p_incr : forall n, p_ n <= p_ (S n).
Hint Resolve p_incr.
Definition p : nat -m> U := fnatO_intro p_ p_incr.
Lemma pS_simpl : forall n, p (S n) = [1/2] * p n + [1/2].
Lemma p_eq : forall n:nat, p n == [1-]([1/2]^n).
Hint Resolve p_eq.
Lemma p_le : forall n:nat, [1-]([1/]1+n) <= p n.
Hint Resolve p_le.
Lemma lim_p_one : 1 <= lub p.
Hint Resolve lim_p_one.