Library Cover

Cover.v: Characteristic functions

Require Export Prog.
Require Export Sets.
Require Export Arith.

Properties of zero_one functions

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

Lemma zero_one_not_one :
∀ (A:Type)(f:MF A) x, zero_one f → ¬ 1 ≤ f x → f x ≈ 0.

Lemma zero_one_not_zero :
∀ (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 ctrue_zero_one: zero_one ctrue.

Lemma cfalse_zero_one: zero_one cfalse.

Lemma ctrue_zero_one2: ∀ b:bool,
  orc ((if b then 1 else 0) ≈ 0) ((if b then 1 else 0) ≈ 1).

Lemma cfalse_zero_one2: ∀ b:bool,
  orc ((if b then 0 else 1) ≈ 0) ((if b then 0 else 1) ≈ 1).

Hint Immediate ctrue_zero_one cfalse_zero_one ctrue_zero_one2 cfalse_zero_one2.

Definition fesp_zero_one : ∀ (A:Type)(f g:MF A),
      zero_one f → zero_one g → zero_one (fesp f g).
Save.

Lemma fesp_conj_zero_one : ∀ (A:Type)(f g:MF A),
      zero_one f → fesp f g ≈ fconj f g.

Lemma fconj_zero_one : ∀ (A:Type)(f g:MF A),
      zero_one f → zero_one g → zero_one (fconj f g).

Lemma fplus_zero_one : ∀ (A:Type)(f g:MF A),
      zero_one f → zero_one g → zero_one (fplus f g).

Lemma finv_zero_one : ∀ (A:Type)(f :MF A),
      zero_one f → zero_one (finv f).

Lemma fesp_zero_one_mult_left : ∀ (A:Type)(f:MF A)(p:U),
      zero_one f → ∀ x, f x & p ≈ f x * p.

Lemma fesp_zero_one_mult_right : ∀ (A:Type)(p:U)(f:MF A),
     zero_one f → ∀ 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) :=
      ∀ x, (P x → 1 ≤ f x) ∧ (¬ P x → f x ≤ 0).

Lemma cover_eq_one : ∀ (A:Type)(P:set A)(f:MF A) (z:A),
       cover P f → P z → f z ≈ 1.

Lemma cover_eq_zero : ∀ (A:Type)(P:set A)(f:MF A) (z:A),
       cover P f → ¬ P z → f z ≈ 0.

Lemma cover_orc_0_1 : ∀ (A:Type)(P:set A)(f:MF A),
   cover P f → ∀ x, orc (f x ≈ 0) (f x ≈ 1).

Lemma cover_zero_one : ∀ (A:Type)(P:set A)(f:MF A),
   cover P f → zero_one f.

Lemma zero_one_cover : ∀ (A:Type)(f:MF A),
   zero_one f → cover (fun x ⇒ 1 ≤ f x) f.

Lemma cover_esp_mult_left : ∀ (A:Type)(P:set A)(f:MF A)(p:U),
      cover P f → ∀ x, f x & p ≈ f x * p.

Lemma cover_esp_mult_right : ∀ (A:Type)(P:set A)(p:U)(f:MF A),
     cover P f → ∀ x, p & f x ≈ p * f x.
Hint Immediate cover_esp_mult_left cover_esp_mult_right.

Lemma cover_elim : ∀ (A:Type)(P:set A)(f:MF A),
cover P f → ∀ x, orc (¬P x ∧ f x ≈ 0) (P x ∧ f x ≈ 1).

Lemma cover_eq_one_elim_class : ∀ (A:Type)(P Q:set A)(f:MF A),
       cover P f → ∀ z, f z ≈ 1 → class (Q z) → incl P Q → Q z.

Lemma cover_eq_one_elim : ∀ (A:Type)(P:set A)(f:MF A),
       cover P f → ∀ z, f z ≈ 1 → ¬ ¬ P z.

Lemma cover_eq_zero_elim : ∀ (A:Type)(P:set A)(f:MF A) (z:A),
       cover P f → f z ≈ 0 → ¬ P z.

Lemma cover_unit : ∀ (A:Type)(P:set A)(f:MF A)(a:A),
             cover P f → P a → 1 ≤ μ (Munit a) f.

Lemma cover_let : ∀ (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 ≤ μ m1 cP → (∀ x:A, P x → p ≤ μ (m2 x) f) → p ≤ μ (Mlet m1 m2) f.

Lemma cover_incl_fle : ∀ (A:Type)(P Q:set A)(f g:MF A),
      cover P f → cover Q g → incl P Q → f ≤ g.

Lemma cover_incl_eq: ∀ (A:Type)(P:set A)(f g:MF A),
      cover P f → cover P g → f ≈ g.

Lemma cover_eqset_stable : ∀ (A:Type)(P Q:set A)(EQ:eqset P Q)(f:MF A),
      cover P f → cover Q f.

Lemma cover_eq_stable : ∀ (A:Type)(P:set A)(f g:MF A),
      cover P f → f ≈ g → cover P g.

Lemma cover_eqset_eq_stable : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (A:Type)(P:set A)(f:MF A),
      cover P f → cover (compl P) (finv f).

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

Lemma cover_comp : ∀ (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)).

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: ∀ (A:Type)(P Q:A → Prop)(Pdec: dec P)(Qdec: dec Q),
                                incl P Q → carac Pdec ≤ carac Qdec.

Lemma carac_monotonic : ∀ (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 : ∀ (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 : ∀ (A:Type)(P:A → Prop)(Pdec:dec P)(z:A),
       P z → carac Pdec z ≈ 1.

Lemma carac_zero : ∀ (A:Type)(P:A → Prop)(Pdec:dec P)(z:A),
       ¬ P z → carac Pdec z ≈ 0.

Lemma cover_dec : ∀ (A:Type)(P:set A)(Pdec : dec P), cover P (carac Pdec).

Lemma cover_mult_fun : ∀ (A:Type)(P:set A)(cP : MF A)(f g:A→U),
  (∀ x, P x → f x ≈ g x) → cover P cP → ∀ x, cP x * f x ≈ cP x * g x.

Lemma cover_esp_fun : ∀ (A:Type)(P:set A)(cP : MF A)(f g:A→U),
  (∀ x, P x → f x ≈ g x) → cover P cP → ∀ x, cP x & f x ≈ cP x & g x.

Lemma cover_esp_fun_le : ∀ (A:Type)(P:set A)(cP : MF A)(f g:A→U),
  (∀ x, P x → f x ≤ g x) → cover P cP → ∀ x, cP x & f x ≤ cP x & g x.
Hint Resolve cover_esp_fun_le.

Lemma cover_ok : ∀ (A:Type)(P Q:set A)(f g : MF A),
        (∀ x, P x → ¬ Q x) → cover P f → cover Q g → fplusok f g.
Hint Resolve cover_ok.

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 : ∀ A cp (m:M A) f, Mrestr cp m f = cp * (m f).

Lemma Mrestr0 : ∀ A cP (m:M A), cP ≤ 0 → ∀ f, Mrestr cP m f ≈ 0.

Lemma Mrestr1 : ∀ A cP (m:M A), 1 ≤ cP → ∀ f, Mrestr cP m f ≈ m f.

Definition distr_restr : ∀ 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 : ∀ 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,
     μ (distr_restr cp Hp Hinv Hplus Hmult Hcont) f = cp * m f.

Modular reasoning on programs

Lemma range_cover : ∀ A (P:A → Prop) d cP, range P d → cover P cP →
∀ f, μ d f ≈ μ d (fun x ⇒ cP x * f x).

Lemma mu_cut : ∀ (A:Type)(m:distr A)(P:set A)(cP f g:MF A),
cover P cP → (∀ x, P x → f x ≈ g x) → 1 ≤ μ m cP → μ m f ≈ μ m g.

Uniform measure on finite sets

Section SigmaFinite.
Variable A:Type.
Variable decA : ∀ x y:A, {x=y}+{¬x=y}.

Section RandomFinite.

Distribution for random_fin P 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) :=
     ∀ Q (FQ: finite Q), incl Q P → ∀ x, ¬(Q x) → (P x) → f x ≤ [1-](sigma_fin f FQ).

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

Hint Immediate retract_fin_inv.

Lemma retract_fin_incl : ∀ P Q f, retract_fin P f → incl Q P → retract_fin Q f.

Lemma sigma_fin_monotonic : ∀ (f g : A → U)(P:A->Prop)(FP:finite P),
       (∀ x, P x → (f x) ≤ (g x))→ sigma_fin f FP ≤ sigma_fin g FP.

Lemma sigma_fin_eq_compat :
∀ (f g : A → U)(P:A->Prop)(FP:finite P),
       (∀ x, P x → (f x) ≈ (g x))→ sigma_fin f FP ≈ sigma_fin g FP.

Lemma retract_fin_le : ∀ (P:A->Prop) (f g:A->U),
        (∀ x, P x → f x ≤ g x) → retract_fin P g → retract_fin P f.

Lemma sigma_fin_mult : ∀ (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 : ∀ (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 :
∀ (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 :
∀ (f g : A → U) (c:U) , (∀ k, f k ≤ c) → ∀ (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 :
∀ (f g : A → U) (c:U) , (∀ k, c ≤ f k) → ∀ (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 : ∀ (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 : ∀ 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 : ∀ 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 : ∀ f P (FP:finite P) Q (FQ:finite Q),
              (incl P Q) → sigma_fin f FP ≤ sigma_fin f FQ.

Lemma sigma_fin_unique : ∀ f P Q (FP:finite P) (FQ:finite Q), (eqset P Q)
                         → sigma_fin f FP ≈ sigma_fin f FQ.

Lemma sigma_fin_cte : ∀ c P (FP:finite P),
       sigma_fin (fun _ ⇒ c) FP ≈ (size FP) */ c.

End RandomFinite.

End SigmaFinite.

Properties of the Random distribution

Definition le_dec (n:nat) : dec (fun x ⇒ (x ≤ n)%nat).
Defined.

Definition lt_dec (n:nat) : dec (fun x ⇒ (x < n)%nat).
Defined.

Definition gt_dec : ∀ x, dec (lt x).
Defined.

Definition ge_dec : ∀ x, dec (le x).
Defined.

Definition carac_eq n := carac (eq_nat_dec n).
Definition carac_le n := carac (le_dec n).
Definition carac_lt n := carac (lt_dec n).
Definition carac_gt n := carac (gt_dec n).
Definition carac_ge n := carac (ge_dec 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 (le_dec n).
Definition is_lt (n:nat) : cover (fun x ⇒ (x < n)%nat) (carac_lt n) := cover_dec (lt_dec n).
Definition is_gt (n:nat) : cover (fun x ⇒ (n < x)%nat) (carac_gt n):= cover_dec (gt_dec n).
Definition is_ge (n:nat) : cover (fun x ⇒ (n ≤ x)%nat) (carac_ge n) := cover_dec (ge_dec n).

Lemma carac_gt_S :
  ∀ x y, carac_gt (S y) (S x) ≈ carac_gt y x.

Lemma carac_lt_S : ∀ x y, carac_lt (S x) (S y) ≈ carac_lt x y.

Lemma carac_le_S : ∀ x y, carac_le (S x) (S y) ≈ carac_le x y.

Lemma carac_ge_S : ∀ x y, carac_ge (S x) (S y) ≈ carac_ge x y.

Lemma carac_eq_S : ∀ x y, carac_eq (S x) (S y) ≈ carac_eq x y.

Lemma carac_lt_0 : ∀ y, carac_lt 0 y ≈ 0.

Lemma carac_lt_zero : carac_lt 0 ≈ fzero _.

Lemma carac_lt_if_compat : ∀ 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.

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 : ∀ (P:nat → Prop)(Pdec : dec P)(n:nat),
        (∀ k, (k < n)%nat → P k) → nb_elts Pdec n =n.
Hint Resolve nb_elts_true.

Lemma nb_elts_false : ∀ P,∀ Pdec:dec P,∀ n,
  (∀ 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 : ∀ (P:nat → Prop)(Pdec : dec P)(n:nat),
    μ (Random n) (carac Pdec) ≈ (nb_elts Pdec (S n)) */ [1/]1+n.

Lemma nb_elts_lt_le : ∀ k n, (k ≤ n)%nat → nb_elts (lt_dec k) n = k.

Lemma nb_elts_lt_ge : ∀ k n, (n ≤ k)%nat → nb_elts (lt_dec k) n = n.

Lemma nb_elts_eq_nat_ge :∀ n k,
  (n ≤ k)%nat → nb_elts (eq_nat_dec k) n = 0%nat.

Lemma beq_nat_neq: ∀ x y : nat, x <> y → false = beq_nat x y.

Lemma nb_elt_eq :∀ 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 : ∀ n k, μ (Random n) (carac_lt k) ≈ k */ [1/]1+n.

Hint Resolve Random_lt.

Lemma Random_le : ∀ n k, μ (Random n) (carac_le k) ≈ (S k) */ [1/]1+n.

Hint Resolve Random_le.

Lemma Random_eq : ∀ n k, (k ≤ n)%nat → μ (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 : ∀ x, cover (eq x) (ceq x).

Variable d : distr A.

Variable k : U.

Hypothesis deqP : ∀ x, P x → k ≤ μ d (ceq x).

Lemma d_coverP : ∀ x, P x → k ≤ μ d cP.

Lemma d_coverP_exists : (exists x, P x) → k ≤ μ d cP.

Lemma d_coverP_not_empty : ¬ (∀ x, ¬ P x) → k ≤ μ d cP.

End PickElemts.