# Cover.v: Characteristic functions

Require Export Prog.
Set Implicit Arguments.
Require Export Sets.
Require Export Arith.
Require Import Setoid.

Properties of zero_one functions

Definition zero_one (A:Type)(f:MF A) := forall x, orc (f x == 0) (f x == 1).
Hint Unfold zero_one.

Lemma zero_one_not_one :
forall (A:Type)(f:MF A) x, zero_one f -> ~ 1 <= f x -> f x == 0.

Lemma zero_one_not_zero :
forall (A:Type)(f:MF A) x, zero_one f -> ~ f x <= 0 -> f x == 1.

Hint Resolve zero_one_not_one zero_one_not_zero.

Lemma B2U_zero_one: zero_one B2U.

Lemma NB2U_zero_one: zero_one NB2U.

Lemma B2U_zero_one2: forall b:bool,
orc ((if b then 1 else 0) == 0) ((if b then 1 else 0) == 1).

Lemma NB2U_zero_one2: forall b:bool,
orc ((if b then 0 else 1) == 0) ((if b then 0 else 1) == 1).

Hint Immediate B2U_zero_one NB2U_zero_one B2U_zero_one2 NB2U_zero_one2.

Definition fesp_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> zero_one g -> zero_one (fesp f g).
Save.

Lemma fesp_conj_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> fesp f g == fconj f g.

Lemma fconj_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> zero_one g -> zero_one (fconj f g).

Lemma fplus_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> zero_one g -> zero_one (fplus f g).

Lemma finv_zero_one : forall (A:Type)(f :MF A),
zero_one f -> zero_one (finv f).

Lemma fesp_zero_one_mult_left : forall (A:Type)(f:MF A)(p:U),
zero_one f -> forall x, f x & p == f x * p.

Lemma fesp_zero_one_mult_right : forall (A:Type)(p:U)(f:MF A),
zero_one f -> forall x, p & f x == p * f x.
Hint Resolve fesp_zero_one_mult_left fesp_zero_one_mult_right.

## Covering functions

Definition cover (A:Type)(P:set A)(f:MF A) :=
forall x, (P x -> 1 <= f x) /\ (~ P x -> f x <= 0).

Lemma cover_eq_one : forall (A:Type)(P:set A)(f:MF A) (z:A),
cover P f -> P z -> f z == 1.

Lemma cover_eq_zero : forall (A:Type)(P:set A)(f:MF A) (z:A),
cover P f -> ~ P z -> f z == 0.

Lemma cover_orc_0_1 : forall (A:Type)(P:set A)(f:MF A),
cover P f -> forall x, orc (f x == 0) (f x == 1).

Lemma cover_zero_one : forall (A:Type)(P:set A)(f:MF A),
cover P f -> zero_one f.

Lemma zero_one_cover : forall (A:Type)(f:MF A),
zero_one f -> cover (fun x => 1 <= f x) f.

Lemma cover_esp_mult_left : forall (A:Type)(P:set A)(f:MF A)(p:U),
cover P f -> forall x, f x & p == f x * p.

Lemma cover_esp_mult_right : forall (A:Type)(P:set A)(p:U)(f:MF A),
cover P f -> forall x, p & f x == p * f x.
Hint Immediate cover_esp_mult_left cover_esp_mult_right.

Lemma cover_elim : forall (A:Type)(P:set A)(f:MF A),
cover P f -> forall x, orc (~P x /\ f x == 0) (P x /\ f x == 1).

Lemma cover_eq_one_elim_class : forall (A:Type)(P Q:set A)(f:MF A),
cover P f -> forall z, f z == 1 -> class (Q z) -> incl P Q -> Q z.

Lemma cover_eq_one_elim : forall (A:Type)(P:set A)(f:MF A),
cover P f -> forall z, f z == 1 -> ~ ~ P z.

Lemma cover_eq_zero_elim : forall (A:Type)(P:set A)(f:MF A) (z:A),
cover P f -> f z == 0 -> ~ P z.

Lemma cover_unit : forall (A:Type)(P:set A)(f:MF A)(a:A),
cover P f -> P a -> 1 <= mu (Munit a) f.

Lemma compose_let : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 (fun x => p * cP x)) <= mu (Mlet m1 m2) f.

Lemma compose_mu : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 (fun x => p * cP x)) <= mu m1 (fun x => mu (m2 x) f).

Lemma cover_let : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 cP) * p <= mu (Mlet m1 m2) f.

Lemma cover_mu : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 cP) * p <= mu m1 (fun x => mu (m2 x) f).

Lemma cover_let_one : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> 1 <= mu m1 cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> p <= mu (Mlet m1 m2) f.

Lemma cover_incl_fle : forall (A:Type)(P Q:set A)(f g:MF A),
cover P f -> cover Q g -> incl P Q -> f <= g.

Lemma cover_same_feq: forall (A:Type)(P:set A)(f g:MF A),
cover P f -> cover P g -> f == g.

Lemma cover_incl_le : forall (A:Type)(P Q:set A)(f g:MF A) x,
cover P f -> cover Q g -> incl P Q -> f x <= g x.

Lemma cover_same_eq : forall (A:Type)(P:set A)(f g:MF A) x,
cover P f -> cover P g -> f x == g x.

Lemma cover_eqset_stable : forall (A:Type)(P Q:set A)(EQ:eqset P Q)(f:MF A),
cover P f -> cover Q f.

Lemma cover_eq_stable : forall (A:Type)(P:set A)(f g:MF A),
cover P f -> f == g -> cover P g.

Lemma cover_eqset_eq_stable : forall (A:Type)(P Q:set A)(f g:MF A),
cover P f -> eqset P Q -> f == g -> cover Q g.

Add Parametric Morphism (A:Type) : (cover (A:=A))
with signature eqset (A:=A) ==> Oeq ==> iff as cover_eqset_compat.
Save.

Lemma cover_union : forall (A:Type)(P Q:set A)(f g : MF A),
cover P f -> cover Q g -> cover (union P Q) (fplus f g).

Lemma cover_inter_esp : forall (A:Type)(P Q:set A)(f g : MF A),
cover P f -> cover Q g -> cover (inter P Q) (fesp f g).

Lemma cover_inter_mult : forall (A:Type)(P Q:set A)(f g : MF A),
cover P f -> cover Q g -> cover (inter P Q) (fun x => f x * g x).

Lemma cover_compl : forall (A:Type)(P:set A)(f:MF A),
cover P f -> cover (compl P) (finv f).

Lemma cover_empty : forall (A:Type), cover (empty A) (fzero A).

Lemma cover_full : forall (A:Type), cover (full A) (fone A).

Lemma cover_comp : forall (A B:Type)(h:A -> B)(P:set B)(f:MF B),
cover P f -> cover (fun a => P (h a)) (fun a => f (h a)).

Covering and image This direction requires a covering function for the property
Lemma im_range_elim A B (f : A -> B) :
forall (d : distr A) (P : B -> Prop) (cP : B -> U),
cover P cP -> range P (im_distr f d) -> range (fun x => P (f x)) d.
Hint Resolve im_range.

## Caracteristic functions for decidable predicates

Definition carac (A:Type)(P:set A)(Pdec : dec P) : MF A
:= fun z => if Pdec z then 1 else 0.

Lemma carac_incl: forall (A:Type)(P Q:A -> Prop)(Pdec: dec P)(Qdec: dec Q),
incl P Q -> carac Pdec <= carac Qdec.

Lemma carac_monotonic : forall (A B:Type)(P:A -> Prop)(Q:B->Prop)(Pdec: dec P)(Qdec: dec Q) x y,
(P x -> Q y) -> carac Pdec x <= carac Qdec y.
Hint Resolve carac_monotonic.

Lemma carac_eq_compat : forall (A B:Type)(P:A -> Prop)(Q:B->Prop)(Pdec: dec P)(Qdec: dec Q) x y,
(P x <-> Q y) -> carac Pdec x == carac Qdec y.
Hint Resolve carac_eq_compat.

Lemma carac_one : forall (A:Type)(P:A -> Prop)(Pdec:dec P)(z:A),
P z -> carac Pdec z == 1.

Lemma carac_zero : forall (A:Type)(P:A -> Prop)(Pdec:dec P)(z:A),
~ P z -> carac Pdec z == 0.
Hint Resolve carac_zero carac_one.

Lemma carac_compl : forall (A:Type)(P:A -> Prop)(Pdec:dec P),
carac (compl_dec Pdec) == finv (carac Pdec).
Hint Resolve carac_compl.

Lemma cover_dec : forall (A:Type)(P:set A)(Pdec : dec P), cover P (carac Pdec).
Hint Resolve cover_dec.

Lemma carac_zero_one : forall (A:Type)(P:set A)(Pdec : dec P), zero_one (carac Pdec).
Hint Resolve carac_zero_one.

Lemma cover_mult_fun : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U),
(forall x, P x -> f x == g x) -> cover P cP -> forall x, cP x * f x == cP x * g x.

Lemma cover_esp_fun : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U),
(forall x, P x -> f x == g x) -> cover P cP -> forall x, cP x & f x == cP x & g x.

Lemma cover_esp_fun_le : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U),
(forall x, P x -> f x <= g x) -> cover P cP -> forall x, cP x & f x <= cP x & g x.
Hint Resolve cover_esp_fun_le.

Lemma cover_ok : forall (A:Type)(P Q:set A)(f g : MF A),
(forall x, P x -> ~ Q x) -> cover P f -> cover Q g -> fplusok f g.
Hint Resolve cover_ok.

## Boolean functions

Lemma cover_bool : forall (A:Type) (P: A -> bool), cover (fun x => P x = true) (fun x => B2U (P x)).
Hint Resolve cover_bool.

Like compose_mu but with boolean properties
Theorem compositional_reasoning :
forall A B (m1 : distr A) (m2 : A -> distr B)
(P : A -> bool) (f : B -> U) (p : U),
(forall x, P x = true -> p <= mu (m2 x) f) ->
mu m1 (fun x => p * B2U (P x)) <= mu m1 (fun x => mu (m2 x) f).

## Distribution by restriction

Assuming m is a distribution under assumption P and cP is 0 or 1, builds a distribution which is m if cP is 1 and 0 otherwise

Definition Mrestr A (cp:U) (m:M A) : M A := UMult cp @ m.

Lemma Mrestr_simpl : forall A cp (m:M A) f, Mrestr cp m f = cp * (m f).

Lemma Mrestr0 : forall A cP (m:M A), cP <= 0 -> forall f, Mrestr cP m f == 0.

Lemma Mrestr1 : forall A cP (m:M A), 1 <= cP -> forall f, Mrestr cP m f == m f.

Definition distr_restr : forall A (P:Prop) (cp:U) (m:M A),
((P -> 1 <= cp) /\ (~ P -> cp <= 0)) -> (P -> stable_inv m) ->
(P -> stable_plus m) -> (P -> stable_mult m) -> (P -> continuous m)
-> distr A.
Defined.

Lemma distr_restr_simpl : forall A (P:Prop) (cp:U) (m:M A)
(Hp: (P -> 1 <= cp) /\ (~ P -> cp <= 0)) (Hinv:P -> stable_inv m)
(Hplus:P -> stable_plus m)(Hmult:P -> stable_mult m)(Hcont:P -> continuous m) f,
mu (distr_restr cp Hp Hinv Hplus Hmult Hcont) f = cp * m f.

Modular reasoning on programs

Lemma range_cover : forall A (P:A -> Prop) d cP, range P d -> cover P cP ->
forall f, mu d f == mu d (fun x => cP x * f x).

Lemma mu_cut : forall (A:Type)(m:distr A)(P:set A)(cP f g:MF A),
cover P cP -> (forall x, P x -> f x == g x) -> 1 <= mu m cP
-> mu m f == mu m g.

## Uniform measure on finite sets

Section SigmaFinite.
Variable A:Type.
Variable decA : forall x y:A, { x=y }+{ ~ x=y }.

Section RandomFinite.

### Distribution for random_finP over {k:nat|k<=n}

The distribution associated to random_fin P is f --> sigma (a in P) [1/]1+n (f a) with [n+1] the size of [P] we cannot factorize [ [1/]1+n ] because of possible overflow

Fixpoint sigma_fin (f:A -> U )(P: A -> Prop)(FP:finite P){struct FP} : U :=
match FP with
| (fin_eq_empty eq) => 0
| (fin_eq_add x Q nQx FQ eq) => f x + sigma_fin f FQ
end.

Definition retract_fin (P:A -> Prop) (f:A -> U) :=
forall Q (FQ: finite Q), incl Q P -> forall x, ~ (Q x) -> P x
-> f x <= [1-](sigma_fin f FQ).

Lemma retract_fin_inv :
forall (P: A -> Prop) (f: A -> U),
retract_fin P f -> forall Q (FQ: finite Q), incl Q P ->
forall x, ~ (Q x) -> P x -> sigma_fin f FQ <= [1-]f x.

Hint Immediate retract_fin_inv.

Lemma retract_fin_incl : forall P Q f, retract_fin P f -> incl Q P -> retract_fin Q f.

Lemma sigma_fin_monotonic : forall (f g : A -> U)(P: A -> Prop)(FP: finite P),
(forall x, P x -> f x <= g x)-> sigma_fin f FP <= sigma_fin g FP.

Lemma sigma_fin_eq_compat :
forall (f g : A -> U)(P: A -> Prop)(FP:finite P),
(forall x, P x -> f x == g x)-> sigma_fin f FP == sigma_fin g FP.

Instance sigma_fin_mon : forall (P: A -> Prop)(FP:finite P),
monotonic (fun (f:MF A) => sigma_fin f FP).
Save.

Lemma retract_fin_le : forall (P: A -> Prop) (f g: A -> U),
(forall x, P x -> f x <= g x) -> retract_fin P g -> retract_fin P f.

Lemma sigma_fin_mult : forall (f: A -> U) c (P: A -> Prop)(FP: finite P),
retract_fin P f -> sigma_fin (fun k => c * f k) FP == c * sigma_fin f FP.

Lemma sigma_fin_plus : forall (f g: A -> U) (P:A -> Prop)(FP: finite P),
sigma_fin (fun k => f k + g k) FP == sigma_fin f FP + sigma_fin g FP.

Lemma sigma_fin_prod_maj :
forall (f g : A -> U)(P:A -> Prop)(FP: finite P),
sigma_fin (fun k => f k * g k) FP <= sigma_fin f FP.

Lemma sigma_fin_prod_le :
forall (f g : A -> U) (c:U) , (forall k, f k <= c) -> forall (P: A -> Prop)(FP:finite P),
retract_fin P g -> sigma_fin (fun k => f k * g k) FP <= c * sigma_fin g FP.

Lemma sigma_fin_prod_ge :
forall (f g : A -> U) (c:U) , (forall k, c <= f k) ->
forall (P: A -> Prop)(FP: finite P),
retract_fin P g -> c * sigma_fin g FP <= sigma_fin (fun k => f k * g k) FP.
Hint Resolve sigma_fin_prod_maj sigma_fin_prod_ge sigma_fin_prod_le.

Lemma sigma_fin_inv : forall (f g : A -> U)(P: A -> Prop)(FP:finite P),
retract_fin P f ->
[1-] sigma_fin (fun k => f k * g k) FP ==
sigma_fin (fun k => f k * [1-] g k) FP + [1-] sigma_fin f FP.

Lemma sigma_fin_eqset : forall f P Q (FP:finite P) (e:eqset P Q),
sigma_fin f (fin_eqset e FP) = sigma_fin f FP.

Lemma sigma_fin_rem : forall f P (FP:finite P) a,
P a -> sigma_fin f FP == f a + sigma_fin f (finite_rem decA a FP).

Lemma sigma_fin_incl : forall f P (FP: finite P) Q (FQ: finite Q),
incl P Q -> sigma_fin f FP <= sigma_fin f FQ.

Lemma sigma_fin_unique : forall f P Q (FP: finite P) (FQ: finite Q),
eqset P Q -> sigma_fin f FP == sigma_fin f FQ.

Lemma sigma_fin_cte : forall c P (FP:finite P),
sigma_fin (fun _ => c) FP == (size FP) */ c.

Definition Sigma_fin P (FP:finite P) := mon (fun (f:MF A) => sigma_fin f FP).

Lemma Sigma_fin_simpl : forall P (FP:finite P) f, Sigma_fin FP f = sigma_fin f FP.

Lemma sigma_fin_continuous : forall P (FP:finite P),
continuous (Sigma_fin FP).

### Definition and Properties of random_fin

Variable P : A -> Prop.
Variable FP : finite P.
Let s:= (size FP - 1)%nat.

Lemma pred_size_le : (size FP <=S s)%nat.
Hint Resolve pred_size_le.

Lemma pred_size_eq : notempty P -> size FP = S s.

Instance fmult_mon : forall A k, monotonic (fmult (A:=A) k).
Save.

Definition random_fin : M A := Sigma_fin FP @ (Fmult A ([1/]1+s)).

Lemma random_fin_simpl : forall (f:MF A),
random_fin f = sigma_fin (fun x => ([1/]1+s) * f x) FP.

Lemma fnth_retract_fin:
forall n, (size FP <= S n)%nat -> retract_fin P (fun _ => [1/]1+n).

Lemma random_fin_stable_inv : stable_inv random_fin.

Lemma random_fin_stable_plus : stable_plus random_fin.

Lemma random_fin_stable_mult : stable_mult random_fin.

Lemma random_fin_monotonic : monotonic random_fin.

Lemma random_fin_continuous : continuous random_fin.

Definition Random_fin : distr A.
Defined.

Lemma Random_fin_simpl : mu Random_fin = random_fin.

Lemma random_fin_total : notempty P -> mu Random_fin (fone A) == 1.
End RandomFinite.

Lemma random_fin_cover :
forall P Q (FP:finite P) (decQ:dec Q),
mu (Random_fin FP) (carac decQ) == size (finite_inter decQ FP) */ [1/]1+(size FP-1)%nat.

Lemma random_fin_P : forall P (FP:finite P) (decP:dec P),
notempty P -> mu (Random_fin FP) (carac decP) == 1.

End SigmaFinite.

## Properties of the Random distribution

Definition dec_le (n:nat) : dec (fun x => (x <= n)%nat).
Defined.

Definition dec_lt (n:nat) : dec (fun x => (x < n)%nat).
Defined.

Definition dec_gt : forall x, dec (lt x).
Defined.

Definition dec_ge : forall x, dec (le x).
Defined.

Definition carac_eq n := carac (eq_nat_dec n).
Definition carac_le n := carac (dec_le n).
Definition carac_lt n := carac (dec_lt n).
Definition carac_gt n := carac (dec_gt n).
Definition carac_ge n := carac (dec_ge n).

Definition is_eq (n:nat) : cover (fun x => n = x) (carac_eq n) := cover_dec (eq_nat_dec n).
Definition is_le (n:nat) : cover (fun x => (x <=n)%nat) (carac_le n) := cover_dec (dec_le n).
Definition is_lt (n:nat) : cover (fun x => (x < n)%nat) (carac_lt n) := cover_dec (dec_lt n).
Definition is_gt (n:nat) : cover (fun x => (n < x)%nat) (carac_gt n):= cover_dec (dec_gt n).
Definition is_ge (n:nat) : cover (fun x => (n <= x)%nat) (carac_ge n) := cover_dec (dec_ge n).

Lemma carac_gt_S :
forall x y, carac_gt (S y) (S x) == carac_gt y x.

Lemma carac_lt_S : forall x y, carac_lt (S x) (S y) == carac_lt x y.

Lemma carac_le_S : forall x y, carac_le (S x) (S y) == carac_le x y.

Lemma carac_ge_S : forall x y, carac_ge (S x) (S y) == carac_ge x y.

Lemma carac_eq_S : forall x y, carac_eq (S x) (S y) == carac_eq x y.

Lemma carac_lt_0 : forall y, carac_lt 0 y == 0.

Lemma carac_lt_zero : carac_lt 0 == fzero _.

lifting "if then else".
Lemma carac_if_compat : forall A (P:set A) (Pdec : dec P) (t:bool) u v,
(carac Pdec (if t then u else v))
==
(if t
then (carac Pdec u)
else (carac Pdec v)).

Lemma carac_lt_if_compat : forall x (t:bool) u v,
(carac_lt x (if t then u else v))
==
(if t
then (carac_lt x u)
else (carac_lt x v)).

Hint Resolve carac_le_S carac_eq_S carac_lt_S carac_ge_S carac_gt_S carac_lt_0 carac_lt_zero.

Instance carac_ge_mon (n:nat) : monotonic (carac_ge n).
Save.

Definition Carac_ge (n:nat) : nat -m> U := mon (carac_ge n).

Lemma dec_inter : forall A (P Q : set A), dec P -> dec Q -> dec (inter P Q).

Lemma dec_union : forall A (P Q : set A), dec P -> dec Q -> dec (union P Q).

Lemma carac_conj : forall A (P Q : set A) (dP:dec P) (dQ:dec Q),
carac (dec_inter dP dQ) == fconj (carac dP) (carac dQ).

Lemma carac_plus : forall A (P Q : set A) (dP:dec P) (dQ:dec Q),
carac (dec_union dP dQ) == fplus (carac dP) (carac dQ).

Count the number of elements between 0 and n-1 which satisfy P

Fixpoint nb_elts (P:nat -> Prop)(Pdec : dec P)(n:nat) {struct n} : nat :=
match n with
0 => 0%nat
| S n => if Pdec n then (S (nb_elts Pdec n)) else (nb_elts Pdec n)
end.

Lemma nb_elts_true : forall (P:nat -> Prop)(Pdec : dec P)(n:nat),
(forall k, (k < n)%nat -> P k) -> nb_elts Pdec n =n.
Hint Resolve nb_elts_true.

Lemma nb_elts_false : forall P,forall Pdec:dec P,forall n,
(forall x, (x<n)%nat -> ~ P x) -> nb_elts Pdec n = 0%nat.

• the probability for a random number between 0 and n to satisfy P is equal to the number of elements below n which satisfy P divided by n+1

Lemma Random_carac : forall (P:nat -> Prop)(Pdec : dec P)(n:nat),
mu (Random n) (carac Pdec) == (nb_elts Pdec (S n)) */ [1/]1+n.

Lemma nb_elts_lt_le : forall k n, (k <= n)%nat -> nb_elts (dec_lt k) n = k.

Lemma nb_elts_lt_ge : forall k n, (n <= k)%nat -> nb_elts (dec_lt k) n = n.

Lemma nb_elts_eq_nat_ge :forall n k,
(n <= k)%nat -> nb_elts (eq_nat_dec k) n = 0%nat.

Lemma beq_nat_neq: forall x y : nat, x <> y -> false = beq_nat x y.

Lemma nb_elt_eq :forall n k,
(k < n)%nat -> nb_elts (eq_nat_dec k) n = 1%nat.

Hint Resolve nb_elts_lt_ge nb_elts_lt_le nb_elts_eq_nat_ge nb_elt_eq.

Lemma Random_lt : forall n k, mu (Random n) (carac_lt k) == k */ [1/]1+n.

Hint Resolve Random_lt.

Lemma Random_le : forall n k, mu (Random n) (carac_le k) == (S k) */ [1/]1+n.

Hint Resolve Random_le.

Lemma Random_eq : forall n k, (k <= n)%nat -> mu (Random n) (carac_eq k) == 1 */ [1/]1+n.

Hint Resolve Random_eq.

## Properties of distributions and set

Section PickElemts.
Variable A : Type.
Variable P : A -> Prop.
Variable cP : A -> U.
Hypothesis coverP : cover P cP.
Variable ceq : A -> A -> U.
Hypothesis covereq : forall x, cover (eq x) (ceq x).

Variable d : distr A.

Variable k : U.

Hypothesis deqP : forall x, P x -> k <= mu d (ceq x).

Lemma d_coverP : forall x, P x -> k <= mu d cP.

Lemma d_coverP_exists : (exists x, P x) -> k <= mu d cP.

Lemma d_coverP_not_empty : ~ (forall x, ~ P x) -> k <= mu d cP.

End PickElemts.