diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 27 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 2 | ||||
| -rw-r--r-- | mathcomp/character/character.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 38 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 6 |
7 files changed, 58 insertions, 37 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index f32db72..e0ac874 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1309,10 +1309,10 @@ Lemma matrix_sum_delta A : A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j. Proof. apply/matrixP=> i j. -rewrite summxE (bigD1 i) // summxE (bigD1 j) //= !mxE !eqxx mulr1. -rewrite !big1 ?addr0 //= => [i' | j']; rewrite eq_sym => /negPf diff. - by rewrite summxE big1 // => j' _; rewrite !mxE diff mulr0. -by rewrite !mxE eqxx diff mulr0. +rewrite summxE (bigD1_ord i) // summxE (bigD1_ord j) //= !mxE !eqxx mulr1. +rewrite !big1 ?addr0 //= => [i' | j'] _. + by rewrite summxE big1// => j' _; rewrite !mxE eq_liftF mulr0. +by rewrite !mxE eqxx eq_liftF mulr0. Qed. End RingModule. @@ -1425,9 +1425,8 @@ Canonical diag_mx_linear n := Linear (@diag_mx_is_linear n). Lemma diag_mx_sum_delta n (d : 'rV_n) : diag_mx d = \sum_i d 0 i *: delta_mx i i. Proof. -apply/matrixP=> i j; rewrite summxE (bigD1 i) //= !mxE eqxx /=. -rewrite eq_sym mulr_natr big1 ?addr0 // => i' ne_i'i. -by rewrite !mxE eq_sym (negPf ne_i'i) mulr0. +apply/matrixP=> i j; rewrite summxE (bigD1_ord i) //= !mxE eqxx /=. +by rewrite eq_sym mulr_natr big1 ?addr0 // => i'; rewrite !mxE eq_liftF mulr0. Qed. Lemma row_diag_mx n (d : 'rV_n) i : @@ -1638,8 +1637,8 @@ Qed. Lemma rowE m n i (A : 'M_(m, n)) : row i A = delta_mx 0 i *m A. Proof. -apply/rowP=> j; rewrite !mxE (bigD1 i) //= mxE !eqxx mul1r. -by rewrite big1 ?addr0 // => i' ne_i'i; rewrite mxE /= (negPf ne_i'i) mul0r. +apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. +by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. Qed. Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) : @@ -1655,9 +1654,9 @@ Qed. Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) : delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2). Proof. -apply/matrixP => i k; rewrite !mxE (bigD1 j1) //=. +apply/matrixP => i k; rewrite !mxE (bigD1_ord j1) //=. rewrite mulmxnE !mxE !eqxx andbT -natrM -mulrnA !mulnb !andbA andbAC. -by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM; move/negPf->. +by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM lift_eqF. Qed. Lemma mul_delta_mx m n p (j : 'I_n) (i : 'I_m) (k : 'I_p) : @@ -2844,10 +2843,8 @@ have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0]. rewrite !mxE unlift_none -wjA'0; split=> //. apply: contraNneq nzwj => w0; apply/eqP/rowP=> k'. by move/rowP/(_ (lift j k')): w0; rewrite !mxE liftK. - apply/rowP=> k; rewrite !mxE (bigD1 j) //= mxE unlift_none mul0r add0r. - rewrite (reindex_onto (lift j) (odflt k \o unlift j)) /= => [|k']. - by apply: eq_big => k'; rewrite ?mxE liftK eq_sym neq_lift eqxx. - by rewrite eq_sym; case/unlift_some=> ? ? ->. + apply/rowP=> k; rewrite !mxE (bigD1_ord j) //= mxE unlift_none mul0r add0r. + by apply: eq_big => //= k'; rewrite !mxE/= liftK. have [w0 [/rV0Pn[j nz_w0j] w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. have{w_} [wj [nz_wj wj0_0 wjA']] := w_ j; pose aj := (wj *m vA) 0 0. have [aj0 | nz_aj] := eqVneq aj 0. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index cbac070..f33e291 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -188,7 +188,7 @@ have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by have [->|] := eqP; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; - try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)). + try by apply/matrixP=> i j; rewrite !mxE lift_eqF. have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r. rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _]. rewrite add0r; congr (\det _)%:P. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 113ef8b..e7ea1e0 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -722,7 +722,7 @@ Lemma irr_free : free (irr G). Proof. apply/freeP=> s s0 i; apply: (mulIf (irr1_neq0 i)). rewrite mul0r -(raddf0 (xcfun_r_additive 'e_i)) -{}s0 raddf_sum /=. -rewrite (bigD1 i) //= -tnth_nth xcfunZl xcfun_id eqxx big1 ?addr0 // => j ne_ji. +rewrite (bigD1 i)//= -tnth_nth xcfunZl xcfun_id eqxx big1 ?addr0 // => j ne_ji. by rewrite -tnth_nth xcfunZl xcfun_id (negbTE ne_ji) mulr0. Qed. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 997255b..821a21e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -150,8 +150,8 @@ Lemma mem_Crat_span s : {subset s <= Crat_span s}. Proof. move=> _ /(nthP 0)[ix ltxs <-]; pose i0 := Ordinal ltxs. apply/Crat_spanP; exists [ffun i => (i == i0)%:R]. -rewrite (bigD1 i0) //= ffunE eqxx // rmorph1 mul1r. -by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl => /negbTE->. +rewrite (bigD1_ord i0) //= ffunE eqxx // rmorph1 mul1r. +by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl lift_eqF. Qed. Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s). diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 1b580c0..ee3aedb 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1464,18 +1464,29 @@ 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) -> +Lemma reindex_omap (I J : finType) (h : J -> I) h' (P : pred I) F : + (forall i, P i -> omap h (h' i) = some i) -> \big[*%M/1]_(i | P i) F i = - \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). + \big[*%M/1]_(j | P (h j) && (h' (h j) == some j)) F (h j). Proof. move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *. case: (pickP P) => [i Pi | P0]; last first. by rewrite !big_pred0 // => j; rewrite P0. -rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eqxx //=; congr (_ * _). -rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. -apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. -by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K. +have := h'K i Pi; case h'i_eq : (h' i) => [/= j|//] [hj_eq]. +rewrite (bigD1 i Pi) (bigD1 j) hj_eq ?Pi ?h'i_eq ?eqxx //=; congr (_ * _). +rewrite {}IHn => [|k /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. +apply: eq_bigl => k; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. +congr (_ && ~~ _); apply/eqP/eqP => [|->//]. +by move=> /(congr1 h'); rewrite h'i_eq hK => -[]. +Qed. +Arguments reindex_omap [I J] h h' [P F]. + +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 = + \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). +Proof. +by move=> h'K; rewrite (reindex_omap h (some \o h'))//= => i Pi; rewrite h'K. Qed. Arguments reindex_onto [I J] h h' [P F]. @@ -1493,6 +1504,15 @@ Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F : Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed. Arguments reindex_inj [I h P F]. +Lemma bigD1_ord n j (P : pred 'I_n) F : + P j -> \big[*%M/1]_(i < n | P i) F i + = F j * \big[*%M/1]_(i < n.-1 | P (lift j i)) F (lift j i). +Proof. +move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=. + by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. +by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF. +Qed. + Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F : \big[op/idx]_(x in A | P x) F x = \big[op/idx]_(i < #|A| | P (enum_val i)) F (enum_val i). @@ -1656,7 +1676,9 @@ Arguments bigID [R idx op I r]. Arguments bigU [R idx op I]. Arguments bigD1 [R idx op I] j [P F]. Arguments bigD1_seq [R idx op I r] j [F]. +Arguments bigD1_ord [R idx op n] j [P F]. Arguments partition_big [R idx op I J P] p Q [F]. +Arguments reindex_omap [R idx op I J] h h' [P F]. Arguments reindex_onto [R idx op I J] h h' [P F]. Arguments reindex [R idx op I J] h [P F]. Arguments reindex_inj [R idx op I h P F]. @@ -1749,7 +1771,7 @@ Proof. 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. + 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. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 9bd8c1f..4262ed7 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1453,17 +1453,13 @@ Lemma big_imset h (A : {pred I}) G : {in A &, injective h} -> \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i). Proof. move=> injh; pose hA := mem (image h A). -have [x0 Ax0 | A0] := pickP A; last first. - by rewrite !big_pred0 // => x; apply/imsetP=> [[i]]; rewrite unfold_in A0. rewrite (eq_bigl hA) => [|j]; last exact/imsetP/imageP. -pose h' j := if insub j : {? j | hA j} is Some u then iinv (svalP u) else x0. -rewrite (reindex_onto h h') => [|j hAj]; rewrite {}/h'; last first. - by rewrite (insubT hA hAj) f_iinv. -apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]. - set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). - by apply/eqP/idP=> [<- // | Ai]; apply: injh; rewrite ?f_iinv. -symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai. -by case/imageP: nhAhi; exists i. +pose h' := omap (fun u : {j | hA j} => iinv (svalP u)) \o insub. +rewrite (reindex_omap h h') => [|j hAj]; rewrite {}/h'/= ?insubT/= ?f_iinv//. +apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]; last first. + by apply/andP/idP => [[]//| Ai]; case/imageP: nhAhi; exists i. +set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). +by apply/eqP/idP => [[<-] // | Ai]; congr Some; apply: injh; rewrite ?f_iinv. Qed. Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} -> diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 88d0f92..3472a1d 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2074,6 +2074,12 @@ Qed. Lemma neq_lift n (h : 'I_n) i : h != lift h i. Proof. exact: neq_bump. Qed. +Lemma eq_liftF n (h : 'I_n) i : (h == lift h i) = false. +Proof. exact/negbTE/neq_lift. Qed. + +Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false. +Proof. by rewrite eq_sym eq_liftF. Qed. + Lemma unlift_none n (h : 'I_n) : unlift h h = None. Proof. by case: unliftP => // j Dh; case/eqP: (neq_lift h j). Qed. |