From 4bd5ba38e4f6c6456a8fcc39364a67b51fde92f2 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Tue, 26 Nov 2019 17:28:36 +0100
Subject: 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.
---
 mathcomp/character/integral_char.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/character/integral_char.v')

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.
-- 
cgit v1.2.3