diff --git a/.travis.yml b/.travis.yml index 14ec9529..dc93d653 100644 --- a/.travis.yml +++ b/.travis.yml @@ -14,7 +14,7 @@ env: - NJOBS="2" - CONTRIB_NAME="infotheo" matrix: - - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.10" + - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11" install: | # Prepare the COQ container diff --git a/README.org b/README.org index 7d601bad..373ae0f6 100644 --- a/README.org +++ b/README.org @@ -13,16 +13,16 @@ *** Last stable version: -Version 0.1: +Version 0.1.1: 3. ~opam install coq-infotheo~ **** Requirements -- [[https://coq.inria.fr][Coq]] 8.10.2 or 8.11 -- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.10.0 -- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.2.3 +- [[https://coq.inria.fr][Coq]] 8.11 +- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.11.0 +- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.3.1 which requires - + [[https://github.com/math-comp/finmap][finmap]] 1.2.0 or greater + + [[https://github.com/math-comp/finmap][finmap]] 1.5.0 or greater All versions available from opam. diff --git a/_CoqProject b/_CoqProject index 3dff40b5..cb52d9be 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,7 +18,6 @@ lib/natbin.v lib/binary_entropy_function.v lib/num_occ.v lib/hamming.v -lib/arg_rmax.v lib/poly_ext.v lib/euclid.v lib/dft.v @@ -93,4 +92,5 @@ toy_examples/expected_value_variance.v toy_examples/expected_value_variance_ordn.v toy_examples/expected_value_variance_tuple.v toy_examples/conditional_entropy.v + -R . infotheo diff --git a/changelog.txt b/changelog.txt index 0e6338eb..ab96d4d2 100644 --- a/changelog.txt +++ b/changelog.txt @@ -1,13 +1,25 @@ ------------------- -from 0.0.7 to ??? : +from 0.1 to 0.1.1 : ------------------- +added: +- order canonical structures in ssrR.v renamings: - imageA -> image_comp (deprecated) - image_idfun -> image_id (deprecated) +- bigcup0 -> bigcup_set0 +- bigcup1 -> bigcup_set1 +- bigcup_set1 -> bigcup_of_singletons +- bigcup_const -> bigcup_of_const - altConvType -> naryConvType added: - <&>_ notation for the operator of naryContType + _ <& _ &> _ for its binary version +removed: +- Lemma to_bivar_entropy (redundant with entropy_to_bivar) +- file arg_rmax.v +replaced: +- custom arg_rmax with new order.v's [arg max_(i > i0) F]%O + ------------------- from 0.0.7 to 0.1 : ------------------- diff --git a/ecc_classic/bch.v b/ecc_classic/bch.v index 39b6fac3..780b2c21 100644 --- a/ecc_classic/bch.v +++ b/ecc_classic/bch.v @@ -102,7 +102,7 @@ case/boolP : (odd j) => [odd_j|even_j]; last first. by rewrite (negbTE even_j) add0n => ->. move: (IH j.-1./2). rewrite -{1}divn2 leq_divLR; last first. - rewrite dvdn2 -subn1 odd_sub; last by destruct j. + rewrite dvdn2 -subn1 oddB; last by destruct j. by rewrite /= addbT odd_j. have -> : (j.-1 <= i * 2)%N. rewrite muln2 -addnn -subn1 leq_subLR addnA add1n (leq_trans ji) //. diff --git a/ecc_classic/decoding.v b/ecc_classic/decoding.v index 97a577ab..99cf4555 100644 --- a/ecc_classic/decoding.v +++ b/ecc_classic/decoding.v @@ -85,10 +85,10 @@ Proof. split => [H /= y x yx x' x'C | H /= y x yx]. - move: {H}(H _ _ yx) => H. rewrite dH_sym H dH_sym. - case: arg_minP; first by case: c_not_empty. + case: arg_minnP; first by case: c_not_empty. move=> /= i ic ij; by rewrite dH_sym (dH_sym x') ij. - move: {H}(H _ _ yx) => H. - case: arg_minP; first by case: c_not_empty. + case: arg_minnP; first by case: c_not_empty. move=> /= i Hi /(_ x) Ki. apply/eqP; rewrite eqn_leq; apply/andP; split. - by rewrite dH_sym (dH_sym y) H. diff --git a/ecc_classic/hamming_code.v b/ecc_classic/hamming_code.v index 18ba0935..6dbb6b84 100644 --- a/ecc_classic/hamming_code.v +++ b/ecc_classic/hamming_code.v @@ -331,13 +331,13 @@ have syndrome_not_0 : syndrome (Hamming.PCM m) y != 0. by rewrite /hamming_err syndrome_is_0 nat_of_rV_0 addr0 dHE subrr wH0. move=> dHy. suff : dH y x != O. - move: dHy; rewrite leq_eqVlt => /orP[/eqP //|]; by rewrite ltnS leqn0 => ->. + by move: dHy; rewrite leq_eqVlt => /orP[/eqP //|]; rewrite ltnS leqn0 => ->. apply/negP => abs. have : y = x by move: abs; rewrite dHE wH_eq0 subr_eq0 => /eqP. -rewrite /x; case: arg_minP => [|/=]; first by case: C_not_empty. +rewrite /x; case: arg_minnP => [|/=]; first by case: C_not_empty. move=> y' Hy' _ yy'; rewrite -{}yy' in Hy'. move/negP : syndrome_not_0; apply. -rewrite -mem_kernel_syndrome0; by rewrite inE in Hy'. +by rewrite -mem_kernel_syndrome0; rewrite inE in Hy'. Qed. Lemma hamming_repair_img : oimg hamming_repair \subset Hamming.code m. @@ -380,14 +380,14 @@ case Hi : (0 < wH i^T). exists (Ordinal H0) => //. apply/trmx_inj. rewrite col_matrix /= trmxK -{1}(nat_of_rVK i^T) subn1 prednK // lt0n nat_of_rV_eq0. - apply/eqP => abs; by rewrite abs lt0n wH0 eqxx in Hi. + by apply/eqP => abs; rewrite abs lt0n wH0 eqxx in Hi. apply/esym/negbTE; move/negbT : Hi; apply contra. case/imsetP => j Hj ->. case HwH : (wH (col j (Hamming.PCM m))^T); last by []. exfalso. move/eqP: HwH. rewrite col_matrix wH_eq0 trmxK => /eqP. -apply rV_of_nat_neq0 => //; by apply Hamming.len_two_m. +by apply rV_of_nat_neq0 => //; apply Hamming.len_two_m. Qed. Lemma col_PCM_inj : injective (fun i => col i (Hamming.PCM m)). @@ -421,7 +421,7 @@ case HwH : (wH i^T == _). rewrite !mxE /=. move/setP/(_ j): Hx. rewrite in_set1 in_set tnth_mktuple mxE => <-. - rewrite F2_eq1; by case: F2P. + by rewrite F2_eq1; case: F2P. apply/negbTE; move/negbT: HwH; apply contra. case/imsetP => x Hx ->. by apply/eqP/wH_col_1. @@ -431,7 +431,7 @@ Lemma cols_1_inj : injective (fun i => col i 1 : 'cV['F_2]_m). Proof. move=> i j /= /matrixP/(_ j 0). rewrite !mxE eqxx /=. -case Hji : (j == i) => // _. by apply/esym/eqP. +by case Hji : (j == i) => // _; apply/esym/eqP. Qed. Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1]. @@ -443,12 +443,12 @@ Proof. rewrite /non_unit_cols /unit_cols. transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1%nat]|. apply eq_card=> c; by rewrite !in_set orbC eq_sym -leq_eqVlt. -rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj. +by rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj. Qed. Lemma card_unit_cols : #|unit_cols| = m. Proof. -rewrite /unit_cols cols_1 card_imset; by [apply card_ord | apply cols_1_inj]. +by rewrite /unit_cols cols_1 card_imset; [apply card_ord | apply cols_1_inj]. Qed. Lemma card_non_unit : #|non_unit_cols| = (n - m)%nat. @@ -475,11 +475,11 @@ have Hin : col i 1 \in image (fun j => col j (Hamming.PCM m)) 'I_n. rewrite -cols_PCM inE. have : col i 1 \in [set c : 'cV['F_2]_m | wH c^T == 1%nat]. rewrite cols_1. - apply/imsetP; by exists i. + by apply/imsetP; exists i. by rewrite inE => /eqP ->. case/imsetP : Hi => j Hj Hj'. - exists j => //; by rewrite mem_enum. -exists (iinv Hin); by apply (f_iinv Hin). + by exists j => //; rewrite mem_enum. +by exists (iinv Hin); apply (f_iinv Hin). Defined. Definition ord_split (i : 'I_n) : 'I_(n - m + m) := @@ -509,7 +509,7 @@ have Hcols x : x \in non_unit_cols -> x \in [set col i (Hamming.PCM m) | i : 'I_ case Hc : (c \in non_unit_cols). apply/imsetP. case/imsetP: (Hcols _ Hc) => x Hx Hx'. - exists x => //; by rewrite inE -Hx'. + by exists x => //; rewrite inE -Hx'. apply/negbTE. move/negbT: Hc; apply contra. case/imsetP => x Hx Hx'. @@ -555,7 +555,7 @@ have Hij : i' = j'. apply cols_1_inj. by rewrite -(proj2_sig (ids1 i')) -(proj2_sig (ids1 j')) Htmp. rewrite Hij -Hj' /= in Hi'. -by apply val_inj. +exact: val_inj. Qed. Definition systematic : 'S_n := perm perm_ids_inj. @@ -576,7 +576,7 @@ case/boolP : (j < n - m) => Hcond. rewrite castmxE /=. rewrite /PCM 2!cast_ord_id. rewrite esymK [in X in _ = X]mxE. - congr (Hamming.PCM m _ (systematic _)); by apply val_inj. + by congr (Hamming.PCM m _ (systematic _)); exact: val_inj. rewrite [in X in _ = X]mxE. move: (splitP (cast_ord (esym (subnK (Hamming.dim_len m'))) j)) => [k Hk|k Hk]. have jk : j = k :> nat by []. @@ -901,9 +901,9 @@ move=> /= y c Hy c'. rewrite !(dH_sym _ y). move: (@hamming_MD_alt r' y c). move=> ->. -- case: arg_minP. +- case: arg_minnP. by destruct C_not_empty. - move => /= i Hi; by apply. + by move => /= i Hi; apply. - by rewrite -Hy /Decoder.repair /= /hamming_repair ffunE. Defined. diff --git a/ecc_classic/linearcode.v b/ecc_classic/linearcode.v index dc743672..2526793a 100644 --- a/ecc_classic/linearcode.v +++ b/ecc_classic/linearcode.v @@ -244,7 +244,7 @@ Proof. apply: sigW. case: C_not_trivial => g /andP[gC g0]. have := erefl [arg min_(g' < g | (g' \in C) && (g' != 0)) (size (rVpoly g'))]. -case: arg_minP => /=; [by apply/andP | move=> g']. +case: arg_minnP => /=; [by apply/andP | move=> g']. case/andP=> g'C g'0 g_min _. exists g'. rewrite /non0_codeword_lowest_deg g'C g'0 /= /codeword_lowest_deg. @@ -293,36 +293,34 @@ Proof. by rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial). Qed. Lemma wH_non_0_cw : wH non_0_cw != O. Proof. -rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial); by rewrite wH_eq0. +by rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial); rewrite wH_eq0. Qed. -Definition min_wH_cw := arg_min non_0_cw [pred cw | (cw \in C) && (wH cw != O)] (@wH F n). - -(*Definition min_wH_cw := arg_min non_0_cw [pred cw in C | wH cw != O] (@wH F n).*) +Definition min_wH_cw := + arg_min non_0_cw [pred cw | (cw \in C) && (wH cw != O)] (@wH F n). Definition min_dist := wH min_wH_cw. Lemma min_dist_is_min c : c \in C -> c != 0 -> min_dist <= wH c. Proof. -move=> cC c0. -rewrite /min_dist /min_wH_cw. -case: arg_minP => /= [|c1 /andP [] Hc1 wHc1]. +move=> cC c0; rewrite /min_dist /min_wH_cw. +case: arg_minnP => /= [|c1 /andP [] Hc1 wHc1]. by rewrite non_0_cw_mem wH_non_0_cw. -apply; by rewrite cC /= wH_eq0. +by apply; rewrite cC /= wH_eq0. Qed. Lemma min_dist_achieved : exists c, c \in C /\ c <> 0 /\ wH c = min_dist. Proof. exists min_wH_cw; split. rewrite /min_wH_cw /=. - case: arg_minP => /=. + case: arg_minnP => /=. by rewrite non_0_cw_mem wH_non_0_cw. by move=> /= c /andP[]. split; last reflexivity. rewrite /min_wH_cw /=. -case: arg_minP => /=. +case: arg_minnP => /=. by rewrite non_0_cw_mem wH_non_0_cw. -move=> /= c /andP[_ /negP]; by rewrite wH_eq0 => /negP/eqP. +by move=> /= c /andP[_ /negP]; rewrite wH_eq0 => /negP/eqP. Qed. Lemma min_dist_neq0 : min_dist <> O. @@ -339,7 +337,7 @@ Lemma min_distP d : Proof. case=> H1 [y [yC [y0 yd]]]. rewrite /min_dist /min_wH_cw. -case: arg_minP => /=. +case: arg_minnP => /=. by rewrite non_0_cw_mem wH_non_0_cw. move=> x /andP[xC x0] H. apply/eqP. @@ -371,7 +369,7 @@ move=> even_d. rewrite /mdd_err_cor (_ : min_dist.-1./2 = min_dist./2 - 1)%N //. move Hd : min_dist => d. case: d Hd even_d => //= d -> /=. -rewrite negbK uphalf_half => ->; by rewrite add1n subn1. +by rewrite negbK uphalf_half => ->; rewrite add1n subn1. Qed. Definition sbound_f' k (H : k.-1 <= n) := @@ -379,17 +377,17 @@ Definition sbound_f' k (H : k.-1 <= n) := Lemma sbound_f'Z k (H : k.-1 <= n) a y : sbound_f' H (a *: y) = a *: sbound_f' H y. -Proof. apply/rowP => i; by rewrite !mxE. Qed. +Proof. by apply/rowP => i; rewrite !mxE. Qed. Lemma sbound_f'D k (H : k.-1 <= n) y y' : sbound_f' H (y + y') = sbound_f' H y + sbound_f' H y'. Proof. by apply/rowP => i; rewrite !mxE. Qed. Lemma sbound_f'N k (H : k.-1 <= n) y : sbound_f' H (- y) = - sbound_f' H y. -Proof. apply/rowP => i; by rewrite !mxE. Qed. +Proof. by apply/rowP => i; rewrite !mxE. Qed. Lemma additive_sbound_f' k (H : k.-1 <= n) : additive (sbound_f' H). -Proof. move=> x y; by rewrite sbound_f'D sbound_f'N. Qed. +Proof. by move=> x y; rewrite sbound_f'D sbound_f'N. Qed. Definition sbound_f_linear k (H : k.-1 <= n) : {linear 'rV[F]_n -> 'rV[F]_k.-1} := @@ -439,9 +437,8 @@ have Kcw : wH cw <= n - k + 1. move/rowP => /= /(_ (Ordinal Hi)). rewrite !mxE /=. set x := widen_ord _ _. - suff -> : x = i. - by move/eqP. - by apply val_inj. + suff -> : x = i by move/eqP. + exact: val_inj. have X : forall i : 'I_n, ~~ (i < k.-1) -> (cw ord0 i != 0) <= 1. move=> i Hi. by case: (_ != _). @@ -471,8 +468,7 @@ have Kcw : wH cw <= n - k + 1. move: dimCn. by rewrite prednK // not_trivial_dim. by rewrite addn1. -apply: (leq_trans _ Kcw). -by apply min_dist_is_min. +exact/(leq_trans _ Kcw)/min_dist_is_min. Qed. Definition maximum_distance_separable := (min_dist == n - \dim C + 1)%N. @@ -502,7 +498,8 @@ have gk : size (rVpoly g) <= size (rVpoly k). - apply: contra j0. by rewrite /k subr_eq addrC -subr_eq subrr eq_sym. - rewrite /k; move: abs; apply contra; by rewrite subr_eq0. -suff kg : size (rVpoly k) < size (rVpoly g) by move: (leq_ltn_trans gk kg); rewrite ltnn. +suff kg : size (rVpoly k) < size (rVpoly g). + by move: (leq_ltn_trans gk kg); rewrite ltnn. rewrite /k linearB /=; case/boolP: (1 < size (rVpoly g)) => size_1g. - apply: size_sub => //=; last by apply lead_coef_F2. apply/eqP; apply: contra g0; by rewrite rVpoly0. @@ -510,7 +507,7 @@ rewrite /k linearB /=; case/boolP: (1 < size (rVpoly g)) => size_1g. (* this means that g is constant *) have sz_g1 : size (rVpoly g) = 1%N. have : size (rVpoly g) != O by rewrite size_poly_eq0 rVpoly0. - case: (size _) size_1g => //; by case. + by case: (size _) size_1g => //; case. rewrite (@size1_polyC_F2 _ sz_g1). rewrite gj in sz_g1. by rewrite (@size1_polyC_F2 _ sz_g1) size_polyC subrr size_poly0. @@ -549,24 +546,26 @@ case/boolP : (odd (min_dist C_not_trivial)) => [odd_d | even_d]. have : min_dist C_not_trivial <= (min_dist C_not_trivial)./2.*2. move: abs. rewrite eq_sym => /(min_dist_prop C_not_trivial)/leq_trans; apply => //. - move/subsetP : f_img; apply. - rewrite inE; apply/existsP; exists y; by apply/eqP. + move/subsetP : f_img; apply. + by rewrite inE; apply/existsP; exists y; apply/eqP. by rewrite (@min_dist_double y). by rewrite -{1}(odd_double_half (min_dist C_not_trivial)) odd_d ltnNge leqnn. - rewrite (mdd_evenE even_d) in enc_m_v. apply/eqP/negPn/negP => abs. have {}abs : m0 != x by apply: contra abs; rewrite Hm0 => /eqP ->. have : (min_dist C_not_trivial)./2 <= (min_dist C_not_trivial)./2 - 1. - move: (odd_double_half (min_dist C_not_trivial)); rewrite -leq_double (negbTE even_d) /= add0n => ->. + move: (odd_double_half (min_dist C_not_trivial)). + rewrite -leq_double (negbTE even_d) /= add0n => ->. move: abs. rewrite eq_sym. move/(min_dist_prop C_not_trivial)/leq_trans; apply => //. - move/subsetP: f_img; apply. - rewrite inE; apply/existsP; exists y; by apply/eqP. + move/subsetP: f_img; apply. + by rewrite inE; apply/existsP; exists y; apply/eqP. by rewrite (@min_dist_double y). apply/negP. rewrite -ltnNge subn1 prednK // half_gt0 ltnNge; apply: contra even_d. - rewrite leq_eqVlt => /orP[/eqP->//|]; by rewrite ltnS leqn0 => /eqP/min_dist_neq0. + rewrite leq_eqVlt => /orP[/eqP->//|]. + by rewrite ltnS leqn0 => /eqP/min_dist_neq0. Qed. (* see for example [F.J. MacWilliams and N.J.A. Sloane, The diff --git a/ecc_classic/repcode.v b/ecc_classic/repcode.v index 52493512..f4873d81 100644 --- a/ecc_classic/repcode.v +++ b/ecc_classic/repcode.v @@ -37,10 +37,10 @@ Lemma seq_block_inv A : forall r (l : seq A) k, Proof. elim=> [l r | r IH l [ | k H] ]. - rewrite !mul0n => Hl. - exists l, nil; by rewrite cats0. + by exists l, nil; rewrite cats0. - rewrite muln1 => H. exists (take (r.+1) l), nil. - rewrite cats0 take_oversize; by [rewrite muln0 | rewrite H]. + by rewrite cats0 take_oversize; [rewrite muln0 | rewrite H]. - exists (take (r.+1) l), (drop (r.+1) l). rewrite cat_take_drop size_drop H size_take H ltn_Pmulr //. repeat (split => //). @@ -210,7 +210,7 @@ Lemma min_dist_repcode (Hr : odd r.+1) : min_dist not_trivial_replcode = r.+1. Proof. rewrite /min_dist /= (_ : min_wH_cw _ = const_mx 1) ?wH_const_mx //. rewrite /min_wH_cw. -case: arg_minP => /=. +case: arg_minnP => /=. rewrite non_0_codeword_replcode (Rep.const_mx_in_code r 1) /= wH_eq0 /=. by apply/eqP => /matrixP/(_ 0 0); rewrite !mxE. move=> i Hi _. diff --git a/ecc_modern/degree_profile.v b/ecc_modern/degree_profile.v index e058ce3b..52b86550 100644 --- a/ecc_modern/degree_profile.v +++ b/ecc_modern/degree_profile.v @@ -18,7 +18,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GRing.Theory. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. Section SumCoef. @@ -55,8 +55,6 @@ End DegreeDistribution. Definition degdistp := DegreeDistribution.p. Coercion degdistp : DegreeDistribution.Lambda >-> poly_of. -Import Num.Theory. - Lemma sum_coef_pos (K : numFieldType) (p : DegreeDistribution.Lambda K) : p.[1] > 0. Proof. destruct p. @@ -482,8 +480,8 @@ case/boolP : (size p > 0)%nat => [Hp|]. case/boolP : (p`_(size p).-1 > 0) => [Hp'|]. move: Hp. rewrite -(ltr0n K) => /(divr_gt0 Hp') H1 /eqP H2. - by rewrite H2 ltrr in H1. - rewrite ltr_def p0 andbT negbK lead_coef_eq0 => /eqP ->. + by rewrite H2 ltxx in H1. + rewrite lt_def p0 andbT negbK lead_coef_eq0 => /eqP ->. by rewrite size_poly0. by rewrite lt0n negbK. Qed. @@ -513,7 +511,7 @@ Definition norm_deg (p : DegreeDistribution.Lambda K) : apply (@NormalizedDegreeDistribution.mkL _ (norm p)). move=> i. rewrite /norm coefZ mulr_ge0 //; last by destruct p. - by rewrite invr_ge0 ltrW // sum_coef_pos. + by rewrite invr_ge0 ltW // sum_coef_pos. by rewrite /norm hornerZ mulVf // lt0r_neq0 // sum_coef_pos. Defined. @@ -578,7 +576,7 @@ move Hs : l.+1.*2 => [ // | [|s]]. move=> t. rewrite (tree_node_children t). case Hch: (tree_children t). - by apply lerr. + by apply lexx. rewrite /tree_dist_children. apply mulr_ge0. by apply LR_pos. @@ -2753,19 +2751,19 @@ Proof. move=> Hr1p Hr2p HGp HF HG Hr1. have HGneq0 : forall i, i \in P -> r2 <= F i / G i -> G i != 0. move=> i Hi Hir2. - have : 0 < F i / G i by apply (ltr_le_trans Hr2p). + have : 0 < F i / G i by apply (Order.POrderTheory.lt_le_trans Hr2p). move: (HF i Hi) (HG i Hi). rewrite le0r. move/orP => [|] HFi HGi. - by rewrite (eqP HFi) mul0r ltrr. + by rewrite (eqP HFi) mul0r ltxx. rewrite pmulr_rgt0 // => /lt0r_neq0 HGi1. by rewrite -(invrK (G i)) invr_neq0. -apply (@ler_trans K ((\sum_(i in P | r2 <= F i / G i) G i / \sum_(i in P) G i) * (\sum_(i in P | r2 <= F i / G i) F i / \sum_(i in P | r2 <= F i / G i) G i))). - apply ler_pmul; try by assumption || apply ltrW. +apply (@Order.POrderTheory.le_trans _ K ((\sum_(i in P | r2 <= F i / G i) G i / \sum_(i in P) G i) * (\sum_(i in P | r2 <= F i / G i) F i / \sum_(i in P | r2 <= F i / G i) G i))). + apply ler_pmul; try by assumption || apply ltW. rewrite -big_distrl -(mulr1 r1) -(mulfV (lt0r_neq0 HGp)) mulrA /=. apply ler_pmul => //. - by rewrite mulr_ge0 // ltrW. - by rewrite invr_ge0 ltrW. + by rewrite mulr_ge0 // ltW. + by rewrite invr_ge0 ltW. rewrite -big_distrl /=. rewrite (_ : \sum_(i in P | r2 <= F i / G i) F i = \sum_(i in P | r2 <= F i / G i) (F i / G i) * G i); first last. @@ -2773,29 +2771,29 @@ apply (@ler_trans K ((\sum_(i in P | r2 <= F i / G i) G i / \sum_(i in P) G i) * rewrite -mulrA (mulrC _ (G i)) mulfV ?mulr1 //. by apply HGneq0. have HGp' : \sum_(i in P | r2 <= F i / G i) G i > 0. - apply (@ltr_le_trans K (r1 * (\sum_(i in P) G i))) => //. + apply (@Order.POrderTheory.lt_le_trans _ K (r1 * (\sum_(i in P) G i))) => //. by apply mulr_gt0. rewrite -{1}(mulr1 r2) -(mulfV (lt0r_neq0 HGp')). rewrite mulrA big_distrr /=. apply ler_pmul => //. apply sumr_ge0 => i /andP [Hi Hir2]. - rewrite mulr_ge0 //; try by apply ltrW. + rewrite mulr_ge0 //; try by apply ltW. by apply HG. - by rewrite ltrW // invr_gt0. + by rewrite ltW // invr_gt0. apply ler_sum => i /andP [Hi Hir2]. - apply ler_pmul => //; try by apply ltrW. + apply ler_pmul => //; try by apply ltW. by apply HG. -apply (@ler_trans K (\sum_(i in P | r2 <= F i / G i) F i / \sum_(i in P) G i)). +apply (@Order.POrderTheory.le_trans _ K (\sum_(i in P | r2 <= F i / G i) F i / \sum_(i in P) G i)). rewrite -!big_distrl /= mulrC -mulrA (mulrA _ _ (\sum_(i in P) G i)^-1). rewrite mulVf ?mul1r //. apply lt0r_neq0. - eapply ltr_le_trans; try apply Hr1. + apply: @Order.POrderTheory.lt_le_trans; try apply Hr1. by apply mulr_gt0. rewrite -big_distrl /=. apply ler_pmul => //. apply sumr_ge0 => i /andP [Hi Hir2]. by apply HF. - by rewrite ltrW // invr_gt0. + by rewrite ltW // invr_gt0. rewrite [\sum_(i in P) F i](bigID (fun i => r2 <= F i / G i)) /=. apply ler_paddr => //. apply sumr_ge0 => i /andP [Hi Hir2]. @@ -2988,7 +2986,7 @@ Lemma weighted_count_it_ge0 i r k P c c' : 0 < r -> 0 <= weighted_count P [seq step_dist_it c r (i :: tval y) | y in dest_ports c' k]. Proof. rewrite /weighted_count big_map => ?. -apply sumr_ge0 => ? _; by rewrite step_dist_it_ge0 // ltrW. +apply sumr_ge0 => ? _; by rewrite step_dist_it_ge0 // ltW. Qed. Lemma tree_like_empty_border c r : @@ -3046,7 +3044,7 @@ rewrite [X in _ <= X](bigID (fun i : port * {set port} => i.2 \notin conodes c)) apply ler_paddr; first by apply sumr_ge0 => i _; apply weighted_count_it_ge0. (* simplify rhs formula *) set F := BIG_F. -apply (@ler_trans _ +apply (@Order.POrderTheory.le_trans _ _ (\sum_(i in dest_port c | tree_like (step c (bnext c) i.1 i.2)) F i)). rewrite (bigID xpredT) /= [in X in _ + X]big_pred0 ?addr0; last first. by move=> ?; rewrite andbF. @@ -3061,12 +3059,12 @@ apply (@ler_trans _ move: (tree_like_step Htl Hhead (leq_trans Hmax Hlam') Hpc). rewrite /weighted_count 2!big_map big_enum_in -2!big_distrl /=. rewrite -2!big_distrr /= 2!mul1r big_mkcond big_enum_in -big_mkcondr /=. - rewrite -3!mulf_div (@mulfV _ r) ?gtr_eqF // mulfV; last first. + rewrite -3!mulf_div (@mulfV _ r) ?gt_eqF // mulfV; last first. by rewrite invr_neq0 // pnatr_eq0 -lt0n. rewrite mul1r /bnext eqb /= => ->. - by rewrite ler_pmul // ?ler_nat ?leq_subr // ?invr_ge0 ltrW // ltr0n. + by rewrite ler_pmul // ?ler_nat ?leq_subr // ?invr_ge0 ltW // ltr0n. (* prove this is equal to the original rhs *) -rewrite {}/F ler_eqVlt. +rewrite {}/F le_eqVlt. apply /orP /or_introl /eqP. (* remove impossible cases from sum *) rewrite (bigID (fun i => dest_dist c i.2 == 0)) /= big1; last first. @@ -3105,10 +3103,10 @@ move: (free_step_coports_gt Hlam Hhead Hi Hd) => Hlam1. move/(_ Hk (connected_step Hpc) Htl' Hrd Hlam1). rewrite /weighted_count /step_dist_it eqb /= /(step_dist c r s i). rewrite (enum_step_border eqb Hi) -/r'. -apply ler_trans. +apply Order.POrderTheory.le_trans. rewrite /r2 /r1. apply ler_expn2r. - by rewrite nnegrE ltrW. + by rewrite nnegrE ltW. by rewrite nnegrE divr_ge0 // ler0n. rewrite ler_pmul // ?invr_ge0 ?ler0n //. rewrite ler_nat mulnS subnDA leq_sub2r // -subnDA leq_sub2l //. @@ -3352,7 +3350,7 @@ Lemma weighted_count_switch_ge0 P lam rho c c' r i l : | y in dest_ports_seqs c' l] >= 0. Proof. rewrite /weighted_count big_map => Hr. -by apply sumr_ge0 => ? _; rewrite switch_step_dist_it_ge0 // ltrW. +by apply sumr_ge0 => ? _; rewrite switch_step_dist_it_ge0 // ltW. Qed. Lemma switch_step_dist_it_const lam rho c r y : @@ -3575,7 +3573,7 @@ rewrite [X in _ <= X](bigID(fun i : _ .-tuple _ => tree_like (step_it c i))) /=. apply ler_paddr; first by apply sumr_ge0 => i _;apply weighted_count_switch_ge0. (* simplify rhs formula *) set F := BIG_F. -apply (@ler_trans _ (\sum_(i in dest_ports c #|border (nodes c)| +apply (@Order.POrderTheory.le_trans _ _ (\sum_(i in dest_ports c #|border (nodes c)| | tree_like (step_it c i)) F i)). rewrite (bigID xpredT) /= [in X in _ + X]big_pred0 ?addr0; last first. by move=> ?; rewrite andbF. @@ -3630,8 +3628,8 @@ apply (@ler_trans _ (\sum_(i in dest_ports c #|border (nodes c)| apply (leq_ltn_trans (leq_subr _ _)). apply (leq_ltn_trans Hclen). by rewrite (leq_ltn_trans _ Hlenmax) // leq_addr. - apply ler_trans. - apply (@ler_trans K (r0 ^+ len)). + apply Order.POrderTheory.le_trans. + apply (@Order.POrderTheory.le_trans _ K (r0 ^+ len)). rewrite /r1. apply ler_expn2r. by rewrite rpred_div // nnegrE ler0n. @@ -3665,7 +3663,7 @@ apply (@ler_trans _ (\sum_(i in dest_ports c #|border (nodes c)| by rewrite ltr0n ltn_subRL addn0 mulnC. by rewrite invr_gt0 ltr0n. (* prove this is equal to the original rhs *) -rewrite {}/F ler_eqVlt. +rewrite {}/F le_eqVlt. apply /orP /or_introl /eqP. (* remove impossible cases from sum *) rewrite (bigID (fun i : _ .-tuple _ => (step_dist_it lam c r i).2 == 0)) @@ -3710,11 +3708,11 @@ have Hlen': (#|known_coports (switch (step_it c i))| <= len')%nat. rewrite /known_coports /ports part_nodes_step_it. by rewrite /len' mulnS (leq_trans Hlen) // leq_addr. have Hd': (step_dist_it lam c r i).2 > 0. - by rewrite ltr_def Hd step_dist_it_ge0 // ltrW. + by rewrite lt_def Hd step_dist_it_ge0 // ltW. have Hlenmaxrec: (len' * tree_max l.+1 < #|port|)%nat. by rewrite (leq_ltn_trans _ Hlenmax) // leq_addl. move/(_ Hlen' (border_nodes_step_it Hi) Hd' Hlenmaxrec) => /=. -apply ler_trans. +apply Order.POrderTheory.le_trans. apply ler_expn2r. by rewrite rpred_div // nnegrE ler0n. by rewrite rpred_div // nnegrE ler0n. @@ -4394,7 +4392,7 @@ rewrite /start_dist. case: ifP => Hi0; try by rewrite eqxx. rewrite mulf_eq0 => Hi. move: (@max_card port (mem i)); rewrite -bin_gt0. -rewrite -(ltr0n K) -invr_gt0 ltr_def => /andP [HC _]. +rewrite -(ltr0n K) -invr_gt0 lt_def => /andP [HC _]. rewrite (negbTE HC) orbF in Hi. move/leq_sizeP/(_ #|i|.-1): (leq_maxl (size lam) (size rho)). rewrite -/maxdeg. @@ -4482,7 +4480,7 @@ apply le_sum_all. - move=> i. case: ifP => // Hi _. rewrite (@weighted_count_switch_it maxdeg def_port maxdeg) //. - + rewrite ltr_def Hi /=; exact: start_dist_ge0. + + rewrite lt_def Hi /=; exact: start_dist_ge0. + by rewrite card_ports_nodes_start // Hi. + by rewrite /known_coports /ports /= big_set0 cards0. - move=> /= i. @@ -4492,7 +4490,7 @@ apply le_sum_all. + by apply tree_like_start. + by rewrite card_ports_nodes_start // Hi. + by rewrite /known_coports /ports /= big_set0 cards0. - + rewrite ltr_def Hi /=; exact: start_dist_ge0. + + rewrite lt_def Hi /=; exact: start_dist_ge0. Qed. End tree_like_start. diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v index 309d0670..8b71fcf6 100644 --- a/ecc_modern/ldpc_algo.v +++ b/ecc_modern/ldpc_algo.v @@ -157,6 +157,8 @@ Fixpoint estimation {k} (n : tn_tree' k R2 R2) := End Algo. +Require Import Extraction. + Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive seq => "list" [ "[]" "(::)" ]. @@ -165,6 +167,13 @@ Extract Inductive option => "option" ["Some" "None"]. Extract Inlined Constant R => "float". Extract Inlined Constant R0 => "0.". Extract Inlined Constant R1 => "1.". +Extract Constant RbaseSymbolsImpl.R => "float". +Extract Constant RbaseSymbolsImpl.R0 => "0.". +Extract Constant RbaseSymbolsImpl.R1 => "1.". +Extract Constant ConstructiveCauchyReals.CReal => "float". +Extract Constant ClassicalDedekindReals.DReal => "float". +Extract Constant ClassicalDedekindReals.DRealQlim => "Obj.magic". +Extract Constant ClassicalDedekindReals.DRealAbstr => "(fun x -> x)". Extract Constant Rmult => "( *.)". Extract Constant Rplus => "(+.)". Extract Constant Rinv => "fun x -> 1. /. x". diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v index 556e7799..67fd5255 100644 --- a/ecc_modern/ldpc_algo_proof.v +++ b/ecc_modern/ldpc_algo_proof.v @@ -1090,37 +1090,16 @@ Lemma beta_def n0 m0 (d : 'rV_n) : beta (rW n0) [seq (alpha' m1 n0 d0, alpha' m1 n0 d1) | m1 in 'F n0 :\ m0] = (beta' n0 m0 d0, beta' n0 m0 d1). Proof. -(*move=> d0 d1. -rewrite /beta. -rewrite /beta'. -rewrite /ldpc.beta. -rewrite -big_filter. -rewrite -[in X in _ = (_, X)]big_filter. -rewrite foldlE /=. -rewrite big_cons /=. -rewrite /d0 /d1 /row_set !mxE !eqxx. -rewrite big_map. -rewrite big_enum /=. -rewrite -big_filter. -have [e He [_ _ _]] := big_enumP _. -elim: e He. - move=> He. - by rewrite !big_nil. -move=> h t ih He. -rewrite !big_cons /=.*) rewrite /rW /beta' /alpha' /ldpc.beta /=. rewrite /image_mem /enum_mem. rewrite -big_filter. rewrite -[in X in _ = (_, X)]big_filter. -rewrite !filter_index_enum. +have [e He [ue Pe perme]] := big_enumP _. rewrite {3 5}/row_set !mxE !eqxx /=. move: (W 0 (vb ``_ n0)) (W 1 (vb ``_ n0)). -elim: (enum (mem _)) => [|a l IH] p0 p1. - rewrite !big_nil /=. - by rewrite !mulR1. -rewrite !big_cons /=. -rewrite IH. -by rewrite !mulRA. +elim: e {He ue Pe perme} => [|a l IH] p0 p1. + by rewrite /= !big_nil !mulR1. +by rewrite /= !big_cons /= IH // !mulRA. Qed. Local Open Scope R_scope. @@ -1258,6 +1237,7 @@ rewrite [in X in _ = (_, X)](eq_bigr (fun t : 'rV_n => move=> i _; by rewrite (checksubsum_D1 _ Hn0) eq_sym. rewrite !summary_powersetE !summary_foldE /summary_fold /=. rewrite /image_mem /enum_mem. + rewrite !filter_index_enum. set f := 'V m0 :\ n0. rewrite {2 3 5 6}(set_mem f). diff --git a/extraction/sumprod_test.ml b/extraction/sumprod_test.ml index 7928da9a..bcc43c09 100644 --- a/extraction/sumprod_test.ml +++ b/extraction/sumprod_test.ml @@ -1,6 +1,12 @@ (* #load "sumprod.cmo" *) open Sumprod;; +let rabst = RbaseSymbolsImpl.coq_Rabst +let rrepr = RbaseSymbolsImpl.coq_Rrepr + +let to_r2 (x,y) = rabst x, rabst y +let of_r2 (x,y) = rrepr x, rrepr y + type ('a,'b) sum = Inl of 'a | Inr of 'b;; let rec iota m n = if m >= n then [] else m :: iota (succ m) n;; @@ -17,7 +23,7 @@ end;; module BT (C : Code) = struct open C - + let select_children s i = match i with | Inl i -> @@ -42,9 +48,10 @@ module BT (C : Code) = struct children = chrn; up = (); down = ()} let decode _W = + let _W i = to_r2 (_W i) in let tree = build_tree_rec _W [] (Inr (List.hd enum_n)) in let computed_tree = sumprod Kv tree in - estimation Kv computed_tree + List.map (fun (a, x) -> a, of_r2 x) (estimation Kv computed_tree) end;; (* A practical example, based on a simpler variant of the fig. 6 of @@ -149,7 +156,7 @@ end;; module BTC' = BT(C');; -let f0 : three ord -> r2 = function +let f0 : three ord -> float * float = function | OZ -> (0.2, 0.8) | OS OZ -> (0.2, 0.8) | OS (OS OZ) -> (0.8, 0.2) diff --git a/information_theory/channel_coding_converse.v b/information_theory/channel_coding_converse.v index 5dae56b1..3ce368b9 100644 --- a/information_theory/channel_coding_converse.v +++ b/information_theory/channel_coding_converse.v @@ -2,10 +2,9 @@ (* infotheo v2 (c) AIST, Nagoya University. GNU GPLv3. *) From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix. Require Import Reals. -Require Import ssrR Reals_ext ssr_ext ssralg_ext logb ln_facts Rbigop arg_rmax. -Require Import num_occ fdist entropy types jtypes divergence. -Require Import conditional_divergence error_exponent channel_code channel. -Require Import success_decode_bound. +Require Import ssrR Reals_ext ssr_ext ssralg_ext logb ln_facts Rbigop num_occ. +Require Import fdist entropy types jtypes divergence conditional_divergence. +Require Import error_exponent channel_code channel success_decode_bound. (******************************************************************************) (* Channel coding theorem (converse part) *) @@ -48,16 +47,17 @@ Lemma channel_coding_converse_gen : exists Delta, 0 < Delta /\ forall n', minRate <= CodeRate c -> scha(W, c) <= n.+1%:R ^ (#|A| + #|A| * #|B|) * exp2 (- n%:R * Delta). Proof. -move: error_exponent_bound => /(_ _ _ Bnot0 W _ Hc _ HminRate); case => Delta [Delta_pos HDelta]. +move: error_exponent_bound => /(_ _ _ Bnot0 W _ Hc _ HminRate). +case => Delta [Delta_pos HDelta]. exists Delta; split => // n' n M c Mnot0 H. apply: (leR_trans (success_bound W Mnot0 c)). -set Pmax := arg_rmax _ _ _. +set Pmax := [arg max_(P > _) _]%O. set tc := _.-typed_code _. rewrite pow_add -mulRA. apply leR_wpmul2l; first exact/pow_le/leR0n. -apply (leR_trans (typed_success_bound W Mnot0 (Pmax.-typed_code c))). +apply: (leR_trans (typed_success_bound W Mnot0 (Pmax.-typed_code c))). apply leR_wpmul2l; first exact/pow_le/leR0n. -set Vmax := arg_rmax _ _ _. +set Vmax := [arg max_(V > _) _]%O. rewrite /success_factor_bound /exp_cdiv. case : ifP => Hcase; last by rewrite mul0R. rewrite -ExpD. diff --git a/information_theory/chap2.v b/information_theory/chap2.v index 43f4d21d..0f06814b 100644 --- a/information_theory/chap2.v +++ b/information_theory/chap2.v @@ -217,18 +217,6 @@ End chain_rule. Section chain_rule_generalization. -(* TODO: move *) -Lemma to_bivar_entropy (A : finType) (n : nat) (P : {fdist 'rV[A]_n.+1}) : - `H P = `H (Multivar.to_bivar P). -Proof. -rewrite /entropy /=; congr (- _). -apply/esym. -rewrite (eq_bigr (fun a => (Multivar.to_bivar P) (a.1, a.2) * log ((Multivar.to_bivar P) (a.1, a.2)))); last by case. -rewrite -(pair_bigA _ (fun a1 a2 => (Multivar.to_bivar P) (a1, a2) * log ((Multivar.to_bivar P) (a1, a2)))) /=. -rewrite -(big_rV_cons_behead _ xpredT xpredT) /=. -by apply eq_bigr => a _; under eq_bigr do rewrite Multivar.to_bivarE. -Qed. - Local Open Scope ring_scope. (* TODO: move *) @@ -320,13 +308,14 @@ rewrite inordK ?prednK ?lt0n // -1?ltnS // ltnS add1n prednK ?lt0n // => ik. by congr (v _ _); apply val_inj => /=; rewrite /unbump ik subn1. Qed. -Lemma chain_rule_multivar (A : finType) (n : nat) (P : {fdist 'rV[A]_n.+1}) (i : 'I_n.+1) : - i != ord0 -> - (`H P = `H (MargFDist.d P i) + CondEntropy.h (Multivar.to_bivar (MultivarPerm.d P (put_front_perm i))))%R. +Lemma chain_rule_multivar (A : finType) (n : nat) (P : {fdist 'rV[A]_n.+1}) + (i : 'I_n.+1) : i != ord0 -> + (`H P = `H (MargFDist.d P i) + + CondEntropy.h (Multivar.to_bivar (MultivarPerm.d P (put_front_perm i))))%R. Proof. move=> i0; rewrite MargFDistd_put_front // -Swap.fst. rewrite -{2}(Swap.dI (Multivar.to_bivar _)) -chain_rule JointEntropy.hC Swap.dI. -by rewrite -to_bivar_entropy entropy_multivarperm. +by rewrite entropy_to_bivar entropy_multivarperm. Qed. End chain_rule_generalization. diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v index fbd0143f..cbddaa41 100644 --- a/information_theory/joint_typ_seq.v +++ b/information_theory/joint_typ_seq.v @@ -264,9 +264,7 @@ apply (@leR_trans (\sum_(i | i \in `JTS P W n epsilon) rewrite (_ : \sum_(_ | _) _ = INR #| `JTS P W n epsilon| * exp2 (- INR n * (`H P - epsilon)) * exp2 (- INR n * (`H( P `o W) - epsilon))); last first. - rewrite big_const_seq /= (_ : count _ _ = #|`JTS P W n epsilon|); last first. - by rewrite -size_filter filter_index_enum -cardE. - by rewrite iter_addR -mulRA. + by rewrite big_const iter_addR mulRA. apply (@leR_trans (exp2 (INR n * (`H( P , W ) + epsilon)) * exp2 (- INR n * (`H P - epsilon)) * exp2 (- INR n * (`H( P `o W ) - epsilon)))). do 2 apply leR_wpmul2r => //. diff --git a/information_theory/kraft.v b/information_theory/kraft.v index 9eec332a..c33e1c56 100644 --- a/information_theory/kraft.v +++ b/information_theory/kraft.v @@ -1,6 +1,6 @@ (* infotheo v2 (c) AIST, Nagoya University. GNU GPLv3. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq. -From mathcomp Require Import choice fintype tuple bigop finset path ssralg. +From mathcomp Require Import choice fintype order tuple bigop finset path ssralg. From mathcomp Require Import fingroup zmodp poly ssrnum. Require FunctionalExtensionality. Require Import ssr_ext. @@ -506,7 +506,7 @@ move=> /= a b [] /eqP. rewrite eqseq_cat // => /andP[_ /eqP ab]; by apply val_inj. Qed. -Import Num.Theory GRing.Theory. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. Section prefix_implies_kraft_cond. @@ -583,7 +583,7 @@ rewrite (eq_bigr (fun i : 'I_n => #|suffixes C``_i|%:R)%R); last first. by apply/leq_lmax/nthP; exists i. by rewrite unitfE pnatr_eq0 -lt0n. (*\color{comment}{\framebox{the goal is now $\sum_{i < n} | \{ x | \prefix{c_i}{x} \} | \leq |T|^{\ell_{\mathrm{max}}}$}} *) -apply (@ler_trans _ (#|\bigcup_(i < n) suffixes (C ``_ i)|%:R)%R). +apply (@le_trans _ _ (#|\bigcup_(i < n) suffixes (C ``_ i)|%:R)%R). rewrite -sum1_card. rewrite partition_disjoint_bigcup /=. rewrite natr_sum ler_sum // => i _. @@ -632,7 +632,7 @@ rewrite (eq_bigr (fun j : 'I__ => #|T|%:R ^-nth O l j))%R; last first. by rewrite (leq_trans (ltn_ord i)) // ltnW. by rewrite unitfE pnatr_eq0. by rewrite mulrA mulVr ?unitfE -?natrX ?pnatr_eq0 ?expn_eq0 // mul1r. -rewrite ler_subr_addr natrX (ler_trans _ H') //. +rewrite ler_subr_addr natrX (le_trans _ H') //. rewrite [X in (X <= _)%R](_ : _ = \sum_(k < j.+1) #|T|%:R^-nth O l k)%R; last first. by rewrite big_ord_recr /= card_ord. rewrite (@big_ord_widen _ _ _ j.+1 n (fun i => #|T|%:R ^- nth O l i))%R //. @@ -753,7 +753,7 @@ have H2 : (r - 1 < (w j)%:R)%R. (* \color{comment}{\framebox{here we prove $r - rewrite ltr_pdivr_mulr; [|by rewrite -natrX ltr0n expn_gt0 card_ord]. by rewrite mul1r -natrX ltr_nat ltn_mod expn_gt0 card_ord. by rewrite {}wkE ltr_sub_addl addrC ltr_add2r. -by rewrite ltr_subl_addl addrC ltrNge H1 in H2. +by rewrite ltr_subl_addl addrC ltNge H1 in H2. Qed. End kraft_cond_implies_prefix. diff --git a/information_theory/source_code.v b/information_theory/source_code.v index d2eb1c02..5169c8e4 100644 --- a/information_theory/source_code.v +++ b/information_theory/source_code.v @@ -17,6 +17,8 @@ Import Prenex Implicits. Local Open Scope R_scope. +Declare Scope source_code_scope. + Section scode_definition. Variables (A : finType) (B : Type) (k n : nat). diff --git a/information_theory/success_decode_bound.v b/information_theory/success_decode_bound.v index 3213b12b..fa062bee 100644 --- a/information_theory/success_decode_bound.v +++ b/information_theory/success_decode_bound.v @@ -3,8 +3,8 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix. Require Import Reals. Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop fdist entropy. -Require Import ln_facts arg_rmax num_occ types jtypes divergence. -Require Import conditional_divergence entropy channel_code channel. +Require Import ln_facts num_occ types jtypes divergence conditional_divergence. +Require Import entropy channel_code channel. (******************************************************************************) (* Lemmas for the converse of the channel coding theorem *) @@ -259,32 +259,31 @@ Proof. move: (jtype_not_empty n Anot0 Bnot0) => H; exact (enum_val (Ordinal H)). Qed. +Hypothesis HV0 : V0 \in \nu^{B}(P). + Let exp_cdiv_bound := fun V => exp_cdiv P V W * success_factor_bound M V P. +Let Vmax := [arg max_(V > V0) exp_cdiv_bound V]%O. + Lemma typed_success_bound : - let Vmax := arg_rmax V0 [pred V | V \in \nu^{B}(P)] exp_cdiv_bound in scha(W, tc) <= n.+1%:R ^ (#|A| * #|B|) * exp_cdiv_bound Vmax. Proof. -move=> Vmax. rewrite (typed_success W Mnot0 tc). apply (@leR_trans ( \sum_(V|V \in \nu^{B}(P)) exp_cdiv P V W * exp2 (- n%:R * +| log #|M|%:R * / n%:R - `I(P, V) |))). - apply: ler_rsum => V HV. + apply: ler_rsum => V Vnu. rewrite -mulRA; apply leR_wpmul2l. - rewrite /exp_cdiv. - case : ifP => _ //; exact/leRR. - rewrite /success_factor mulRA; exact: success_factor_ub. + by rewrite /exp_cdiv; case : ifP => _ //; exact/leRR. + by rewrite /success_factor mulRA; exact: success_factor_ub. apply (@leR_trans (\sum_(V | V \in \nu^{B}(P)) exp_cdiv P Vmax W * exp2 (- n%:R * +| log #|M|%:R * / n%:R - `I(P, Vmax)|))). apply ler_rsum => V HV. - move: (@arg_rmax2 [finType of (P_ n (A, B))] V0 [pred V | V \in \nu^{B}(P) ] - (fun V => exp_cdiv P V W * success_factor_bound M V P)). - apply => //; by exists V. -rewrite big_const iter_addR /success_factor_bound. -apply leR_wpmul2r. + by move/leRP: (@arg_rmax2 [finType of (P_ n (A, B))] V0 + (fun V => exp_cdiv P V W * success_factor_bound M V P) V). +rewrite big_const iter_addR /success_factor_bound; apply leR_wpmul2r. - apply mulR_ge0; last exact/exp2_ge0. - rewrite /exp_cdiv; case: ifP => _ //; exact/leRR. -- rewrite natRexp; exact/le_INR/leP/card_nu. + by rewrite /exp_cdiv; case: ifP => _ //; exact/leRR. +- by rewrite natRexp; exact/le_INR/leP/card_nu. Qed. End typed_success_bound_sect. @@ -309,7 +308,7 @@ Defined. Local Open Scope num_occ_scope. Lemma success_bound : - let Pmax := arg_rmax P0 predT (fun P => scha(W, P.-typed_code c)) in + let Pmax := [arg max_(P > P0) scha(W, P.-typed_code c)]%O in scha(W, c) <= n.+1%:R ^ #|A| * scha(W, Pmax.-typed_code c). Proof. move=> Pmax. @@ -321,7 +320,7 @@ apply (@leR_trans (\sum_(P : P_ n ( A )) scha W (P.-typed_code c))); last first. \sum_(P : P_ n ( A )) scha W (Pmax.-typed_code c)); last first. by rewrite big_const iter_addR. apply ler_rsum => P _. - exact: (@arg_rmax2 _ P0 xpredT (fun P1 : P_ n (A) => scha(W, P1.-typed_code c))). + by move/leRP : (arg_rmax2 P0 (fun P1 : P_ n (A) => scha(W, P1.-typed_code c)) P). rewrite schaE // -(sum_messages_types c). rewrite div1R (big_morph _ (morph_mulRDr _) (mulR0 _)). apply ler_rsum => P _. @@ -334,7 +333,7 @@ apply/(@leR_trans (\sum_(m | m \in enc_pre_img c P) apply Req_le, eq_big => tb // _. rewrite inE in Hm. by rewrite /tcode /= ffunE Hm. -- apply ler_rsum_l => //= i ?; [ exact/leRR | exact: rsumr_ge0]. +- by apply ler_rsum_l => //= i ?; [exact/leRR | exact: rsumr_ge0]. Qed. End success_bound_sect. diff --git a/lib/Rbigop.v b/lib/Rbigop.v index aca679ca..eb1a05cc 100644 --- a/lib/Rbigop.v +++ b/lib/Rbigop.v @@ -776,11 +776,7 @@ Local Open Scope min_scope. Lemma bigminn_min (A : finType) (C : {set A}) (cnot0 : {c0 | c0 \in C}) a (Ha : a \in C) (h : A -> nat) : (\min^ (sval cnot0) _(c in C) h c <= h a)%nat. -Proof. -case: arg_minP. -by destruct cnot0. -move=> a0 a0C; exact. -Qed. +Proof. by case: arg_minnP; [case: cnot0|move=> a0 a0C; exact]. Qed. (* TODO: useless ? *) Lemma big_rmax_bigminn_helper (A : finType) n (g : nat -> R) : diff --git a/lib/Reals_ext.v b/lib/Reals_ext.v index 46963f6c..5aaa6ee1 100644 --- a/lib/Reals_ext.v +++ b/lib/Reals_ext.v @@ -43,10 +43,6 @@ Reserved Notation "x %:pr" (at level 0, format "x %:pr"). Reserved Notation "x %:pos" (at level 0, format "x %:pos"). Reserved Notation "x %:nng" (at level 0, format "x %:nng"). -Notation "'min(' x ',' y ')'" := (Rmin x y) - (format "'min(' x ',' y ')'") : reals_ext_scope. -Notation "'max(' x ',' y ')'" := (Rmax x y) - (format "'max(' x ',' y ')'") : reals_ext_scope. Notation "+| r |" := (Rmax 0 r) : reals_ext_scope. Set Implicit Arguments. @@ -55,8 +51,6 @@ Import Prenex Implicits. Arguments INR : simpl never. -Canonical R_choiceType := ChoiceType R Rstruct.R_choiceMixin. - Local Open Scope R_scope. Local Open Scope reals_ext_scope. @@ -283,6 +277,17 @@ Qed. End reals_ext. +Section rExtrema. +Variables (I : finType) (i0 : I) (F : I -> R). + +Lemma arg_rmax2 : forall j, (F j <= F [arg max_(i > i0) F i]%O)%O. +Proof. +move=> j; case: (@Order.TotalTheory.arg_maxP _ _ I i0 xpredT F isT) => i _. +exact. +Qed. + +End rExtrema. + Section pos_finfun. Variable (T : finType). diff --git a/lib/arg_rmax.v b/lib/arg_rmax.v deleted file mode 100644 index b6a44440..00000000 --- a/lib/arg_rmax.v +++ /dev/null @@ -1,188 +0,0 @@ -(* infotheo (c) AIST. R. Affeldt, M. Hagiwara, J. Senizergues. GNU GPLv3. *) -From mathcomp Require Import all_ssreflect. -Require Import Reals. -Require Import ssrR Reals_ext ssr_ext num_occ. - -(** * Variation of the SSReflect standard library *) - -Set Implicit Arguments. -Unset Strict Implicit. -Import Prenex Implicits. - -Local Open Scope R_scope. - -Section MinFintype. - -Local Open Scope nat_scope. - -Variables (I : finType) (i0 : I) (P : pred I) (ord : rel I). - -Let arg_pred_min := [pred i | P i && [forall j, P j ==> ord i j]]. - -Definition arg_minord := odflt i0 (pick arg_pred_min). - -CoInductive minimum_spec_ord : I -> Type := - MinimumSpecOrd i of P i & (forall j, P j -> ord i j) - : minimum_spec_ord i. - -Hypothesis P_not_pred0 : {i | P i}. -Hypothesis ord_trans : transitive ord. -Hypothesis ord_refl : reflexive ord. -Hypothesis ord_total : total ord. - -Lemma in_sort a s : a \in (sort ord s) = (a \in s). -Proof. rewrite -2!has_pred1; exact/eq_has_r/mem_sort. Qed. - -Lemma all_sort s : all P (sort ord s) = all P s. -Proof. exact/eq_all_r/mem_sort. Qed. - -Lemma in_sorted a s : sorted ord s -> a \in s -> ord (head a s) a. -Proof. -case: s; first by rewrite in_nil. -move=> hd tl Hs a_in_s. -rewrite -nth0. -rewrite {2}(_ : a = nth a (hd :: tl) (find (pred1 a) (hd :: tl))); last first. - apply/esym/eqP. - rewrite (_ : nth a (hd :: tl) (find (pred1 a) (hd :: tl)) == a = pred1 a (nth a (hd :: tl) (find (pred1 a) (hd :: tl)))) //. - by rewrite nth_find // has_pred1. -case/boolP : (find (pred1 a) (hd :: tl) == 0) => [/eqP -> //|H]. -apply sorted_of_nth => //. -apply/andP; split. -- rewrite ltn_neqAle leq0n andbT. - apply/negP => /eqP abs; contradict H; rewrite abs; exact/negP/negPn/eqP. -by rewrite -has_find has_pred1. -Qed. - -Lemma find_ex_minord : {i | P i & forall j, P j -> ord i j}. -Proof. -case P_not_pred0 => j0 Pj0. -exists (head j0 (sort ord (filter P (enum I)))). -- move Hs : (sort _ _) => s. - case: s Hs ; first by move=> _ /=. - move=> hd tl hd_tl /=. - have : all P (hd :: tl) ; last move=> /allP Hs. - by rewrite -hd_tl all_sort filter_all. - apply Hs. - by rewrite in_cons eqxx. -- move=> i Pi. - move Hs : (sort _ _) => s. - have i_in_s: i \in s. - by rewrite -Hs in_sort mem_filter Pi /= mem_enum. - rewrite (_ : head j0 s = head i s); last first. - clear Hs. - case: s i_in_s => //; by rewrite in_nil. - apply in_sorted => //. - rewrite -Hs. - exact/sort_sorted. -Qed. - -Definition ex_minord := s2val find_ex_minord. - -Inductive ex_minord_spec : I -> Type := - ExMinordSpec i of P i & (forall j, P j -> ord i j) : ex_minord_spec i. - -Lemma ex_minordP : ex_minord_spec ex_minord. -Proof. by rewrite /ex_minord; case: find_ex_minord. Qed. - -Hypothesis Pi0 : P i0. - -Let FP j := [exists i, P i && (i == j)]. - -Let FP_F i : P i -> FP i. -Proof. by move=> Pi; apply/existsP; exists i; rewrite Pi /=. Qed. - -Let exFP : exists r, FP r. Proof. by exists i0; exact: FP_F. Qed. - -Lemma arg_minordP : minimum_spec_ord arg_minord. -Proof. -rewrite /arg_minord; case: pickP => [i /andP[Pi /forallP min_i] | no_i]. - split=> // j ; exact/implyP. -case: (ex_minordP) => n ex_i min_i. -move/FP_F : ex_i. -case/pred0P => i. -apply: contraFF (no_i i) => /andP[Pi def_n]; rewrite /= Pi. -apply/forallP=> j; apply/implyP=> Pj. -move/eqP in def_n. -rewrite def_n. -exact/min_i/Pj. -Qed. - -End MinFintype. - -Section MaxFintype. - -Variables (I : finType) (i0 : I) (P : pred I) (ord : rel I). - -Let ord_inv i j := ord j i. - -Definition arg_maxord := arg_minord i0 P ord_inv. - -CoInductive maximum_spec_ord : I -> Type := - MaximumSpecOrd i of P i & (forall j, P j -> ord j i) - : maximum_spec_ord i. - -Hypothesis P_not_pred0 : {i | P i}. -Hypothesis ord_trans : transitive ord. - -Let ord_inv_trans : transitive ord_inv. -Proof. move => x y z Hxy Hzx; apply (ord_trans Hzx Hxy). Qed. - -Hypothesis ord_refl : reflexive ord. - -Let ord_inv_refl : reflexive ord_inv. -Proof. by rewrite /reflexive /ord_inv. Qed. - -Hypothesis ord_total : total ord. - -Let ord_inv_total : total ord_inv. -Proof. rewrite /total => x y ; apply ord_total. Qed. - -Lemma arg_maxordP : maximum_spec_ord arg_maxord. -Proof. -rewrite /arg_maxord. -case: (@arg_minordP _ i0 P ord_inv P_not_pred0 ord_inv_trans ord_inv_refl ord_inv_total) => ???. -exact: MaximumSpecOrd. -Qed. - -End MaxFintype. - -Section rExtrema. - -Variables (I : finType) (i0 : I) (P : pred I) (F : I -> R). - -Let ord_F_Rle i j := F i x y z /leRP Hyx /leRP Hxz; apply/leRP. -exact/(@leR_trans (F x)). -Qed. - -Let ord_refl : reflexive ord_F_Rle. -Proof. rewrite /reflexive /ord_F_Rle => x ; exact/leRP/leRR. Qed. - -Let ord_total : total ord_F_Rle. -Proof. -rewrite /total /ord_F_Rle => x y. apply/orP. -case (Rlt_le_dec (F x) (F y)) => [/ltRW|] /leRP H; by [left|right]. -Qed. - -Definition arg_rmax := arg_maxord i0 P ord_F_Rle. - -CoInductive maximum_spec_r : I -> Type := - MaximumSpecR i of P i & (forall j, P j -> ord_F_Rle j i) - : maximum_spec_r i. - -Hypothesis P_not_pred0 : {i | P i}. - -Lemma arg_rmaxP : maximum_spec_r arg_rmax. -Proof. -rewrite /arg_rmax. -case: (@arg_maxordP _ i0 P ord_F_Rle P_not_pred0 ord_trans ord_refl ord_total) => ???. -exact: MaximumSpecR. -Qed. - -Lemma arg_rmax2 : forall j, P j -> F j <= F arg_rmax. -Proof. case: arg_rmaxP => ? ? H ? ?; exact/leRP/H. Qed. - -End rExtrema. diff --git a/lib/classical_sets_ext.v b/lib/classical_sets_ext.v index 4dff3112..2b71f76c 100644 --- a/lib/classical_sets_ext.v +++ b/lib/classical_sets_ext.v @@ -20,14 +20,14 @@ rewrite propeqE; split => [H|H]; first by split => x Hx; apply H; [left|right]. move=> x [] Hx; [exact: (proj1 H)|exact: (proj2 H)]. Qed. -Lemma set0P A : (A != set0) <-> (A !=set0). +(*Lemma set0P A : (A != set0) <-> (A !=set0). Proof. split; [move=> A_neq0|by case=> t tA; apply/negP => /eqP A0; rewrite A0 in tA]. apply/existsp_asboolP; rewrite -(negbK `[exists _, _]); apply/negP. rewrite existsbE => /forallp_asboolPn H. move/negP : A_neq0; apply; apply/eqP; rewrite funeqE => t; rewrite propeqE. move: (H t); by rewrite asboolE. -Qed. +Qed.*) Lemma eq_imagel (f g : T -> U) A : (forall a, A a -> f a = g a) -> f @` A = g @` A. @@ -71,9 +71,9 @@ rewrite (_ : (forall a, Y (f a)) <-> (forall a, setT a -> Y (f a))) ?image_subse by firstorder. Qed. -Lemma eq_bigcupl (P Q : set U) (X : U -> set T) : +(*Lemma eq_bigcupl (P Q : set U) (X : U -> set T) : P = Q -> bigsetU P X = bigsetU Q X. -Proof. by move ->. Qed. +Proof. by move ->. Qed.*) Lemma eq_bigcupr (P : set U) (X Y : U -> set T) : X =1 Y -> bigsetU P X = bigsetU P Y. @@ -83,32 +83,31 @@ Lemma eq_bigcup (P Q : set U) (X Y : U -> set T) : P = Q -> X =1 Y -> bigsetU P X = bigsetU Q Y. Proof. by move=> -> /funext ->. Qed. -Lemma bigcup_set1 (P : set U) (f : U -> T) : +Lemma bigcup_of_singleton (P : set U) (f : U -> T) : \bigcup_(x in P) [set f x] = f @` P. Proof. -apply eqEsubset=> a. -- by case=> i Pi ->; apply imageP. -- by case=> i Pi <-; exists i. +apply eqEsubset=> a; + by [case=> i Pi ->; apply imageP | case=> i Pi <-; exists i]. Qed. -Lemma bigcup0 (X : U -> set T) : bigsetU set0 X = set0. +Lemma bigcup_set0 (X : U -> set T) : \bigcup_(i in set0) X i = set0. Proof. by apply eqEsubset => a // [] //. Qed. -Lemma bigcup1 (i : U) (X : U -> set T) : bigsetU [set i] X = X i. -Proof. -apply eqEsubset => a. -- by case=> j ->. -- by exists i. -Qed. +Lemma bigcup_set1 (i : U) (X : U -> set T) : \bigcup_(i in [set i]) X i = X i. +Proof. apply eqEsubset => a; by [case=> j -> | exists i]. Qed. -Lemma bigcup_const (P : set U) (X : U -> set T) (i : U) : - P i -> (forall j, P j -> X j = X i) -> bigsetU P X = X i. +Lemma bigcup_image V (P : set V) (f : V -> U) (X : U -> set T) : + \bigcup_(x in f @` P) X x = \bigcup_(x in P) X (f x). Proof. -move=> Pi H; apply eqEsubset=> a. -- by case=> j /H ->. -- by exists i. +apply eqEsubset=> x. +- by case=> j [] i pi <- Xfix; exists i. +- by case=> i Pi Xfix; exists (f i); first by exists i. Qed. +Lemma bigcup_of_const (P : set U) (X : U -> set T) (i : U) : + P i -> (forall j, P j -> X j = X i) -> \bigcup_(j in P) X j = X i. +Proof. move=> Pi H; apply eqEsubset=> a; by [case=> j /H -> | exists i]. Qed. + Lemma bigsubsetU (P : set U) (X : U -> set T) (Y : set T) : (forall i, P i -> X i `<=` Y) <-> bigsetU P X `<=` Y. Proof. @@ -125,15 +124,11 @@ apply: (iffP idP). - by case=> i [] Si [] a Fia; apply/set0P; exists a, i. Qed. -Lemma bigcup_image V (P : set V) (f : V -> U) (X : U -> set T) : - \bigcup_(x in f @` P) X x = \bigcup_(x in P) X (f x). -Proof. -apply eqEsubset=> x. -- by case=> j [] i pi <- Xfix; exists i. -- by case=> i Pi Xfix; exists (f i); first by exists i. -Qed. - End PR_to_classical_sets. Notation imageA := (deprecate imageA image_comp _) (only parsing). Notation image_idfun := (deprecate image_idfun image_id _) (only parsing). +(*Notation bigcup_set1 := (deprecate bigcup_set1 bigcup_of_singleton _) (only parsing).*) +Notation bigcup0 := (deprecate bigcup0 bigcup_set0 _) (only parsing). +Notation bigcup1 := (deprecate bigcup1 bigcup_set1 _) (only parsing). +Notation bigcup_const := (deprecate bigcup_const bigcup_of_const _) (only parsing). diff --git a/lib/ssrR.v b/lib/ssrR.v index f897c1a6..fc3ef200 100644 --- a/lib/ssrR.v +++ b/lib/ssrR.v @@ -1,7 +1,8 @@ (* infotheo (c) AIST. R. Affeldt, M. Hagiwara, J. Senizergues. GNU GPLv3. *) (* infotheo v2 (c) AIST, Nagoya University. GNU GPLv3. *) -From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. +From mathcomp Require Import all_ssreflect. Require Import Reals. +From mathcomp Require Rstruct. (*****************************************************************************) (* SSReflect-like lemmas for Coq Reals *) @@ -59,6 +60,8 @@ Reserved Notation "a '>b' b" (at level 70). Reserved Notation "a ' /ltRP; [move/ltRW/Rmin_left|rewrite -leRNgt => /Rmin_right]. +Qed. + +Lemma maxRE x y : max(x, y) = if (x /ltRP; [move/ltRW/Rmax_right|rewrite -leRNgt => /Rmax_left]. +Qed. + +Lemma ltR_def x y : (x x x y /andP[/leRP xy /leRP yx]; rewrite eqR_le. Qed. + +Lemma leR_trans : transitive (fun x y => x z x y => /leRP xz /leRP zy; apply/leRP/(leR_trans xz). Qed. + +Lemma leR_total : forall x y, (x x y; case: (Rle_or_lt x y) => xy; apply/orP; + [left; exact/leRP|right; exact/leRP/ltRW]. +Qed. + +Definition orderMixin := + LeOrderMixin ltR_def minRE maxRE anti_leR leR_trans leR_total. + +End ROrder. + +Canonical porderType := POrderType ssrnum.ring_display R ROrder.orderMixin. +Canonical latticeType := LatticeType R ROrder.orderMixin. +Canonical distrLatticeType := DistrLatticeType R ROrder.orderMixin. +Canonical orderType := OrderType R ROrder.orderMixin. + Definition maxRA : associative Rmax := Rmax_assoc. Definition maxRC : commutative Rmax := Rmax_comm. Lemma maxRR : idempotent Rmax. Proof. move=> x; rewrite Rmax_left //; exact/leRR. Qed. -Definition leR_maxl m n : m <= Rmax m n := Rmax_l m n. -Definition leR_maxr m n : n <= Rmax m n := Rmax_r m n. -Definition geR_minl m n : Rmin m n <= m := Rmin_l m n. -Definition geR_minr m n : Rmin m n <= n := Rmin_r m n. +Definition leR_maxl m n : m <= max(m, n) := Rmax_l m n. +Definition leR_maxr m n : n <= max(m, n) := Rmax_r m n. +Definition geR_minl m n : min(m, n) <= m := Rmin_l m n. +Definition geR_minr m n : min(m, n) <= n := Rmin_r m n. -Lemma leR_max x y z : (Rmax y z <= x) <-> (y <= x) /\ (z <= x). +Lemma leR_max x y z : max(y, z) <= x <-> (y <= x) /\ (z <= x). Proof. split => [| [yx zx] ]. move/leRP; rewrite leR_eqVlt' => /orP[/eqP <-|/ltRP/Rmax_Rlt]. @@ -822,7 +867,7 @@ split => [| [yx zx] ]. rewrite -(Rmax_right _ _ yx); exact: Rle_max_compat_l. Qed. -Lemma leR_max' x y z : (Rmax y z [/leRP/leR_max[] /leRP -> /leRP -> //|]. case/andP=> /leRP ? /leRP ?; exact/leRP/leR_max. diff --git a/opam b/opam index 4d2d1130..0d8fbae6 100644 --- a/opam +++ b/opam @@ -25,9 +25,9 @@ install: [ [make "install"] ] depends: [ - "coq" {>= "8.10~"} - "coq-mathcomp-field" {>= "1.10.0"} - "coq-mathcomp-analysis" {(>= "0.2.0" & <= "0.2.3")} + "coq" {>= "8.10" & < "8.12~"} + "coq-mathcomp-field" {>= "1.11" & < "1.12~"} + "coq-mathcomp-analysis" {>= "0.3.1" & < "0.4~"} ] synopsis: "Infotheo" description: """ @@ -39,5 +39,5 @@ tags: [ "keyword: probability" "keyword: error-correcting codes" "logpath:infotheo" - "date:2020-03-21" + "date:2020-06-12" ] diff --git a/probability/fdist.v b/probability/fdist.v index e0bd8ed2..74b9d29c 100644 --- a/probability/fdist.v +++ b/probability/fdist.v @@ -1289,8 +1289,9 @@ have HB : \sum_(x in s) P `^ _ x <= INR #|s| * B. rewrite -big_filter /= big_const_seq /= iter_addR /=. apply leR_wpmul2r; first lra. apply Req_le. - rewrite filter_index_enum count_predT cardE; congr (INR (size _)). - apply eq_enum => i; by rewrite /in_mem /= andbC. + have [/= l el [ul ls] [pl sl]] := big_enumP _. + rewrite count_predT sl; congr (_%:R)%R. + by apply: eq_card => /= v; rewrite inE andbT. apply/(leR_trans _ HB)/Req_le/eq_bigl => i; by rewrite andbC. have HA : INR #|s| * A <= \sum_(x in s) P `^ _ x. have HA : INR #|s| * A <= \sum_(x in s | predT s) P `^ _ x. @@ -1299,8 +1300,9 @@ have HA : INR #|s| * A <= \sum_(x in s) P `^ _ x. rewrite -big_filter /= big_const_seq /= iter_addR /=. apply leR_wpmul2r; first lra. apply Req_le. - rewrite filter_index_enum count_predT cardE; congr (INR (size _)). - apply eq_enum => i; by rewrite /in_mem /= andbC. + have [/= l el [ul ls] [pl sl]] := big_enumP _. + rewrite count_predT sl; congr (_%:R)%R. + by apply: eq_card => /= v; rewrite inE andbT. apply/(leR_trans HA)/Req_le/eq_bigl => i; by rewrite andbC. split. - rewrite leR_pdivr_mulr //; move/leR_trans : Ha; exact. diff --git a/probability/necset.v b/probability/necset.v index dba4759d..9ab61adf 100644 --- a/probability/necset.v +++ b/probability/necset.v @@ -309,7 +309,8 @@ apply eqEsubset => u; rewrite conv_pt_setE. Qed. Lemma conv1_set X (Y : neset L) : X :<| 1%:pr |>: Y = X. Proof. -transitivity (\bigcup_(x in X) [set x]); last by rewrite bigcup_set1 image_id. +transitivity (\bigcup_(x in X) [set x]); last first. + by rewrite bigcup_of_singleton image_id. by congr bigsetU; apply funext => x /=; rewrite conv1_pt_set. Qed. Lemma conv0_set (X : neset L) Y : X :<| 0%:pr |>: Y = Y. @@ -327,7 +328,8 @@ Fixpoint iter_conv_set (X : set L) (n : nat) := end. Lemma iter0_conv_set (X : set L) : iter_conv_set X 0 = X. Proof. by []. Qed. -Lemma iterS_conv_set (X : set L) (n : nat) : iter_conv_set X (S n) = oplus_conv_set X (iter_conv_set X n). +Lemma iterS_conv_set (X : set L) (n : nat) : + iter_conv_set X (S n) = oplus_conv_set X (iter_conv_set X n). Proof. by []. Qed. Lemma probset_neq0 : probset != set0. Proof. by apply/set0P; exists 0%:pr. Qed. @@ -1070,9 +1072,9 @@ Definition pre_pre_conv (X Y : necset A) (p : prob) : set A := Lemma pre_pre_conv_convex X Y p : is_convex_set (pre_pre_conv X Y p). Proof. apply/asboolP => u v q. -rewrite -in_setE; rewrite inE => /asboolP [] x0 [] y0 [] x0X [] y0Y ->. -rewrite -in_setE; rewrite inE => /asboolP [] x1 [] y1 [] x1X [] y1Y ->. -rewrite -in_setE convACA inE asboolE. +rewrite -in_setE => /asboolP [] x0 [] y0 [] x0X [] y0Y ->. +rewrite -in_setE => /asboolP [] x1 [] y1 [] x1X [] y1Y ->. +rewrite -in_setE convACA asboolE. exists (x0 <|q|> x1), (y0 <|q|> y1). split; [exact: mem_convex_set | split; [exact: mem_convex_set | by []]]. Qed. @@ -1083,7 +1085,7 @@ Proof. case/set0P: (neset_neq0 X) => x; rewrite -in_setE => xX. case/set0P: (neset_neq0 Y) => y; rewrite -in_setE => yY. apply/set0P; exists (x <| p |> y); rewrite -in_setE. -by rewrite inE asboolE; exists x, y. +by rewrite asboolE; exists x, y. Qed. Definition conv p X Y : necset A := locked (NECSet.Pack (NECSet.Class (CSet.Class (pre_pre_conv_convex X Y p)) @@ -1116,11 +1118,11 @@ rewrite/conv; unlock; apply/necset_ext => /=; apply eqEsubset => a; case => x [] - move=> y [] xX []. rewrite in_setE => -[] y0 [] z0 [] y0Y [] z0Z -> ->. exists (x <| [r_of p, q] |> y0), z0. - by rewrite inE asboolE /= convA; split; try exists x, y0. + by rewrite asboolE /= convA; split; try exists x, y0. - move=> z []; rewrite in_setE => -[] x0 [] y [] x0X [] yY -> [] zZ ->. exists x0, (y <| q |> z). split => //. - by rewrite inE asboolE /= -convA; split; try exists y, z. + by rewrite asboolE /= -convA; split; try exists y, z. Qed. Definition mixin : ConvexSpace.mixin_of _ := @ConvexSpace.Mixin _ conv conv1 convmm convC convA. @@ -1147,15 +1149,20 @@ Module necset_semiCompSemiLattType. Section def. Local Open Scope classical_set_scope. Variable (A : convType). + Definition pre_op (X : neset (necset A)) : {convex_set A} := CSet.Pack (CSet.Class (hull_is_convex (bigsetU X idfun)%:ne)). + Lemma pre_op_neq0 X : pre_op X != set0 :> set _. Proof. by rewrite hull_eq0 neset_neq0. Qed. + Definition lub_necset (X : neset (necset A)) : necset A := NECSet.Pack (NECSet.Class (CSet.Class (hull_is_convex (bigsetU X idfun)%:ne)) (NESet.Mixin (pre_op_neq0 X))). + Lemma lub_necset1 x : lub_necset [set x]%:ne = x. -Proof. by apply necset_ext => /=; rewrite bigcup1 hull_cset. Qed. +Proof. by apply necset_ext => /=; rewrite bigcup_set1 hull_cset. Qed. + Lemma lub_necset_bigsetU (I : Type) (S : neset I) (F : I -> neset (necset A)) : lub_necset (bignesetU S F) = lub_necset (lub_necset @` (F @` S))%:ne. Proof. @@ -1175,11 +1182,15 @@ apply hull_eqEsubset => a. exists x0 => //; exists i => //. by rewrite Fiu. Qed. + Definition mixin := SemiCompleteSemiLattice.Mixin lub_necset1 lub_necset_bigsetU. + Definition class := SemiCompleteSemiLattice.Class mixin. + End def. End necset_semiCompSemiLattType. + Canonical necset_semiCompSemiLattType A := SemiCompleteSemiLattice.Pack (necset_semiCompSemiLattType.class A). @@ -1316,12 +1327,11 @@ apply neset_ext => /=. apply eqEsubset=> i /=. - move/set0P: (set1_neq0 x)=> Hx. move/set0P: (set1_neq0 y)=> Hy. - move/(@hull_setU _ _ (necset1 x) (necset1 y) Hx Hy)=> [] a. - rewrite inE=> /asboolP ->. - case=> b; rewrite inE=> /asboolP ->. + move/(@hull_setU _ _ (necset1 x) (necset1 y) Hx Hy)=> [] a /asboolP ->. + case=> b /asboolP ->. case=> p ->. by eexists. - case=> p ? <-. - by apply/mem_hull_setU. + exact/mem_hull_setU. Qed. End technical_corollaries.