diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 13 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 5 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 2 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 20 | ||||
| -rw-r--r-- | mathcomp/character/inertia.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/integral_char.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/vcharacter.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 22 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 11 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 7 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 32 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 36 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 191 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 4 |
17 files changed, 224 insertions, 146 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fb9381f..5b42377 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,9 +36,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `eq_enum_rank_in`, `enum_rank_in_inj`, `lshift_inj`, and `rshift_inj`. -- Bigop theorems: `big_rmcond`, `bigD1_seq`, +- Bigop theorems: `index_enum_uniq`, `big_rmcond`, `bigD1_seq`, `big_enum_val_cond`, `big_enum_rank_cond`, - `big_enum_val`, `big_enum_rank`, `big_set`. + `big_enum_val`, `big_enum_rank`, `big_set`, + `big_enumP`, `big_enum_cond`, `big_enum` - Arithmetic theorems in ssrnat and div: - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`, @@ -101,7 +102,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`, ...., (see above). The new idiom is documented in `ssrnat`. - This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release. + This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release (see [PR #434](https://github.com/math-comp/math-comp/pull/434) for examples). + + - Replaced the use of the accidental convertibility between `enum A` and + `filter A (index_enum T)` with more explicit lemmas `big_enumP`, `big_enum`, `big_enum_cond`, `big_image` added to the `bigop` library, and deprecated the `filter_index_enum` lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future `mathcomp` releases when sets over `finType`s are generalised to finite sets over `choiceType`s, so client libraries should stop relying on this identity. File `bigop.v` has some boilerplate to help with the port; also see [PR #441](https://github.com/math-comp/math-comp/pull/441) for examples. + + - Restricted `big_image`, `big_image_cond`, `big_image_id` and `big_image_cond_id` + to `bigop`s over _abelian_ monoids, anticipating the change in the definition of `enum`. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of `big_map` and `big_enumP`. - `eqVneq` lemma is changed from `{x = y} + {x != y}` to `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs 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) : diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index c35cdd6..3f461e3 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -528,8 +528,7 @@ Qed. Lemma cfun_on_sum A : 'CF(G, A) = (\sum_(xG in classes G | xG \subset A) <['1_xG]>)%VS. Proof. -rewrite ['CF(G, A)]span_def big_map big_filter. -by apply: eq_bigl => xG; rewrite !inE. +by rewrite ['CF(G, A)]span_def big_image; apply: eq_bigl => xG; rewrite !inE. Qed. Lemma cfun_onP A phi : @@ -2047,15 +2046,14 @@ Lemma cfBigdprodEi i (phi : 'CF(A i)) x : P i -> (forall j, P j -> x j \in A j) -> cfBigdprodi phi (\prod_(j | P j) x j)%g = phi (x i). Proof. -set r := enum P => Pi /forall_inP; have r_i: i \in r by rewrite mem_enum. -have:= bigdprodWcp defG; rewrite -big_andE -!(big_filter _ P) filter_index_enum. -rewrite -/r big_all => defGr /allP Ax. -rewrite (perm_bigcprod defGr Ax (perm_to_rem r_i)) big_cons cfDprodEl ?Pi //. -- by rewrite cfRes_id. -- by rewrite Ax. -rewrite big_seq group_prod // => j; rewrite mem_rem_uniq ?enum_uniq //. -case/andP=> i'j /= r_j; apply/mem_gen/bigcupP; exists j; last exact: Ax. -by rewrite -[P j](mem_enum P) r_j. +have [r big_r [Ur mem_r] _] := big_enumP P => Pi AxP. +have:= bigdprodWcp defG; rewrite -!big_r => defGr. +have{AxP} [r_i Axr]: i \in r /\ {in r, forall j, x j \in A j}. + by split=> [|j]; rewrite mem_r // => /AxP. +rewrite (perm_bigcprod defGr Axr (perm_to_rem r_i)) big_cons. +rewrite cfDprodEl ?Pi ?cfRes_id ?Axr // big_seq group_prod // => j. +rewrite mem_rem_uniq // => /andP[i'j /= r_j]. +by apply/mem_gen/bigcupP; exists j; [rewrite -mem_r r_j | apply: Axr]. Qed. Lemma cfBigdprodi_iso i : P i -> isometry (@cfBigdprodi i). diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index d3dfd38..c644150 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -481,7 +481,7 @@ Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) -> R) i : \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j. Proof. -move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_map big_filter /=. +move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_image /=. by apply: eq_bigl => j; rewrite cfclass_IirrE. Qed. @@ -1174,7 +1174,7 @@ have [inj_Mphi | /injectivePn[i [j i'j eq_mm_ij]]] := boolP (injectiveb mmLth). rewrite ['Ind phi]cfun_sum_cfdot sum_cfunE (bigID (mem (codom mmLth))) /=. rewrite ler_paddr ?sumr_ge0 // => [i _|]. by rewrite char1_ge0 ?rpredZ_Cnat ?Cnat_cfdot_char ?cfInd_char ?irr_char. - rewrite -big_uniq //= big_map big_filter -sumr_const ler_sum // => i _. + rewrite -big_uniq //= big_image -sumr_const ler_sum // => i _. rewrite cfunE -[in rhs in _ <= rhs](cfRes1 L) -cfdot_Res_r mmLthL cfRes1. by rewrite DthL cfdotZr rmorph_nat cfnorm_irr mulr1. constructor 2; exists e; first by exists p0. 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. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 4a113b6..72bacc3 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -464,7 +464,7 @@ Proof. move=> Zphi def_n lt_n_4. pose S := [seq '[phi, 'chi_i] *: 'chi_i | i in irr_constt phi]. have def_phi: phi = \sum_(xi <- S) xi. - rewrite big_map /= big_filter big_mkcond {1}[phi]cfun_sum_cfdot. + rewrite big_image big_mkcond {1}[phi]cfun_sum_cfdot. by apply: eq_bigr => i _; rewrite if_neg; case: eqP => // ->; rewrite scale0r. have orthS: orthonormal S. apply/orthonormalP; split=> [|_ _ /mapP[i phi_i ->] /mapP[j _ ->]]. 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). 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. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index f596c3f..8bdbe60 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -545,20 +545,35 @@ Canonical bigop_unlock := Unlockable BigOp.bigopE. Definition index_iota m n := iota m (n - m). -Definition index_enum (T : finType) := Finite.enum T. - Lemma mem_index_iota m n i : i \in index_iota m n = (m <= i < n). Proof. rewrite mem_iota; case le_m_i: (m <= i) => //=. by rewrite -leq_subLR subSn // -subn_gt0 -subnDA subnKC // subn_gt0. Qed. +(* Legacy mathcomp scripts have been relying on the fact that enum A and *) +(* filter A (index_enum T) are convertible. This is likely to change in the *) +(* next mathcomp release when enum, pick, subset and card are generalised to *) +(* predicates with finite support in a choiceType - in fact the two will only *) +(* be equal up to permutation in this new theory. *) +(* It is therefore advisable to stop relying on this, and use the new *) +(* facilities provided in this library: lemmas big_enumP, big_enum, big_image *) +(* and such. Users wishing to test compliance should change the Defined in *) +(* index_enum_key to Qed, and comment out the filter_index_enum compatibility *) +(* definition below (or Import Deprecation.Reject). *) +Fact index_enum_key : unit. Proof. split. Defined. (* Qed. *) +Definition index_enum (T : finType) := + locked_with index_enum_key (Finite.enum T). + +Lemma deprecated_filter_index_enum T P : filter P (index_enum T) = enum P. +Proof. by rewrite [index_enum T]unlock. Qed. + Lemma mem_index_enum T i : i \in index_enum T. -Proof. by rewrite -[index_enum T]enumT mem_enum. Qed. +Proof. by rewrite [index_enum T]unlock -enumT mem_enum. Qed. Hint Resolve mem_index_enum : core. -Lemma filter_index_enum T P : filter P (index_enum T) = enum P. -Proof. by []. Qed. +Lemma index_enum_uniq T : uniq (index_enum T). +Proof. by rewrite [index_enum T]unlock -enumT enum_uniq. Qed. Notation "\big [ op / idx ]_ ( i <- r | P ) F" := (bigop idx r (fun i => BigBody i op P%B F)) : big_scope. @@ -872,10 +887,6 @@ rewrite -big_filter -(big_filter r2) filter_cat. by rewrite has_count -size_filter; case: filter. Qed. -Lemma big_const_seq r (P : pred I) x : - \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx. -Proof. by rewrite unlock; elim: r => //= i r ->; case: (P i). Qed. - End SeqExtension. Lemma big_map_id J (h : J -> R) r (P : pred R) : @@ -971,7 +982,7 @@ Lemma big_mkord n (P : pred nat) F : \big[op/idx]_(0 <= i < n | P i) F i = \big[op/idx]_(i < n | P i) F i. Proof. rewrite /index_iota subn0 -(big_map (@nat_of_ord n)). -by congr bigop; rewrite /index_enum unlock val_ord_enum. +by congr bigop; rewrite /index_enum 2!unlock val_ord_enum. Qed. Lemma big_nat_widen m n1 n2 (P : pred nat) F : @@ -1070,45 +1081,72 @@ rewrite big_ltn // big_add1 /= big_mkord; congr op. by apply: eq_bigr => i _; rewrite eqFG. Qed. -Lemma big_const (I : finType) (A : pred I) x : - \big[op/idx]_(i in A) x = iter #|A| (op x) idx. -Proof. by rewrite big_const_seq -size_filter cardE. Qed. - -Lemma big_const_nat m n x : - \big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx. -Proof. by rewrite big_const_seq count_predT size_iota. Qed. - -Lemma big_const_ord n x : - \big[op/idx]_(i < n) x = iter n (op x) idx. -Proof. by rewrite big_const card_ord. Qed. - Lemma big_nseq_cond I n a (P : pred I) F : - \big[op/idx]_(i <- nseq n a | P i) F i = if P a then iter n (op (F a)) idx else idx. + \big[op/idx]_(i <- nseq n a | P i) F i + = if P a then iter n (op (F a)) idx else idx. Proof. by rewrite unlock; elim: n => /= [|n ->]; case: (P a). Qed. Lemma big_nseq I n a (F : I -> R): \big[op/idx]_(i <- nseq n a) F i = iter n (op (F a)) idx. Proof. exact: big_nseq_cond. Qed. -Lemma big_image_cond I (J : finType) (h : J -> I) (A : pred J) (P : pred I) F : - \big[op/idx]_(i <- [seq h j | j in A] | P i) F i - = \big[op/idx]_(j in A | P (h j)) F (h j). -Proof. by rewrite big_map big_filter_cond. Qed. +End Extensionality. -Lemma big_image I (J : finType) (h : J -> I) (A : pred J) F : - \big[op/idx]_(i <- [seq h j | j in A]) F i = \big[op/idx]_(j in A) F (h j). -Proof. by rewrite big_map big_filter. Qed. +Variant big_enum_spec (I : finType) (P : pred I) : seq I -> Type := + BigEnumSpec e of + forall R idx op (F : I -> R), + \big[op/idx]_(i <- e) F i = \big[op/idx]_(i | P i) F i + & uniq e /\ (forall i, i \in e = P i) + & (let cP := [pred i | P i] in perm_eq e (enum cP) /\ size e = #|cP|) + : big_enum_spec P e. + +(* This lemma can be used to introduce an enumeration into a non-abelian *) +(* bigop, in one of three ways: *) +(* have [e big_e [Ue mem_e] [e_enum size_e]] := big_enumP P. *) +(* gives a permutation e of enum P alongside a equation big_e for converting *) +(* between bigops iterating on (i <- e) and ones on (i | P i). Usually not *) +(* all properties of e are needed, but see below the big_distr_big_dep proof *) +(* where most are. *) +(* rewrite -big_filter; have [e ...] := big_enumP. *) +(* uses big_filter to do this conversion first, and then abstracts the *) +(* resulting filter P (index_enum T) enumeration as an e with the same *) +(* properties (see big_enum_cond below for an example of this usage). *) +(* Finally *) +(* rewrite -big_filter; case def_e: _ / big_enumP => [e ...] *) +(* does the same while remembering the definition of e. *) + +Lemma big_enumP I P : big_enum_spec P (filter P (index_enum I)). +Proof. +set e := filter P _; have Ue: uniq e by apply/filter_uniq/index_enum_uniq. +have mem_e i: i \in e = P i by rewrite mem_filter mem_index_enum andbT. +split=> // [R idx op F | cP]; first by rewrite big_filter. +suffices De: perm_eq e (enum cP) by rewrite (perm_size De) cardE. +by apply/uniq_perm=> // [|i]; rewrite ?enum_uniq ?mem_enum ?mem_e. +Qed. -Lemma big_image_cond_id (J : finType) (h : J -> R) (A : pred J) (P : pred R) : - \big[op/idx]_(i <- [seq h j | j in A] | P i) i - = \big[op/idx]_(j in A | P (h j)) h j. -Proof. exact: big_image_cond. Qed. +Section BigConst. -Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) : - \big[op/idx]_(i <- [seq h j | j in A]) i = \big[op/idx]_(j in A) h j. -Proof. exact: big_image. Qed. +Variables (R : Type) (idx : R) (op : R -> R -> R). -End Extensionality. +Lemma big_const_seq I r (P : pred I) x : + \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx. +Proof. by rewrite unlock; elim: r => //= i r ->; case: (P i). Qed. + +Lemma big_const (I : finType) (A : {pred I}) x : + \big[op/idx]_(i in A) x = iter #|A| (op x) idx. +Proof. +by have [e <- _ [_ <-]] := big_enumP A; rewrite big_const_seq count_predT. +Qed. + +Lemma big_const_nat m n x : + \big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx. +Proof. by rewrite big_const_seq count_predT size_iota. Qed. + +Lemma big_const_ord n x : + \big[op/idx]_(i < n) x = iter n (op x) idx. +Proof. by rewrite big_const card_ord. Qed. + +End BigConst. Section MonoidProperties. @@ -1214,7 +1252,10 @@ Proof. exact: big_allpairs_dep. Qed. Lemma big_pred1_eq (I : finType) (i : I) F : \big[*%M/1]_(j | j == i) F j = F i. -Proof. by rewrite -big_filter filter_index_enum enum1 big_seq1. Qed. +Proof. +have [e1 <- _ [e_enum _]] := big_enumP (pred1 i). +by rewrite (perm_small_eq _ e_enum) enum1 ?big_seq1. +Qed. Lemma big_pred1 (I : finType) i (P : pred I) F : P =1 pred1 i -> \big[*%M/1]_(j | P j) F j = F i. @@ -1251,7 +1292,7 @@ Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) F : (\big[*%M/1]_(i | P (inl _ i)) F (inl _ i)) * (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)). Proof. -by rewrite /index_enum {1}[@Finite.enum]unlock /= big_cat !big_map. +by rewrite ![index_enum _]unlock [@Finite.enum in LHS]unlock big_cat !big_map. Qed. Lemma big_split_ord m n (P : pred 'I_(m + n)) F : @@ -1261,8 +1302,8 @@ Lemma big_split_ord m n (P : pred 'I_(m + n)) F : Proof. rewrite -(big_map _ _ (lshift n) _ P F) -(big_map _ _ (@rshift m _) _ P F). rewrite -big_cat; congr bigop; apply: (inj_map val_inj). -rewrite /index_enum -!enumT val_enum_ord map_cat -map_comp val_enum_ord. -rewrite -map_comp (map_comp (addn m)) val_enum_ord. +rewrite map_cat -!map_comp (map_comp (addn m)) /=. +rewrite ![index_enum _]unlock unlock !val_ord_enum. by rewrite -iota_addl addn0 iota_add. Qed. @@ -1295,11 +1336,21 @@ rewrite mulmCA; congr (_ * _); rewrite -big_cat; apply: IHr1 => a. by move/(_ a): eq_r12; rewrite !count_cat /= addnCA; apply: addnI. Qed. +Lemma big_enum_cond (I : finType) (A : {pred I}) (P : pred I) F : + \big[*%M/1]_(i <- enum A | P i) F i = \big[*%M/1]_(i in A | P i) F i. +Proof. +by rewrite -big_filter_cond; have [e _ _ [/perm_big->]] := big_enumP. +Qed. + +Lemma big_enum (I : finType) (A : {pred I}) F : + \big[*%M/1]_(i <- enum A) F i = \big[*%M/1]_(i in A) F i. +Proof. by rewrite big_enum_cond big_andbC. Qed. + Lemma big_uniq (I : finType) (r : seq I) F : uniq r -> \big[*%M/1]_(i <- r) F i = \big[*%M/1]_(i in r) F i. Proof. -move=> uniq_r; rewrite -(big_filter _ _ _ (mem r)); apply: perm_big. -by rewrite filter_index_enum uniq_perm ?enum_uniq // => i; rewrite mem_enum. +move=> uniq_r; rewrite -big_enum; apply: perm_big. +by rewrite uniq_perm ?enum_uniq // => i; rewrite mem_enum. Qed. Lemma big_rem (I : eqType) r x (P : pred I) F : @@ -1403,6 +1454,24 @@ Qed. Arguments partition_big [I J P] p Q [F]. +Lemma big_image_cond I (J : finType) (h : J -> I) (A : pred J) (P : pred I) F : + \big[*%M/1]_(i <- [seq h j | j in A] | P i) F i + = \big[*%M/1]_(j in A | P (h j)) F (h j). +Proof. by rewrite big_map big_enum_cond. Qed. + +Lemma big_image I (J : finType) (h : J -> I) (A : pred J) F : + \big[*%M/1]_(i <- [seq h j | j in A]) F i = \big[*%M/1]_(j in A) F (h j). +Proof. by rewrite big_map big_enum. Qed. + +Lemma big_image_cond_id (J : finType) (h : J -> R) (A : pred J) (P : pred R) : + \big[*%M/1]_(i <- [seq h j | j in A] | P i) i + = \big[*%M/1]_(j in A | P (h j)) h j. +Proof. exact: big_image_cond. Qed. + +Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) : + \big[*%M/1]_(i <- [seq h j | j in A]) i = \big[*%M/1]_(j in A) h j. +Proof. exact: big_image. Qed. + Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : (forall i, P i -> h (h' i) = i) -> \big[*%M/1]_(i | P i) F i = @@ -1635,13 +1704,11 @@ Lemma big_distr_big_dep (I J : finType) j0 (P : pred I) (Q : I -> pred J) F : \big[+%M/0]_(f in pfamily j0 P Q) \big[*%M/1]_(i | P i) F i (f i). Proof. pose fIJ := {ffun I -> J}; pose Pf := pfamily j0 (_ : seq I) Q. -rewrite -big_filter filter_index_enum; set r := enum P; symmetry. -transitivity (\big[+%M/0]_(f in Pf r) \big[*%M/1]_(i <- r) F i (f i)). - apply: eq_big => f; last by rewrite -big_filter filter_index_enum. - by apply: eq_forallb => i; rewrite /= mem_enum. -have: uniq r by apply: enum_uniq. -elim: {P}r => /= [_ | i r IHr]. - rewrite (big_pred1 [ffun => j0]) ?big_nil //= => f. +have [r big_r [Ur mem_r] _] := big_enumP P. +symmetry; transitivity (\big[+%M/0]_(f in Pf r) \big[*%M/1]_(i <- r) F i (f i)). + by apply: eq_big => // f; apply: eq_forallb => i; rewrite /= mem_r. +rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr]. + rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f. apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE. by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df. case/andP=> /negbTE nri; rewrite big_cons big_distrl => {IHr}/IHr <-. @@ -1674,14 +1741,16 @@ Lemma bigA_distr_big_dep (I J : finType) (Q : I -> pred J) F : \big[*%M/1]_i \big[+%M/0]_(j | Q i j) F i j = \big[+%M/0]_(f in family Q) \big[*%M/1]_i F i (f i). Proof. -case: (pickP J) => [j0 _ | J0]; first exact: (big_distr_big_dep j0). -rewrite {1 4}/index_enum -enumT; case: (enum I) (mem_enum I) => [I0 | i r _]. - have f0: I -> J by move=> i; have:= I0 i. - rewrite (big_pred1 (finfun f0)) ?big_nil // => g. - by apply/familyP/eqP=> _; first apply/ffunP; move => i; have:= I0 i. -have Q0 i': Q i' =1 pred0 by move=> j; have:= J0 j. -rewrite big_cons /= big_pred0 // mul0m big_pred0 // => f. -by apply/familyP=> /(_ i); rewrite [_ \in _]Q0. +have [j _ | J0] := pickP J; first by rewrite (big_distr_big_dep j). +have Q0 i: Q i =i pred0 by move=> /J0/esym/notF[]. +transitivity (iter #|I| ( *%M 0) 1). + by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i. +have [i _ | I0] := pickP I. + rewrite (cardD1 i) //= mul0m big_pred0 // => f. + by apply/familyP=> /(_ i); rewrite Q0. +have f: I -> J by move=> /I0/esym/notF[]. +rewrite eq_card0 // (big_pred1 (finfun f)) ?big_pred0 // => g. +by apply/familyP/eqP=> _; first apply/ffunP; move=> /I0/esym/notF[]. Qed. Lemma bigA_distr_big (I J : finType) (Q : pred J) (F : I -> J -> R) : @@ -1874,3 +1943,7 @@ Notation "@ 'eq_big_perm'" := Notation eq_big_perm := ((fun R idx op I r1 P F r2 => @eq_big_perm R idx op I r1 r2 P F) _ _ _ _ _ _ _) (only parsing). + +Notation filter_index_enum := + ((fun _ => @deprecated_filter_index_enum _) + (deprecate filter_index_enum big_enumP)) (only parsing). diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 8bdb426..1649a89 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -386,8 +386,8 @@ rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. -rewrite !inE -(big_andE predT) -big_filter big_all -all_map. -by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK. +rewrite !inE -(big_andE predT) -big_image /= big_all. +by rewrite -[t in RHS]FinfunK -codom_ffun. Qed. Lemma card_inj_ffuns D T : |