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, 22 insertions, 21 deletions

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 18fa55a..acafd8f 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -216,7 +216,8 @@ have FpxF q: Fpx (q ^ FtoL) = root (q ^ FtoL) x.
 pose p_ (I : {set 'I_n}) := \prod_(i <- enum I) ('X - (r`_i)%:P).
 have{px0 Dp} /ex_minset[I /minsetP[/andP[FpI pIx0] minI]]: exists I, Fpx (p_ I).
   exists setT; suffices ->: p_ setT = p ^ FtoL by rewrite FpxF.
-  by rewrite Dp (big_nth 0) big_mkord /p_ (eq_enum (in_set _)) big_filter.
+  rewrite Dp (big_nth 0) big_mkord /p_ big_enum /=.
+  by apply/eq_bigl=> i; rewrite inE.
 have{p} [p DpI]: {p | p_ I = p ^ FtoL}.
   exists (p_ I ^ (fun y => if isF y is left Fy then sval (sig_eqW Fy) else 0)).
   rewrite -map_poly_comp map_poly_id // => y /(allP FpI) /=.
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index d80a909..6e7432f 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -39,8 +39,9 @@ Proof. exact: monic_prod_XsubC. Qed.
 
 Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n).+1.
 Proof.
-rewrite /cyclotomic -big_filter filter_index_enum size_prod_XsubC; congr _.+1.
-rewrite -cardE -sum1_card totient_count_coprime -big_mkcond big_mkord.
+rewrite /cyclotomic -big_filter size_prod_XsubC; congr _.+1.
+case: big_enumP => _ _ _ [_ ->].
+rewrite totient_count_coprime -big_mkcond big_mkord -sum1_card.
 by apply: eq_bigl => k; rewrite coprime_sym.
 Qed.
 
@@ -63,14 +64,13 @@ Let n_gt0 := prim_order_gt0 prim_z.
 
 Lemma root_cyclotomic x : root (cyclotomic z n) x = n.-primitive_root x.
 Proof.
-rewrite /cyclotomic -big_filter filter_index_enum.
-rewrite -(big_map _ xpredT (fun y => 'X - y%:P)) root_prod_XsubC.
+transitivity (x \in [seq z ^+ i | i : 'I_n in [pred i : 'I_n | coprime i n]]).
+  by rewrite -root_prod_XsubC big_image.
 apply/imageP/idP=> [[k co_k_n ->] | prim_x].
   by rewrite prim_root_exp_coprime.
 have [k Dx] := prim_rootP prim_z (prim_expr_order prim_x).
-exists (Ordinal (ltn_pmod k n_gt0)) => /=.
-  by rewrite unfold_in /= coprime_modl -(prim_root_exp_coprime k prim_z) -Dx.
-by rewrite prim_expr_mod.
+exists (Ordinal (ltn_pmod k n_gt0)) => /=; last by rewrite prim_expr_mod.
+by rewrite inE coprime_modl -(prim_root_exp_coprime k prim_z) -Dx.
 Qed.
 
 Lemma prod_cyclotomic :
@@ -212,9 +212,7 @@ Proof.
 have [-> | n_gt0] := posnP n; first by rewrite Cyclotomic0 polyseq1.
 have [z prim_z] := C_prim_root_exists n_gt0.
 rewrite -(size_map_inj_poly (can_inj intCK)) //.
-rewrite (Cintr_Cyclotomic prim_z) -[_ n]big_filter filter_index_enum.
-rewrite size_prod_XsubC -cardE totient_count_coprime big_mkord -big_mkcond /=.
-by rewrite (eq_card (fun _ => coprime_sym _ _)) sum1_card.
+by rewrite (Cintr_Cyclotomic prim_z) size_cyclotomic.
 Qed.
 
 Lemma minCpoly_cyclotomic n z :
@@ -252,8 +250,8 @@ have [zk gzk0]: exists zk, root (pZtoC g) zk.
   by exists rg`_0; rewrite Dg root_prod_XsubC mem_nth.
 have [k cokn Dzk]: exists2 k, coprime k n & zk = z ^+ k.
   have: root pz zk by rewrite -Dpz -Dfg rmorphM rootM gzk0 orbT.
-  rewrite -[pz]big_filter -(big_map _ xpredT (fun a => 'X - a%:P)).
-  by rewrite root_prod_XsubC => /imageP[k]; exists k.
+  rewrite -[pz](big_image _ _ _ (fun r => 'X - r%:P)) root_prod_XsubC.
+  by case/imageP=> k; exists k.
 have co_fg (R : idomainType): n%:R != 0 :> R -> @coprimep R (intrp f) (intrp g).
   move=> nz_n; have: separable_poly (intrp ('X^n - 1) : {poly R}).
     by rewrite rmorphB rmorph1 /= map_polyXn separable_Xn_sub_1.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index b184ed7..19871cb 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -99,7 +99,7 @@ set n := #|F|; set oppX := - 'X; set pF := LHS.
 have le_oppX_n: size oppX <= n by rewrite size_opp size_polyX finRing_gt1.
 have: size pF = (size (enum F)).+1 by rewrite -cardE size_addl size_polyXn.
 move/all_roots_prod_XsubC->; last by rewrite uniq_rootsE enum_uniq.
-  by rewrite enumT lead_coefDl ?size_polyXn // lead_coefXn scale1r.
+  by rewrite big_enum lead_coefDl ?size_polyXn // lead_coefXn scale1r.
 by apply/allP=> x _; rewrite rootE !hornerE hornerXn expf_card subrr.
 Qed.
 
@@ -186,7 +186,7 @@ Canonical fieldExt_finFieldType fT := [finFieldType of fT].
 Lemma finField_splittingField_axiom fT : SplittingField.axiom fT.
 Proof.
 exists ('X^#|fT| - 'X); first by rewrite rpredB 1?rpredX ?polyOverX.
-exists (enum fT); first by rewrite enumT finField_genPoly eqpxx.
+exists (enum fT); first by rewrite big_enum finField_genPoly eqpxx.
 by apply/vspaceP=> x; rewrite memvf seqv_sub_adjoin ?mem_enum.
 Qed.
 
@@ -363,9 +363,10 @@ without loss {K} ->: K / K = 1%AS.
   by move=> IH_K; apply: galoisS (IH_K _ (erefl _)); rewrite sub1v subvf.
 apply/splitting_galoisField; pose finL := FinFieldExtType L.
 exists ('X^#|finL| - 'X); split; first by rewrite rpredB 1?rpredX ?polyOverX.
-  rewrite (finField_genPoly finL) -big_filter.
+  rewrite (finField_genPoly finL) -big_enum /=.
   by rewrite separable_prod_XsubC ?(enum_uniq finL).
-exists (enum finL); first by rewrite enumT (finField_genPoly finL) eqpxx.
+exists (enum finL).
+  by rewrite (@big_enum _ _ _ _ finL) (finField_genPoly finL) eqpxx.
 by apply/vspaceP=> x; rewrite memvf seqv_sub_adjoin ?(mem_enum finL).
 Qed.
 
@@ -390,7 +391,7 @@ have idfP x: reflect (f x = x) (x \in 1%VS).
     rewrite /q rmorphB /= map_polyXn map_polyX.
     by rewrite rootE !(hornerE, hornerXn) [x ^+ _]xFx subrr.
   have{q} ->: q = \prod_(z <- [seq b%:A | b : F]) ('X - z%:P).
-    rewrite /q finField_genPoly rmorph_prod big_map enumT.
+    rewrite /q finField_genPoly rmorph_prod big_image /=.
     by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC.
   by rewrite root_prod_XsubC => /mapP[a]; exists a.
 have fM: rmorphism f.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 4aaef57..72cd0df 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -448,14 +448,15 @@ pose mkf (z : L) := 'X - z%:P.
 exists (\prod_i \prod_(j < \dim {:L} | j < size (r i)) mkf (r i)`_j).
   apply: rpred_prod => i _; rewrite big_ord_narrow /= /r; case: sigW => rs /=.
   by rewrite (big_nth 0) big_mkord => /eqP <- {rs}; apply: minPolyOver.
-rewrite pair_big_dep /= -big_filter filter_index_enum -(big_map _ xpredT mkf).
+rewrite pair_big_dep /= -big_filter -(big_map _ xpredT mkf).
 set rF := map _ _; exists rF; first exact: eqpxx.
 apply/eqP; rewrite eqEsubv subvf -(span_basis (vbasisP {:L})).
 apply/span_subvP=> _ /tnthP[i ->]; set x := tnth _ i.
 have /tnthP[j ->]: x \in in_tuple (r i).
   by rewrite -root_prod_XsubC /r; case: sigW => _ /=/eqP<-; apply: root_minPoly.
-apply/seqv_sub_adjoin/imageP; rewrite (tnth_nth 0) /in_mem/=.
-by exists (i, widen_ord (sz_r i) j) => /=.
+apply/seqv_sub_adjoin/mapP; rewrite (tnth_nth 0).
+exists (i, widen_ord (sz_r i) j) => //.
+by rewrite mem_filter /= ltn_ord mem_index_enum.
 Qed.
 
 Fact regular_splittingAxiom F : SplittingField.axiom (regular_fieldExtType F).