Merge pull request #77 from affeldt-aist/renaming_20211227

fixes #74

changelog.txt

@@ -10,6 +10,10 @@ from 0.3.4 to ?.?.?
 * renamed:
 - in ssrR.v
   + subr_le0 -> subR_le0
+- in reals_ext.v
+  + pos_ffun -> nneg_finfun
+  + pos_ff_ge0 -> nneg_finfun_ge0
+  + pos_fun -> nneg_fun
 * changed:
 - row_nth moved and renamed to bitseq_row_nth
 * removed:

ecc_classic/bch.v

@@ -465,16 +465,14 @@ Lemma BCH_key_equation_old (y : 'rV[F]_n) : a ^+ n = 1 ->
 Proof.
 move=> an1.
 rewrite dftE big_distrr /=.
-evar (tmp : 'I_n -> {poly F}).
-rewrite (eq_bigr (fun i => tmp i)); last first.
+under eq_bigr.
   move=> i ie.
   rewrite -scalerAr.
   rewrite (_ : \sigma_(rVexp a n, y) =
     \sigma_(rVexp a n, y, i) * (1 - ((rVexp a n) ``_ i) *: 'X)); last first.
     rewrite /errloc (bigD1 i) //= mulrC; congr (_ * _).
     apply eq_bigl => ij; by rewrite in_setD1 andbC.
-  rewrite /tmp; reflexivity.
-rewrite {}/tmp.
+  over.
 transitivity (\sum_(i in supp y) y ``_ i *:
      (\sigma_(rVexp a n, y, i) * (1 - a ^+ (i * n) *: 'X^n))).
   apply eq_bigr => /= i ie; congr (_ *: _).

ecc_classic/decoding.v

@@ -341,7 +341,7 @@ simpl in H.
 set tmp := \rmax_(_ <- _ | _) _ in H.
 rewrite /tmp in H.
 evar (h : 'rV[A]_n -> R); rewrite (eq_bigr h) in H; last first.
-  move=> v vC; rewrite ffunE /h; reflexivity.
+  by move=> v vC; rewrite ffunE /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.
@@ -360,8 +360,8 @@ have x0 : / x <> 0 by apply/eqP/invR_neq0'; rewrite -receivableE Receivable.defE
 move/(eqR_mul2r x0) in H.
 rewrite /= UniformSupport.dET ?inE // in H; last first.
   move/subsetP : dec_img; apply.
-  rewrite inE; apply/existsP; by exists (Receivable.y tb); apply/eqP.
-move/eqR_mul2l :  H => -> //; exact/eqP/gtR_eqF.
+  by rewrite inE; apply/existsP; exists (Receivable.y tb); apply/eqP.
+by move/eqR_mul2l :  H => -> //; exact/eqP/gtR_eqF.
 Qed.
 
 End MAP_decoding_prop.

ecc_classic/reed_solomon.v

@@ -170,9 +170,9 @@ rewrite (bigD1 i') //= coefXn insubT //= => Hj.
 rewrite eqxx mulr1 (_ : Ordinal Hj = j); last by apply val_inj.
 rewrite mxE inordK; last by rewrite ltnS (leq_trans (ltn_ord i)).
 rewrite mulrC; apply/eqP.
-  rewrite addrC -subr_eq subrr; apply/eqP/esym.
+rewrite addrC -subr_eq subrr; apply/eqP/esym.
 rewrite big1 // => k ki'; rewrite coefXn (_ : (_ == _) = false) ?mulr0 //.
-apply: contraNF ki'; by rewrite -val_eqE /= eq_sym.
+by apply: contraNF ki'; rewrite -val_eqE /= eq_sym.
 Qed.
 
 Lemma codebook_syndrome (c : 'rV_n) :
@@ -859,13 +859,12 @@ suff H : size (rVpoly (encoder m - c)) <= d.
     case: (RS.addr_closed a n' d) => _.
     move/(_ _ (- c) Hencm); apply.
     by rewrite RS.oppr_closed.
-  case/(@RS.deg_lb _ a _ _ dn a_neq0 a_not_uroot_on)/orP => [/eqP -> | ].
+  case/(@RS.deg_lb _ a _ _ dn a_neq0 a_not_uroot_on)/orP => [/eqP ->|].
     apply/eqP/polyP => i.
     rewrite coef_poly coef0.
     case: ifP => // _.
-    case: (insub i) => // ?; by rewrite mxE.
-  move=> H'.
-  by move: (leq_trans H' H); rewrite ltnn.
+    by case: (insub i) => // ?; rewrite mxE.
+  by move=> /leq_trans/(_ H); rewrite ltnn.
 rewrite /encoder ffunE linearB /= poly_rV_K; last first.
   rewrite (leq_trans (size_add _ _)) // geq_max.
   apply/andP; split.
@@ -892,11 +891,12 @@ rewrite /RS_discard -/(high c); apply RS_enc_surjective.
 by rewrite -RS.lcode0_codebook // ?inE.
 Qed.
 
-Definition RS_as_lcode (an1 : a ^+ n = 1) (Hchar : ([char F]^').-nat n) : Lcode.t _ _ _ [finType of 'rV_(n - d.+1).+1] :=
- @Lcode.mk _ _ _ _ _
-   (Encoder.mk RS_enc_injective RS_enc_img)
-   (Decoder.mk (RS_repair_img an1 Hchar) RS_discard)
-   RS_enc_discard_is_id.
+Definition RS_as_lcode (an1 : a ^+ n = 1) (Hchar : ([char F]^').-nat n) :
+  Lcode.t _ _ _ [finType of 'rV_(n - d.+1).+1] :=
+    @Lcode.mk _ _ _ _ _
+      (Encoder.mk RS_enc_injective RS_enc_img)
+      (Decoder.mk (RS_repair_img an1 Hchar) RS_discard)
+      RS_enc_discard_is_id.
 
 End RS_encoder_sect.
 
@@ -931,8 +931,7 @@ Local Open Scope cyclic_code_scope.
 
 Lemma rs_gen_is_gen : poly_rV \gen_(a, d) \in 'cgen[Ccode.mk RS_cyclic].
 Proof.
-apply pgen_is_cgen => /=.
-  exact: RS_not_trivial.
+apply pgen_is_cgen => /=; first exact: RS_not_trivial.
 apply/forallP => /= p; apply/eqP; apply/idP/idP.
   move=> Hp.
   move: (proj1 (rs_genP dn a0 (prim_root_not_uroot_on an) p)).
@@ -947,8 +946,7 @@ rewrite -(@RS.codebook_syndrome _ a n' d) //.
 apply: (proj2 (rs_genP dn a0 (prim_root_not_uroot_on an) p)).
 rewrite poly_rV_K // ?size_rs_gen // in Hp.
 case/dvdpP : Hp => x Hx.
-exists x; split => //.
-by apply: RS_message_size Hx.
+by exists x; split => //; exact: RS_message_size Hx.
 Qed.
 
 End RS_cyclic.

ecc_modern/degree_profile.v

@@ -710,9 +710,8 @@ Proof. rewrite ffunE; apply RofKpos, f0. Qed.
 
 Lemma f1R l : (\sum_(t : @fintree tw l) [ffun x => RofK (@fintree_dist l x)] t = 1)%R.
 Proof.
-evar (h : fintree_finType tw l -> R); rewrite (eq_bigr h); last first.
-  move=> i _; rewrite ffunE /h; reflexivity.
-by rewrite {}/h -(@big_morph _ _ RofK 0%R Rplus 0%:R (@GRing.add K)) // f1 RofK1.
+under eq_bigr do rewrite ffunE /=.
+by rewrite -(@big_morph _ _ RofK 0%R Rplus 0%:R (@GRing.add K)) // f1 RofK1.
 Qed.
 
 Definition tree_ensemble l : ensemble tw l := FDist.make (@f0R l) (@f1R l).

information_theory/channel.v

@@ -181,10 +181,9 @@ Lemma f0 (b : B) : 0 <= f b.
 Proof. by rewrite ffunE; apply: sumR_ge0 => a _; exact: mulR_ge0. Qed.
 Lemma f1 : \sum_(b in B) f b = 1.
 Proof.
-rewrite /f; evar (h : B -> R); rewrite (eq_bigr h); last first.
-  move=> a _; rewrite ffunE /h; reflexivity.
-rewrite {}/h exchange_big /= -(FDist.f1 P).
-apply eq_bigr => a _; by rewrite -big_distrl /= (FDist.f1 (W a)) mul1R.
+under eq_bigr do rewrite ffunE /=.
+rewrite exchange_big /= -(FDist.f1 P).
+by apply eq_bigr => a _; rewrite -big_distrl /= (FDist.f1 (W a)) mul1R.
 Qed.
 Definition d : fdist B := locked (FDist.make f0 f1).
 Lemma dE b : d b = \sum_(a in A) W a b * P a.

information_theory/channel_coding_direct.v

@@ -1,5 +1,5 @@
-(* infotheo: information theory and error-correcting codes in Coq               *)
-(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later              *)
+(* infotheo: information theory and error-correcting codes in Coq             *)
+(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix perm.
 Require Import Reals Lra Classical.
 From mathcomp Require Import Rstruct.
@@ -41,11 +41,10 @@ Definition f := [ffun g : encT A M n => \prod_(m in M) P `^ n (g m)].
 Lemma f0 g : 0 <= f g. Proof. rewrite ffunE; exact: prodR_ge0. Qed.
 Lemma f1 : \sum_(g in {ffun M -> 'rV[A]_n}) f g = 1.
 Proof.
-rewrite /f; evar (h : {ffun M -> 'rV[A]_n} -> R); rewrite (eq_bigr h); last first.
-  move=> a _; rewrite ffunE /h; reflexivity.
-rewrite {}/h -(bigA_distr_bigA (fun _ v => P `^ n v)) /=.
+under eq_bigr do rewrite ffunE /=.
+rewrite -(bigA_distr_bigA (fun _ v => P `^ n v)) /=.
 rewrite [RHS](_ : _ = \prod_(m0 : M | xpredT m0) 1); last by rewrite big1.
-apply eq_bigr => _ _; by rewrite (FDist.f1 (P `^ n)).
+by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)).
 Qed.
 Definition d : {fdist encT A M n} := locked (FDist.make f0 f1).
 Lemma dE x : d x = f x. Proof. by rewrite /d; unlock; rewrite ffunE. Qed.

information_theory/conditional_divergence.v

@@ -126,9 +126,8 @@ move=> PQ.
 rewrite /cre cdiv_is_div_joint_dist; last first.
   by apply/dom_by_cdom_by; rewrite /JointFDistChan.d; unlock.
 rewrite /div.
-evar (f : A -> Rdefinitions.R); rewrite (eq_bigr f); last first.
-  move=> b _; rewrite big_distrr /= /f; reflexivity.
-rewrite {}/f pair_big /=; apply eq_bigr => -[a b] _ /=.
+under eq_bigr do rewrite big_distrr /=.
+rewrite pair_big /=; apply eq_bigr => -[a b] _ /=.
 rewrite (_ : JointFDistChan.d R P (a, b) = (CJFDist.joint_of P) (a, b)); last first.
   by rewrite JointFDistChan.dE ProdFDist.dE.
 rewrite (_ : JointFDistChan.d R Q (a, b) = (CJFDist.joint_of Q) (a, b)); last first.
@@ -147,10 +146,10 @@ rewrite !Swap.snd.
 case/boolP : (CJFDist.joint_of Q (a, b) == 0) => [/eqP|] H'.
   have : (CJFDist.joint_of P) (a, b) = 0 by move/dominatesP : PQ => ->.
   rewrite /P ProdFDist.dE /= mulR_eq0 => -[| -> ].
-    move/eqP : H; tauto.
+    by move/eqP : H; tauto.
   by rewrite !(mulR0,mul0R,div0R).
 rewrite 2!ProdFDist.fst /=; field.
-split; exact/eqP.
+by split; exact/eqP.
 Qed.
 
 End conditional_divergence_vs_conditional_relative_entropy.

information_theory/convex_fdist.v

@@ -55,25 +55,22 @@ Lemma entropy_log_div : entropy p = log #|A|%:R - D(p || u).
 Proof.
 rewrite /entropy /div.
 evar (RHS : A -> R).
-have H : forall a : A, p a * log (p a / u a) = RHS a.
-  move => a.
-  move : (pos_ff_ge0 p a) => [H|H].
+have H a : p a * log (p a / u a) = RHS a.
+  case : (nneg_finfun_ge0 p a) => H.
   - rewrite Uniform.dE.
     change (p a * log (p a / / #|A|%:R)) with (p a * log (p a * / / #|A|%:R)).
     have H0 : 0 < #|A|%:R by rewrite A_not_empty ltR0n.
     have /eqP H1 : #|A|%:R <> 0 by apply/eqP/gtR_eqF.
     rewrite invRK // logM // mulRDr.
     by instantiate (RHS := fun a => p a * log (p a) + p a * log #|A|%:R).
   - by rewrite /RHS -H /= 3!mul0R add0R.
-have H0 : \sum_(a in A) p a * log (p a / u a) = \sum_(a in A) RHS a.
-  move : H; rewrite /RHS => H.
-  exact: eq_bigr.
-rewrite H0 /RHS big_split /= -big_distrl /= (FDist.f1 p) mul1R.
+have -> : \sum_(a in A) p a * log (p a / u a) = \sum_(a in A) RHS a.
+  by move : H; rewrite /RHS => H; exact: eq_bigr.
+rewrite /RHS big_split /= -big_distrl /= (FDist.f1 p) mul1R.
 by rewrite -addR_opp oppRD addRC -addRA Rplus_opp_l addR0.
 Qed.
 End entropy_log_div.
 
-(* convexity of relative entropy *)
 Section dominated_pair.
 Variable A : finType.
 Implicit Types p q : prob.
@@ -153,7 +150,7 @@ have h0 p1 p2 : [forall i, 0 <b= h p1 p2 i].
   case: ifPn => [_ | _]; first exact/mulR_ge0.
   case: ifPn => [_ |  _]; [|exact/leRR].
   by apply/mulR_ge0 => //; exact/onem_ge0/prob_le1.
-move: (log_sum setT (mkPosFfun (h0 x.1 y.1)) (mkPosFfun (h0 x.2 y.2)) hdom).
+move: (log_sum setT (mkNNFinfun (h0 x.1 y.1)) (mkNNFinfun (h0 x.2 y.2)) hdom).
 rewrite /= -!sumR_ord_setT !big_ord_recl !big_ord0 !addR0.
 rewrite /h /= !ffunE => /leR_trans; apply.
 rewrite !eqxx eq_sym (negbTE (neq_lift ord0 ord0)).

information_theory/jtypes.v

@@ -91,15 +91,15 @@ Qed.
 Definition jtype_eqMixin A B n := EqMixin (@jtype_eqP A B n).
 Canonical jtype_eqType A B n := Eval hnf in EqType _ (@jtype_eqMixin A B n).
 
-Definition pos_fun_of_pre_jtype (A B : finType) (Bnot0 : (0 < #|B|)%nat) n
-  (f : {ffun A -> {ffun B -> 'I_n.+1}}) : A -> pos_ffun B.
+Definition nneg_fun_of_pre_jtype (A B : finType) (Bnot0 : (0 < #|B|)%nat) n
+  (f : {ffun A -> {ffun B -> 'I_n.+1}}) : A -> nneg_finfun B.
 pose pf := fun a => [ffun b : B =>
   let ln := (\sum_(b1 in B) (f a b1))%nat in
   if ln == O
     then / #|B|%:R
     else (f a b)%:R / ln%:R].
 move=> a.
-refine (@mkPosFfun _ (pf a) _); apply/forallP_leRP => b.
+refine (@mkNNFinfun _ (pf a) _); apply/forallP_leRP => b.
 rewrite /pf ffunE.
 case: ifP => [_ | Hcase].
 - exact/invR_ge0/ltR0n.
@@ -115,10 +115,8 @@ set pf := fun a b =>
   then / #|B|%:R
   else (f a b)%:R / ln%:R.
 refine (@Channel1.mkChan A B _ Anot0) => a.
-apply: (@FDist.mk _ (@pos_fun_of_pre_jtype _ _ Bnot0 n f a)).
-rewrite /=; evar (h : B -> R); rewrite (eq_bigr h); last first.
-  move=> b _; rewrite ffunE /h; reflexivity.
-rewrite {}/h.
+apply: (@FDist.mk _ (@nneg_fun_of_pre_jtype _ _ Bnot0 n f a)).
+under eq_bigr do rewrite ffunE /=.
 case/boolP : (\sum_(b1 in B) (f a b1) == O)%nat => Hcase.
 - by rewrite /Rle big_const iter_addR mulRV // INR_eq0' -lt0n.
 - rewrite big_morph_natRD /Rdiv -big_distrl /= mulRV //.
@@ -653,9 +651,8 @@ have d0 : forall b, (0 <= d b)%R.
   apply mulR_ge0; first exact/leR0n.
   apply/invR_ge0/ltR0n; by rewrite lt0n.
 have d1 : (\sum_(b : B) d b)%R = 1%R.
-  rewrite /=; evar (h : B -> R); rewrite (eq_bigr h); last first.
-    move=> b _; rewrite ffunE /h; reflexivity.
-  rewrite {}/h -big_distrl /= -big_morph_natRD.
+  under eq_bigr do rewrite ffunE /=.
+  rewrite -big_distrl /= -big_morph_natRD.
   set lhs := \sum_i _.
   suff -> : lhs = N(a | ta) by rewrite mulRV // INR_eq0'.
   rewrite /lhs /f /= -[in X in _ = X](Hrow_num_occ Hta a).
@@ -1110,10 +1107,9 @@ Proof. rewrite ffunE; apply divR_ge0; [exact/leR0n | exact/ltR0n]. Qed.
 
 Lemma f1 : (\sum_(b in B) f b = 1)%R.
 Proof.
-rewrite /f; evar (h : B -> R); rewrite (eq_bigr h); last first.
-  move=> b _; rewrite ffunE /h; reflexivity.
-rewrite {}/h -big_distrl /= -big_morph_natRD exchange_big /=.
-move/eqP : (JType.sum_f V) => ->; by rewrite mulRV // INR_eq0'.
+under eq_bigr do rewrite ffunE /=.
+rewrite -big_distrl /= -big_morph_natRD exchange_big /=.
+by move/eqP : (JType.sum_f V) => ->; rewrite mulRV // INR_eq0'.
 Qed.
 
 Definition d : fdist B := FDist.make f0 f1.

information_theory/pproba.v

@@ -123,9 +123,8 @@ Qed.
 
 Lemma f1 : \sum_(x in 'rV_n) f x = 1.
 Proof.
-rewrite /f /Rdiv; evar (h : 'rV[A]_n -> R); rewrite (eq_bigr h); last first.
-  move=> a _; rewrite ffunE /h; reflexivity.
-by rewrite {}/h -big_distrl /= mulRC mulVR // -receivableE Receivable.defE.
+under eq_bigr do rewrite ffunE /=.
+by rewrite -big_distrl /= mulRC mulVR // -receivableE Receivable.defE.
 Qed.
 
 Definition d : {fdist 'rV[A]_n} := locked (FDist.make f0 f1).
@@ -203,10 +202,8 @@ Definition Kmpp : R := / \sum_(t in 'rV_n) f' t.
 
 Lemma f'_neq0 : \sum_(t in 'rV_n) f' t <> 0.
 Proof.
-evar (x : 'rV[A]_n -> R).
-rewrite (eq_bigr x); last first.
-  move=> i _; rewrite /f' PosteriorProbability.dE /Rdiv /x; reflexivity.
-rewrite -big_distrl { x} /= mulR_eq0 => -[/eqP|].
+under eq_bigr do rewrite /f' PosteriorProbability.dE /Rdiv.
+rewrite -big_distrl /= mulR_eq0 => -[/eqP|].
 - by apply/negP; rewrite -receivableE Receivable.defE.
 - by apply/invR_neq0/eqP; rewrite -receivableE Receivable.defE.
 Qed.
@@ -225,9 +222,8 @@ Qed.
 
 Lemma f1 i : \sum_(a in A) f i a = 1.
 Proof.
-rewrite /f; evar (h : A -> R); rewrite (eq_bigr h); last first.
-  move=> a _; rewrite ffunE /h; reflexivity.
-rewrite {}/h -big_distrr /= /Kmpp.
+under eq_bigr do rewrite ffunE /=.
+rewrite -big_distrr /= /Kmpp.
 set tmp1 := \sum_( _ | _ ) _.
 set tmp2 := \sum_( _ | _ ) _.
 suff : tmp1 = tmp2.

information_theory/shannon_fano.v

@@ -127,10 +127,8 @@ apply (@ltR_leR_trans (\sum_(x in A) P x * (- Log #|T|%:R (P x) + 1))).
     by rewrite -(Log_1 2); apply Log_increasing_le.
   case: (ceilP x) => _.
   by rewrite -LogV // -/(log _) -(div1R _) /x.
-evar (h : A -> R).
-rewrite (eq_bigr h); last first.
-  move=> i _; rewrite mulRDr mulR1 mulRN  /h; reflexivity.
-rewrite {}/h big_split /= FDist.f1 leR_add2r.
+under eq_bigr do rewrite mulRDr mulR1 mulRN.
+rewrite big_split /= FDist.f1 leR_add2r.
 apply Req_le.
 rewrite /entropy big_morph_oppR; apply eq_bigr => i _.
 by rewrite card_ord (_ : 2%:R = 2).