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.

4 files changed, 14 insertions, 16 deletions

diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index c35cdd6..3f461e3 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -528,8 +528,7 @@ Qed.
 Lemma cfun_on_sum A :
   'CF(G, A) = (\sum_(xG in classes G | xG \subset A) <['1_xG]>)%VS.
 Proof.
-rewrite ['CF(G, A)]span_def big_map big_filter.
-by apply: eq_bigl => xG; rewrite !inE.
+by rewrite ['CF(G, A)]span_def big_image; apply: eq_bigl => xG; rewrite !inE.
 Qed.
 
 Lemma cfun_onP A phi :
@@ -2047,15 +2046,14 @@ Lemma cfBigdprodEi i (phi : 'CF(A i)) x :
     P i -> (forall j, P j -> x j \in A j) ->
   cfBigdprodi phi (\prod_(j | P j) x j)%g = phi (x i).
 Proof.
-set r := enum P => Pi /forall_inP; have r_i: i \in r by rewrite mem_enum.
-have:= bigdprodWcp defG; rewrite -big_andE -!(big_filter _ P) filter_index_enum.
-rewrite -/r big_all => defGr /allP Ax.
-rewrite (perm_bigcprod defGr Ax (perm_to_rem r_i)) big_cons cfDprodEl ?Pi //.
-- by rewrite cfRes_id.
-- by rewrite Ax.
-rewrite big_seq group_prod // => j; rewrite mem_rem_uniq ?enum_uniq //.
-case/andP=> i'j /= r_j; apply/mem_gen/bigcupP; exists j; last exact: Ax.
-by rewrite -[P j](mem_enum P) r_j.
+have [r big_r [Ur mem_r] _] := big_enumP P => Pi AxP.
+have:= bigdprodWcp defG; rewrite -!big_r => defGr.
+have{AxP} [r_i Axr]: i \in r /\ {in r, forall j, x j \in A j}.
+  by split=> [|j]; rewrite mem_r // => /AxP.
+rewrite (perm_bigcprod defGr Axr (perm_to_rem r_i)) big_cons.
+rewrite cfDprodEl ?Pi ?cfRes_id ?Axr // big_seq group_prod // => j.
+rewrite mem_rem_uniq // => /andP[i'j /= r_j].
+by apply/mem_gen/bigcupP; exists j; [rewrite -mem_r r_j | apply: Axr].
 Qed.
 
 Lemma cfBigdprodi_iso i : P i -> isometry (@cfBigdprodi i).
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.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index c6d40e2..22bd171 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -56,7 +56,7 @@ have Q_Xn1: ('X^n - 1 : {poly Qn}) \is a polyOver 1%AS.
 have splitXn1: splittingFieldFor 1 ('X^n - 1) {:Qn}.
   pose r := codom (fun i : 'I_n => w ^+ i).
   have Dr: 'X^n - 1 = \prod_(y <- r) ('X - y%:P).
-    by rewrite -(factor_Xn_sub_1 prim_w) big_mkord big_map enumT.
+    by rewrite -(factor_Xn_sub_1 prim_w) big_mkord big_image.
   exists r; first by rewrite -Dr eqpxx.
   apply/eqP; rewrite eqEsubv subvf -genQn adjoin_seqSr //; apply/allP=> /=.
   by rewrite andbT -root_prod_XsubC -Dr; apply/unity_rootP/prim_expr_order.
@@ -657,7 +657,7 @@ have Qpi1: pi1 \in Crat.
     have /vlineP[q ->] := mem_galNorm galQn (memvf a).
     by rewrite rmorphZ_num rmorph1 mulr1 Crat_rat.
   rewrite /galNorm rmorph_prod -/calG imItoQ big_imset //=.
-  rewrite /pi1 -(eq_bigl _ _ imItoS) -big_uniq // big_map big_filter /=.
+  rewrite /pi1 -(eq_bigl _ _ imItoS) -big_uniq // big_image /=.
   apply: eq_bigr => k _; have [nuC DnuC] := gQnC (ItoQ k); rewrite DnuC Da.
   have [r ->] := char_sum_irr Nchi; rewrite !sum_cfunE rmorph_sum.
   apply: eq_bigr => i _; have /QnGg[b Db] := irr_char i.
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 4a113b6..72bacc3 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -464,7 +464,7 @@ Proof.
 move=> Zphi def_n lt_n_4.
 pose S := [seq '[phi, 'chi_i] *: 'chi_i | i in irr_constt phi].
 have def_phi: phi = \sum_(xi <- S) xi.
-  rewrite big_map /= big_filter big_mkcond {1}[phi]cfun_sum_cfdot.
+  rewrite big_image big_mkcond {1}[phi]cfun_sum_cfdot.
   by apply: eq_bigr => i _; rewrite if_neg; case: eqP => // ->; rewrite scale0r.
 have orthS: orthonormal S.
   apply/orthonormalP; split=> [|_ _ /mapP[i phi_i ->] /mapP[j _ ->]].