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.

2 files changed, 32 insertions, 36 deletions

diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index ac785a3..699a1ba 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
-From mathcomp Require Import fintype div path bigop prime finset.
+From mathcomp Require Import fintype div path tuple bigop prime finset.
 
 (******************************************************************************)
 (* This file defines the main interface for finite groups :                   *)
@@ -858,14 +858,13 @@ Lemma prodsgP (I : finType) (P : pred I) (A : I -> {set gT}) x :
   reflect (exists2 c, forall i, P i -> c i \in A i & x = \prod_(i | P i) c i)
           (x \in \prod_(i | P i) A i).
 Proof.
-rewrite -big_filter filter_index_enum; set r := enum P.
-pose inA c := all (fun i => c i \in A i); set piAx := x \in _.
-suffices IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx.
-  apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_filter].
-    by move=> i Pi; rewrite (allP inAc) ?mem_enum.
-  by apply/allP=> i; rewrite mem_enum => /inAc.
-have: uniq r by rewrite enum_uniq.
-elim: {P}r x @piAx => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]].
+have [r big_r [Ur mem_r] _] := big_enumP P.
+pose inA c := all (fun i => c i \in A i); rewrite -big_r; set piAx := x \in _.
+suffices{big_r} IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx.
+  apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_r].
+    by move=> i Pi; rewrite (allP inAc) ?mem_r.
+  by apply/allP=> i; rewrite mem_r => /inAc.
+elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]].
   by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun=> x).
 rewrite big_cons; apply: (iffP idP) => [|[c /andP[Aci Ac] ->]]; last first.
   by rewrite big_cons mem_mulg //; apply/IHr=> //; exists c.
@@ -2174,19 +2173,14 @@ Lemma gen_prodgP A x :
 Proof.
 apply: (iffP idP) => [|[n [c Ac ->]]]; last first.
   by apply: group_prod => i _; rewrite mem_gen ?Ac.
-have [n ->] := gen_expgs A; rewrite /expgn /expgn_rec Monoid.iteropE.
-have ->: n = count 'I_n (index_enum _).
-  by rewrite -size_filter filter_index_enum -cardT card_ord.
-rewrite -big_const_seq; case/prodsgP=> /= c Ac def_x.
+have [n ->] := gen_expgs A; rewrite /expgn /expgn_rec Monoid.iteropE /=.
+rewrite -[n]card_ord -big_const => /prodsgP[/= c Ac def_x]. 
 have{Ac def_x} ->: x = \prod_(i | c i \in A) c i.
   rewrite big_mkcond {x}def_x; apply: eq_bigr => i _.
   by case/setU1P: (Ac i isT) => -> //; rewrite if_same.
-rewrite -big_filter; set e := filter _ _; case def_e: e => [|i e'].
-  by exists 0; exists (fun _ => 1) => [[] // |]; rewrite big_nil big_ord0.
-rewrite -{e'}def_e (big_nth i) big_mkord.
-exists (size e); exists (c \o nth i e \o val) => // j /=.
-have: nth i e j \in e by rewrite mem_nth.
-by rewrite mem_filter; case/andP.
+have [e <- [_ /= mem_e] _] := big_enumP [preim c of A].
+pose t := in_tuple e; rewrite -[e]/(val t) big_tuple.
+by exists (size e), (c \o tnth t) => // i; rewrite -mem_e mem_tnth.
 Qed.
 
 Lemma genD A B : A \subset <<A :\: B>> -> <<A :\: B>> = <<A>>.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 8357bc4..b1181c0 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -634,13 +634,13 @@ Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x :
     {in SimplPred P, forall i, x i \in A i} ->
   \prod_(i | P i) x i = \prod_(j | P (h j)) x (h j).
 Proof.
-case=> h1 hK h1K; rewrite -!(big_filter _ P) filter_index_enum => defG Ax.
-rewrite -(big_map h P x) -(big_filter _ P) filter_map filter_index_enum.
-apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_enum => /Ax.
-apply: uniq_perm (enum_uniq P) _ _ => [|i].
-  by apply/dinjectiveP; apply: (can_in_inj hK).
-rewrite mem_enum; apply/idP/imageP=> [Pi | [j Phj ->//]].
-by exists (h1 i); rewrite ?inE h1K.
+case=> h1 hK h1K defG Ax; have [e big_e [Ue mem_e] _] := big_enumP P.
+rewrite -!big_e in defG *; rewrite -(big_map h P x) -[RHS]big_filter filter_map.
+apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_e => /Ax.
+have [r _ [Ur /= mem_r] _] := big_enumP; apply: uniq_perm Ue _ _ => [|i].
+  by rewrite map_inj_in_uniq // => i j; rewrite !mem_r ; apply: (can_in_inj hK).
+rewrite mem_e; apply/idP/mapP=> [Pi|[j r_j ->]]; last by rewrite -mem_r.
+by exists (h1 i); rewrite ?mem_r h1K.
 Qed.
 
 (* Direct product *)
@@ -849,18 +849,20 @@ Lemma mem_bigdprod (I : finType) (P : pred I) F G x :
                 forall i, P i -> e i = c i].
 Proof.
 move=> defG; rewrite -(bigdprodW defG) => /prodsgP[c Fc ->].
-exists c; split=> // e Fe eq_ce i Pi.
-set r := index_enum _ in defG eq_ce.
-have: i \in r by rewrite -[r]enumT mem_enum.
-elim: r G defG eq_ce => // j r IHr G; rewrite !big_cons inE.
-case Pj: (P j); last by case: eqP (IHr G) => // eq_ij; rewrite eq_ij Pj in Pi.
-case/dprodP=> [[K H defK defH] _ _]; rewrite defK defH => tiFjH eq_ce.
-suffices{i Pi IHr} eq_cej: c j = e j.
-  case/predU1P=> [-> //|]; apply: IHr defH _.
+have [r big_r [_ mem_r] _] := big_enumP P.
+exists c; split=> // e Fe eq_ce i Pi; rewrite -!{}big_r in defG eq_ce.
+have{Pi}: i \in r by rewrite mem_r.
+have{mem_r}: all P r by apply/allP=> j; rewrite mem_r.
+elim: r G defG eq_ce => // j r IHr G.
+rewrite !big_cons inE /= => /dprodP[[K H defK defH] _ _].
+rewrite defK defH => tiFjH eq_ce /andP[Pj Pr].
+suffices{i IHr} eq_cej: c j = e j.
+  case/predU1P=> [-> //|]; apply: IHr defH _ Pr.
   by apply: (mulgI (c j)); rewrite eq_ce eq_cej.
 rewrite !(big_nth j) !big_mkord in defH eq_ce.
-move/(congr1 (divgr K H)) : eq_ce; move/bigdprodW: defH => defH.
-by rewrite !divgrMid // -?defK -?defH ?mem_prodg // => *; rewrite ?Fc ?Fe.
+move/(congr1 (divgr K H)): eq_ce; move/bigdprodW: defH => defH.
+move/(all_nthP j) in Pr.
+by rewrite !divgrMid // -?defK -?defH ?mem_prodg // => *; rewrite ?Fc ?Fe ?Pr.
 Qed.
 
 End InternalProd.