Library IterFlip

IterFlip.v: An example of probabilistic termination


Require Export Prog.
Set Implicit Arguments.

Module IterFlip (Univ:Universe).
Module RP := (Rules Univ).

Definition of a random walk

We interpret the probabilistic program 
let rec iter x = if flip() then iter (x+1) else x
Require Import ZArith.

Definition Fiter : (Z -o> Distr Z) -m> Z-o> Distr Z.
exists (fun f (x:Z) => Mif Flip (f (Zsucc x)) (Munit x)); red; intros.
intro p; apply Mif_mon; auto.
Defined.

Lemma Fiter_simpl : forall f x, Fiter f x = Mif Flip (f (Zsucc x)) (Munit x).
trivial.
Save.

Definition iterflip : Z -o> (Distr Z) := Mfix Fiter.

Main result

Probability for iter to terminate is

Auxiliary function

Definition

Fixpoint 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).
simpl; intros.
apply Ole_trans with ([1/2]*p_ n + [1/2]*p_ n); auto.
rewrite <- Udistr_plus_right; auto.
apply Ole_trans with (1 * p_ n); auto.
Save.

Hint Resolve p_incr.

Definition p : natO -m> U := fnatO_intro p_incr.

Lemma pS_simpl : forall n, p (S n) = [1/2] * p n + [1/2].
trivial.
Save.

Lemma p_eq : forall n:nat, p n == [1-]([1/2]^n).
induction n; auto; rewrite pS_simpl.
rewrite IHn.
apply Oeq_trans with ([1/2] * [1-]([1/2]^n) + [1-][1/2]);simpl; auto.
Save.
Hint Resolve p_eq.

Lemma p_le : forall n:nat, [1-]([1/]1+n) <= p n.
intro; rewrite (p_eq n).
apply Uinv_le_compat.
induction n; simpl; intros; auto.
apply Ole_trans with ([1/2] * ([1/]1+n)); auto.
Save.

Hint Resolve p_le.

Lemma lim_p_one : 1 <= lub p.
apply Ule_lt_lim; intros.
assert (exc (fun n : nat => t <= [1-] ([1/]1+n))).
assert (~0==[1-] t).
red; intro; apply H; auto.
apply Ole_trans with ([1-] 0); auto.
apply (archimedian H0); auto; intros m H1.
apply exc_intro with m; auto.
apply H0; auto; intros.
apply Ole_trans with (p x); auto.
apply Ole_trans with ([1-] ([1/]1+x)); auto.
Save.

Hint Resolve lim_p_one.

Proof of probabilistic termination

Definition q1 (z1 z2:Z) := 1.

Lemma iterflip_term : okfun (fun k => 1) iterflip q1.
unfold iterflip; intros.
apply okfun_le_compat with (fun (k:Z) => lub p) q1; auto.
intro x; auto.
apply fixrule with (p:= fun (x:Z) => p); auto; intros.
red; simpl; intros.
unfold Fiter.
red.
rewrite (Mif_eq Flip (f (Zsucc x0)) (Munit x0) (q1 x0)); simpl.
repeat Usimpl.
unfold q1 at 2; repeat Usimpl.
apply Ole_trans with (mu (f (Zsucc x0)) (q1 (Zsucc x0))); auto.
exact (H (Zsucc x0)).
Save.

End IterFlip.
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 _ (15 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 _ (7 entries)
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 _ (6 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