diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 17 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 22 |
2 files changed, 36 insertions, 3 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9108947..815d62a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -124,6 +124,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `root_mxminpoly`, and `mxminpoly_diag` - in `mxalgebra.v`, new lemma `sub_sums_genmxP` (generalizes `sub_sumsmxP`). +- in `bigop.v` new lemma `big_uncond`. The ideal name is `big_rmcond` + but it has just been deprecated from its previous meaning (see + Changed section) so as to reuse it in next mathcomp release. + +- in `bigop.v` new lemma `big_uncond_in` is a new alias of + `big_rmcond_in` for the sake of uniformity, but it is already + deprecated and will be removed two releases from now. + ### Changed - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 @@ -141,8 +149,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - The `dual_*` notations such as `dual_le` in order.v are now qualified with the `Order` module. +- Lemma `big_rmcond` is deprecated and has been renamed + `big_rmcomd_in` (and aliased `big_uncond_in`, see Added). The + variant which does not require an `eqType` is currently named + `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the + next release. + + ### Renamed +- `big_rmcond` -> `big_rmcond_in` (cf Changed section) + ### Removed ### Infrastructure diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 405ee08..6b26968 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1212,12 +1212,20 @@ Lemma big_mkcondl I r (P Q : pred I) F : \big[*%M/1]_(i <- r | Q i) (if P i then F i else 1). Proof. by rewrite big_andbC big_mkcondr. Qed. -Lemma big_rmcond (I : eqType) (r : seq I) (P : pred I) F : +Lemma big_uncond I (r : seq I) (P : pred I) F : + (forall i, ~~ P i -> F i = 1) -> + \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i. +Proof. +move=> F_eq1; rewrite big_mkcond; apply: eq_bigr => i. +by case: (P i) (F_eq1 i) => // ->. +Qed. + +Lemma big_rmcond_in (I : eqType) (r : seq I) (P : pred I) F : (forall i, i \in r -> ~~ P i -> F i = 1) -> \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i. Proof. -move=> Fidx; rewrite big_mkcond big_seq_cond [in RHS]big_seq_cond ?big_mkcondr. -by apply: eq_bigr => i /Fidx {Fidx}; case: (P i) => // ->. +move=> F_eq1; rewrite big_seq_cond [RHS]big_seq_cond !big_mkcondl big_uncond//. +by move=> i /F_eq1; case: ifP => // _ ->. Qed. Lemma big_cat I r1 r2 (P : pred I) F : @@ -1971,3 +1979,11 @@ Arguments biggcdn_inf [I] i0 [P F m]. Notation filter_index_enum := ((fun _ => @deprecated_filter_index_enum _) (deprecate filter_index_enum big_enumP)) (only parsing). + +Notation big_rmcond := + ((fun _ _ _ _ => @big_rmcond_in _ _ _ _) + (deprecate big_rmcond big_rmcond_in)) (only parsing). + +Notation big_uncond_in := + ((fun _ _ _ _ => @big_rmcond_in _ _ _ _) + (deprecate big_uncond_in big_rmcond_in)) (only parsing). |