Library Ycart
Program giving an example of partiality
Given a function K : nat ->nat, N:natlet 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.
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.
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.