fixes #122

Author: affeldt-aist

ecc_modern/ldpc_algo.v

@@ -203,7 +203,7 @@ Extract Constant Rmult => "( *.)".
 Extract Constant Rplus => "(+.)".
 Extract Constant Rinv  => "fun x -> 1. /. x".
 Extract Constant Ropp  => "(~-.)".
-(*Extraction "extraction/sumprod.ml" sumprod estimation.*)
+Extraction "extraction/sumprod.ml" sumprod estimation.
 
 Section ToGraph.
 

information_theory/channel_code.v

@@ -73,7 +73,7 @@ Proof.
 rewrite /CodeErrRate div1R.
 apply/RleP/ (@leR_pmul2l (INR #|M|)); first exact/ltR0n.
 rewrite mulRA mulRV ?INR_eq0' -?lt0n // mul1R -iter_addR -big_const.
-by apply: leR_sumR => m _; exact: Pr_1.
+by apply: leR_sumR => m _; exact: Pr_le1.
 Qed.
 
 Definition scha (W : `Ch(A, B)) (c : code) := (1 - echa(W , c))%R.

information_theory/channel_coding_direct.v

@@ -734,7 +734,7 @@ apply (@leR_ltR_trans
     move: (preimC_Cal_E epsilon0 i tb); by rewrite inE.
   apply (@leR_trans (Pr (W ``(| i ord0)) (~: Cal_E i ord0) +
     Pr (W ``(| i ord0)) (\bigcup_(i0 | i0 != ord0) (Cal_E i i0)))%R).
-    exact: Pr_union.
+    exact: le_Pr_setU.
   exact/leR_add2l/Pr_bigcup.
 rewrite first_summand //.
 set lhs := (\sum_(_ < _ | _) _)%R.
@@ -756,7 +756,7 @@ rewrite card_ord /=.
 apply (@leR_ltR_trans (epsilon0 + k%:R *
    Pr P `^ n `x (`O(P , W)) `^ n [set x | prod_rV x \in `JTS P W n epsilon0])%R).
   apply leR_add2r.
-  rewrite Pr_of_cplt leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //.
+  rewrite Pr_setC leR_subl_addr addRC -leR_subl_addr; apply/JTS_1 => //.
   by case: Hepsilon0.
   by case: Hn => _ [_ []].
 apply (@leR_ltR_trans (epsilon0 +

information_theory/entropy.v

@@ -490,8 +490,8 @@ rewrite fdistXE fdist_proj13E big_distrl /= -big_split; apply eq_bigr => b _ /=.
 rewrite !(fdistXE,fdistAE,fdistC12E) /= -mulRDr.
 have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R.
 rewrite -logM; last 2 first.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1 fdistAE /= fdistC12E.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1 fdistAE /= fdistC12E.
 congr (_ * log _).
 by rewrite -setX1 product_ruleC !setX1 mulRC.
 Qed.
@@ -570,7 +570,7 @@ transitivity (- (\sum_(a in A) \sum_(b in B) PQ (a, b) * log (P a)) +
   rewrite addRC -mulRN -mulRDr addR_opp.
   have [->|H0] := eqVneq (PQ (a, b)) 0; first by rewrite !mul0R.
   congr (_ * _); rewrite logDiv //.
-  - by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1.
+  - by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1.
   - by apply/RltP; rewrite -fdist_gt0; exact: dom_by_fdist_fstN H0.
 rewrite -subR_opp; congr (_ - _).
 - rewrite /entropy; congr (- _); apply/eq_bigr => a _.
@@ -759,12 +759,12 @@ rewrite fdistXE fdistAE /= -mulRN -mulRDr.
 have [->|H0] := eqVneq (PQR (a, b, c)) 0; first by rewrite !mul0R.
 congr (_ * _).
 rewrite addRC addR_opp -logDiv; last 2 first.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdistA_dominN H0.
-  by rewrite -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdistA_dominN H0.
+  by rewrite -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0.
 congr (log _).
 rewrite divRM; last 2 first.
-  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj13_dominN H0.
-  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0 setX1 Pr_set1; exact: fdist_proj23_dominN H0.
+  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj13_dominN H0.
+  by rewrite -jcPr_gt0 -Pr_jcPr_gt0 Pr_gt0P setX1 Pr_set1; exact: fdist_proj23_dominN H0.
 rewrite {2}/Rdiv -mulRA mulRCA {1}/Rdiv [in LHS]mulRC; congr (_ * _).
 rewrite -[in X in _ = X * _]setX1 jproduct_rule_cond setX1 -mulRA mulRV ?mulR1 //.
 rewrite /jcPr divR_neq0' // ?setX1 !Pr_set1.

information_theory/joint_typ_seq.v

@@ -130,7 +130,7 @@ have : (JTS_1_bound <= n)%nat ->
     have : 1 <= 3 by lra.
     move/(set_typ_seq_incl P m (ltRW He)) => Hincl.
     rewrite (Pr_DMC_fst P W (fun x => x \notin `TS P m epsilon)).
-    apply/Pr_incl/subsetP => i /=; rewrite !inE.
+    apply/subset_Pr/subsetP => i /=; rewrite !inE.
     apply contra.
     by move/subsetP : Hincl => /(_ i); rewrite !inE.
   have {H1}HnP : forall n, ('| up (aep_bound P (epsilon / 3)) | <= n)%nat ->
@@ -159,7 +159,7 @@ have : (JTS_1_bound <= n)%nat ->
     have : 1 <= 3 by lra.
     move/(set_typ_seq_incl (`O(P , W)) m (ltRW He)) => Hincl.
     rewrite Pr_DMC_out.
-    apply/Pr_incl/subsetP => i /=; rewrite !inE.
+    apply/subset_Pr/subsetP => i /=; rewrite !inE.
     apply contra.
     move/subsetP : Hincl => /(_ i).
     by rewrite !inE.
@@ -187,7 +187,7 @@ have : (JTS_1_bound <= n)%nat ->
     Pr (((P `X W) ) `^ m) (~: `TS ((P `X W)) m (epsilon / 3)).
     have : 1 <= 3 by lra.
     move/(set_typ_seq_incl ((P `X W)) m (ltRW He)) => Hincl.
-    apply/Pr_incl/subsetP => /= v; rewrite !inE.
+    apply/subset_Pr/subsetP => /= v; rewrite !inE.
     apply contra.
     by move/subsetP : Hincl => /(_ v); by rewrite !inE.
   have {H1}HnP_W m : ('| up (aep_bound ((P `X W)) (epsilon / 3)) | <= m)%nat ->
@@ -229,8 +229,8 @@ apply (@leR_trans (
  Pr ((P `X W) `^ n) [set x | (rV_prod x).1 \notin `TS P n epsilon] +
  Pr ((P `X W) `^ n) ([set x | ((rV_prod x).2 \notin `TS (`O( P , W)) n epsilon)] :|:
                       (~: `TS ((P `X W)) n epsilon)))).
-  exact: Pr_union.
-rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (Pr_union _ _ _).
+  exact: le_Pr_setU.
+rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (le_Pr_setU _ _ _).
 by apply/Req_le; congr Pr; apply/setP => t; rewrite !inE rV_prodK.
 Qed.
 

information_theory/jtypes.v

@@ -252,13 +252,13 @@ by move=> a b; rewrite ffunE.
 Defined.
 
 Definition jtype_enum A B n := pmap (@jtype_enum_f A B n)
-  (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat}]).
+  (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} | (\sum_(a in A) \sum_(b in B) f a b == n)%nat})).
 
 Lemma jtype_enumP A B n : Finite.axiom (@jtype_enum A B n).
 Proof.
 case=> d f Hf H /=.
-have : Finite.axiom (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}}  |
-    (\sum_(a in A) \sum_(b in B) f a b == n)%nat }]).
+have : Finite.axiom (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}}  |
+    (\sum_(a in A) \sum_(b in B) f a b == n)%nat })).
   rewrite enumT; by apply enumP.
 move/(_ (@exist _ _ f Hf)) => <-.
 rewrite /jtype_enum /=.
@@ -291,8 +291,8 @@ eq_ind_r
                                               else
                                                 (sval f a b)%:R /
                                                     (\sum_(b0 in B) (sval f a) b0)%:R)*) |}
-                     ) (enum [finType of { f : {ffun A -> {ffun B -> 'I_n.+1}} |
-                                           (\sum_(a in A) \sum_(b in B) f a b)%nat == n}]).
+                     ) (enum (Finite.clone _ { f : {ffun A -> {ffun B -> 'I_n.+1}} |
+                                           (\sum_(a in A) \sum_(b in B) f a b)%nat == n})).
   apply: eq_pmap => V.
   destruct Sumbool.sumbool_of_bool; last by rewrite Anot0 in e.
   destruct Sumbool.sumbool_of_bool; last by rewrite Bnot0 in e0.
@@ -357,13 +357,13 @@ move=> Anot0 Bnot0.
 move: (Anot0); case/card_gt0P => a _.
 move: (Bnot0); case/card_gt0P => b _.
 apply/card_gt0P.
-have [tmp Htmp] : [finType of {f : {ffun A -> {ffun B -> 'I_n.+1}} |
-                     \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}].
+have [tmp Htmp] : {f : {ffun A -> {ffun B -> 'I_n.+1}} |
+                     \sum_(a1 in A) \sum_(b1 in B) f a1 b1 == n}.
   exists [ffun a1 => [ffun b1 => if (a1, b1) == (a, b) then
     Ordinal (ltnSn n) else Ordinal (ltn0Sn n)]].
   rewrite pair_big /=.
   rewrite (bigD1 (a, b)) //= big1 ; first by rewrite 2!ffunE eqxx addn0.
-  move=> p /negbTE Hp ; by rewrite 2!ffunE -surjective_pairing Hp.
+  by move=> p /negbTE Hp ; rewrite 2!ffunE -surjective_pairing Hp.
 have Htmp' : (forall a b,
         (chan_of_jtype Anot0 Bnot0 tmp) a b =
         (let ln := \sum_(b0 in B) (tmp a) b0 in

information_theory/source_coding_vl_converse.v

@@ -689,9 +689,9 @@ Proof.
 pose m' := m.-1.
 have mpos : m = m'.+1.
   rewrite prednK // -ltR_nat ltR_neqAle; split => //; exact/leR0n.
-have: (@extension [finType of 'rV[A]_n] _ f) \o
+have: (@extension 'rV[A]_n _ f) \o
       (flatten \o map (fun x => @tval m _ (tuple_of_row x))) =1
-      @extension [finType of {: 'rV[ 'rV[A]_n ]_m} ] _ fm.
+      @extension {: 'rV[ 'rV[A]_n ]_m} _ fm.
    by elim => //= ta sta; rewrite /extension /= map_cat flatten_cat => <-.
 apply: eq_inj.
 apply: inj_comp => //.

information_theory/typ_seq.v

@@ -237,7 +237,7 @@ Lemma TS_inf : aep_bound P epsilon <= n.+1%:R ->
 Proof.
 move=> k0_k.
 have H1 : (1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon) <= 1)%mcR.
-  by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_1].
+  by apply/andP; split; apply/RleP; [exact: Pr_TS_1 | exact: Pr_le1].
 have H2 : (forall x, x \in `TS P n.+1 epsilon ->
     exp2 (- n.+1%:R * (`H P + epsilon)) <=
     P `^ n.+1 x <= exp2 (- n.+1%:R * (`H P - epsilon)))%mcR.

information_theory/types.v

@@ -473,10 +473,11 @@ case/boolP : [exists x, x \in T_{P}] => x_T_P.
   rewrite -(row_of_tupleK ta) in Hta.
   rewrite -(tuple_dist_type_entropy Hta).
   rewrite [X in X <= _](_ : _ = Pr (type.d P) `^ n (@row_of_tuple A n @: T_{P})).
-    by apply Pr_1.
+    exact: Pr_le1.
   symmetry.
   rewrite /Pr.
-  transitivity (\sum_(a| (a \in [finType of 'rV[A]_n]) && [pred x in (@row_of_tuple A n @: T_{P})] a)
+  transitivity (\sum_(a | (a \in [finType of 'rV[A]_n]) &&
+                          [pred x in (@row_of_tuple A n @: T_{P})] a)
       exp2 (- INR n * `H P)).
     apply eq_big => // ta'/= Hta'.
     rewrite -(@tuple_dist_type_entropy ta') //.

probability/bayes.v

@@ -421,10 +421,10 @@ split.
       case ac: (a == c).
         rewrite -(eqP ac); exact.
       move=> _ _ _.
-      rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+      rewrite (proj2 (cPr_eq0P _ _ _)); last first.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ac.
-      rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+      rewrite (proj2 (cPr_eq0P _ _ _)); last first.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /= /eqP ->; rewrite ac.
       by rewrite mul0R.
@@ -441,7 +441,7 @@ split.
       set x := (X in X = X * X).
       move/Rxx2 => [] Hx.
         rewrite -/x Hx.
-        rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //.
+        rewrite (proj2 (cPr_eq0P _ _ _)) ?mul0R //.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /andP [] /= /eqP ->; rewrite ab.
       rewrite /cPr.
@@ -459,17 +459,17 @@ split.
       move/eqP in Hden.
       rewrite /cPr /Rdiv -mulRA mulVR // mulR1 mul1R.
       move/(f_equal (Rminus den)).
-      rewrite subRR setIC -Pr_diff => /Pr_set0P/(_ u).
-      rewrite !inE (eqP Hi) Hk eq_sym ab; exact.
+      rewrite subRR setIC -Pr_setD => /Pr_set0P/(_ u).
+      by rewrite !inE (eqP Hi) Hk eq_sym ab; exact.
     case: (ord_eq_dec k j).
       move=> <- {j} ik b.
       case bc: (b == c).
         rewrite (eqP bc); exact.
       move=> _ _ _.
-      rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+      rewrite (proj2 (cPr_eq0P _ _ _)); last first.
         apply/Pr_set0P => u.
         by rewrite !inE => /andP [] /andP [] _ /= /eqP ->; rewrite bc.
-      rewrite mulRC (proj2 (cPr_eq0 _ _ _)) ?mul0R //.
+      rewrite mulRC (proj2 (cPr_eq0P _ _ _)) ?mul0R //.
       by apply/Pr_set0P => u; rewrite !inE => /andP [] /= /eqP ->; rewrite bc.
     move=> nkj nij b HG Hvals; apply: HG => //.
     by rewrite Hvals set_val_tl // set_val_tl // set_val_hd.
@@ -631,10 +631,10 @@ case /boolP: [forall i in (e :&: g), _].
 rewrite negb_forall => /existsP [i].
 rewrite inE negb_imply => /andP [] /andP [Hie Hig] /eqP Hvi.
 right; rewrite /cinde_events.
-rewrite (proj2 (cPr_eq0 _ _ _)); last first.
+rewrite (proj2 (cPr_eq0P _ _ _)); last first.
   apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi.
   case/andP: Hprod => /andP[] /eqP <- _ /eqP <-; exact: prod_vars_inter.
-rewrite (proj2 (cPr_eq0 _ _ _)) ?mul0R //.
+rewrite (proj2 (cPr_eq0P _ _ _)) ?mul0R //.
 apply/Pr_set0P => u; rewrite !inE => Hprod; elim: Hvi.
 case/andP: Hprod => /eqP <- /eqP <-; exact: prod_vars_inter.
 Qed.
@@ -664,7 +664,7 @@ rewrite (proj2 (Pr_set0P _ _)); last first.
 suff : `Pr_P[finset (prod_vars f @^-1 B) | finset (prod_vars g @^-1 C)] = 0.
   by rewrite /cPr => ->; rewrite mulR0 div0R.
 (* prove incompatibility between B and C *)
-apply/cPr_eq0/Pr_set0P => u.
+apply/cPr_eq0P/Pr_set0P => u.
 rewrite !inE => /andP [] /eqP HB /eqP HC.
 move: Hnum; rewrite /den.
 have -> : g = (e :&: f :|: g) :\: ((e :&: f) :\: g).
@@ -745,7 +745,7 @@ split.
   rewrite negb_imply /vals => /andP [Hif].
   case /boolP: (i \in g) => Hig.
     (* B and C are incompatible *)
-    move: (Hfg i); by rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->.
+    by move: (Hfg i); rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->.
   case /boolP: (i \in e) => Hie;
     last by rewrite set_vals_tl // set_vals_tl // eqxx.
   (* A and B are incompatible *)
@@ -756,7 +756,7 @@ split.
   rewrite {1}/cinde_events -!preim_vars_inter setUid /=.
   case/Rxx2.
     (* cPr = 0 *)
-    move/cPr_eq0/Pr_set0P => Hx.
+    move/cPr_eq0P/Pr_set0P => Hx.
     have HAC :
       Pr P (finset (prod_vars e @^-1 A) :&: finset (prod_vars g @^-1 C)) = 0.
       apply Pr_set0P => u Hu; apply Hx.
@@ -767,8 +767,8 @@ split.
         by rewrite set_vals_prod_vars.
       case/boolP: (j \in e) => // je.
       by rewrite set_vals_tl // set_vals_prod_vars.
-    rewrite /cinde_events (proj2 (cPr_eq0 _ _ _)).
-      by rewrite (proj2 (cPr_eq0 _ _ _)) // mul0R.
+    rewrite /cinde_events (proj2 (cPr_eq0P _ _ _)).
+      by rewrite (proj2 (cPr_eq0P _ _ _)) // mul0R.
     apply/Pr_set0P => u Hu.
     apply(proj1 (Pr_set0P _ _) HAC).
     move: Hu; by rewrite !inE => /andP[] /andP[] -> _ ->.

probability/jfdist_cond.v

@@ -20,7 +20,7 @@ Require Import fdist proba.
 (*      jfdist_cond PQ a == The conditional distribution derived from PQ      *)
 (*                          given a; same as fdist_cond0 when                 *)
 (*                          fdist_fst PQ a != 0.                              *)
-(*           PQ `(| a |) == notation jfdist_cond PQ a                         *)
+(*            PQ `(| a ) == notation jfdist_cond PQ a                         *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -59,10 +59,10 @@ Lemma jcPr_ge0 E F : 0 <= \Pr_[E | F].
 Proof. by rewrite jcPrE. Qed.
 
 Lemma jcPr_le1 E F : \Pr_[E | F] <= 1.
-Proof. by rewrite jcPrE; exact: cPr_max. Qed.
+Proof. by rewrite jcPrE; exact: cPr_le1. Qed.
 
 Lemma jcPr_gt0 E F : 0 < \Pr_[E | F] <-> \Pr_[E | F] != 0.
-Proof. by rewrite !jcPrE; apply cPr_gt0. Qed.
+Proof. by rewrite !jcPrE; apply cPr_gt0P. Qed.
 
 Lemma Pr_jcPr_gt0 E F : 0 < Pr P (E `* F) <-> 0 < \Pr_[E | F].
 Proof.
@@ -73,11 +73,13 @@ split.
   by apply/Pr_cPr_gt0; move: H; rewrite jcPrE -setTE -EsetT.
 Qed.
 
+(* TODO: rename *)
 Lemma jcPr_cplt E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F].
 Proof.
 by move=> PF0; rewrite 2!jcPrE EsetT setCX cPr_cplt ?EsetT // setTE Pr_setTX.
 Qed.
 
+(* TODO: rename *)
 Lemma jcPr_diff E1 E2 F : \Pr_[E1 :\: E2 | F] = \Pr_[E1 | F] - \Pr_[E1 :&: E2 | F].
 Proof.
 rewrite jcPrE DsetT cPr_diff jcPrE; congr (_ - _).