# IterFlip.v: An example of probabilistic termination

Require Export Prog.
Set Implicit Arguments.

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

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 1

### Auxiliary function p

Definition p_n = 1 - [1/2] ^ n

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

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.

### Proof of probabilistic termination

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

Lemma iterflip_term : okfun (fun k => 1) iterflip q1.