address comment from review

Co-authored-by: Takafumi Saikawa <[email protected]>

_CoqProject

@@ -29,7 +29,7 @@ probability/fsdist.v
 probability/convex.v
 probability/convex_equiv.v
 probability/convex_stone.v
-probability/jfdist.v
+probability/jfdist_cond.v
 probability/graphoid.v
 probability/jensen.v
 probability/ln_facts.v
@@ -42,7 +42,6 @@ probability/necset.v
 probability/bayes.v
 information_theory/source_code.v
 information_theory/entropy.v
-information_theory/chap2.v
 information_theory/channel.v
 information_theory/pproba.v
 information_theory/channel_code.v
@@ -63,7 +62,7 @@ information_theory/channel_coding_converse.v
 information_theory/kraft.v
 information_theory/shannon_fano.v
 information_theory/string_entropy.v
-information_theory/convex_fdist.v
+information_theory/entropy_convex.v
 information_theory/source_coding_vl_direct.v
 information_theory/source_coding_vl_converse.v
 ecc_classic/linearcode.v

changelog.txt

@@ -164,10 +164,10 @@ from 0.4.0 to 0.4.1
   + CondJFDist.dNE -> jfdist_cond_dflt
   + CJFDist.t -> jfdist_prod0
   + CJFDist.joint_of -> jfdist_prod
-  + CJFDist.CondJFDistE -> jfdist_prod_cond
-  + CJFDist.E -> jfdist_prodE
-  + CJFDist.split -> jfdist_split
-  + CJFDist.splitE -> jfdist_prodK
+  + CJFDist.CondJFDistE -> fdist_cond_prod
+  + CJFDist.E -> jcPr_fdistX_prod
+  + CJFDist.split -> fdist_split
+  + CJFDist.splitE -> fdist_prodK
   + Multivar.to_bivar -> fdist_prod_of_rV
   + Multivar.to_bivarE -> fdist_prod_of_rVE
   + Multivar.belast_last -> fdist_belast_last_of_rV
@@ -309,14 +309,29 @@ from 0.4.0 to 0.4.1
   + tuple_pmf_out_fdist -> fdist_rV_out
   + MutualInfoChan.mut_info ->  mutual_info_chan
   + mut_info_chanE -> mutual_info_chanE
-- removed:
+  + jcPr_max -> jcPr_le1
+  + CondEntropyChan.h -> cond_entropy_chan
+  + CondEntropyChanE -> cond_entropy_chanE
+  + CondEntropyChanE2 -> cond_entropy_chanE2
+  + Receivable.t -> receivable
+  + Receivable.def -> receivable_prop
+  + Receivable.mk -> mkReceivable
+  + receivableE -> receivable_propE
+  + not_receivable_uniformE -> not_receivable_prop_uniform
+  + PosteriorProbability.d -> fdist_post_prob
+  + PosteriorProbability.dE -> fdist_post_probE
+  + PosteriorProbability.ppE -> post_probE
+  + PosteriorProbability.Kppu -> post_prob_uniform_cst
+  + MarginalPostProbability.d -> fdist_marginal_post_prob
+- Removed:
   + Module TripA'
   + imset_fst
   + big_scalept
   + `p_
   + big_rV_0
   + CJFDist.make_joint
   + JointFDistChan.d
+  + `J(P, W) notation
 - changed:
   + scaledptR0 (now derived from the interface of quasi real cones)
     and renamed scalept0

ecc_classic/decoding.v

@@ -138,10 +138,10 @@ Lemma ML_err_rate x1 x2 y : repair y = Some x1 ->
 Proof.
 move=> Hx1 Hx2.
 case/boolP : (W ``(y | x2) == 0%R) => [/eqP -> //| Hcase].
-have Hy : Receivable.def P W y.
+have PWy : receivable_prop P W y.
   apply/existsP; exists x2.
   by rewrite Hcase andbT fdist_uniform_supp_neq0 inE.
-case: (ML_dec (Receivable.mk Hy)) => x' [].
+case: (ML_dec (mkReceivable PWy)) => x' [].
 rewrite /= Hx1 => -[<-] ->.
 rewrite -big_filter.
 apply (leR_bigmaxR (fun i => W ``(y | i))).
@@ -178,9 +178,9 @@ rewrite (eq_bigl (fun m => phi tb == Some m)); last by move=> m; rewrite inE.
 rewrite [in X in _ <= X](eq_bigl (fun m => dec tb == Some m)); last by move=> m; rewrite inE.
 (* show that phi_ML succeeds more often than phi *)
 have [dectb_None|dectb_Some] := boolP (dec tb == None).
-  case/boolP : (Receivable.def P W tb) => [Hy|Htb].
-    case: (ML_dec (Receivable.mk Hy)) => [m' [tb_m']].
-    move: dectb_None; by rewrite {1}/dec {1}ffunE tb_m'.
+  case/boolP : (receivable_prop P W tb) => [Hy|Htb].
+    case: (ML_dec (mkReceivable Hy)) => [m' [tb_m']].
+    by move: dectb_None; rewrite {1}/dec {1}ffunE tb_m'.
   have W_tb m : W ``(tb | enc m) = 0%R.
     apply/eqP; apply/contraR : Htb => Htb.
     apply/existsP; exists (enc m).
@@ -286,7 +286,7 @@ have -> : W ``(y | c) = g (dH_y c).
   clear cast_card.
   rewrite -/W compatible //.
   move/subsetP : f_img; apply.
-  by rewrite inE; apply/existsP; exists (Receivable.y y); apply/eqP.
+  by rewrite inE; apply/existsP; exists (receivable_rV y); apply/eqP.
 transitivity (\big[Rmax/R0]_(c in C) (g (dH_y c))); last first.
   apply eq_bigr => /= c' Hc'.
   move: (DMC_BSC_prop p enc (discard c') y).
@@ -301,8 +301,8 @@ rewrite (@bigmaxR_bigmin_vec_helper _ _ _ _ _ _ _ _ _ _ codebook_not_empty) //.
 - move=> r; rewrite /g.
   apply mulR_ge0; apply pow_le => //; lra.
 - rewrite inE; move/subsetP: f_img; apply.
-  rewrite inE; apply/existsP; by exists (Receivable.y y); apply/eqP.
-- move=> ? _; by rewrite /dH_y max_dH.
+  rewrite inE; apply/existsP; by exists (receivable_rV y); apply/eqP.
+- by move=> ? _; rewrite /dH_y max_dH.
 - by rewrite /dH_y MD.
 Qed.
 
@@ -333,42 +333,43 @@ Lemma MAP_implies_ML : MAP_decoding W C dec P -> ML_decoding W C dec P.
 Proof.
 move=> HMAP.
 rewrite /ML_decoding => /= tb.
-have Hunpos : INR 1 / INR #| [set cw in C] | > 0.
-  rewrite div1R; exact/invR_gt0/ltR0n/vspace_not_empty.
-move: (HMAP tb) => H.
-rewrite /PosteriorProbability.d in H.
-unlock in H.
-simpl in H.
-set tmp := \rmax_(_ <- _ | _) _ in H.
-rewrite /tmp in H.
+have Hunpos : 1%:R / INR #| [set cw in C] | > 0.
+  by rewrite div1R; exact/invR_gt0/ltR0n/vspace_not_empty.
+move: (HMAP tb) => [m [tbm]].
+rewrite /fdist_post_prob. unlock. simpl.
+set tmp := \rmax_(_ <- _ | _) _.
+rewrite /tmp.
+under [in X in _ = X -> _]eq_bigr do rewrite ffunE.
+move=> H.
 evar (h : 'rV[A]_n -> R); rewrite (eq_bigr h) in H; last first.
-  by move=> v vC; rewrite ffunE /h; reflexivity.
+  by move=> v vC; rewrite /h; reflexivity.
 rewrite -bigmaxR_distrl in H; last first.
   apply/invR_ge0; rewrite ltR_neqAle; split.
-    apply/eqP; by rewrite eq_sym -receivableE Receivable.defE.
-  exact/PosteriorProbability.den_ge0.
-move: H.
-rewrite {2 3}/P.
-case => [m' [Hm' H]].
+    apply/eqP; by rewrite eq_sym -receivable_propE receivableP.
+  exact/fdist_post_prob_den_ge0.
+rewrite {2 3}/P in H.
 set r := index_enum _ in H.
-rewrite (eq_bigr (fun i => 1 / INR #|[set cw in C]| * W ``(tb | i))) in H; last first.
-  move=> i iC; by rewrite fdist_uniform_supp_in // inE.
+move: H.
+under [in X in _ = X -> _]eq_bigr.
+  move=> i iC.
+  rewrite fdist_uniform_supp_in; last by rewrite inE.
+  over.
+move=> H.
 rewrite -bigmaxR_distrr in H; last exact/ltRW/Hunpos.
-exists m'; split; first exact Hm'.
-rewrite /PosteriorProbability.f ffunE in H.
-set x := PosteriorProbability.den _ in H.
-have x0 : / x <> 0 by apply/eqP/invR_neq0'; rewrite -receivableE Receivable.defE.
+exists m; split; first exact tbm.
+rewrite ffunE in H.
+set x := (X in _ * _ / X) in H.
+have x0 : / x <> 0 by apply/eqP/invR_neq0'; rewrite -receivable_propE receivableP.
 move/(eqR_mul2r x0) in H.
 rewrite /= fdist_uniform_supp_in ?inE // in H; last first.
   move/subsetP : dec_img; apply.
-  by rewrite inE; apply/existsP; exists (Receivable.y tb); apply/eqP.
+  by rewrite inE; apply/existsP; exists (receivable_rV tb); apply/eqP.
 by move/eqR_mul2l :  H => -> //; exact/eqP/gtR_eqF.
 Qed.
 
 End MAP_decoding_prop.
 
 Section MPM_decoding.
-
 (* in the special case of a binary code... *)
 Variable W : `Ch('F_2, [finType of 'F_2]).
 Variable n : nat.

ecc_modern/checksum.v

@@ -176,12 +176,12 @@ Hypothesis HC : 0 < #| [set cw in C] |.
 Local Open Scope proba_scope.
 Variable y : (`U HC).-receivable W.
 
-Lemma post_proba_uniform_checksubsum (x : 'rV['F_2]_n) :
+Lemma post_prob_uniform_checksubsum (x : 'rV['F_2]_n) :
   (`U HC) `^^ W (x | y) =
-    (PosteriorProbability.Kppu [set cw in C] y *
+    (post_prob_uniform_cst [set cw in C] y *
      (\prod_m0 (\delta ('V m0) x))%:R * W ``(y | x))%R.
 Proof.
-rewrite PosteriorProbability.uniform_kernel; congr (_ * _ * _)%R.
+rewrite post_prob_uniform_kernel; congr (_ * _ * _)%R.
 by rewrite big_morph_natRM checksubsum_in_kernel inE mem_kernel_syndrome0.
 Qed.
 

ecc_modern/ldpc.v

@@ -84,22 +84,20 @@ Local Open Scope vec_ext_scope.
 
 (* TODO: move to the file on bsc? *)
 Section post_proba_bsc_unif.
-
 Variable A : finType.
 Hypothesis card_A : #|A| = 2%nat.
 Variable p : R.
 Hypothesis p_01' : 0 < p < 1.
 Let p_01 := Eval hnf in Prob.mk_ (ltR2W p_01').
 Let P := fdist_uniform card_A.
 Variable a' : A.
-Hypothesis Ha' : Receivable.def (P `^ 1) (BSC.c card_A p_01) (\row_(i < 1) a').
+Hypothesis Ha' : receivable_prop (P `^ 1) (BSC.c card_A p_01) (\row_(i < 1) a').
 
 Lemma bsc_post (a : A) :
-  (P `^ 1) `^^ (BSC.c card_A p_01) (\row_(i < 1) a | Receivable.mk Ha') =
+  (P `^ 1) `^^ (BSC.c card_A p_01) (\row_(i < 1) a | mkReceivable Ha') =
   (if a == a' then 1 - p else p)%R.
 Proof.
-rewrite PosteriorProbability.dE /= /PosteriorProbability.den /=.
-rewrite !fdist_rVE DMCE big_ord_recl big_ord0.
+rewrite fdist_post_probE /= !fdist_rVE DMCE big_ord_recl big_ord0.
 rewrite (eq_bigr (fun x : 'M_1 => P a * (BSC.c card_A p_01) ``( (\row__ a') | x))%R); last first.
   by move=> i _; rewrite /P !fdist_rVE big_ord_recl big_ord0 !fdist_uniformE mulR1.
 rewrite -big_distrr /= (_ : \sum_(_ | _) _ = 1)%R; last first.
@@ -450,18 +448,18 @@ Local Open Scope R_scope.
 Lemma estimation_correctness (d : 'rV_n) n0 :
   let b := d ``_ n0 in let P := `U C_not_empty in
   P '_ n0 `^^ W (b | y) =
-    MarginalPostProbability.Kmpp y * PosteriorProbability.Kppu [set cw in C] y *
+    marginal_post_prob_den y * post_prob_uniform_cst [set cw in C] y *
     W `(y ``_ n0 | b) * \prod_(m0 in 'F n0) alpha m0 n0 d.
 Proof.
 move=> b P.
-rewrite MarginalPostProbability.probaE -2!mulRA; congr (_ * _).
-transitivity (PosteriorProbability.Kppu [set cw in C] y *
+rewrite fdist_marginal_post_probE -2!mulRA; congr (_ * _).
+transitivity (post_prob_uniform_cst [set cw in C] y *
               (\sum_(x = d [~ setT :\ n0])
                 W ``(y | x) * \prod_(m0 < m) (\delta ('V m0) x)%:R))%R.
   rewrite [RHS]big_distrr [in RHS]/=.
   apply eq_big => t; first by rewrite -freeon_all.
   rewrite inE andTb => td_n0.
-  rewrite PosteriorProbability.uniform_kernel -mulRA; congr (_ * _)%R.
+  rewrite post_prob_uniform_kernel -mulRA; congr (_ * _)%R.
   rewrite mulRC; congr (_ * _)%R.
   by rewrite checksubsum_in_kernel inE mem_kernel_syndrome0.
 congr (_ * _)%R.
@@ -480,7 +478,8 @@ transitivity (
     \prod_(m0 in 'F n0) \prod_(m1 in 'F(m0, n0)) (\delta ('V m1) x)%:R).
   apply eq_bigr => /= t Ht.
   congr (_ * _)%R.
-  by rewrite -(rprod_Fgraph_part_fnode (Tanner.connected tanner) (Tanner.acyclic tanner) (fun m0 => (\delta ('V m0) t)%:R)).
+  by rewrite -(rprod_Fgraph_part_fnode (Tanner.connected tanner) (Tanner.acyclic tanner)
+      (fun m0 => (\delta ('V m0) t)%:R)).
 transitivity (
   \sum_(x = d [~ setT :\ n0]) \prod_(m0 in 'F n0)
     (W ``(y # 'V(m0, n0) :\ n0 | x # 'V(m0, n0) :\ n0) *
@@ -498,38 +497,36 @@ Definition K949 (n0 : 'I_n) df := /
     W Zp1 (y ``_ n0) * \prod_(m1 in 'F n0) alpha m1 n0 (df `[ n0 := Zp1 ])).
 
 Lemma K949_lemma df n0 : K949 n0 df =
-  MarginalPostProbability.Kmpp y * PosteriorProbability.Kppu [set cw in C] y.
+  marginal_post_prob_den y * post_prob_uniform_cst [set cw in C] y.
 Proof.
-rewrite /K949 /MarginalPostProbability.Kmpp /PosteriorProbability.Kppu -invRM; last 2 first.
+rewrite /K949 /marginal_post_prob_den /post_prob_uniform_cst -invRM; last 2 first.
   apply/eqP; rewrite FDist.f1 => ?; lra.
-  by rewrite -not_receivable_uniformE Receivable.defE.
+  by rewrite -not_receivable_prop_uniform receivableP.
 congr (/ _).
 transitivity (\sum_(t in 'rV['F_2]_n)
   if t \in kernel H then W ``(y | t) else 0); last first.
   rewrite big_distrl /=.
   apply eq_bigr => /= t Ht.
   case: ifP => HtH.
-    rewrite PosteriorProbability.dE.
-    rewrite fdist_uniform_supp_in ?inE //.
-    rewrite /PosteriorProbability.den.
+    rewrite fdist_post_probE fdist_uniform_supp_in ?inE //.
     have HH : #|[set cw in kernel H]|%:R <> 0.
       apply/INR_eq0/eqP.
       rewrite cards_eq0.
-      apply/set0Pn; exists t; by rewrite inE.
+      by apply/set0Pn; exists t; rewrite inE.
     rewrite -(mulRC (W ``(y | t))) -[X in X = _]mulR1.
     rewrite -!mulRA.
     congr (_ * _).
     rewrite mul1R fdist_uniform_supp_restrict /= fdist_uniform_supp_distrr /=; last first.
     rewrite invRM; last 2 first.
       exact/eqP/invR_neq0.
       rewrite (eq_bigl (fun x => x \in [set cw in C])); last by move=> i; rewrite inE.
-      by rewrite -not_receivable_uniformE Receivable.defE.
+      by rewrite -not_receivable_prop_uniform receivableP.
     rewrite invRK //; last  exact/eqP.
     rewrite -mulRA mulRC mulVR ?mulR1 ?mulRV //; first by exact/eqP.
     set tmp1 := \sum_(_ | _) _.
     rewrite /tmp1 (eq_bigl (fun x => x \in [set cw in C])); last by move=> i; rewrite inE.
-    by rewrite -not_receivable_uniformE Receivable.defE.
-  rewrite PosteriorProbability.dE fdist_uniform_supp_notin; last by rewrite inE; exact/negbT.
+    by rewrite -not_receivable_prop_uniform receivableP.
+  rewrite fdist_post_probE fdist_uniform_supp_notin; last by rewrite inE; exact/negbT.
   by rewrite !(mul0R,div0R).
 rewrite -big_mkcond /=.
 rewrite /alpha.
@@ -544,9 +541,11 @@ transitivity (W Zp0 (y ``_ n0) *
       (W ``(y # 'V(m1, n0) :\ n0 | ta # 'V(m1, n0) :\ n0) *
       (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) ta)%:R)))).
   congr (_ * _ + _ * _).
-    rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y (fun m x y => W ``(x | y))) // => m1 m0 t Hm1 tdf.
+    rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y
+             (fun m x y => W ``(x | y))) // => m1 m0 t Hm1 tdf.
     by rewrite checksubsum_dprojs_V.
-  rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y (fun m x y => W ``(x | y))) // => m1 m0 t Hm1 tdf.
+  rewrite (rmul_rsum_commute0 (Tanner.connected tanner) (Tanner.acyclic tanner) y
+           (fun m x y => W ``(x | y))) // => m1 m0 t Hm1 tdf.
   by rewrite checksubsum_dprojs_V.
 transitivity (\sum_(ta : 'rV_n) W (ta ``_ n0) (y ``_ n0) *
     \prod_(m1 in 'F n0)

information_theory/binary_symmetric_channel.v

@@ -20,6 +20,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
+Local Open Scope fdist_scope.
 Local Open Scope channel_scope.
 Local Open Scope R_scope.
 
@@ -34,7 +35,6 @@ Definition c : `Ch(A, A) := fdist_binary card_A p.
 End BSC_sect.
 End BSC.
 
-Local Open Scope channel_scope.
 Local Open Scope entropy_scope.
 
 Section bsc_capacity_proof.
@@ -48,10 +48,10 @@ Let p_01 : prob := Eval hnf in Prob.mk_ (ltR2W p_01').
 Lemma HP_HPW : `H P - `H(P, BSC.c card_A p_01) = - H2 p.
 Proof.
 rewrite {2}/entropy /=.
-rewrite (eq_bigr (fun a => (`J( P, (BSC.c card_A p_01))) (a.1, a.2) *
-  log ((`J( P, (BSC.c card_A p_01))) (a.1, a.2)))); last by case.
-rewrite -(pair_big xpredT xpredT (fun a b => (`J( P, (BSC.c card_A p_01)))
-  (a, b) * log ((`J( P, (BSC.c card_A p_01))) (a, b)))) /=.
+rewrite (eq_bigr (fun a => ((P `X (BSC.c card_A p_01))) (a.1, a.2) *
+  log (((P `X (BSC.c card_A p_01))) (a.1, a.2)))); last by case.
+rewrite -(pair_big xpredT xpredT (fun a b => (P `X (BSC.c card_A p_01))
+  (a, b) * log ((P `X (BSC.c card_A p_01)) (a, b)))) /=.
 rewrite {1}/entropy .
 set a := \sum_(_ in _) _. set b := \sum_(_ <- _) _.
 apply trans_eq with (- (a + (-1) * b)); first by field.
@@ -86,7 +86,7 @@ transitivity (p * (P a + P b) * log p + (1 - p) * (P a + P b) * log (1 - p) ).
 by move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b => ->; rewrite /log; field.
 Qed.
 
-Lemma IPW : `I(P; BSC.c card_A p_01) = `H(P `o BSC.c card_A p_01) - H2 p.
+Lemma IPW : `I(P, BSC.c card_A p_01) = `H(P `o BSC.c card_A p_01) - H2 p.
 Proof.
 rewrite /mutual_info_chan addRC.
 set a := `H(_ `o _).
@@ -136,8 +136,8 @@ apply: (@leR_trans (H2 q)); last exact: H2_max.
 by rewrite /H2 !mulNR; apply Req_le; field.
 Qed.
 
-Lemma bsc_out_H_half' : 0 < INR 1 / INR 2 < 1.
-Proof. by rewrite /= (_ : INR 1 = 1) // (_ : INR 2 = 2) //; lra. Qed.
+Lemma bsc_out_H_half' : 0 < 1%:R / 2%:R < 1.
+Proof. by rewrite /= (_ : 1%:R = 1) // (_ : 2%:R = 2) //; lra. Qed.
 
 Lemma H_out_binary_uniform : `H(fdist_uniform card_A `o BSC.c card_A p_01) = 1.
 Proof.
@@ -167,7 +167,7 @@ set p' := Prob.mk_ (ltR2W p_01').
 have has_sup_E : has_sup E.
   split.
     set d := fdist_binary card_A p' (Set2.a card_A).
-    by exists (`I(d; BSC.c card_A p')), d.
+    by exists (`I(d, BSC.c card_A p')), d.
   exists 1 => y [P _ <-{y}].
   rewrite IPW; apply/RleP/leR_subl_addr/(leR_trans (H_out_max card_A P p_01')).
   rewrite addRC -leR_subl_addr subRR.