Library Ycart

Require Export Cover.
Set Implicit Arguments.
Require Arith.

Ycart.v: An exemple of partial termination

Section YcartExample.

Program giving an example of partiality

Given a function K : nat ->nat, N:nat
```let rec ycart p x = if random p < K x then x else ycart (x+1)
```
The probability of termination is
Variable K : nat -> nat.
Variable N : nat.

Instance FYcart_mon : monotonic
(fun (f:nat -> distr nat) n =>
Mlet (Random N) (fun x => if dec_lt (K n) x then Munit n else f (S n))).
Save.

Definition FYcart : (nat -> distr nat) -m> (nat -> distr nat)
:= mon (fun (f:nat -> distr nat) n =>
Mlet (Random N) (fun x => if dec_lt (K n) x then Munit n else f (S n))).

Lemma FYcart_simpl : forall f n,
FYcart f n = Mlet (Random N) (fun x => if dec_lt (K n) x then Munit n else f (S n)).

Definition Ycart : nat -> distr nat := Mfix FYcart.

Definition F x := (K x) */ [1/]1+N.

Properties of Ycart

Lemma FYcart_val : forall (q: MF nat) f x,
mu (FYcart f x) q == F x * q x + [1-](F x) * mu (f (S x)) q.

Definition P (x : nat) : nat -m-> U := Prod (fun i => [1-]F (x+i)).

Definition p (x:nat) : nat -m> U := sigma (fun k => F (x+k) * P x k).

Lemma P_prod : forall x k, F (x+k) * P x k == P x k - P x (S k).
Hint Resolve P_prod.

Lemma p_diff : forall x n, (p x n : U) == [1-] P x n.
Hint Resolve p_diff.

Lemma p_lub : forall x, lub (p x) == [1-] prod_inf (fun i => [1-]F (x+i)).
Hint Resolve p_lub.

Lemma p_equation : forall x n, p x (S n) == F x + [1-](F x) * p (S x) n.
Hint Resolve p_equation.

Lemma Ycart_term1 : forall x, mu (Ycart x) (fone nat) == [1-] prod_inf (fun i => [1-]F (x+i)).

A shorter proof using mu (Ycart x) (f_one nat) = mu h. muYcart h x

Instance Ycart_one_mon
: monotonic (fun (p:nat -> U) (y:nat) => F y + [1-](F y) * p (S y)).
Save.

Definition Ycart_one : (nat -> U) -m> (nat -> U) :=
mon (fun (p:nat->U) (y:nat) => F y + [1-](F y) * p (S y)).

Lemma Ycart_one_simpl : forall p y, Ycart_one p y = F y + [1-](F y) * p (S y).

Lemma Ycart_term2 : forall x, mu (Ycart x) (fone nat) == [1-] prod_inf (fun i => [1-]F (x+i)).

Instance FYcart_lt_mon : monotonic (fun (p: nat -> U) (y:nat) => [1-](F y) * p (S y)).
Save.

Definition FYcart_lt : (nat -> U) -m> (nat -> U) :=
mon (fun (p:nat->U) (y:nat) => [1-](F y) * p (S y)).

Lemma FYcart_lt_simpl : forall (p:nat -> U) (y:nat), FYcart_lt p y = [1-](F y) * p (S y).

Lemma Ycart_ltx : forall x, mu (Ycart x) (carac_lt x) <= 0.

Lemma Ycart_eqx : forall x, mu (Ycart x) (carac (eq_nat_dec x)) == F x.

End YcartExample.