Library probsa.probability.independence
From prosa Require Import classic.util.list.
From probsa.util Require Export zip bigop r_mult tr_eq.
From probsa.probability Require Export conditional.
Lemma pr_cond_indep2 :
∀ {Ω : countType} {μ : measure Ω} (A B : pred Ω) ρ,
indep2 (mkRvar μ A) (mkRvar μ B) →
ℙ<μ,ρ>{[ A | B ]} = ℙ<μ>{[ A ]}.
Proof.
intros × IND.
rewrite pr_cond_axiomatic; specialize (IND true true).
rewrite (pr_eq_pred_pos _ (A ∩ B)) in IND; last first.
{ by intros × POS; unfold "∩", pred.pred_intersection ⇒ //=; destruct A, B. }
rewrite IND; clear IND.
rewrite /pr_eq //= /Rdiv Rmult_assoc.
rewrite -[RHS]Rmult_1_r; apply Rmult_eq_compat.
{ by apply pr_eq_pred ⇒ ω; rewrite !unfold_in; destruct A. }
{ rewrite (pr_eq_pred_pos _ B); last by intros × _; destruct B.
by apply Rinv_r ⇒ Z; move: ρ; rewrite /PosProb Z ⇒ ρ; apply Rgt_irrefl in ρ. }
Qed.
Section Indep2.
Section IndepExt.
Context {Ω : countType} {μ : measure Ω} (B1 B2 C1 C2 : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ C1) (Y1 : rvar μ B2) (Y2 : rvar μ C2).
Variables (f1 : B1 → C1) (f2 : B2 → C2).
Lemma indep2_fn_ext :
(∀ ω, μ ω > 0 → rvar_comp X1 f1 ω = X2 ω) →
(∀ ω, μ ω > 0 → rvar_comp Y1 f2 ω = Y2 ω) →
indep2 X1 Y1 →
indep2 X2 Y2.
Proof.
intros × EQU1 EQU2 IND ? ?.
erewrite pr_eq_pred_pos; last first.
{ by intros ω POS; rewrite -EQU1 -?EQU2 //. }
rewrite indep2_fn //; apply Rmult_eq_compat.
- by apply pr_eq_pred_pos ⇒ ω POS; rewrite EQU1.
- by apply pr_eq_pred_pos ⇒ ω POS; rewrite EQU2.
Qed.
End IndepExt.
Section IndepExtL.
Context {Ω : countType} {μ: measure Ω} (B1 B2 C : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ B2) (Y : rvar μ C).
Variable f : B1 → B2.
Lemma indep2_fn_extl :
(∀ ω, μ ω > 0 → rvar_comp X1 f ω = X2 ω) →
indep2 X1 Y →
indep2 X2 Y.
Proof.
by intros; eapply indep2_fn_ext with (f2 := fun x ⇒ x); eauto 1.
Qed.
End IndepExtL.
End Indep2.
Section IndependentCat.
Context {Ω} {μ : measure Ω} {T : eqType}.
Lemma indep_catC :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent (ys ++ xs).
Proof.
intros × IND ? LEN.
have [xlb [ylb [EQ [SIZE1 SIZE2]]]] :
∃ xlb ylb,
ylb ++ xlb = lb
∧ size ylb = size ys
∧ size xlb = size xs.
{ ∃ (drop (size ys) lb), (take (size ys) lb).
rewrite cat_take_drop; split ⇒ //; split.
- rewrite size_take.
move: LEN; rewrite -!seq_ext.size_legacy size_cat ⇒ →.
destruct xs; first by rewrite addn0 ltnn.
by rewrite -{1}[size ys]addn0 ltn_add2l ltn0Sn.
- rewrite size_drop.
move: LEN; rewrite -!seq_ext.size_legacy size_cat ⇒ →.
by rewrite addKn.
}
apply: eq_tr4; first apply IND with (lb := xlb ++ ylb); subst lb.
{ by move: LEN; rewrite -!seq_ext.size_legacy !size_cat addnC ⇒ ->; rewrite addnC. }
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
rewrite !zip_cat; [| rewrite SIZE2 | rewrite SIZE1] ⇒ //.
by rewrite !map_cat !foldr_big !big_cat //= andbC.
}
{ rewrite !zip_cat; [| rewrite SIZE2 | rewrite SIZE1] ⇒ //.
by rewrite !map_cat !foldr_big !big_cat //= Rmult_comm.
}
Qed.
Lemma indep_cat_split :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent xs ∧ independent ys.
Proof.
have L :
∀ (xs : seq (rvar μ T)) (ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent ys.
{ clear; induction xs; intros ⇒ //.
by apply independent_tl in H; apply IHxs. }
intros; split.
{ by apply indep_catC in H; apply: L; apply H. }
{ by apply: L; apply H. }
Qed.
Lemma indep_cat_indep2_list :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_list xs) (rvar_list ys).
Proof.
intros × IND ? ?.
move: (IND) ⇒ G; apply indep_cat_split in G; move: G ⇒ [IND1 IND2].
specialize (IND (b1 ++ b2)).
destruct (size xs == size b1) eqn:EQ1, (size ys == size b2) eqn:EQ2; move: EQ1 EQ2 ⇒ /eqP EQ1 /eqP EQ2.
{ feed IND; first by rewrite -!seq_ext.size_legacy !size_cat EQ1 EQ2.
apply: eq_tr4; first by apply IND.
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in zip_cat //= map_cat.
rewrite foldr_big big_cat //=; f_equal.
{ clear IND IND1; move: xs EQ1; clear.
elim: b1 ⇒ [| b bs IND]; first by move ⇒ [ | x xs]; rewrite //= big_nil.
move ⇒ [ | x xs] ⇒ //=.
by move ⇒ EQ; apply eq_add_S in EQ; rewrite //= big_cons -IND // eqseq_cons. }
{ clear IND IND2; move: ys EQ2; clear.
elim: b2 ⇒ [| b bs IND]; first by move ⇒ [ | y ys]; rewrite //= big_nil.
move ⇒ [ | y ys] ⇒ //=.
by move ⇒ EQ; apply eq_add_S in EQ; rewrite //= big_cons -IND // eqseq_cons. }
}
{ rewrite zip_cat //= map_cat foldr_big big_cat //=; f_equal.
{ apply: eq_tr4.
{ by apply IND1; rewrite -!seq_ext.size_legacy; symmetry; eassumption. }
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in /rvar_list //=.
{ clear IND IND1; move: xs EQ1; clear.
elim: b1 ⇒ [| b bs IND]; first by move ⇒ [ | x xs]; rewrite //= big_nil.
move ⇒ [ | x xs] ⇒ //=.
by move ⇒ EQ; apply eq_add_S in EQ; rewrite //= -IND // eqseq_cons. }
}
{ by rewrite foldr_big. }
}
{ rewrite independent_rvar_list ⇒ //.
by rewrite foldr_big.
}
}
}
{ apply eq_tr3 with 0; [ | symmetry; apply Rmult_eq_0_compat_l].
by apply pr_zero ⇒ ω; rewrite andb_false_intro2 // rvar_list_eq_short //= ⇒ ?; apply EQ2.
by apply pr_zero ⇒ ω; rewrite rvar_list_eq_short //= ⇒ ?; apply EQ2.
}
{ apply eq_tr3 with 0; [ | symmetry; apply Rmult_eq_0_compat_r].
by apply pr_zero ⇒ ω; rewrite andb_false_intro1 // rvar_list_eq_short //= ⇒ ?; apply EQ1.
by apply pr_zero ⇒ ω; rewrite rvar_list_eq_short //= ⇒ ?; apply EQ1.
}
{ apply eq_tr3 with 0; [ | symmetry; apply Rmult_eq_0_compat_r].
by apply pr_zero ⇒ ω; rewrite andb_false_intro1 // rvar_list_eq_short //= ⇒ ?; apply EQ1.
by apply pr_zero ⇒ ω; rewrite rvar_list_eq_short //= ⇒ ?; apply EQ1.
}
Qed.
Fact indep_cat_indep2_list_comp :
∀ (f : seq T → nat) (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_comp (rvar_list xs) f) (rvar_comp (rvar_list ys) f).
Proof.
intros × IND.
apply indep_cat_indep2_list in IND.
by apply indep2_fn.
Qed.
End IndependentCat.
Section IndependentMap.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → rvar μ B.
Lemma indep_perm_eq :
∀ (xs ys : seq A),
perm_eq xs ys →
independent [seq F i | i <- xs] →
independent [seq F i | i <- ys].
Proof.
intros × PERM IND lb LEN.
rewrite -!seq_ext.size_legacy size_map in LEN; symmetry in LEN.
have [plb [PERM2 SIZE2]] := perm_eq_zippable xs ys lb PERM LEN.
unshelve (apply: eq_tr4; first apply IND with (lb := plb)).
{ by rewrite -!seq_ext.size_legacy -SIZE2 size_map. }
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
rewrite !foldr_big; apply perm_big.
rewrite !zip_map_rvar_eq; apply perm_map; rewrite perm_sym.
by rewrite -[plb]map_id -[lb]map_id !zip_map; apply perm_map.
}
{ rewrite !foldr_big; apply perm_big.
rewrite !zip_map_pr_eq.
apply (perm_map (fun Xb ⇒ pr_eq (F Xb.1) Xb.2)).
by rewrite !map_id perm_sym.
}
Qed.
Lemma indep_filter :
∀ (P : pred A) (xs : seq A),
independent [seq F i | i <- xs] →
independent [seq F i | i <- xs & P i].
Proof.
intros.
eapply indep_cat_split with [seq F i | i <- xs & (!P) i].
rewrite -map_cat; eapply indep_perm_eq; last by eassumption.
rewrite perm_sym.
eapply perm_trans; last by apply/permPl; apply perm_filterC.
eapply perm_trans; last by apply/permPl; apply perm_catC.
by apply perm_cat; apply perm_refl.
Qed.
Lemma indep_subset :
∀ (xs ys : seq A),
(∀ x, x \in xs → x \in ys) →
uniq xs →
uniq ys →
independent [seq F y | y <- ys] →
independent [seq F x | x <- xs].
Proof.
intros × SUB UNIQx UNIQy IND.
eapply indep_filter in IND.
have EQ:
perm_eq xs [seq y <- ys | y \in xs].
{ clear IND.
apply uniq_perm ⇒ //.
- by apply filter_uniq.
- intros ?; rewrite mem_filter.
destruct (_ \in _ ) eqn:IN; last by done.
symmetry; rewrite andTb.
by apply SUB.
}
apply: indep_perm_eq.
- by rewrite perm_sym; apply: EQ.
- by apply IND.
Qed.
Lemma indep_comp :
∀ {C : eqType} (f : B → C) (xs : seq A),
independent [seq F x | x <- xs] →
independent [seq rvar_comp (F x) f | x <- xs].
Proof.
intros × IND.
induction xs as [| x l].
- apply independent_nil.
- rewrite map_cons; apply indep2_independent_cons.
× apply: indep2_ext;
[ intros ω; reflexivity
| | eapply indep2_fn; apply independent_indep2_tl; simpl in *; apply IND].
instantiate (1 := map f).
intros ω; unfold rvar_comp, "\o" ⇒ //=.
clear IHl IND; induction l; first by done.
by simpl; f_equal; apply IHl.
× by apply IHl; eapply independent_tl; eauto.
Qed.
Lemma indep_irr :
∀ (G : A → rvar μ B) (xs : seq A),
(∀ x ω, x \in xs → μ ω > 0 → F x ω = G x ω) →
independent [seq F x | x <- xs] →
independent [seq G x | x <- xs].
Proof.
intros × EQ IND vs LEN.
apply: eq_tr4; [apply IND | | ]; first last.
{ f_equal; instantiate (1 := vs).
rewrite -!seq_ext.size_legacy !size_map in LEN.
destruct xs as [ | x xs], vs as [ | v vs]; try done.
inversion LEN as [LE]; clear LEN; rename LE into LEN.
apply eq_from_nth with 0.
{ by rewrite !size_map !size_zip !size_map. }
intros i LT; erewrite !nth_map with (x1 := (F x, v));
try by move: LT; rewrite !size_map !size_zip !size_map //.
erewrite !nth_zip; try by rewrite !size_map //= LEN.
erewrite !nth_map with (x1 := x);
try by move: LT; rewrite size_map size_zip size_map //= LEN minnn.
apply pr_eq_pred_pos ⇒ ω POS. f_equal; symmetry.
by apply EQ ⇒ //; apply mem_nth; move: LT; rewrite size_map size_zip size_map //= LEN minnn.
}
{ apply pr_eq_pred_pos ⇒ ω POS; f_equal.
rewrite -!seq_ext.size_legacy !size_map in LEN.
destruct xs as [ | x xs], vs as [ | v vs]; try done.
inversion LEN as [LE]; clear LEN; rename LE into LEN.
apply eq_from_nth with false.
{ by rewrite !size_map !size_zip !size_map. }
intros i LT; erewrite !nth_map with (x1 := (F x, v));
try by move: LT; rewrite !size_map !size_zip !size_map //.
erewrite !nth_zip; try by rewrite !size_map //= LEN.
erewrite !nth_map with (x1 := x);
try by move: LT; rewrite size_map size_zip size_map //= LEN minnn.
symmetry; simpl; f_equal.
by apply EQ ⇒ //; apply mem_nth; move: LT; rewrite size_map size_zip size_map //= LEN minnn.
}
{ by move: LEN; rewrite -!seq_ext.size_legacy !size_map ⇒ →. }
Qed.
End IndependentMap.
Section IndependentPair.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Lemma indep_pair_swap :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Ω → Z),
independent [seq (mkRvar μ (fun ω ⇒ (B x ω, A x ω))) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x ω))) | x <- xs].
Proof.
clear; intros × IND vs LEN; rewrite -!seq_ext.size_legacy size_map in LEN.
specialize (IND (map (fun '(a,b) ⇒ (b,a)) vs)); feed IND.
{ by rewrite -!seq_ext.size_legacy !size_map. }
apply: eq_tr4; [apply IND | clear IND | clear IND].
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
move: vs LEN; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
by rewrite //= IHxs // !xpair_eqE; f_equal; rewrite andbC.
}
{ move: vs LEN; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= IHxs //; apply Rmult_eq_compat_r.
by apply pr_eq_pred ⇒ ω; rewrite !unfold_in //= !xpair_eqE andbC.
}
Qed.
Lemma indep_pair_const_r :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Z),
independent [seq (mkRvar μ (A x)) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x))) | x <- xs].
Proof.
clear; intros × IND vs LEN; rewrite -!seq_ext.size_legacy size_map in LEN.
destruct (map B xs == map snd vs) eqn:EQ; last first.
{ clear IND; apply eq_tr3 with 0; last symmetry.
{ apply pr_zero ⇒ ω POS.
move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /eqP.
rewrite eqbF_neg negb_and ⇒ /orP [NEQ|NEQ].
- apply/eqP; rewrite eqbF_neg negb_and; apply/orP; left.
by apply/negP ⇒ /eqP EQ; inversion EQ; subst; rewrite eq_refl in NEQ.
- apply/eqP; rewrite eqbF_neg negb_and; apply/orP; right.
by rewrite IHxs //; apply/neqP ⇒ EQ; rewrite EQ eq_refl in NEQ.
}
{ move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /eqP.
rewrite eqbF_neg negb_and ⇒ /orP [NEQ|NEQ].
- apply Rmult_eq_0_compat_r, pr_zero ⇒ ω POS.
by apply/negP ⇒ /eqP EQ; inversion EQ; subst; rewrite eq_refl in NEQ.
- apply Rmult_eq_0_compat_l.
by rewrite IHxs //; apply/neqP ⇒ EQ; rewrite EQ eq_refl in NEQ.
}
}
{ specialize (IND (map fst vs)); feed IND.
{ by rewrite -!seq_ext.size_legacy !size_map. }
apply: eq_tr4; [apply IND | clear IND | clear IND].
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /andP [/eqP EQ1 EQ2].
rewrite //= IHxs //; f_equal.
by rewrite EQ1 xpair_eqE eq_refl andbT.
}
{ move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /andP [/eqP EQ1 EQ2].
rewrite //= IHxs //; f_equal.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
by rewrite EQ1 xpair_eqE eq_refl andbT.
}
}
Qed.
End IndependentPair.
Section IndependentFlatten.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Variable f : X → Ω → Y → Z.
Variables (xs : seq X) (ys : X → seq Y).
Lemma independent_flatten :
independent [seq mkRvar μ (fun ω ⇒ f x ω y) | x <- xs, y <- ys x] →
independent [seq mkRvar μ (fun ω ⇒ [ seq f x ω y | y <- ys x]) | x <- xs].
Proof.
intros × IND vss LEN; rewrite -!seq_ext.size_legacy size_map in LEN.
have [NEQ | EQ] :
(∃ x v, (x,v) \in zip xs vss ∧ size (ys x) != size v)
∨ (∀ x v, (x,v) \in zip xs vss → size (ys x) = size v).
{ clear IND; move: vss LEN; induction xs.
{ by intros [] ⇒ //; move ⇒ _; right. }
intros [ | ]; try done.
intros; inversion LEN as [LEN2]; clear LEN; rename LEN2 into LEN.
specialize (IHl _ LEN) ⇒ //=.
destruct (size (ys a) == size s) eqn:EQ; last first.
{ left; ∃ a, s; split.
- by rewrite in_cons eq_refl orTb.
- by apply/negP; rewrite EQ. }
{ destruct IHl as [[x [v [ZIP NEQ]]]| ].
- by left; ∃ x, v; rewrite in_cons ZIP orbT //.
- right ⇒ x v; rewrite in_cons ⇒ /orP [/eqP EQ2 | ].
+ by inversion EQ2; subst; move: EQ ⇒ /eqP.
+ by intros; apply H.
}
}
{ apply eq_tr3 with 0; [ | symmetry]; clear IND.
{ apply pr_zero ⇒ ω POS.
move : NEQ ⇒ [x [v [ZIP NEQ]]].
move: vss LEN ZIP; induction xs.
- by intros [].
- intros [ | w vss] ? ? ⇒ //.
rewrite //=; destruct (_ == w) eqn:EQ; last by done.
rewrite andTb; move: ZIP; rewrite //= in_cons ⇒ /orP [/eqP EQT | ZIP].
+ inversion EQT; clear EQT; subst; exfalso.
by move: EQ ⇒ /eqP EQ; subst w; rewrite size_map eq_refl in NEQ.
+ by inversion LEN; erewrite IHl.
}
{ move : NEQ ⇒ [x [v [ZIP NEQ]]].
move: vss LEN ZIP; induction xs.
- by intros [].
- intros [ | w vss] ? ? ⇒ //.
rewrite //=; edestruct Req_dec as [EQ|POS];
apply Rmult_eq_0_compat; [left | right]; first by apply EQ.
move: ZIP; rewrite //= in_cons ⇒ /orP [/eqP EQT | ZIP].
+ inversion EQT; clear EQT; subst; exfalso.
apply: POS; apply pr_zero ⇒ ω POS ⇒ //=; apply /negP ⇒ /eqP EQ; subst w.
by rewrite size_map eq_refl in NEQ.
+ by inversion LEN; apply IHl.
}
}
{ move: (IND) (IND (flatten vss)) ⇒ INDS INDL; clear IND.
feed INDL.
{ clear INDL INDS.
rewrite -!seq_ext.size_legacy size_allpairs_dep.
move: vss LEN EQ; induction xs.
- by intros [].
- move ⇒ []; first by done.
intros v vss T EQ; inversion T as [LEN]; clear T.
rewrite //= size_cat; erewrite EQ; last first.
+ by rewrite //= in_cons; apply/orP; left; apply/eqP.
+ f_equal; apply IHl ⇒ //.
by intros; apply EQ; rewrite in_cons H orbT.
}
{ eapply eq_tr4; first by apply: INDL.
{ clear INDL INDS; apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
move: vss LEN EQ; induction xs.
- by intros [].
- move ⇒ []; first by done.
move ⇒ v vss LEN EQ.
rewrite //= zip_cat; last first.
+ by rewrite size_map; apply EQ; rewrite //= in_cons eq_refl orTb.
+ rewrite map_cat IHl; first last.
{ by intros; apply EQ; rewrite //= in_cons H orbT. }
{ by inversion LEN. }
rewrite [RHS]foldr_big big_cat -!foldr_big //=.
f_equal; move: (EQ a v) ⇒ EQo.
feed EQo; first by rewrite in_cons eq_refl orTb.
move: EQo; clear; move: v; induction (ys a); first by move ⇒ [].
move ⇒ [] ⇒ //.
intros v vs EQo; rewrite //= eqseq_cons IHl //.
by inversion EQo.
}
{ clear INDL; move: vss LEN EQ; induction xs; first by intros [].
move ⇒ []; first by done.
move ⇒ v vss LEN EQ; rewrite //= zip_cat; last first.
{ rewrite size_map; apply EQ; by rewrite //= in_cons eq_refl. }
rewrite map_cat IHl; first last.
{ by intros; apply EQ; rewrite //= in_cons H orbT. }
{ by inversion LEN. }
{ by simpl in INDS; eapply indep_cat_split; apply INDS. }
rewrite [RHS]foldr_big big_cat -!foldr_big //=; f_equal.
move: (EQ a v) ⇒ EQo.
feed EQo; first by rewrite in_cons eq_refl orTb.
simpl in INDS; apply indep_cat_split in INDS. destruct INDS as [INDS _ ].
move: EQo INDS; clear; move: v; induction (ys a).
{ by move ⇒ [] ⇒ //; intros _ _; apply pr_xpredT_ext ⇒ ω. }
intros []; [done | intros].
simpl in *; rewrite -IHl; last first.
{ by apply: independent_tl; eassumption. }
{ by inversion EQo. }
clear IHl; inversion EQo as [LEN]; clear EQo.
apply independent_indep2_tl in INDS.
apply: eq_tr4; first by apply INDS with (b1 := s) (b2 := l0).
- apply pr_eq_pred ⇒ ω; rewrite !unfold_in //= eqseq_cons.
f_equal; clear INDS; move: l0 LEN.
induction l; first by intros [].
intros []; first by done.
intros; inversion LEN.
by rewrite //= eqseq_cons IHl ⇒ //.
- f_equal; apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
clear INDS; move: l0 LEN; induction l; first by done.
intros []; first by done.
intros; inversion LEN.
by rewrite eqseq_cons IHl ⇒ //.
}
}
}
Qed.
End IndependentFlatten.
Section IndependentExtend.
Context {Ω} {μ : measure Ω} {X Y : eqType}.
Variable F : X → rvar μ Y.
Lemma indep_consts :
∀ (xs : seq X),
(∀ x, x \in xs → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs].
Proof.
intros × CON ys SIZE; rewrite -!seq_ext.size_legacy size_map in SIZE.
have [cs VE] : ∃ cs, ∀ ω, [seq F x ω | x <- xs] = cs.
{ clear ys SIZE; induction xs; first by (∃ [::]).
destruct (CON a) as [c EQ]; first by rewrite in_cons eq_refl orTb.
destruct IHxs as [cs EQs]; first by intros; apply CON; rewrite in_cons H orbT.
∃ (c::cs) ⇒ ω; apply/eqP.
by rewrite //= eqseq_cons EQ EQs //= !eq_refl.
}
destruct (ys == cs) eqn:EQ.
{ apply eq_tr3 with 1; last symmetry.
{ apply pr_xpredT_ext ⇒ ω.
rewrite zip_map_rvar_eq VE -zip_foldr_andb_seq_eq.
{ by rewrite eq_sym EQ. }
{ by move: EQ ⇒ /eqP →. }
}
{ rewrite foldr_big big1_seq //.
move: EQ ⇒ /eqP EQ; subst cs.
move ⇒ r ⇒ /andP [_ IN]; rewrite zip_map_pr_eq in IN.
move: IN ⇒ /mapP2; move ⇒ [[x y] /Iter.In_mem IN EQ]; subst r.
apply pr_xpredT_ext ⇒ ω.
specialize (VE ω); subst ys.
apply mem_zip_exists with (elem := x) (elem' := y) in IN; last by rewrite !size_map.
destruct IN as [idx [LT1 [LT2 [EQ1 EQ2]]]].
rewrite EQ1 EQ2 map_id.
by erewrite nth_map; [apply/eqP | rewrite size_map in LT1].
}
}
{ apply eq_tr3 with 0; last symmetry.
{ apply pr_zero ⇒ ω POS.
rewrite zip_map_rvar_eq VE -zip_foldr_andb_seq_eq.
{ by rewrite eq_sym EQ. }
{ by rewrite -(VE ω) size_map; symmetry. }
}
{ destruct (@nonempty_sample_space Ω μ) as [ω _].
rewrite zip_map_pr_eq.
move: cs ys SIZE EQ VE; induction xs as [ | x xs]; intros.
specialize (VE ω); subst cs; destruct ys ⇒ //.
feed IHxs; first by intros; apply CON; rewrite in_cons; apply/orP; right.
destruct ys as [ | y ys]; first by done.
destruct cs as [ | c cs]; first by specialize (VE ω).
move: EQ; rewrite eqseq_cons ⇒ /eqP; rewrite eqbF_neg negb_and ⇒ /orP [NEQ|NEQ].
{ apply Rmult_eq_0_compat_r, pr_zero ⇒ ωo _.
move: (VE ωo) ⇒ /eqP; rewrite eqseq_cons ⇒ /andP [/eqP → _].
by rewrite eq_sym; apply/negP/negP; rewrite NEQ.
}
{ apply Rmult_eq_0_compat_l; apply (IHxs cs).
{ by apply eq_add_S in SIZE. }
{ by apply/negP/negP; rewrite NEQ. }
{ by intros ωo; move: (VE ωo) ⇒ /eqP; rewrite //= eqseq_cons ⇒ /andP [_ /eqP EQ]. }
}
}
}
Qed.
Lemma indep_extend_consts :
∀ (xs1 xs2 : seq X),
(∀ x, x \in xs2 → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs1] →
independent [seq F x | x <- xs1 ++ xs2].
Proof.
intros × CONS IND.
rewrite map_cat; apply indep_catC; rewrite -map_cat ⇒ ys LEN.
have [ys1 [ys2 [EQ [LEN1 LEN2]]]] :
∃ ys1 ys2, ys = ys2 ++ ys1 ∧ size xs1 = size ys1 ∧ size xs2 = size ys2.
{ rewrite -!seq_ext.size_legacy size_map size_cat in LEN.
∃ (drop (size xs2) ys), (take (size xs2) ys).
rewrite cat_take_drop; split ⇒ //.
by split; [rewrite size_drop LEN addKn | rewrite size_takel // LEN leq_addr].
}
subst ys; clear LEN.
rewrite !map_cat zip_cat; last by rewrite size_map.
rewrite foldr_big map_cat big_cat //=.
specialize (IND ys1); feed IND; first by rewrite -!seq_ext.size_legacy size_map LEN1.
rewrite -!foldr_big -IND; clear IND.
rewrite -(indep_consts _ CONS ys2); last by rewrite -!seq_ext.size_legacy size_map LEN2.
move: ys2 LEN2; induction xs2; intros.
{ symmetry; rewrite pr_xpredT_ext; last by intros ω; rewrite zip_nil.
rewrite Rmult_1_l; apply pr_eq_pred' ⇒ ω.
by rewrite zip_nil.
}
destruct ys2 as [ | y ys2]; first by done.
feed IHxs2; first by intros; apply CONS; rewrite in_cons; apply/orP; right.
specialize (IHxs2 ys2); feed IHxs2; first by apply eq_add_S in LEN2.
specialize (CONS a); feed CONS; first by rewrite in_cons eq_refl orTb.
destruct CONS as [c EQU]; simpl.
destruct (y == c) eqn:EQ.
{ erewrite pr_eq_pred_pos; first last.
{ by intros; rewrite EQU eq_sym EQ andTb; reflexivity. }
rewrite IHxs2; apply Rmult_eq_compat_r; symmetry.
erewrite pr_eq_pred_pos; first last.
{ by intros; rewrite EQU eq_sym EQ andTb; reflexivity. }
reflexivity.
}
{ apply eq_tr3 with 0.
{ apply pr_zero ⇒ ω POS.
by rewrite EQU //= eq_sym EQ andFb.
}
{ symmetry; apply Rmult_eq_0_compat_r, pr_zero ⇒ ω POS.
by rewrite EQU //= eq_sym EQ andFb.
}
}
Qed.
End IndependentExtend.
Section IndependentSum.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → nrvar μ.
Lemma indep2_sum :
∀ (P : pred A) (xs ys : seq A),
independent [seq F i | i <- xs ++ ys] →
indep2 (∑[rv]_{x <- xs | P x} F x) (∑[rv]_{y <- ys | P y} F y).
Proof.
intros × IND ? ?.
apply indep_filter with (P0 := P) in IND; apply: eq_tr4.
eapply indep_cat_indep2_list_comp with (f := fun ns ⇒ fold_right addn 0%N ns).
{ by rewrite filter_cat map_cat in IND; apply IND. }
{ clear IND.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in; f_equal.
{ rewrite /rvar_comp //=; f_equal.
induction xs; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHxs. }
{ rewrite /rvar_comp //=; f_equal.
induction ys; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHys. }
}
{ clear IND; f_equal; apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=.
{ f_equal; induction xs; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHxs. }
{ f_equal; induction ys; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHys. }
}
Qed.
Lemma indep2_sum_cons :
∀ (x : A) (xs : seq A),
independent [seq F i | i <- x::xs] →
indep2 (F x) (∑[rv]_{x <- xs} F x).
Proof.
intros.
have IND := indep2_sum xpredT [::x] xs H.
intros a b; apply: eq_tr4; first by apply (IND a b).
{ clear IND.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in; f_equal.
rewrite /rvar_comp //=; f_equal.
by rewrite sum_nrvar_sum_nat big_seq1.
}
{ rewrite /rvar_comp //=; f_equal.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in; f_equal.
by rewrite sum_nrvar_sum_nat big_seq1.
}
Qed.
End IndependentSum.
From probsa.util Require Export zip bigop r_mult tr_eq.
From probsa.probability Require Export conditional.
Lemma pr_cond_indep2 :
∀ {Ω : countType} {μ : measure Ω} (A B : pred Ω) ρ,
indep2 (mkRvar μ A) (mkRvar μ B) →
ℙ<μ,ρ>{[ A | B ]} = ℙ<μ>{[ A ]}.
Proof.
intros × IND.
rewrite pr_cond_axiomatic; specialize (IND true true).
rewrite (pr_eq_pred_pos _ (A ∩ B)) in IND; last first.
{ by intros × POS; unfold "∩", pred.pred_intersection ⇒ //=; destruct A, B. }
rewrite IND; clear IND.
rewrite /pr_eq //= /Rdiv Rmult_assoc.
rewrite -[RHS]Rmult_1_r; apply Rmult_eq_compat.
{ by apply pr_eq_pred ⇒ ω; rewrite !unfold_in; destruct A. }
{ rewrite (pr_eq_pred_pos _ B); last by intros × _; destruct B.
by apply Rinv_r ⇒ Z; move: ρ; rewrite /PosProb Z ⇒ ρ; apply Rgt_irrefl in ρ. }
Qed.
Section Indep2.
Section IndepExt.
Context {Ω : countType} {μ : measure Ω} (B1 B2 C1 C2 : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ C1) (Y1 : rvar μ B2) (Y2 : rvar μ C2).
Variables (f1 : B1 → C1) (f2 : B2 → C2).
Lemma indep2_fn_ext :
(∀ ω, μ ω > 0 → rvar_comp X1 f1 ω = X2 ω) →
(∀ ω, μ ω > 0 → rvar_comp Y1 f2 ω = Y2 ω) →
indep2 X1 Y1 →
indep2 X2 Y2.
Proof.
intros × EQU1 EQU2 IND ? ?.
erewrite pr_eq_pred_pos; last first.
{ by intros ω POS; rewrite -EQU1 -?EQU2 //. }
rewrite indep2_fn //; apply Rmult_eq_compat.
- by apply pr_eq_pred_pos ⇒ ω POS; rewrite EQU1.
- by apply pr_eq_pred_pos ⇒ ω POS; rewrite EQU2.
Qed.
End IndepExt.
Section IndepExtL.
Context {Ω : countType} {μ: measure Ω} (B1 B2 C : eqType).
Variables (X1 : rvar μ B1) (X2 : rvar μ B2) (Y : rvar μ C).
Variable f : B1 → B2.
Lemma indep2_fn_extl :
(∀ ω, μ ω > 0 → rvar_comp X1 f ω = X2 ω) →
indep2 X1 Y →
indep2 X2 Y.
Proof.
by intros; eapply indep2_fn_ext with (f2 := fun x ⇒ x); eauto 1.
Qed.
End IndepExtL.
End Indep2.
Section IndependentCat.
Context {Ω} {μ : measure Ω} {T : eqType}.
Lemma indep_catC :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent (ys ++ xs).
Proof.
intros × IND ? LEN.
have [xlb [ylb [EQ [SIZE1 SIZE2]]]] :
∃ xlb ylb,
ylb ++ xlb = lb
∧ size ylb = size ys
∧ size xlb = size xs.
{ ∃ (drop (size ys) lb), (take (size ys) lb).
rewrite cat_take_drop; split ⇒ //; split.
- rewrite size_take.
move: LEN; rewrite -!seq_ext.size_legacy size_cat ⇒ →.
destruct xs; first by rewrite addn0 ltnn.
by rewrite -{1}[size ys]addn0 ltn_add2l ltn0Sn.
- rewrite size_drop.
move: LEN; rewrite -!seq_ext.size_legacy size_cat ⇒ →.
by rewrite addKn.
}
apply: eq_tr4; first apply IND with (lb := xlb ++ ylb); subst lb.
{ by move: LEN; rewrite -!seq_ext.size_legacy !size_cat addnC ⇒ ->; rewrite addnC. }
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
rewrite !zip_cat; [| rewrite SIZE2 | rewrite SIZE1] ⇒ //.
by rewrite !map_cat !foldr_big !big_cat //= andbC.
}
{ rewrite !zip_cat; [| rewrite SIZE2 | rewrite SIZE1] ⇒ //.
by rewrite !map_cat !foldr_big !big_cat //= Rmult_comm.
}
Qed.
Lemma indep_cat_split :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent xs ∧ independent ys.
Proof.
have L :
∀ (xs : seq (rvar μ T)) (ys : seq (rvar μ T)),
independent (xs ++ ys) →
independent ys.
{ clear; induction xs; intros ⇒ //.
by apply independent_tl in H; apply IHxs. }
intros; split.
{ by apply indep_catC in H; apply: L; apply H. }
{ by apply: L; apply H. }
Qed.
Lemma indep_cat_indep2_list :
∀ (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_list xs) (rvar_list ys).
Proof.
intros × IND ? ?.
move: (IND) ⇒ G; apply indep_cat_split in G; move: G ⇒ [IND1 IND2].
specialize (IND (b1 ++ b2)).
destruct (size xs == size b1) eqn:EQ1, (size ys == size b2) eqn:EQ2; move: EQ1 EQ2 ⇒ /eqP EQ1 /eqP EQ2.
{ feed IND; first by rewrite -!seq_ext.size_legacy !size_cat EQ1 EQ2.
apply: eq_tr4; first by apply IND.
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in zip_cat //= map_cat.
rewrite foldr_big big_cat //=; f_equal.
{ clear IND IND1; move: xs EQ1; clear.
elim: b1 ⇒ [| b bs IND]; first by move ⇒ [ | x xs]; rewrite //= big_nil.
move ⇒ [ | x xs] ⇒ //=.
by move ⇒ EQ; apply eq_add_S in EQ; rewrite //= big_cons -IND // eqseq_cons. }
{ clear IND IND2; move: ys EQ2; clear.
elim: b2 ⇒ [| b bs IND]; first by move ⇒ [ | y ys]; rewrite //= big_nil.
move ⇒ [ | y ys] ⇒ //=.
by move ⇒ EQ; apply eq_add_S in EQ; rewrite //= big_cons -IND // eqseq_cons. }
}
{ rewrite zip_cat //= map_cat foldr_big big_cat //=; f_equal.
{ apply: eq_tr4.
{ by apply IND1; rewrite -!seq_ext.size_legacy; symmetry; eassumption. }
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in /rvar_list //=.
{ clear IND IND1; move: xs EQ1; clear.
elim: b1 ⇒ [| b bs IND]; first by move ⇒ [ | x xs]; rewrite //= big_nil.
move ⇒ [ | x xs] ⇒ //=.
by move ⇒ EQ; apply eq_add_S in EQ; rewrite //= -IND // eqseq_cons. }
}
{ by rewrite foldr_big. }
}
{ rewrite independent_rvar_list ⇒ //.
by rewrite foldr_big.
}
}
}
{ apply eq_tr3 with 0; [ | symmetry; apply Rmult_eq_0_compat_l].
by apply pr_zero ⇒ ω; rewrite andb_false_intro2 // rvar_list_eq_short //= ⇒ ?; apply EQ2.
by apply pr_zero ⇒ ω; rewrite rvar_list_eq_short //= ⇒ ?; apply EQ2.
}
{ apply eq_tr3 with 0; [ | symmetry; apply Rmult_eq_0_compat_r].
by apply pr_zero ⇒ ω; rewrite andb_false_intro1 // rvar_list_eq_short //= ⇒ ?; apply EQ1.
by apply pr_zero ⇒ ω; rewrite rvar_list_eq_short //= ⇒ ?; apply EQ1.
}
{ apply eq_tr3 with 0; [ | symmetry; apply Rmult_eq_0_compat_r].
by apply pr_zero ⇒ ω; rewrite andb_false_intro1 // rvar_list_eq_short //= ⇒ ?; apply EQ1.
by apply pr_zero ⇒ ω; rewrite rvar_list_eq_short //= ⇒ ?; apply EQ1.
}
Qed.
Fact indep_cat_indep2_list_comp :
∀ (f : seq T → nat) (xs ys : seq (rvar μ T)),
independent (xs ++ ys) →
indep2 (rvar_comp (rvar_list xs) f) (rvar_comp (rvar_list ys) f).
Proof.
intros × IND.
apply indep_cat_indep2_list in IND.
by apply indep2_fn.
Qed.
End IndependentCat.
Section IndependentMap.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → rvar μ B.
Lemma indep_perm_eq :
∀ (xs ys : seq A),
perm_eq xs ys →
independent [seq F i | i <- xs] →
independent [seq F i | i <- ys].
Proof.
intros × PERM IND lb LEN.
rewrite -!seq_ext.size_legacy size_map in LEN; symmetry in LEN.
have [plb [PERM2 SIZE2]] := perm_eq_zippable xs ys lb PERM LEN.
unshelve (apply: eq_tr4; first apply IND with (lb := plb)).
{ by rewrite -!seq_ext.size_legacy -SIZE2 size_map. }
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
rewrite !foldr_big; apply perm_big.
rewrite !zip_map_rvar_eq; apply perm_map; rewrite perm_sym.
by rewrite -[plb]map_id -[lb]map_id !zip_map; apply perm_map.
}
{ rewrite !foldr_big; apply perm_big.
rewrite !zip_map_pr_eq.
apply (perm_map (fun Xb ⇒ pr_eq (F Xb.1) Xb.2)).
by rewrite !map_id perm_sym.
}
Qed.
Lemma indep_filter :
∀ (P : pred A) (xs : seq A),
independent [seq F i | i <- xs] →
independent [seq F i | i <- xs & P i].
Proof.
intros.
eapply indep_cat_split with [seq F i | i <- xs & (!P) i].
rewrite -map_cat; eapply indep_perm_eq; last by eassumption.
rewrite perm_sym.
eapply perm_trans; last by apply/permPl; apply perm_filterC.
eapply perm_trans; last by apply/permPl; apply perm_catC.
by apply perm_cat; apply perm_refl.
Qed.
Lemma indep_subset :
∀ (xs ys : seq A),
(∀ x, x \in xs → x \in ys) →
uniq xs →
uniq ys →
independent [seq F y | y <- ys] →
independent [seq F x | x <- xs].
Proof.
intros × SUB UNIQx UNIQy IND.
eapply indep_filter in IND.
have EQ:
perm_eq xs [seq y <- ys | y \in xs].
{ clear IND.
apply uniq_perm ⇒ //.
- by apply filter_uniq.
- intros ?; rewrite mem_filter.
destruct (_ \in _ ) eqn:IN; last by done.
symmetry; rewrite andTb.
by apply SUB.
}
apply: indep_perm_eq.
- by rewrite perm_sym; apply: EQ.
- by apply IND.
Qed.
Lemma indep_comp :
∀ {C : eqType} (f : B → C) (xs : seq A),
independent [seq F x | x <- xs] →
independent [seq rvar_comp (F x) f | x <- xs].
Proof.
intros × IND.
induction xs as [| x l].
- apply independent_nil.
- rewrite map_cons; apply indep2_independent_cons.
× apply: indep2_ext;
[ intros ω; reflexivity
| | eapply indep2_fn; apply independent_indep2_tl; simpl in *; apply IND].
instantiate (1 := map f).
intros ω; unfold rvar_comp, "\o" ⇒ //=.
clear IHl IND; induction l; first by done.
by simpl; f_equal; apply IHl.
× by apply IHl; eapply independent_tl; eauto.
Qed.
Lemma indep_irr :
∀ (G : A → rvar μ B) (xs : seq A),
(∀ x ω, x \in xs → μ ω > 0 → F x ω = G x ω) →
independent [seq F x | x <- xs] →
independent [seq G x | x <- xs].
Proof.
intros × EQ IND vs LEN.
apply: eq_tr4; [apply IND | | ]; first last.
{ f_equal; instantiate (1 := vs).
rewrite -!seq_ext.size_legacy !size_map in LEN.
destruct xs as [ | x xs], vs as [ | v vs]; try done.
inversion LEN as [LE]; clear LEN; rename LE into LEN.
apply eq_from_nth with 0.
{ by rewrite !size_map !size_zip !size_map. }
intros i LT; erewrite !nth_map with (x1 := (F x, v));
try by move: LT; rewrite !size_map !size_zip !size_map //.
erewrite !nth_zip; try by rewrite !size_map //= LEN.
erewrite !nth_map with (x1 := x);
try by move: LT; rewrite size_map size_zip size_map //= LEN minnn.
apply pr_eq_pred_pos ⇒ ω POS. f_equal; symmetry.
by apply EQ ⇒ //; apply mem_nth; move: LT; rewrite size_map size_zip size_map //= LEN minnn.
}
{ apply pr_eq_pred_pos ⇒ ω POS; f_equal.
rewrite -!seq_ext.size_legacy !size_map in LEN.
destruct xs as [ | x xs], vs as [ | v vs]; try done.
inversion LEN as [LE]; clear LEN; rename LE into LEN.
apply eq_from_nth with false.
{ by rewrite !size_map !size_zip !size_map. }
intros i LT; erewrite !nth_map with (x1 := (F x, v));
try by move: LT; rewrite !size_map !size_zip !size_map //.
erewrite !nth_zip; try by rewrite !size_map //= LEN.
erewrite !nth_map with (x1 := x);
try by move: LT; rewrite size_map size_zip size_map //= LEN minnn.
symmetry; simpl; f_equal.
by apply EQ ⇒ //; apply mem_nth; move: LT; rewrite size_map size_zip size_map //= LEN minnn.
}
{ by move: LEN; rewrite -!seq_ext.size_legacy !size_map ⇒ →. }
Qed.
End IndependentMap.
Section IndependentPair.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Lemma indep_pair_swap :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Ω → Z),
independent [seq (mkRvar μ (fun ω ⇒ (B x ω, A x ω))) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x ω))) | x <- xs].
Proof.
clear; intros × IND vs LEN; rewrite -!seq_ext.size_legacy size_map in LEN.
specialize (IND (map (fun '(a,b) ⇒ (b,a)) vs)); feed IND.
{ by rewrite -!seq_ext.size_legacy !size_map. }
apply: eq_tr4; [apply IND | clear IND | clear IND].
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
move: vs LEN; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
by rewrite //= IHxs // !xpair_eqE; f_equal; rewrite andbC.
}
{ move: vs LEN; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= IHxs //; apply Rmult_eq_compat_r.
by apply pr_eq_pred ⇒ ω; rewrite !unfold_in //= !xpair_eqE andbC.
}
Qed.
Lemma indep_pair_const_r :
∀ (xs : seq X) (A : X → Ω → Y) (B : X → Z),
independent [seq (mkRvar μ (A x)) | x <- xs] →
independent [seq (mkRvar μ (fun ω ⇒ (A x ω, B x))) | x <- xs].
Proof.
clear; intros × IND vs LEN; rewrite -!seq_ext.size_legacy size_map in LEN.
destruct (map B xs == map snd vs) eqn:EQ; last first.
{ clear IND; apply eq_tr3 with 0; last symmetry.
{ apply pr_zero ⇒ ω POS.
move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /eqP.
rewrite eqbF_neg negb_and ⇒ /orP [NEQ|NEQ].
- apply/eqP; rewrite eqbF_neg negb_and; apply/orP; left.
by apply/negP ⇒ /eqP EQ; inversion EQ; subst; rewrite eq_refl in NEQ.
- apply/eqP; rewrite eqbF_neg negb_and; apply/orP; right.
by rewrite IHxs //; apply/neqP ⇒ EQ; rewrite EQ eq_refl in NEQ.
}
{ move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /eqP.
rewrite eqbF_neg negb_and ⇒ /orP [NEQ|NEQ].
- apply Rmult_eq_0_compat_r, pr_zero ⇒ ω POS.
by apply/negP ⇒ /eqP EQ; inversion EQ; subst; rewrite eq_refl in NEQ.
- apply Rmult_eq_0_compat_l.
by rewrite IHxs //; apply/neqP ⇒ EQ; rewrite EQ eq_refl in NEQ.
}
}
{ specialize (IND (map fst vs)); feed IND.
{ by rewrite -!seq_ext.size_legacy !size_map. }
apply: eq_tr4; [apply IND | clear IND | clear IND].
{ apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /andP [/eqP EQ1 EQ2].
rewrite //= IHxs //; f_equal.
by rewrite EQ1 xpair_eqE eq_refl andbT.
}
{ move: vs LEN EQ; induction xs; first by intros [].
intros [ | [v1 v2] vs]; first by done.
intros LEN; simpl in LEN; apply eq_add_S in LEN.
rewrite //= eqseq_cons ⇒ /andP [/eqP EQ1 EQ2].
rewrite //= IHxs //; f_equal.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
by rewrite EQ1 xpair_eqE eq_refl andbT.
}
}
Qed.
End IndependentPair.
Section IndependentFlatten.
Context {Ω} {μ : measure Ω} {X Y Z : eqType}.
Variable f : X → Ω → Y → Z.
Variables (xs : seq X) (ys : X → seq Y).
Lemma independent_flatten :
independent [seq mkRvar μ (fun ω ⇒ f x ω y) | x <- xs, y <- ys x] →
independent [seq mkRvar μ (fun ω ⇒ [ seq f x ω y | y <- ys x]) | x <- xs].
Proof.
intros × IND vss LEN; rewrite -!seq_ext.size_legacy size_map in LEN.
have [NEQ | EQ] :
(∃ x v, (x,v) \in zip xs vss ∧ size (ys x) != size v)
∨ (∀ x v, (x,v) \in zip xs vss → size (ys x) = size v).
{ clear IND; move: vss LEN; induction xs.
{ by intros [] ⇒ //; move ⇒ _; right. }
intros [ | ]; try done.
intros; inversion LEN as [LEN2]; clear LEN; rename LEN2 into LEN.
specialize (IHl _ LEN) ⇒ //=.
destruct (size (ys a) == size s) eqn:EQ; last first.
{ left; ∃ a, s; split.
- by rewrite in_cons eq_refl orTb.
- by apply/negP; rewrite EQ. }
{ destruct IHl as [[x [v [ZIP NEQ]]]| ].
- by left; ∃ x, v; rewrite in_cons ZIP orbT //.
- right ⇒ x v; rewrite in_cons ⇒ /orP [/eqP EQ2 | ].
+ by inversion EQ2; subst; move: EQ ⇒ /eqP.
+ by intros; apply H.
}
}
{ apply eq_tr3 with 0; [ | symmetry]; clear IND.
{ apply pr_zero ⇒ ω POS.
move : NEQ ⇒ [x [v [ZIP NEQ]]].
move: vss LEN ZIP; induction xs.
- by intros [].
- intros [ | w vss] ? ? ⇒ //.
rewrite //=; destruct (_ == w) eqn:EQ; last by done.
rewrite andTb; move: ZIP; rewrite //= in_cons ⇒ /orP [/eqP EQT | ZIP].
+ inversion EQT; clear EQT; subst; exfalso.
by move: EQ ⇒ /eqP EQ; subst w; rewrite size_map eq_refl in NEQ.
+ by inversion LEN; erewrite IHl.
}
{ move : NEQ ⇒ [x [v [ZIP NEQ]]].
move: vss LEN ZIP; induction xs.
- by intros [].
- intros [ | w vss] ? ? ⇒ //.
rewrite //=; edestruct Req_dec as [EQ|POS];
apply Rmult_eq_0_compat; [left | right]; first by apply EQ.
move: ZIP; rewrite //= in_cons ⇒ /orP [/eqP EQT | ZIP].
+ inversion EQT; clear EQT; subst; exfalso.
apply: POS; apply pr_zero ⇒ ω POS ⇒ //=; apply /negP ⇒ /eqP EQ; subst w.
by rewrite size_map eq_refl in NEQ.
+ by inversion LEN; apply IHl.
}
}
{ move: (IND) (IND (flatten vss)) ⇒ INDS INDL; clear IND.
feed INDL.
{ clear INDL INDS.
rewrite -!seq_ext.size_legacy size_allpairs_dep.
move: vss LEN EQ; induction xs.
- by intros [].
- move ⇒ []; first by done.
intros v vss T EQ; inversion T as [LEN]; clear T.
rewrite //= size_cat; erewrite EQ; last first.
+ by rewrite //= in_cons; apply/orP; left; apply/eqP.
+ f_equal; apply IHl ⇒ //.
by intros; apply EQ; rewrite in_cons H orbT.
}
{ eapply eq_tr4; first by apply: INDL.
{ clear INDL INDS; apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
move: vss LEN EQ; induction xs.
- by intros [].
- move ⇒ []; first by done.
move ⇒ v vss LEN EQ.
rewrite //= zip_cat; last first.
+ by rewrite size_map; apply EQ; rewrite //= in_cons eq_refl orTb.
+ rewrite map_cat IHl; first last.
{ by intros; apply EQ; rewrite //= in_cons H orbT. }
{ by inversion LEN. }
rewrite [RHS]foldr_big big_cat -!foldr_big //=.
f_equal; move: (EQ a v) ⇒ EQo.
feed EQo; first by rewrite in_cons eq_refl orTb.
move: EQo; clear; move: v; induction (ys a); first by move ⇒ [].
move ⇒ [] ⇒ //.
intros v vs EQo; rewrite //= eqseq_cons IHl //.
by inversion EQo.
}
{ clear INDL; move: vss LEN EQ; induction xs; first by intros [].
move ⇒ []; first by done.
move ⇒ v vss LEN EQ; rewrite //= zip_cat; last first.
{ rewrite size_map; apply EQ; by rewrite //= in_cons eq_refl. }
rewrite map_cat IHl; first last.
{ by intros; apply EQ; rewrite //= in_cons H orbT. }
{ by inversion LEN. }
{ by simpl in INDS; eapply indep_cat_split; apply INDS. }
rewrite [RHS]foldr_big big_cat -!foldr_big //=; f_equal.
move: (EQ a v) ⇒ EQo.
feed EQo; first by rewrite in_cons eq_refl orTb.
simpl in INDS; apply indep_cat_split in INDS. destruct INDS as [INDS _ ].
move: EQo INDS; clear; move: v; induction (ys a).
{ by move ⇒ [] ⇒ //; intros _ _; apply pr_xpredT_ext ⇒ ω. }
intros []; [done | intros].
simpl in *; rewrite -IHl; last first.
{ by apply: independent_tl; eassumption. }
{ by inversion EQo. }
clear IHl; inversion EQo as [LEN]; clear EQo.
apply independent_indep2_tl in INDS.
apply: eq_tr4; first by apply INDS with (b1 := s) (b2 := l0).
- apply pr_eq_pred ⇒ ω; rewrite !unfold_in //= eqseq_cons.
f_equal; clear INDS; move: l0 LEN.
induction l; first by intros [].
intros []; first by done.
intros; inversion LEN.
by rewrite //= eqseq_cons IHl ⇒ //.
- f_equal; apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
clear INDS; move: l0 LEN; induction l; first by done.
intros []; first by done.
intros; inversion LEN.
by rewrite eqseq_cons IHl ⇒ //.
}
}
}
Qed.
End IndependentFlatten.
Section IndependentExtend.
Context {Ω} {μ : measure Ω} {X Y : eqType}.
Variable F : X → rvar μ Y.
Lemma indep_consts :
∀ (xs : seq X),
(∀ x, x \in xs → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs].
Proof.
intros × CON ys SIZE; rewrite -!seq_ext.size_legacy size_map in SIZE.
have [cs VE] : ∃ cs, ∀ ω, [seq F x ω | x <- xs] = cs.
{ clear ys SIZE; induction xs; first by (∃ [::]).
destruct (CON a) as [c EQ]; first by rewrite in_cons eq_refl orTb.
destruct IHxs as [cs EQs]; first by intros; apply CON; rewrite in_cons H orbT.
∃ (c::cs) ⇒ ω; apply/eqP.
by rewrite //= eqseq_cons EQ EQs //= !eq_refl.
}
destruct (ys == cs) eqn:EQ.
{ apply eq_tr3 with 1; last symmetry.
{ apply pr_xpredT_ext ⇒ ω.
rewrite zip_map_rvar_eq VE -zip_foldr_andb_seq_eq.
{ by rewrite eq_sym EQ. }
{ by move: EQ ⇒ /eqP →. }
}
{ rewrite foldr_big big1_seq //.
move: EQ ⇒ /eqP EQ; subst cs.
move ⇒ r ⇒ /andP [_ IN]; rewrite zip_map_pr_eq in IN.
move: IN ⇒ /mapP2; move ⇒ [[x y] /Iter.In_mem IN EQ]; subst r.
apply pr_xpredT_ext ⇒ ω.
specialize (VE ω); subst ys.
apply mem_zip_exists with (elem := x) (elem' := y) in IN; last by rewrite !size_map.
destruct IN as [idx [LT1 [LT2 [EQ1 EQ2]]]].
rewrite EQ1 EQ2 map_id.
by erewrite nth_map; [apply/eqP | rewrite size_map in LT1].
}
}
{ apply eq_tr3 with 0; last symmetry.
{ apply pr_zero ⇒ ω POS.
rewrite zip_map_rvar_eq VE -zip_foldr_andb_seq_eq.
{ by rewrite eq_sym EQ. }
{ by rewrite -(VE ω) size_map; symmetry. }
}
{ destruct (@nonempty_sample_space Ω μ) as [ω _].
rewrite zip_map_pr_eq.
move: cs ys SIZE EQ VE; induction xs as [ | x xs]; intros.
specialize (VE ω); subst cs; destruct ys ⇒ //.
feed IHxs; first by intros; apply CON; rewrite in_cons; apply/orP; right.
destruct ys as [ | y ys]; first by done.
destruct cs as [ | c cs]; first by specialize (VE ω).
move: EQ; rewrite eqseq_cons ⇒ /eqP; rewrite eqbF_neg negb_and ⇒ /orP [NEQ|NEQ].
{ apply Rmult_eq_0_compat_r, pr_zero ⇒ ωo _.
move: (VE ωo) ⇒ /eqP; rewrite eqseq_cons ⇒ /andP [/eqP → _].
by rewrite eq_sym; apply/negP/negP; rewrite NEQ.
}
{ apply Rmult_eq_0_compat_l; apply (IHxs cs).
{ by apply eq_add_S in SIZE. }
{ by apply/negP/negP; rewrite NEQ. }
{ by intros ωo; move: (VE ωo) ⇒ /eqP; rewrite //= eqseq_cons ⇒ /andP [_ /eqP EQ]. }
}
}
}
Qed.
Lemma indep_extend_consts :
∀ (xs1 xs2 : seq X),
(∀ x, x \in xs2 → ∃ c, F x =1 rvar_const μ c) →
independent [seq F x | x <- xs1] →
independent [seq F x | x <- xs1 ++ xs2].
Proof.
intros × CONS IND.
rewrite map_cat; apply indep_catC; rewrite -map_cat ⇒ ys LEN.
have [ys1 [ys2 [EQ [LEN1 LEN2]]]] :
∃ ys1 ys2, ys = ys2 ++ ys1 ∧ size xs1 = size ys1 ∧ size xs2 = size ys2.
{ rewrite -!seq_ext.size_legacy size_map size_cat in LEN.
∃ (drop (size xs2) ys), (take (size xs2) ys).
rewrite cat_take_drop; split ⇒ //.
by split; [rewrite size_drop LEN addKn | rewrite size_takel // LEN leq_addr].
}
subst ys; clear LEN.
rewrite !map_cat zip_cat; last by rewrite size_map.
rewrite foldr_big map_cat big_cat //=.
specialize (IND ys1); feed IND; first by rewrite -!seq_ext.size_legacy size_map LEN1.
rewrite -!foldr_big -IND; clear IND.
rewrite -(indep_consts _ CONS ys2); last by rewrite -!seq_ext.size_legacy size_map LEN2.
move: ys2 LEN2; induction xs2; intros.
{ symmetry; rewrite pr_xpredT_ext; last by intros ω; rewrite zip_nil.
rewrite Rmult_1_l; apply pr_eq_pred' ⇒ ω.
by rewrite zip_nil.
}
destruct ys2 as [ | y ys2]; first by done.
feed IHxs2; first by intros; apply CONS; rewrite in_cons; apply/orP; right.
specialize (IHxs2 ys2); feed IHxs2; first by apply eq_add_S in LEN2.
specialize (CONS a); feed CONS; first by rewrite in_cons eq_refl orTb.
destruct CONS as [c EQU]; simpl.
destruct (y == c) eqn:EQ.
{ erewrite pr_eq_pred_pos; first last.
{ by intros; rewrite EQU eq_sym EQ andTb; reflexivity. }
rewrite IHxs2; apply Rmult_eq_compat_r; symmetry.
erewrite pr_eq_pred_pos; first last.
{ by intros; rewrite EQU eq_sym EQ andTb; reflexivity. }
reflexivity.
}
{ apply eq_tr3 with 0.
{ apply pr_zero ⇒ ω POS.
by rewrite EQU //= eq_sym EQ andFb.
}
{ symmetry; apply Rmult_eq_0_compat_r, pr_zero ⇒ ω POS.
by rewrite EQU //= eq_sym EQ andFb.
}
}
Qed.
End IndependentExtend.
Section IndependentSum.
Context {Ω} {μ : measure Ω} {A B : eqType}.
Variable F : A → nrvar μ.
Lemma indep2_sum :
∀ (P : pred A) (xs ys : seq A),
independent [seq F i | i <- xs ++ ys] →
indep2 (∑[rv]_{x <- xs | P x} F x) (∑[rv]_{y <- ys | P y} F y).
Proof.
intros × IND ? ?.
apply indep_filter with (P0 := P) in IND; apply: eq_tr4.
eapply indep_cat_indep2_list_comp with (f := fun ns ⇒ fold_right addn 0%N ns).
{ by rewrite filter_cat map_cat in IND; apply IND. }
{ clear IND.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in; f_equal.
{ rewrite /rvar_comp //=; f_equal.
induction xs; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHxs. }
{ rewrite /rvar_comp //=; f_equal.
induction ys; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHys. }
}
{ clear IND; f_equal; apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=.
{ f_equal; induction xs; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHxs. }
{ f_equal; induction ys; first by rewrite big_nil.
by rewrite big_cons //=; destruct (P a) eqn:Pa ⇒ //=; rewrite IHys. }
}
Qed.
Lemma indep2_sum_cons :
∀ (x : A) (xs : seq A),
independent [seq F i | i <- x::xs] →
indep2 (F x) (∑[rv]_{x <- xs} F x).
Proof.
intros.
have IND := indep2_sum xpredT [::x] xs H.
intros a b; apply: eq_tr4; first by apply (IND a b).
{ clear IND.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in; f_equal.
rewrite /rvar_comp //=; f_equal.
by rewrite sum_nrvar_sum_nat big_seq1.
}
{ rewrite /rvar_comp //=; f_equal.
apply pr_eq_pred ⇒ ω; rewrite !unfold_in; f_equal.
by rewrite sum_nrvar_sum_nat big_seq1.
}
Qed.
End IndependentSum.