move generic things out of convex and convex_equiv

lib/ssr_ext.v

@@ -1078,3 +1078,27 @@ destruct boolP.
   by move=> x y; have:= Bool.bool_dec x y => -[]; [left | right].
 Qed.
 End boolP.
+
+Section fintype_extra.
+
+Lemma index_enum_cast_ord n m (e : n = m) :
+  index_enum 'I_m = [seq cast_ord e i | i <- index_enum 'I_n].
+Proof.
+subst m; rewrite -{1}(map_id (index_enum 'I_n)).
+apply eq_map=> [[x xlt]].
+by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance.
+Qed.
+
+Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f ->
+  perm_eq (index_enum T) [seq f i | i <- index_enum T].
+Proof.
+rewrite /index_enum; case: index_enum_key => /= fbij.
+rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=.
+case: fbij => g fg gf.
+rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _
+    (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))).
+  by rewrite size_filter enumP.
+by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//].
+Qed.
+
+End fintype_extra.

probability/convex.v

@@ -156,144 +156,6 @@ Local Notation "{ 'fdist' T }" := (_ .-fdist T) : fdist_scope.
 #[export] Hint Extern 0 (0 <= onem _)%coqR =>
   exact/RleP/onem_ge0 : core.
 
-(* TODO: the following lemmas are currently not in use. Maybe remove? *)
-Section tmp.
-Local Open Scope ring_scope.
-
-Lemma fdist_convn_Add (R : realType)
-      (n m : nat) (d1 : {fdist 'I_n}) (d2 : {fdist 'I_m}) (p : {prob R})
-      (A : finType) (g : 'I_n -> {fdist A}) (h : 'I_m -> {fdist A}) :
-  fdist_convn (fdist_add d1 d2 p)
-    [ffun i => match fintype.split i with inl a => g a | inr a => h a end] =
-  (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist.
-Proof.
-apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE.
-rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _);
-   apply eq_bigr => i _; rewrite fdist_addE ffunE.
-case: splitP => /= j ij.
-rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj.
-move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0.
-case: splitP => /= j ij.
-move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0.
-move/eqP : ij; rewrite eqn_add2l => /eqP ij.
-rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj.
-Qed.
-
-Import realType_ext.
-Lemma fdist_convn_del
-        (R : realType)
-      (A : finType) (n : nat) (g : 'I_n.+1 -> {fdist A}) (P : {fdist 'I_n.+1})
-      (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) :
-  let g' := fun i : 'I_n => g (fdist_del_idx j i) in
-  fdist_convn P g =
-    (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist.
-Proof.
-move=> g' /=; apply/fdist_ext => a.
-rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _).
-rewrite fdist_convnE big_distrr /=.
-rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=.
-rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _).
-  rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW.
-  move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS.
-  move=> jn'.
-  apply/eq_big.
-  by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF.
-  move=> /= i _.
-  rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first.
-    by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF.
-  rewrite mulrA mulrCA mulrV ?mulr1; last first.
-rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //.
-  congr (P _ * _); first exact/val_inj.
-  by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj.
-rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first.
-  move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle.
-rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first.
-  move=> i; by rewrite -leqNgt.
-rewrite big_mkcond.
-rewrite big_ord_recl ltn0 /= add0r.
-rewrite [in RHS]big_mkcond.
-apply eq_bigr => i _.
-rewrite /bump add1n ltnS; case: ifPn => // ji.
-rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first.
-  apply/eqP => /(congr1 val) => /=.
-  rewrite /bump add1n => ij.
-  by move: ji; apply/negP; rewrite -ij ltnn.
-rewrite -[1 - P j]/(P j).~.
-rewrite [_ / _]mulrC !mulrA divrr ?unitfE ?onem_neq0 // mul1r.
-by rewrite /g' /fdist_del_idx ltnNge ji.
-Qed.
-End tmp.
-
-(* TODO: move*)
-Section fintype_extra.
-
-Lemma index_enum_cast_ord n m (e : n = m) :
-  index_enum 'I_m = [seq cast_ord e i | i <- index_enum 'I_n].
-Proof.
-subst m; rewrite -{1}(map_id (index_enum 'I_n)).
-apply eq_map=> [[x xlt]].
-by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance.
-Qed.
-
-Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f ->
-  perm_eq (index_enum T) [seq f i | i <- index_enum T].
-Proof.
-rewrite /index_enum; case: index_enum_key => /= fbij.
-rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=.
-case: fbij => g fg gf.
-rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _
-    (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))).
-  by rewrite size_filter enumP.
-by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//].
-Qed.
-
-End fintype_extra.
-
-Module CodomDFDist.
-Section def.
-Local Open Scope classical_set_scope.
-Local Open Scope ring_scope.
-Variables (R: realType) (A : Type) (n : nat) (g : 'I_n -> A).
-Variables (e : R .-fdist 'I_n) (y : set A).
-Definition f := [ffun i : 'I_n => if g i \in y then e i else 0].
-Lemma f0 i : (0 <= f i). Proof. by rewrite /f ffunE; case: ifPn. Qed.
-Lemma f1 (x : set A) (gX : g @` setT `<=` x `|` y)
-  (ge : forall i : 'I_n, x (g i) -> e i = 0) :
-  (\sum_(i < n) f i = 1).
-Proof.
-rewrite /f -(FDist.f1 e) /=.
-apply eq_bigr => i _; rewrite ffunE.
-case: ifPn => // /negP; rewrite in_setE => ygi.
-rewrite ge //.
-have : (x `|` y) (g i) by apply/gX; by exists i.
-by case.
-Qed.
-Definition d (x : set A) (gX : g @` setT `<=` x `|` y)
-  (ge : forall i : 'I_n, x (g i) -> e i = 0) : {fdist 'I_n} :=
-  locked (FDist.make f0 (f1 gX ge)).
-Lemma dE (x : set A) (gX : g @` setT `<=` x `|` y)
-  (ge : forall i : 'I_n, x (g i) -> e i = 0) i :
-  d gX ge i = if g i \in y then e i else 0.
-Proof. by rewrite /d; unlock; rewrite ffunE. Qed.
-Lemma f1' (x : set A) (gX : g @` setT `<=` x `|` y)
-  (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) :
-  (\sum_(i < n) f i = 1).
-Proof.
-rewrite /f -(FDist.f1 e) /=; apply eq_bigr => i _; rewrite ffunE.
-case: ifPn => // /negP; rewrite in_setE => giy.
-rewrite ge //.
-have : (x `|` y) (g i) by apply/gX; by exists i.
-by case.
-Qed.
-Definition d' (x : set A) (gX : g @` setT `<=` x `|` y)
-  (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) :=
-  locked (FDist.make f0 (f1' gX ge)).
-Lemma dE' (x : set A) (gX : g @` setT `<=` x `|` y)
-  (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) i :
-  d' gX ge i = if g i \in y then e i else 0.
-Proof. by rewrite /d'; unlock; rewrite ffunE. Qed.
-End def.
-End CodomDFDist.
 
 HB.mixin Record isConvexSpace0 T of Choice T := {
   conv : {prob R} -> T -> T -> T ;

probability/convex_equiv.v

@@ -56,70 +56,6 @@ Import NaryConvexSpace.
 (* In this module we use funext to avoid explicitly handling the congruence
    of convn (cf. eq_convn in convex_choice.v for the iterated version). *)
 
-(* These definitions about distributions should probably be elsewhere *)
-Definition fdistE :=
-  (fdistmapE,fdist1E,fdist_prodE,fdistXI,fdistXE,fdist_convnE,fdist_fstE).
-
-Module FDistPart.
-Section fdistpart.
-Local Open Scope fdist_scope.
-Variables (n m : nat) (K : 'I_m -> 'I_n) (e : {fdist 'I_m}) (i : 'I_n).
-
-Definition d := (fdistX (e `X (fun j => fdist1 (K j)))) `(| i).
-Definition den := (fdistX (e `X (fun j => fdist1 (K j))))`1 i.
-
-Lemma denE : den = fdistmap K e i.
-Proof.
-rewrite /den !fdistE [RHS]big_mkcond /=.
-under eq_bigl do rewrite inE.
-apply/eq_bigr => a _.
-rewrite !fdistE /= (big_pred1 (a,i)) ?fdistE /=;
-    last by case=> x y; rewrite /swap /= !xpair_eqE andbC.
-rewrite eq_sym 2!inE.
-by case: eqP => // _; rewrite (mulr0,mulr1).
-Qed.
-
-Lemma dE j : fdistmap K e i != 0%coqR ->
-  d j = (e j * (i == K j)%:R / \sum_(j | K j == i) e j)%coqR.
-Proof.
-rewrite -denE => NE.
-rewrite jfdist_condE // {NE} /jcPr /proba.Pr.
-rewrite (big_pred1 (j,i)); last first.
-  by move=> k; rewrite !inE [in RHS](surjective_pairing k) xpair_eqE.
-rewrite (big_pred1 i); last by move=> k; rewrite !inE.
-rewrite !fdistE big_mkcond [in RHS]big_mkcond /=.
-rewrite -RmultE -INRE.
-congr (_ / _)%R.
-under eq_bigr => k do rewrite {2}(surjective_pairing k).
-rewrite -(pair_bigA _ (fun k l =>
-          if l == i
-          then e `X (fun j0 : 'I_m => fdist1 (K j0)) (k, l)
-          else R0))%R /=.
-apply eq_bigr => k _.
-rewrite -big_mkcond /= big_pred1_eq !fdistE /= eq_sym.
-by case: ifP; rewrite (mulr1,mulr0).
-Qed.
-End fdistpart.
-
-Lemma dK n m K (e : {fdist 'I_m}) j :
-  e j = (\sum_(i < n) fdistmap K e i * d K e i j)%R.
-Proof.
-under eq_bigr => /= a _.
-  have [Ka0|Ka0] := eqVneq (fdistmap K e a) 0%R.
-    rewrite Ka0 mul0R.
-    have <- : (e j * (a == K j)%:R = 0)%R.
-      have [/eqP Kj|] := eqVneq a (K j); last by rewrite mulR0.
-      move: Ka0; rewrite fdistE /=.
-      by move/psumr_eq0P => -> //; rewrite ?(mul0R,inE) // eq_sym.
-  over.
-  rewrite FDistPart.dE // fdistE /= mulRCA mulRV ?mulR1;
-    last by rewrite fdistE in Ka0.
-over.
-move=> /=.
-rewrite (bigD1 (K j)) //= eqxx mulR1.
-by rewrite big1 ?addR0 // => i /negbTE ->; rewrite mulR0.
-Qed.
-End FDistPart.
 
 Section Axioms.
 Variable T : naryConvType.

probability/fdist.v

@@ -1088,10 +1088,17 @@ Qed.
 
 End fdistX_prop.
 
+Section fdistX_prop_ext.
 Lemma fdistX_prod2 {R: realType}
   (A B : finType) (P : fdist R A) (W : A -> fdist R B) :
   (fdistX (P `X W))`2 = P.
 Proof. by rewrite fdistX2 fdist_prod1. Qed.
+End fdistX_prop_ext.
+
+Section fdist_prop_ext.
+Definition fdistE :=
+  (fdistmapE,fdist1E,fdist_prodE,fdistXI,fdistXE,fdist_convnE,fdist_fstE).
+End fdist_prop_ext.
 
 Section fdist_rV.
 Local Open Scope ring_scope.
@@ -1855,3 +1862,119 @@ Defined.
 *)
 
 End tuple_prod_cast.*)
+
+(* TODO: the following lemmas are currently not in use. Maybe remove? *)
+Section moved_from_convex.
+Local Open Scope ring_scope.
+
+Lemma fdist_convn_Add (R : realType)
+      (n m : nat) (d1 : R.-fdist 'I_n) (d2 : R.-fdist 'I_m) (p : {prob R})
+      (A : finType) (g : 'I_n -> R.-fdist A) (h : 'I_m -> R.-fdist A) :
+  fdist_convn (fdist_add d1 d2 p)
+    [ffun i => match fintype.split i with inl a => g a | inr a => h a end] =
+  (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist.
+Proof.
+apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE.
+rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _);
+   apply eq_bigr => i _; rewrite fdist_addE ffunE.
+case: splitP => /= j ij.
+rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj.
+move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0.
+case: splitP => /= j ij.
+move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0.
+move/eqP : ij; rewrite eqn_add2l => /eqP ij.
+rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj.
+Qed.
+
+Import realType_ext.
+Lemma fdist_convn_del
+        (R : realType)
+      (A : finType) (n : nat) (g : 'I_n.+1 -> R.-fdist A) (P : R.-fdist 'I_n.+1)
+      (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) :
+  let g' := fun i : 'I_n => g (fdist_del_idx j i) in
+  fdist_convn P g =
+    (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist.
+Proof.
+move=> g' /=; apply/fdist_ext => a.
+rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _).
+rewrite fdist_convnE big_distrr /=.
+rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=.
+rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _).
+  rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW.
+  move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS.
+  move=> jn'.
+  apply/eq_big.
+  by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF.
+  move=> /= i _.
+  rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first.
+    by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF.
+  rewrite mulrA mulrCA mulrV ?mulr1; last first.
+rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //.
+  congr (P _ * _); first exact/val_inj.
+  by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj.
+rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first.
+  move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle.
+rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first.
+  move=> i; by rewrite -leqNgt.
+rewrite big_mkcond.
+rewrite big_ord_recl ltn0 /= add0r.
+rewrite [in RHS]big_mkcond.
+apply eq_bigr => i _.
+rewrite /bump add1n ltnS; case: ifPn => // ji.
+rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first.
+  apply/eqP => /(congr1 val) => /=.
+  rewrite /bump add1n => ij.
+  by move: ji; apply/negP; rewrite -ij ltnn.
+rewrite -[1 - P j]/(P j).~.
+rewrite [_ / _]mulrC !mulrA divrr ?unitfE ?onem_neq0 // mul1r.
+by rewrite /g' /fdist_del_idx ltnNge ji.
+Qed.
+End moved_from_convex.
+
+
+Module CodomDFDist.
+Import classical_sets.
+Section def.
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+Variables (R: realType) (A : Type) (n : nat) (g : 'I_n -> A).
+Variables (e : R .-fdist 'I_n) (y : set A).
+Definition f := [ffun i : 'I_n => if g i \in y then e i else 0].
+Lemma f0 i : (0 <= f i). Proof. by rewrite /f ffunE; case: ifPn. Qed.
+Lemma f1 (x : set A) (gX : g @` setT `<=` x `|` y)
+  (ge : forall i : 'I_n, x (g i) -> e i = 0) :
+  (\sum_(i < n) f i = 1).
+Proof.
+rewrite /f -(FDist.f1 e) /=.
+apply eq_bigr => i _; rewrite ffunE.
+case: ifPn => // /negP; rewrite in_setE => ygi.
+rewrite ge //.
+have : (x `|` y) (g i) by apply/gX; by exists i.
+by case.
+Qed.
+Definition d (x : set A) (gX : g @` setT `<=` x `|` y)
+  (ge : forall i : 'I_n, x (g i) -> e i = 0) : R.-fdist 'I_n :=
+  locked (FDist.make f0 (f1 gX ge)).
+Lemma dE (x : set A) (gX : g @` setT `<=` x `|` y)
+  (ge : forall i : 'I_n, x (g i) -> e i = 0) i :
+  d gX ge i = if g i \in y then e i else 0.
+Proof. by rewrite /d; unlock; rewrite ffunE. Qed.
+Lemma f1' (x : set A) (gX : g @` setT `<=` x `|` y)
+  (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) :
+  (\sum_(i < n) f i = 1).
+Proof.
+rewrite /f -(FDist.f1 e) /=; apply eq_bigr => i _; rewrite ffunE.
+case: ifPn => // /negP; rewrite in_setE => giy.
+rewrite ge //.
+have : (x `|` y) (g i) by apply/gX; by exists i.
+by case.
+Qed.
+Definition d' (x : set A) (gX : g @` setT `<=` x `|` y)
+  (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) :=
+  locked (FDist.make f0 (f1' gX ge)).
+Lemma dE' (x : set A) (gX : g @` setT `<=` x `|` y)
+  (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) i :
+  d' gX ge i = if g i \in y then e i else 0.
+Proof. by rewrite /d'; unlock; rewrite ffunE. Qed.
+End def.
+End CodomDFDist.