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, 6 insertions, 6 deletions

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 (- _ + _).