CoursePisa2014: distributions_clean.ec

File distributions_clean.ec, 1.6 KB (added by François Dupressoir, 5 years ago)

exercise sheet on distributions

Line
1(** Defining distributions *)
2require import Distr.
3require import Real.
4
5op dapply: ('a -> 'b) -> 'a distr -> 'b distr.
6(* Define dapply f d as the "application of f to d" *)
7axiom dapply_def (f:'a -> 'b) (d:'a distr) (p:'b -> bool):
8 mu (dapply f d) p = ...
9
10(* FILL ME *)
11
12(* Prove *)
13(* Recall that:
14     - "rewrite /op" expands the definition of operator op,
15     - "rewrite -/op" folds the operator's definition back up. *)
16lemma weight_dapply (f:'a -> 'b) (d:'a distr) (p:'b -> bool):
17  mu (dapply f d) True = mu d True.
18proof.
19(* FILL ME *)
20qed.
21
22(* The following result makes use of potentially infinite sets *)
23require import ISet.
24
25op preimage: ('a -> 'b) -> 'b -> 'a set.
26axiom preimage_def (a:'a) (f:'a -> 'b) (b:'b):
27  mem a (preimage f b) <=> f a = b.
28
29(* Prove that the probability of x in dapply f d is the probability
30   of being in x's preimage by f in d *)
31(* You may have to use extensional equality of operators *)
32print axiom fun_ext.
33print op ExtEq.(==).
34
35lemma dapply_x (f:'a -> 'b) (d:'a distr) (p:'b -> bool) (x:'b):
36  mu (dapply f d) ((=) x) = mu d (fun a, mem a (preimage f x)).
37proof.
38(* FILL ME *)
39qed.
40
41(* Prove (either directly, or by making use of the result above and
42   an intermediate lemma about bijections). *)
43(* You can always come back to this proof and try to re-do it with
44   the intermediate lemma when you're finished with the other exercises. *)
45lemma dapply_x_bij (f:'a -> 'b) (g:'b -> 'a) (d:'a distr) (x:'b):
46  (forall x, f (g x) = x) =>
47  (forall x, g (f x) = x) =>
48  mu (dapply f d) ((=) x) = mu d ((=) (g x)).
49proof.
50(* FILL ME *)
51qed.
52