# Library ALEA.Choice

## Definition of a probabilistic choice

We interpret the probabilistic program p which executes two probabilistic programs p1 and p2 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))).

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

## Main result

We estimate the probability for p to satisfy Q given estimations for both p1 and p2.### Assumptions

We need extra properties on p1, p2 and choice.- p1 and p2 terminate with probability 1
- Q value on choice is not less than the sum of values of Q on separate elements.