``` ```

# 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)