Merge pull request #605 from thery/bigop

Adding bigop lemmas for ring : expr_sum and prodr_natmul

3 files changed, 31 insertions, 8 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 251beb6..16ce76c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -46,7 +46,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `ssrnat.v`, new lemma: `oddS`
 - in `ssrnat.v`, new lemmas: `subnA`, `addnBn`, `addnCAC`, `addnACl`
 - in `finset.v`, new lemmas: `mem_imset_eq`, `mem_imset2_eq`.
-  These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become availabe (cf. Renamed section)
+  These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become available (cf. Renamed section)
 
 - Added a factory `distrLatticePOrderMixin` in order.v to build a
   `distrLatticeType` from a `porderType`.
@@ -237,6 +237,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   `comm_horner_mx2`, `horner_mx_stable`, `comm_mx_stable_kermxpoly`,
   and `comm_mx_stable_geigenspace`.
 
+- in `ssralg.v`: 
+   + Lemma `expr_sum` : equivalent for ring of `expn_sum`
+   + Lemma `prodr_natmul` : generalization of `prodrMn_const`.
+   Its name will become `prodrMn` in the next release when this name will become available (cf. Renamed section)
+
+
 ### Changed
 
 - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12
@@ -338,6 +344,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + `itv_gte` -> `itv_ge`
   + `l(t|e)r_in_itv` -> `lt_in_itv`
 
+- in `ssralg.v`
+  + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section)
+
 ### Removed
 
 - in `interval.v`, we remove the following:
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 3100697..5680a24 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1091,6 +1091,10 @@ Proof. by elim: m => [|m IHm]; rewrite ?mul1r // !exprS -mulrA -IHm. Qed.
 Lemma exprSr x n : x ^+ n.+1 = x ^+ n * x.
 Proof. by rewrite -addn1 exprD expr1. Qed.
 
+Lemma expr_sum x (I : Type) (s : seq I) (P : pred I) F : 
+  x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ F i :> R.
+Proof. exact: (big_morph _ (exprD _)). Qed.
+
 Lemma commr_sym x y : comm x y -> comm y x. Proof. by []. Qed.
 Lemma commr_refl x : comm x x. Proof. by []. Qed.
 
@@ -1273,13 +1277,18 @@ rewrite -sum1_card; elim/big_rec3: _ => [|i x n _ _ ->]; first by rewrite mulr1.
 by rewrite exprS !mulrA mulN1r !mulNr commrX //; apply: commrN1.
 Qed.
 
-Lemma prodrMn n (I : finType) (A : pred I) (F : I -> R) :
-  \prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
+Lemma prodr_natmul (I : Type) (s : seq I) (P : pred I) 
+              (F : I -> R) (g : I -> nat) : 
+  \prod_(i <- s | P i) (F i *+ g i) =
+  \prod_(i <- s | P i) (F i) *+ \prod_(i <- s | P i) g i.
 Proof.
-rewrite -sum1_card; elim/big_rec3: _ => // i x m _ _ ->.
-by rewrite mulrnAr mulrnAl expnS mulrnA.
+by elim/big_rec3: _ => // i y1 y2 y3 _ ->; rewrite mulrnAr mulrnAl -mulrnA.
 Qed.
 
+Lemma prodrMn_const n (I : finType) (A : pred I) (F : I -> R) :
+  \prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.
+Proof. by rewrite prodr_natmul prod_nat_const. Qed.
+
 Lemma natr_prod I r P (F : I -> nat) :
   (\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.
 Proof. exact: (big_morph _ natrM). Qed.
@@ -5667,6 +5676,7 @@ Definition expr0n := expr0n.
 Definition expr1n := expr1n.
 Definition exprD := exprD.
 Definition exprSr := exprSr.
+Definition expr_sum := expr_sum.
 Definition commr_sym := commr_sym.
 Definition commr_refl := commr_refl.
 Definition commr0 := commr0.
@@ -5758,7 +5768,8 @@ Definition exprMn := exprMn.
 Definition prodrXl := prodrXl.
 Definition prodrXr := prodrXr.
 Definition prodrN := prodrN.
-Definition prodrMn := prodrMn.
+Definition prodrMn_const := prodrMn_const.
+Definition prodr_natmul := prodr_natmul.
 Definition natr_prod := natr_prod.
 Definition prodr_undup_exp_count := prodr_undup_exp_count.
 Definition exprDn := exprDn.
@@ -6023,6 +6034,9 @@ Definition imaginary_exists := imaginary_exists.
 Notation null_fun V := (null_fun V) (only parsing).
 Notation in_alg A := (in_alg_loc A).
 
+Notation prodrMn :=
+ (fun n A F => deprecate prodrMn prodrMn_const _ n _ A F) (only parsing).
+
 End Theory.
 
 Notation in_alg A := (in_alg_loc A).
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 0244891..a2a2395 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3462,7 +3462,7 @@ have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0.
 apply/leifP; case: ifPn => [/forall_inP-Econstant | Enonconstant].
   have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0.
   have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const.
-  by rewrite exprMn_n prodrMn -(eq_bigr _ E_i) prodr_const.
+  by rewrite exprMn_n prodrMn_const -(eq_bigr _ E_i) prodr_const.
 set mu := \sum_(i in A) E i; pose En i := E i *+ n.
 pose cmp_mu s := [pred i | s * mu < s * En i].
 have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}.
@@ -3495,7 +3495,7 @@ have ->: \sum_(k in A') E' k = mu *+ n'.
   apply: (addrI mu); rewrite -mulrS -Dn -sumrMnl (bigD1 i Ai) big_andbC /=.
   rewrite !(bigD1 j A'j) /= addrCA eqxx !addrA subrK; congr (_ + _).
   by apply: eq_bigr => k /andP[_ /negPf->].
-rewrite prodrMn exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n').
+rewrite prodrMn_const exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n').
 have ->: \prod_(k in A') E' k = E' j * pi.
   by rewrite (bigD1 j) //=; congr *%R; apply: eq_bigr => k /andP[_ /negPf->].
 rewrite -(ler_pmul2l mu_gt0) -exprS -Dn mulrA; apply: lt_le_trans.