Library Choice
Require Export Prog.
Set Implicit Arguments.
Module Choice (Univ:Universe).
Module RP := (Rules Univ).
Definition of a probabilistic choice
We interpret the probabilistic program which executes two probabilistic programs and and then make a choice between the two computed results.let rec p () = let x = p1 () in let y = p2 () in choice x y
Section CHOICE.
Variable A : Type.
Variables p1 p2 : distr A.
Variable choice : A -> A -> A.
Definition p : Distr A := Mlet p1 (fun x => Mlet p2 (fun y => Munit (choice x y))).
Assumptions
We need extra properties on , and .- and terminate with probability
- value on is not less than the sum of values of on separate elements. If is a boolean function it means than if one of or satisfies then will also satisfy
Hypothesis p1_terminates : (mu p1 (fone A))==1.
Hypothesis p2_terminates : (mu p2 (fone A))==1.
Variable Q : MF A.
Hypothesis choiceok : forall x y, Q x + Q y <= Q (choice x y).
Lemma choicerule : forall k1 k2,
k1 <= mu p1 Q -> k2 <= mu p2 Q -> (k1 * ([1-] k2) + k2) <= mu p Q.
unfold p,Mlet,star; simpl; unfold unit; intros.
apply Ole_trans with
(mu p1 (fun x : A => mu p2 (fun y : A => Q x * ([1-] (Q y)) + Q y))).
apply Ole_trans with
(mu p1 (fun x : A =>
((mu p2 (fun y : A => Q x * ([1-] (Q y))))
+(mu p2 Q)))).
change
(k1 * [1-] k2 + k2 <=
mu p1 (fplus (fun x : A => mu p2 (fun y : A => Q x * [1-] (Q y)))
(fun x => mu p2 Q))).
assert (H1 : fplusok (fun x : A => mu p2 (fun y : A => Q x * [1-] (Q y)))
(fun x => mu p2 Q)).
repeat red; unfold finv; intros.
apply Ole_trans with (mu p2 (fun y : A => [1-] (Q y))).
apply (mu_monotonic p2); auto.
apply (mu_stable_inv p2 Q).
setoid_rewrite (mu_stable_plus p1 H1).
assert (Heq1:mu p1 (fun _ : A => mu p2 Q) == mu p2 Q).
exact (mu_cte_eq p1 (mu p2 Q) p1_terminates).
rewrite Heq1.
apply Ole_trans with (k1 * [1-] (mu p2 Q) + (mu p2 Q)); auto.
Usimpl.
apply Ole_trans with (mu p1 (fun x : A => (Q x) * mu p2 (finv Q))).
apply Ole_trans with ((mu p1 Q) * (mu p2 (finv Q))).
rewrite (mu_one_inv p2 p2_terminates Q); auto.
rewrite (mu_stable_mult_right p1 (mu p2 (finv Q)) Q); auto.
apply (mu_monotonic p1); intro x.
rewrite <- (mu_stable_mult p2 (Q x) (finv Q)); auto.
apply (mu_monotonic p1); intro x.
assert (fplusok (fun y : A => Q x * [1-] (Q y)) Q).
intro y; unfold finv; auto.
rewrite <- (mu_stable_plus p2 H1); auto.
apply (mu_monotonic p1); intro x.
apply (mu_monotonic p2); intro y.
apply Ole_trans with ((Q x) + (Q y)); auto.
Save.
End CHOICE.
End Choice.
| 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 | _ | (4 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 | _ | (1 entry) |
| 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 | _ | (1 entry) |
| 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