Explicit `bigop` enumeration handling

Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more
explicitly big ops iterating over explicit enumerations in a `finType`.
   The previous practice was to rely on the convertibility between
`enum A` and `filter A (index_enum T)`, sometimes explicitly via the
`filter_index_enum` equality, more often than not implicitly.
  Both are likely to fail after the integration of `finmap`, as the
`choiceType` theory can’t guarantee that the order in selected
enumerations is consistent.
  For this reason `big_enum` and the related (but currently unused)
`big_image` lemmas are restricted to the abelian case. The `big_enumP`
lemma can be used to handle enumerations in the non-abelian case, as
explained in the `bigop.v` internal documentation.
  The Changelog entry enjoins clients to stop relying on either
`filter_index_enum` and convertibility (though this PR still provides
both), and warns about the restriction of the `big_image` lemma set to
the abelian case, as it it a possible source of incompatibility.

1 files changed, 2 insertions, 2 deletions

diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index d3dfd38..c644150 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -481,7 +481,7 @@ Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) -> R) i :
   \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi
      = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j.
 Proof.
-move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_map big_filter /=.
+move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_image /=.
 by apply: eq_bigl => j; rewrite cfclass_IirrE.
 Qed.
 
@@ -1174,7 +1174,7 @@ have [inj_Mphi | /injectivePn[i [j i'j eq_mm_ij]]] := boolP (injectiveb mmLth).
   rewrite ['Ind phi]cfun_sum_cfdot sum_cfunE (bigID (mem (codom mmLth))) /=.
   rewrite ler_paddr ?sumr_ge0 // => [i _|].
     by rewrite char1_ge0 ?rpredZ_Cnat ?Cnat_cfdot_char ?cfInd_char ?irr_char.
-  rewrite -big_uniq //= big_map big_filter -sumr_const ler_sum // => i _.
+  rewrite -big_uniq //= big_image -sumr_const ler_sum // => i _.
   rewrite cfunE -[in rhs in _ <= rhs](cfRes1 L) -cfdot_Res_r mmLthL cfRes1.
   by rewrite DthL cfdotZr rmorph_nat cfnorm_irr mulr1.
 constructor 2; exists e; first by exists p0.