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, 12 insertions, 9 deletions

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 38beffc..7e1dfbb 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -2091,7 +2091,7 @@ Lemma mxdirect_delta n f : {in P &, injective f} ->
 Proof.
 pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP.
 suffices /mxdirectP : mxdirect (\sum_i <<delta_mx 0 i : 'rV[F]_n>>).
-  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_filter.
+  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_enum.
   by move/mxdirectP; rewrite mxdirect_addsE => /andP[].
 apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)).
   apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 861a7df..c49bec0 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -307,16 +307,16 @@ Implicit Types p q : {poly R}.
 Definition char_poly_mx := 'X%:M - map_mx (@polyC R) A.
 Definition char_poly := \det char_poly_mx.
 
-Let diagA := [seq A i i | i : 'I_n].
+Let diagA := [seq A i i | i <- index_enum _ & true].
 Let size_diagA : size diagA = n.
-Proof. by rewrite size_image card_ord. Qed.
+Proof. by rewrite -[n]card_ord size_map; have [e _ _ []] := big_enumP. Qed.
 
 Let split_diagA :
   exists2 q, \prod_(x <- diagA) ('X - x%:P) + q = char_poly & size q <= n.-1.
 Proof.
 rewrite [char_poly](bigD1 1%g) //=; set q := \sum_(s | _) _; exists q.
-  congr (_ + _); rewrite odd_perm1 mul1r big_map enumT; apply: eq_bigr => i _.
-  by rewrite !mxE perm1 eqxx.
+  congr (_ + _); rewrite odd_perm1 mul1r big_map big_filter /=.
+  by apply: eq_bigr => i _; rewrite !mxE perm1 eqxx.
 apply: leq_trans {q}(size_sum _ _ _) _; apply/bigmax_leqP=> s nt_s.
 have{nt_s} [i nfix_i]: exists i, s i != i.
   apply/existsP; rewrite -negb_forall; apply: contra nt_s => s_1.
@@ -329,7 +329,7 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1).
     by rewrite -subn1 -addnS leq_subLR addnA leq_add.
   rewrite !mxE eq_sym !inE; case: (s j == j); first by rewrite polyseqXsubC.
   by rewrite sub0r size_opp size_polyC leq_b1.
-rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
+rewrite -[n in n.-1]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
 apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j.
 rewrite !inE -{1}fix_j (inj_eq perm_inj) orbb.
 by apply: contraNneq nfix_i => <-; rewrite fix_j.
@@ -354,7 +354,7 @@ Proof.
 move=> n_gt0; have [q <- lt_q_n] := split_diagA; set p := \prod_(x <- _) _.
 rewrite coefD {q lt_q_n}(nth_default 0 lt_q_n) addr0.
 have{n_gt0} ->: p`_n.-1 = ('X * p)`_n by rewrite coefXM eqn0Ngt n_gt0.
-have ->: \tr A = \sum_(x <- diagA) x by rewrite big_map enumT.
+have ->: \tr A = \sum_(x <- diagA) x by rewrite big_map big_filter.
 rewrite -size_diagA {}/p; elim: diagA => [|x d IHd].
   by rewrite !big_nil mulr1 coefX oppr0.
 rewrite !big_cons coefXM mulrBl coefB IHd opprD addrC; congr (- _ + _).
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 2bb3614..25037e8 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -922,7 +922,10 @@ by rewrite size_XsubC.
 Qed.
 
 Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
-Proof. by rewrite -[n]card_ord -prodr_const size_prod_XsubC cardE enumT. Qed.
+Proof.
+rewrite -[n]card_ord -prodr_const -big_filter size_prod_XsubC.
+by have [e _ _ [_ ->]] := big_enumP.
+Qed.
 
 (* Some facts about regular elements. *)
 
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 87ca0f4..1f8ad30 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1879,7 +1879,7 @@ Variable (K : fieldType) (vT : vectType K).
 Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
                   (defV : V = (\sum_(i | P i) Vs i)%VS) :
   v \in V -> \sum_(i | P i) sumv_pi_for defV i v = v :> vT.
-Proof. by apply: sumv_pi_uniq_sum; apply: enum_uniq. Qed.
+Proof. by apply: sumv_pi_uniq_sum; have [e _ []] := big_enumP. Qed.
 
 Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
                       (defV : V = (\sum_(m <= i < n | P i) Vs i)%VS) :