diff options
Diffstat (limited to 'mathcomp')
36 files changed, 821 insertions, 341 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index 147d5b1..c4391ae 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -94,3 +94,5 @@ ssreflect/tuple.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden +-arg -w -arg -duplicate-clear +-arg -w -arg -ambiguous-paths diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject index 450e035..912cc1a 100644 --- a/mathcomp/_CoqProject +++ b/mathcomp/_CoqProject @@ -4,3 +4,4 @@ -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden +-arg -w -arg -duplicate-clear diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 48e9de8..0a5bfde 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -969,7 +969,7 @@ without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z. by exists i; rewrite mxE. exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //. rewrite -[M]trmxK dM !trmx_mul mulmxA; congr (_ *m _ *m _). - by apply/matrixP=> i1 j1; rewrite !mxE eq_sym; case: eqP => // ->. + by apply/matrixP=> i1 j1; rewrite !mxE; case: eqVneq => // ->. without loss{nz_a a_dvM} a1: M a Da / a = 1. pose M1 := map_mx (divz^~ a) M; case/(_ M1 1)=> // [k|L uL [R uR [d dvD dM]]]. by rewrite !mxE Da divzz nz_a. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index d3142d6..9d6e2be 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1392,7 +1392,7 @@ Definition diag_mx n (d : 'rV[R]_n) := \matrix[diag_mx_key]_(i, j) (d 0 i *+ (i == j)). Lemma tr_diag_mx n (d : 'rV_n) : (diag_mx d)^T = diag_mx d. -Proof. by apply/matrixP=> i j; rewrite !mxE eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma diag_mx_is_linear n : linear (@diag_mx n). Proof. @@ -1744,7 +1744,7 @@ by rewrite eqn_leq andbC leqNgt lshift_subproof. Qed. Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m). -Proof. by apply/matrixP=> i j; rewrite !mxE eq_sym; case: eqP => // ->. Qed. +Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n). Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 078fea3..8d6c03b 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2,7 +2,7 @@ (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. From mathcomp Require Import fintype finfun bigop finset fingroup perm. -From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. +From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. (*****************************************************************************) (* In this file we develop the rank and row space theory of matrices, based *) @@ -683,7 +683,7 @@ Qed. Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx). Proof. exact: row_free_unit. Qed. - + Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n. Proof. by rewrite -row_full_unit => /eqnP. Qed. @@ -1488,7 +1488,7 @@ Proof. by rewrite unlock; apply/eqmxP; rewrite !genmxE !capmxE andbb. Qed. Lemma genmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (<<A :\: B>> = A :\: B)%MS. Proof. by rewrite [@diffmx]unlock genmx_id. Qed. - + Lemma diffmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B <= A)%MS. Proof. by rewrite diffmxE capmxSl. Qed. @@ -2202,7 +2202,7 @@ have p_i_gt0: p ^ _ > 0 by move=> i; rewrite expn_gt0 ltnW. rewrite (card_GL _ (ltn0Sn n.-1)) card_ord Fp_cast // big_add1 /=. pose p'gt0 m := m > 0 /\ logn p m = 0%N. suffices [Pgt0 p'P]: p'gt0 (\prod_(0 <= i < n.-1.+1) (p ^ i.+1 - 1))%N. - by rewrite lognM // p'P pfactorK //; case n. + by rewrite lognM // p'P pfactorK // addn0; case n. apply big_ind => [|m1 m2 [m10 p'm1] [m20]|i _]; rewrite {}/p'gt0 ?logn1 //. by rewrite muln_gt0 m10 lognM ?p'm1. rewrite lognE -if_neg subn_gt0 p_pr /= -{1 2}(exp1n i.+1) ltn_exp2r // p_gt1. @@ -2269,7 +2269,7 @@ by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV. Qed. Arguments memmx_sumsP {I P n A R_}. -Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : +Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : (1%:M \in R)%MS -> reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R). Proof. @@ -2765,5 +2765,3 @@ Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS. Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. - - diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index d898774..a3b9211 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -368,7 +368,7 @@ Lemma nil_poly p : nilp p = (p == 0). Proof. exact: size_poly_eq0. Qed. Lemma poly0Vpos p : {p = 0} + {size p > 0}. -Proof. by rewrite lt0n size_poly_eq0; apply: eqVneq. Qed. +Proof. by rewrite lt0n size_poly_eq0; case: eqVneq; [left | right]. Qed. Lemma polySpred p : p != 0 -> size p = (size p).-1.+1. Proof. by rewrite -size_poly_eq0 -lt0n => /prednK. Qed. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 6f9d837..b65742d 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -2037,8 +2037,7 @@ Lemma egcdp_recP : forall k p q, q != 0 -> size q <= k -> size q <= size p -> [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q]. Proof. elim=> [|k ihk] p q /= qn0; first by rewrite leqn0 size_poly_eq0 (negPf qn0). -move=> sqSn qsp; case: (eqVneq q 0)=> q0; first by rewrite q0 eqxx in qn0. -rewrite (negPf qn0). +move=> sqSn qsp; rewrite (negPf qn0). have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0. case: (eqVneq (p %% q) 0) => [r0 | rn0] /=. rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=. @@ -2239,8 +2238,7 @@ Proof. apply/eqP/idP=> [d0|]; last first. case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|]. by move/divp_small. -case: (eqVneq p 0) => [->|pn0]; first by rewrite eqxx. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite eqxx orbT. +case: eqVneq => // _; case: eqVneq => // qn0. move: (divp_eq p q); rewrite d0 mul0r add0r. move/(f_equal (fun x : {poly R} => size x)). by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT. @@ -3039,8 +3037,8 @@ Proof. move=> eqr; rewrite /gdcop; move: (size p)=> n. elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=. move: eqr; case: (eqVneq q 0)=> [-> | nq0 eqr] /=. - by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx. - suff rn0 : r != 0 by rewrite (negPf nq0) (negPf rn0) eqpxx. + by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. + suff rn0 : r != 0 by rewrite (negPf rn0) eqpxx. by apply: contraTneq eqr => ->; rewrite eqp0. rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //. by apply: ihn => //; apply: eqp_div => //; apply: eqp_gcd. @@ -3051,8 +3049,8 @@ Proof. rewrite /rgdcop /gdcop; move: (size p)=> n. elim: n p q {1 3}p {1 3}q (eqpxx p) (eqpxx q) => [|n ihn] p q s t /= sp tq. move: tq; case: (eqVneq t 0)=> [-> | nt0 etq]. - by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx. - suff qn0 : q != 0 by rewrite (negPf nt0) (negPf qn0) eqpxx. + by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. + suff qn0 : q != 0 by rewrite (negPf qn0) eqpxx. by apply: contraTneq etq => ->; rewrite eqp0. rewrite rcoprimep_coprimep (eqp_coprimepl t sp) (eqp_coprimepr p tq). case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 1b1eb77..3c4c002 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1553,7 +1553,7 @@ Lemma abszN1 : `|-1%R| = 1. Proof. by []. Qed. Lemma absz_id m : `|(`|m|)| = `|m|. Proof. by []. Qed. Lemma abszM m1 m2 : `|(m1 * m2)%R| = `|m1| * `|m2|. -Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2]; rewrite //= mulnS mulnC. Qed. +Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2] //=; rewrite ?mulnS mulnC. Qed. Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n. Proof. by elim: n => // n ihn; rewrite exprS expnS abszM ihn. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 97afdfb..12fcecb 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -4384,8 +4384,7 @@ have sz_p: size p = n.+1. pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted. have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P). rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb. - rewrite subr0 eqxx scale1r; apply: eq_big_perm. - by rewrite perm_eq_sym perm_sort. + by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort. have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r). move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0. by rewrite subr_eq0; apply: eqP. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index e73ca33..87ca0f4 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1004,7 +1004,7 @@ Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed. Lemma perm_free X Y : perm_eq X Y -> free X = free Y. Proof. -by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)). +by move=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)). Qed. Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>). @@ -1061,7 +1061,7 @@ Proof. by rewrite cat_free => /and3P[]. Qed. Lemma filter_free p X : free X -> free (filter p X). Proof. -rewrite -(perm_free (etrans (perm_filterC p X _) (perm_eq_refl X))). +rewrite -(perm_free (etrans (perm_filterC p X _) (perm_refl X))). exact: catl_free. Qed. @@ -1170,7 +1170,7 @@ Qed. Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y. Proof. move=> eqXY; congr ((_ == _) && _); last exact: perm_free. -by apply/eq_span; apply: perm_eq_mem. +by apply/eq_span; apply: perm_mem. Qed. Lemma vbasisP U : basis_of U (vbasis U). diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 468aa66..c35cdd6 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1173,7 +1173,7 @@ Qed. Lemma eq_orthonormal R S : perm_eq R S -> orthonormal R = orthonormal S. Proof. -move=> eqRS; rewrite !orthonormalE (eq_all_r (perm_eq_mem eqRS)). +move=> eqRS; rewrite !orthonormalE (eq_all_r (perm_mem eqRS)). by rewrite (eq_pairwise_orthogonal eqRS). Qed. @@ -2412,8 +2412,8 @@ Proof. set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS. have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj). have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. -have [|eqSuS _] := leq_size_perm uniqSu sSuS; first by rewrite size_map. -by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)). +have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map. +by rewrite (perm_free (uniq_perm uniqSu uniqS eqSuS)). Qed. Lemma cfAut_on A phi : (phi^u \in 'CF(G, A)) = (phi \in 'CF(G, A)). diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 5350075..d3dfd38 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -465,14 +465,14 @@ Lemma im_cfclass_Iirr i : H <| G -> perm_eq [seq 'chi_j | j in cfclass_Iirr G i] ('chi_i ^: G)%CF. Proof. move=> nsHG; have UchiG := cfclass_uniq 'chi_i nsHG. -apply: uniq_perm_eq; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi. +apply: uniq_perm; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi. apply/imageP/idP=> [[j iGj ->] | /cfclassP[y]]; first by rewrite -cfclass_IirrE. by exists (conjg_Iirr i y); rewrite ?mem_imset ?conjg_IirrE. Qed. Lemma card_cfclass_Iirr i : H <| G -> #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|. Proof. -move=> nsHG; rewrite -size_cfclass -(perm_eq_size (im_cfclass_Iirr i nsHG)). +move=> nsHG; rewrite -size_cfclass -(perm_size (im_cfclass_Iirr i nsHG)). by rewrite size_map -cardE. Qed. @@ -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/(eq_big_perm _) <-; rewrite big_map big_filter /=. +move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_map big_filter /=. by apply: eq_bigl => j; rewrite cfclass_IirrE. Qed. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 4212fbe..4a113b6 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -314,7 +314,7 @@ Lemma cfproj_sum_orthogonal P z phi : = if P phi then z phi * '[phi] else 0. Proof. move=> Sphi; have defS := perm_to_rem Sphi. -rewrite cfdot_suml (eq_big_perm _ defS) big_cons /= cfdotZl Inu ?Z_S //. +rewrite cfdot_suml (perm_big _ defS) big_cons /= cfdotZl Inu ?Z_S //. rewrite big1_seq ?addr0 // => xi; rewrite mem_rem_uniq ?inE //. by case/and3P=> _ neq_xi Sxi; rewrite cfdotZl Inu ?Z_S // dotSS ?mulr0. Qed. @@ -412,15 +412,15 @@ Lemma vchar_orthonormalP S : Proof. move=> vcS; apply: (equivP orthonormalP). split=> [[uniqS oSS] | [I [b defS]]]; last first. - split=> [|xi1 xi2]; rewrite ?(perm_eq_mem defS). - rewrite (perm_eq_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP. + split=> [|xi1 xi2]; rewrite ?(perm_mem defS). + rewrite (perm_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP. by rewrite eq_signed_irr => /andP[_ /eqP]. case/mapP=> [i _ ->] /mapP[j _ ->]; rewrite eq_signed_irr. rewrite cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr -signr_addb mulr_natr. by rewrite mulrb andbC; case: eqP => //= ->; rewrite addbb eqxx. pose I := [set i | ('chi_i \in S) || (- 'chi_i \in S)]. pose b i := - 'chi_i \in S; exists I, b. -apply: uniq_perm_eq => // [|xi]. +apply: uniq_perm => // [|xi]. rewrite map_inj_uniq ?enum_uniq // => i j /eqP. by rewrite eq_signed_irr => /andP[_ /eqP]. apply/idP/mapP=> [Sxi | [i Ii ->{xi}]]; last first. @@ -453,7 +453,7 @@ move=> Zphi phiN1. have: orthonormal phi by rewrite /orthonormal/= phiN1 eqxx. case/vchar_orthonormalP=> [xi /predU1P[->|] // | I [b def_phi]]. have: phi \in (phi : seq _) := mem_head _ _. -by rewrite (perm_eq_mem def_phi) => /mapP[i _ ->]; exists (b i), i. +by rewrite (perm_mem def_phi) => /mapP[i _ ->]; exists (b i), i. Qed. Lemma zchar_small_norm phi n : diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 6a28884..2d576c4 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -240,8 +240,8 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x. have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map. pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B. apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //. - congr (_ %= _): Dq; apply: eq_big_perm => //. - by rewrite uniq_perm_eq ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. + congr (_ %= _): Dq; apply: perm_big => //. + by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE. rewrite -!(size_map_poly FtoL) Dq -DpI (minI B) // -?Dq ?FpxF //. by apply/subsetP=> j; rewrite inE => /mem_mask; rewrite mem_enum. Qed. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 00a7bad..cb499b3 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -651,10 +651,10 @@ have prod_aq m: m %| n -> \prod_(d < n.+1 | d %| m) aq d = (q ^ m - 1)%:R. by rewrite !hornerE hornerXn -natrX natrB ?expn_gt0 ?prime_gt0. rewrite (prod_cyclotomic (dvdn_prim_root z_prim m_dv_n)). have def_divm: perm_eq (divisors m) [seq d <- index_iota 0 n.+1 | d %| m]. - rewrite uniq_perm_eq ?divisors_uniq ?filter_uniq ?iota_uniq // => d. + rewrite uniq_perm ?divisors_uniq ?filter_uniq ?iota_uniq // => d. rewrite -dvdn_divisors ?(dvdn_gt0 n_gt0) // mem_filter mem_iota ltnS /=. by apply/esym/andb_idr=> d_dv_m; rewrite dvdn_leq ?(dvdn_trans d_dv_m). - rewrite (eq_big_perm _ def_divm) big_filter big_mkord horner_prod. + rewrite (perm_big _ def_divm) big_filter big_mkord horner_prod. by apply: eq_bigr => d d_dv_m; rewrite -exprM muln_divA ?divnK. have /rpredBl<-: (aq n %| #|G|%:R)%C. rewrite oG -prod_aq // (bigD1 ord_max) //= dvdC_mulr //. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 459250f..30bef47 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1329,12 +1329,12 @@ rewrite -fixedKE; apply/polyOverP => i; apply/fixedFieldP=> [|x galEx]. rewrite (polyOverP _) // big_map rpred_prod // => b _. by rewrite polyOverXsubC memv_gal. rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i. -symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x). +symmetry; rewrite (perm_big (map x r)) /= ?(big_map x). by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC. have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj. -have /leq_size_perm: {subset map x r <= r}. +have /uniq_min_size: {subset map x r <= r}. by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM. -by rewrite (size_map x) perm_eq_sym; case=> // /uniq_perm_eq->. +by rewrite (size_map x) perm_sym; case=> // _ /uniq_perm->. Qed. Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 676daf0..853ffb6 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -614,19 +614,19 @@ Lemma perm_bigcprod (I : eqType) r1 r2 (A : I -> {set gT}) G x : \prod_(i <- r1) x i = \prod_(i <- r2) x i. Proof. elim: r1 r2 G => [|i r1 IHr] r2 G defG Ax eq_r12. - by rewrite perm_eq_sym in eq_r12; rewrite (perm_eq_small _ eq_r12) ?big_nil. -have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_eq_mem eq_r12) mem_head. + by rewrite perm_sym in eq_r12; rewrite (perm_small_eq _ eq_r12) ?big_nil. +have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_mem eq_r12) mem_head. transitivity (\prod_(j <- rot n r2) x j). rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG. rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP. - by rewrite -(perm_cons i) -Dr2 perm_eq_sym perm_rot perm_eq_sym. + by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym. rewrite -{-2}(cat_take_drop n r2) in eq_r12 *. -rewrite (eq_big_perm _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *. +rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *. have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG. rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax. - by rewrite (perm_eq_mem eq_r12) mem_cat orbC mem_nth. + by rewrite (perm_mem eq_r12) mem_cat orbC mem_nth. rewrite defG1 -(bigcprodW defG1) mem_prodg // => k _; apply: Ax. -by rewrite (perm_eq_mem eq_r12) mem_cat mem_nth. +by rewrite (perm_mem eq_r12) mem_cat mem_nth. Qed. Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x : @@ -637,7 +637,7 @@ 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_eq (enum_uniq P) _ _ => [|i]. +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. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 33bf82c..f1ff532 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -294,22 +294,22 @@ Proof. by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj. Qed. -Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} : +Lemma tuple_permP {T : eqType} {n} {s : seq T} {t : n.-tuple T} : reflect (exists p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t). Proof. apply: (iffP idP) => [|[p ->]]; last first. rewrite /= (map_comp (tnth t)) -{1}(map_tnth_enum t) perm_map //. - apply: uniq_perm_eq => [||i]; rewrite ?enum_uniq //. + apply: uniq_perm => [||i]; rewrite ?enum_uniq //. by apply/injectiveP; apply: perm_inj. by rewrite mem_enum -[i](permKV p) image_f. case: n => [|n] in t *; last have x0 := tnth t ord0. - rewrite tuple0 => /perm_eq_small-> //. + rewrite tuple0 => /perm_small_eq-> //. by exists 1; rewrite [mktuple _]tuple0. -case/(perm_eq_iotaP x0); rewrite size_tuple => Is eqIst ->{s}. -have uniqIs: uniq Is by rewrite (perm_eq_uniq eqIst) iota_uniq. -have szIs: size Is == n.+1 by rewrite (perm_eq_size eqIst) !size_tuple. +case/(perm_iotaP x0); rewrite size_tuple => Is eqIst ->{s}. +have uniqIs: uniq Is by rewrite (perm_uniq eqIst) iota_uniq. +have szIs: size Is == n.+1 by rewrite (perm_size eqIst) !size_tuple. have pP i : tnth (Tuple szIs) i < n.+1. - by rewrite -[_ < _](mem_iota 0) -(perm_eq_mem eqIst) mem_tnth. + by rewrite -[_ < _](mem_iota 0) -(perm_mem eqIst) mem_tnth. have inj_p: injective (fun i => Ordinal (pP i)). by apply/injectiveP/(@map_uniq _ _ val); rewrite -map_comp map_tnth_enum. exists (perm inj_p); rewrite -[Is]/(tval (Tuple szIs)); congr (tval _). @@ -570,12 +570,13 @@ apply/permP=> i; case: (unliftP j i) => [i'|] ->; last first. apply: ord_inj; rewrite lift_perm_lift !permE /= eq_sym -if_neg neq_lift. rewrite fun_if -val_eqE /= def_k /bump ltn_neqAle andbC. case: leqP => [_ | lt_i'm] /=; last by rewrite -if_neg neq_ltn leqW. -by rewrite add1n eqSS eq_sym; case: eqP. +by rewrite add1n eqSS; case: eqVneq. Qed. End LiftPerm. Prenex Implicits lift_perm lift_permK. - +Notation tuple_perm_eqP := + (deprecate tuple_perm_eqP tuple_permP) (only parsing). diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index ad12189..2e025a2 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -836,9 +836,9 @@ Qed. Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1). Proof. -case: (eqsVneq G 1) => [-> |]; first by rewrite rank1 eqxx. -case: (trivgVpdiv G) => [-> | [p p_pr]]; first by case/eqP. -case/Cauchy=> // x Gx oxp ->; apply: leq_trans (p_rank_le_rank p G). +case: (eqsVneq G 1) => [-> |]; first by rewrite rank1. +case: (trivgVpdiv G) => [/eqP->// | [p p_pr]]. +case/Cauchy=> // x Gx oxp _; apply: leq_trans (p_rank_le_rank p G). have EpGx: <[x]>%G \in 'E_p(G). by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn. by apply: leq_trans (logn_le_p_rank EpGx); rewrite -orderE oxp logn_prime ?eqxx. @@ -1713,11 +1713,11 @@ rewrite orderXdiv ?pfactor_dvdn ?leq_subr // -(dvdn_pmul2r m_gt0). by rewrite -expnS -subSn // subSS divnK pfactor_dvdn ?leq_subr. Qed. -Lemma perm_eq_abelian_type p b G : +Lemma abelian_type_pgroup p b G : p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b -> - perm_eq (map order b) (abelian_type G). + perm_eq (abelian_type G) (map order b). Proof. -move: b => b1 pG defG1 ntb1. +rewrite perm_sym; move: b => b1 pG defG1 ntb1. have cGG: abelian G. elim: (b1) {pG}G defG1 => [_ <-|x b IHb G]; first by rewrite big_nil abelian1. rewrite big_cons; case/dprodP=> [[_ H _ defH]] <-; rewrite defH => cxH _. @@ -1992,8 +1992,8 @@ suffices def_atG: abelian_type K ++ abelian_type H =i abelian_type G. by rewrite size_abelian_type // -abelian_type_homocyclic. have [bK defK atK] := abelian_structure cKK. have [bH defH atH] := abelian_structure cHH. -apply: perm_eq_mem; rewrite -atK -atH -map_cat. -apply: (perm_eq_abelian_type pG); first by rewrite big_cat defK defH. +apply/perm_mem; rewrite perm_sym -atK -atH -map_cat. +apply: (abelian_type_pgroup pG); first by rewrite big_cat defK defH. have: all [pred m | m > 1] (map order (bK ++ bH)). by rewrite map_cat all_cat atK atH !abelian_type_gt1. by rewrite all_map (eq_all (@order_gt1 _)) all_predC has_pred1. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index b5d34a5..18c6509 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -371,7 +371,7 @@ Lemma F_r3 : 'Fix_to[r3] = Proof. apply/setP=> x; rewrite (sameP afix1P eqP) !inE eqperm_map /=. rewrite /act_f r3_inv !ffunE !permE /=. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite // {E}(eqP E)]. +by do 3![case: eqVneq=> // <-]. Qed. Lemma card_n2 : forall x y z t : square, uniq [:: x; y; z; t] -> @@ -950,7 +950,7 @@ Proof. apply sym_equal. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r05_inv !ffunE !permE /=. rewrite !eqxx /= !andbT /col1/col2/col3/col4/col5/col0. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r50 : 'Fix_to_g[r50]= @@ -959,7 +959,7 @@ Lemma F_r50 : 'Fix_to_g[r50]= Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r50_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col2/col3/col4. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r23 : 'Fix_to_g[r23] = @@ -969,7 +969,7 @@ Proof. have r23_inv: r23^-1 = r32 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r23_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r32 : 'Fix_to_g[r32] = @@ -979,7 +979,7 @@ Proof. have r32_inv: r32^-1 = r23 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r32_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r14 : 'Fix_to_g[r14] = @@ -987,7 +987,7 @@ Lemma F_r14 : 'Fix_to_g[r14] = Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r14_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r41 : 'Fix_to_g[r41] = @@ -995,7 +995,7 @@ Lemma F_r41 : 'Fix_to_g[r41] = Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r41_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r024 : 'Fix_to_g[r024] = @@ -1005,7 +1005,7 @@ Proof. have r024_inv: r024^-1 = r042 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r024_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r042 : 'Fix_to_g[r042] = @@ -1015,7 +1015,7 @@ Proof. have r042_inv: r042^-1 = r024 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r042_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r012 : 'Fix_to_g[r012] = @@ -1025,7 +1025,7 @@ Proof. have r012_inv: r012^-1 = r021 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r012_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r021 : 'Fix_to_g[r021] = @@ -1035,7 +1035,7 @@ Proof. have r021_inv: r021^-1 = r012 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r021_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r031 : 'Fix_to_g[r031] = @@ -1045,7 +1045,7 @@ Proof. have r031_inv: r031^-1 = r013 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r031_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r013 : 'Fix_to_g[r013] = @@ -1055,7 +1055,7 @@ Proof. have r013_inv: r013^-1 = r031 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r013_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r043 : 'Fix_to_g[r043] = @@ -1065,7 +1065,7 @@ Proof. have r043_inv: r043^-1 = r034 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r043_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r034 : 'Fix_to_g[r034] = @@ -1075,7 +1075,7 @@ Proof. have r034_inv: r034^-1 = r043 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r034_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s1 : 'Fix_to_g[s1] = @@ -1084,7 +1084,7 @@ Proof. have s1_inv: s1^-1 = s1 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s1_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s2 : 'Fix_to_g[s2] = @@ -1093,7 +1093,7 @@ Proof. have s2_inv: s2^-1 = s2 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s2_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s3 : 'Fix_to_g[s3] = @@ -1102,7 +1102,7 @@ Proof. have s3_inv: s3^-1 = s3 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s3_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s4 : 'Fix_to_g[s4] = @@ -1111,7 +1111,7 @@ Proof. have s4_inv: s4^-1 = s4 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s4_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s5 : 'Fix_to_g[s5] = @@ -1120,7 +1120,7 @@ Proof. have s5_inv: s5^-1 = s5 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s5_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s6 : 'Fix_to_g[s6] = @@ -1129,7 +1129,7 @@ Proof. have s6_inv: s6^-1 = s6 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s6_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma uniq4_uniq6 : forall x y z t : cube, diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index aa3ebed..0aacd7c 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -340,7 +340,7 @@ have ntY: Y != 1 by apply: subG1_contra ntZ. have p_odd: odd p by rewrite -oZ (oddSg sZG). have expY: exponent Y %| p by rewrite exponent_Ohm1_class2 // nil_class2 defG'. rewrite (prime_nt_dvdP p_pr _ expY) -?dvdn1 -?trivg_exponent //. -have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n eqxx; split. +have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n; split. have sG1Z: 'Mho^1(G) \subset Z by rewrite -defPhiG (Phi_joing pG) joing_subr. have Z_Gp: {in G, forall x, x ^+ p \in Z}. by move=> x Gx; rewrite /= (subsetP sG1Z) ?(Mho_p_elt 1) ?(mem_p_elt pG). diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 65c186a..d236575 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -2322,7 +2322,7 @@ have{defZN2} strZN2: \big[dprod/1]_(z <- [:: xpn3; y]) <[z]> = 'Z('Ohm_2(N)). by rewrite unlock /= dprodg1. rewrite -size_abelian_type ?center_abelian //. have pZN2: p.-group 'Z('Ohm_2(N)) by rewrite (pgroupS _ pN) // subIset ?Ohm_sub. -rewrite -(perm_eq_size (perm_eq_abelian_type pZN2 strZN2 _)) //= !inE. +rewrite (perm_size (abelian_type_pgroup pZN2 strZN2 _)) //= !inE. rewrite !(eq_sym 1) -!order_eq1 oy orderE oX2. by rewrite (eqn_exp2l 2 0) // (eqn_exp2l 1 0). Qed. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 1a32bce..d191e20 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -179,9 +179,9 @@ elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2. have [G1 | ntG] := boolP (G :==: 1). have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2). - by rewrite /= perm_eq_refl. + by rewrite /= perm_refl. have [sG | nsG] := boolP (simple G). - by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_eq_refl. + by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_refl. case es1: s1 cs1 => [|N1 st1] cs1. by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG. case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. @@ -228,9 +228,9 @@ have i3 : perm_eq fG1 fG2. rewrite (@perm_catCA _ [::_] [::_]) /mksrepr. rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1). rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). - exact: perm_eq_refl. -apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym. -by apply: perm_eq_trans i2; apply: perm_eq_refl. + exact: perm_refl. +apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym. +by apply: perm_trans i2; apply: perm_refl. Qed. End CompositionSeries. @@ -593,11 +593,11 @@ elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2. case/orP: (orbN (G :==: 1)) => [tG | ntG]. have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2). - by rewrite /= perm_eq_refl. + by rewrite /= perm_refl. case/orP: (orbN (asimple to G))=> [sG | nsG]. have -> : s1 = [:: 1%G ] by apply/(asimple_acompsP cs1). have -> : s2 = [:: 1%G ] by apply/(asimple_acompsP cs2). - by rewrite /= perm_eq_refl. + by rewrite /= perm_refl. case es1: s1 cs1 => [|N1 st1] cs1. by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG. case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. @@ -667,9 +667,9 @@ have i3 : perm_eq fG1 fG2. rewrite (@perm_catCA _ [::_] [::_]) /mksrepr. rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1). rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). - exact: perm_eq_refl. -apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym. -by apply: perm_eq_trans i2; apply: perm_eq_refl. + exact: perm_refl. +apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym. +by apply: perm_trans i2; apply: perm_refl. Qed. End StrongJordanHolder. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index f3d79fc..0dfb4d1 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1642,4 +1642,4 @@ Qed. End SCN. -Arguments SCN_P {gT G A}.
\ No newline at end of file +Arguments SCN_P {gT G A}. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 85fd47c..67e9c4b 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1274,11 +1274,11 @@ Variable op : Monoid.com_law 1. Local Notation "'*%M'" := op (at level 0). Local Notation "x * y" := (op x y). -Lemma eq_big_perm (I : eqType) r1 r2 (P : pred I) F : +Lemma perm_big (I : eqType) r1 r2 (P : pred I) F : perm_eq r1 r2 -> \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i. Proof. -move/perm_eqP; rewrite !(big_mkcond _ _ P). +move/permP; rewrite !(big_mkcond _ _ P). elim: r1 r2 => [|i r1 IHr1] r2 eq_r12. by case: r2 eq_r12 => // i r2; move/(_ (pred1 i)); rewrite /= eqxx. have r2i: i \in r2 by rewrite -has_pred1 has_count -eq_r12 /= eqxx. @@ -1290,8 +1290,8 @@ 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: eq_big_perm. -by rewrite filter_index_enum uniq_perm_eq ?enum_uniq // => i; rewrite mem_enum. +move=> uniq_r; rewrite -(big_filter _ _ _ (mem r)); apply: perm_big. +by rewrite filter_index_enum uniq_perm ?enum_uniq // => i; rewrite mem_enum. Qed. Lemma big_rem (I : eqType) r x (P : pred I) F : @@ -1299,7 +1299,7 @@ Lemma big_rem (I : eqType) r x (P : pred I) F : \big[*%M/1]_(y <- r | P y) F y = (if P x then F x else 1) * \big[*%M/1]_(y <- rem x r | P y) F y. Proof. -by move/perm_to_rem/(eq_big_perm _)->; rewrite !(big_mkcond _ _ P) big_cons. +by move/perm_to_rem/(perm_big _)->; rewrite !(big_mkcond _ _ P) big_cons. Qed. Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F : @@ -1316,15 +1316,15 @@ Lemma eq_big_idem (I : eqType) (r1 r2 : seq I) (P : pred I) F : idempotent *%M -> r1 =i r2 -> \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i. Proof. -move=> idM eq_r; rewrite -big_undup // -(big_undup r2) //; apply/eq_big_perm. -by rewrite uniq_perm_eq ?undup_uniq // => i; rewrite !mem_undup eq_r. +move=> idM eq_r; rewrite -big_undup // -(big_undup r2) //; apply/perm_big. +by rewrite uniq_perm ?undup_uniq // => i; rewrite !mem_undup eq_r. Qed. Lemma big_undup_iterop_count (I : eqType) (r : seq I) (P : pred I) F : \big[*%M/1]_(i <- undup r | P i) iterop (count_mem i r) *%M (F i) 1 = \big[*%M/1]_(i <- r | P i) F i. Proof. -rewrite -[RHS](eq_big_perm _ F (perm_undup_count _)) big_flatten big_map. +rewrite -[RHS](perm_big _ F (perm_count_undup _)) big_flatten big_map. by rewrite big_mkcond; apply: eq_bigr => i _; rewrite big_nseq_cond iteropE. Qed. @@ -1536,7 +1536,7 @@ Arguments big1_eq [R idx op I]. Arguments big1_seq [R idx op I]. Arguments big1 [R idx op I]. Arguments big_pred1 [R idx op I] i [P F]. -Arguments eq_big_perm [R idx op I r1] r2 [P F]. +Arguments perm_big [R idx op I r1] r2 [P F]. Arguments big_uniq [R idx op I] r [F]. Arguments big_rem [R idx op I r] x [P F]. Arguments bigID [R idx op I r]. @@ -1824,4 +1824,9 @@ Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m : Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed. Arguments biggcdn_inf [I] i0 [P F m]. -Unset Implicit Arguments. +Notation "@ 'eq_big_perm'" := + (deprecate eq_big_perm perm_big) (at level 10, only parsing). + +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). diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index c260105..06774ff 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -45,7 +45,7 @@ transitivity (\sum_(1 <= i < n.+1) \sum_(1 <= k < n.+1) (p ^ k %| i)). by apply: andb_idr => /dvdn_leq/(leq_trans (ltn_expl _ (prime_gt1 _)))->. by rewrite exchange_big_nat; apply: eq_bigr => i _; rewrite divn_count_dvd. Qed. - + Theorem Wilson p : p > 1 -> prime p = (p %| ((p.-1)`!).+1). Proof. have dFact n: 0 < n -> (n.-1)`! = \prod_(0 <= i < n | i != 0) i. @@ -310,7 +310,7 @@ Qed. Lemma subn_exp m n k : m ^ k - n ^ k = (m - n) * (\sum_(i < k) m ^ (k.-1 -i) * n ^ i). Proof. -case: k => [|k]; first by rewrite big_ord0. +case: k => [|k]; first by rewrite big_ord0 muln0. rewrite mulnBl !big_distrr big_ord_recl big_ord_recr /= subn0 muln1. rewrite subnn mul1n -!expnS subnDA; congr (_ - _); apply: canRL (addnK _) _. congr (_ + _); apply: eq_bigr => i _. @@ -543,4 +543,3 @@ by apply: val_inj; congr (_ :: _); apply: val_inj; rewrite /= -{1}def_n addnK. Qed. End Combinations. - diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index fda425d..3cb98e8 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -538,7 +538,7 @@ Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n. Proof. by rewrite addnC gcdnDl. Qed. Lemma gcdnMl n m : gcdn n (m * n) = n. -Proof. by case: n => [|n]; rewrite gcdnE modnMl gcd0n. Qed. +Proof. by case: n => [|n]; rewrite gcdnE modnMl // muln0. Qed. Lemma gcdnMr n m : gcdn n (n * m) = n. Proof. by rewrite mulnC gcdnMl. Qed. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 3fbc110..7e1cdc8 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -196,6 +196,15 @@ Proof. exact/eqP/eqP. Qed. Hint Resolve eq_refl eq_sym : core. +Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set := + | EqNotNeq of x = y : eq_xor_neq x y true true + | NeqNotEq of x != y : eq_xor_neq x y false false. + +Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y). +Proof. by rewrite eq_sym; case: (altP eqP); constructor. Qed. + +Arguments eqVneq {T} x y, {T x y}. + Section Contrapositives. Variables (T1 T2 : eqType). @@ -370,9 +379,6 @@ Proof. by move->; rewrite eqxx. Qed. Lemma predU1r : b -> (x == y) || b. Proof. by move->; rewrite orbT. Qed. -Lemma eqVneq : {x = y} + {x != y}. -Proof. by case: eqP; [left | right]. Qed. - End EqPred. Arguments predU1P {T x y b}. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 204843a..beac009 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -72,6 +72,16 @@ From mathcomp Require Import choice fintype finfun bigop. (* comprehension as Coq parsing confuses [x | P] and [E | x]. *) (* minset p A == A is a minimal set satisfying p. *) (* maxset p A == A is a maximal set satisfying p. *) +(* Provided a monotonous function F : {set T} -> {set T}, we get fixpoints *) +(* fixset F := iter #|T| F set0 *) +(* == the least fixpoint of F *) +(* == the minimal set such that F X == X *) +(* fix_order F x == the minimum number of iterations so that *) +(* x is in iter (fix_order F x) F set0 *) +(* funsetC F := fun X => ~: F (~: X) *) +(* cofixset F == the greatest fixpoint of F *) +(* == the maximal set such that F X == X *) +(* := ~: fixset (funsetC F) *) (* We also provide notations A :=: B, A :<>: B, A :==: B, A :!=: B, A :=P: B *) (* that specialize A = B, A <> B, A == B, etc., to {set _}. This is useful *) (* for subtypes of {set T}, such as {group T}, that coerce to {set T}. *) @@ -232,14 +242,16 @@ Definition setTfor (phT : phant T) := [set x : T | true]. Lemma in_setT x : x \in setTfor (Phant T). Proof. by rewrite in_set. Qed. -Lemma eqsVneq A B : {A = B} + {A != B}. -Proof. exact: eqVneq. Qed. +Lemma eqsVneq A B : eq_xor_neq A B (B == A) (A == B). +Proof. by apply: eqVneq. Qed. Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB. Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed. End BasicSetTheory. +Arguments eqsVneq {T} A B, {T A B}. + Definition inE := (in_set, inE). Arguments set0 {T}. @@ -2211,3 +2223,131 @@ Arguments setCK {T}. Arguments minsetP {T P A}. Arguments maxsetP {T P A}. Prenex Implicits minset maxset. + +Section SetFixpoint. + +Section Least. +Variables (T : finType) (F : {set T} -> {set T}). +Hypothesis (F_mono : {homo F : X Y / X \subset Y}). + +Let n := #|T|. +Let iterF i := iter i F set0. + +Lemma subset_iterS i : iterF i \subset iterF i.+1. +Proof. by elim: i => [| i IHi]; rewrite /= ?sub0set ?F_mono. Qed. + +Lemma subset_iter : {homo iterF : i j / i <= j >-> i \subset j}. +Proof. +by apply: homo_leq => //[? ? ?|]; [apply: subset_trans|apply: subset_iterS]. +Qed. + +Definition fixset := iterF n. + +Lemma fixsetK : F fixset = fixset. +Proof. +suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1]. + by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix. +apply: contraT; rewrite negb_exists => /forallP /(_ (Ordinal _)) /= neq_iter. +suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. + by have := iter_big _ (leqnn _); rewrite ltnNge max_card. +elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))). +by rewrite proper_card// properEneq// subset_iterS neq_iter. +Qed. +Hint Resolve fixsetK. + +Lemma minset_fix : minset [pred X | F X == X] fixset. +Proof. +apply/minsetP; rewrite inE fixsetK eqxx; split=> // X /eqP FXeqX Xsubfix. +apply/eqP; rewrite eqEsubset Xsubfix/=. +suff: fixset \subset iter n F X by rewrite iter_fix. +by rewrite /fixset; elim: n => //= [|m IHm]; rewrite ?sub0set ?F_mono. +Qed. + +Lemma fixsetKn k : iter k F fixset = fixset. +Proof. by rewrite iter_fix. Qed. + +Lemma iter_sub_fix k : iterF k \subset fixset. +Proof. +have [/subset_iter //|/ltnW/subnK<-] := leqP k n; +by rewrite /iterF iter_add fixsetKn. +Qed. + +Lemma fix_order_proof x : x \in fixset -> exists n, x \in iterF n. +Proof. by move=> x_fix; exists n. Qed. + +Definition fix_order (x : T) := + if (x \in fixset) =P true isn't ReflectT x_fix then 0 + else (ex_minn (fix_order_proof x_fix)). + +Lemma fix_order_le_max (x : T) : fix_order x <= n. +Proof. +rewrite /fix_order; case: eqP => //= x_in. +by case: ex_minnP => //= ? ?; apply. +Qed. + +Lemma in_iter_fix_orderE (x : T) : + (x \in iterF (fix_order x)) = (x \in fixset). +Proof. +rewrite /fix_order; case: eqP; last by move=>/negP/negPf->; rewrite inE. +by move=> x_in; case: ex_minnP => m ->; rewrite x_in. +Qed. + +Lemma fix_order_gt0 (x : T) : (fix_order x > 0) = (x \in fixset). +Proof. +rewrite /fix_order; case: eqP => [x_in|/negP/negPf->//]. +by rewrite x_in; case: ex_minnP => -[|m]; rewrite ?inE//= => _; apply. +Qed. + +Lemma fix_order_eq0 (x : T) : (fix_order x == 0) = (x \notin fixset). +Proof. by rewrite -fix_order_gt0 -ltnNge ltnS leqn0. Qed. + +Lemma in_iter_fixE (x : T) k : (x \in iterF k) = (0 < fix_order x <= k). +Proof. +rewrite /fix_order; case: eqP => //= [x_in|/negP xNin]; last first. + by apply: contraNF xNin; apply/subsetP/iter_sub_fix. +case: ex_minnP => -[|m]; rewrite ?inE// => xm mP. +by apply/idP/idP=> [/mP//|lt_mk]; apply: subsetP xm; apply: subset_iter. +Qed. + +Lemma in_iter (x : T) k : x \in fixset -> fix_order x <= k -> x \in iterF k. +Proof. by move=> x_in xk; rewrite in_iter_fixE fix_order_gt0 x_in xk. Qed. + +Lemma notin_iter (x : T) k : k < fix_order x -> x \notin iterF k. +Proof. by move=> k_le; rewrite in_iter_fixE negb_and orbC -ltnNge k_le. Qed. + +Lemma fix_order_small x k : x \in iterF k -> fix_order x <= k. +Proof. by rewrite in_iter_fixE => /andP[]. Qed. + +Lemma fix_order_big x k : x \in fixset -> x \notin iterF k -> fix_order x > k. +Proof. by move=> x_in; rewrite in_iter_fixE fix_order_gt0 x_in /= -ltnNge. Qed. + +Lemma le_fix_order (x y : T) : y \in iterF (fix_order x) -> + fix_order y <= fix_order x. +Proof. exact: fix_order_small. Qed. + +End Least. + +Section Greatest. +Variables (T : finType) (F : {set T} -> {set T}). +Hypothesis (F_mono : {homo F : X Y / X \subset Y}). + +Definition funsetC X := ~: (F (~: X)). +Lemma funsetC_mono : {homo funsetC : X Y / X \subset Y}. +Proof. by move=> *; rewrite subCset setCK F_mono// subCset setCK. Qed. +Hint Resolve funsetC_mono. + +Definition cofixset := ~: fixset funsetC. + +Lemma cofixsetK : F cofixset = cofixset. +Proof. by rewrite /cofixset -[in RHS]fixsetK ?setCK. Qed. + +Lemma maxset_cofix : maxset [pred X | F X == X] cofixset. +Proof. +rewrite maxminset setCK. +rewrite (@minset_eq _ _ [pred X | funsetC X == X]) ?minset_fix//. +by move=> X /=; rewrite (can2_eq setCK setCK). +Qed. + +End Greatest. + +End SetFixpoint. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 4d0d208..037adb8 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -430,13 +430,13 @@ Lemma eq_sorted : antisymmetric leT -> forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2. Proof. move=> leT_asym; elim=> [|x1 s1 IHs1] s2 //= ord_s1 ord_s2 eq_s12. - by case: {+}s2 (perm_eq_size eq_s12). -have s2_x1: x1 \in s2 by rewrite -(perm_eq_mem eq_s12) mem_head. + by case: {+}s2 (perm_size eq_s12). +have s2_x1: x1 \in s2 by rewrite -(perm_mem eq_s12) mem_head. case: s2 s2_x1 eq_s12 ord_s2 => //= x2 s2; rewrite in_cons. case: eqP => [<- _| ne_x12 /= s2_x1] eq_s12 ord_s2. by rewrite {IHs1}(IHs1 s2) ?(@path_sorted x1) // -(perm_cons x1). case: (ne_x12); apply: leT_asym; rewrite (allP (order_path_min ord_s2)) //. -have: x2 \in x1 :: s1 by rewrite (perm_eq_mem eq_s12) mem_head. +have: x2 \in x1 :: s1 by rewrite (perm_mem eq_s12) mem_head. case/predU1P=> [eq_x12 | s1_x2]; first by case ne_x12. by rewrite (allP (order_path_min ord_s1)). Qed. @@ -447,7 +447,7 @@ Proof. move=> leT_irr s1 s2 s1_sort s2_sort eq_s12. have: antisymmetric leT. by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm. -by move/eq_sorted; apply=> //; apply: uniq_perm_eq => //; apply: sorted_uniq. +by move/eq_sorted; apply=> //; apply: uniq_perm => //; apply: sorted_uniq. Qed. End Transitive. @@ -482,20 +482,20 @@ Qed. Lemma perm_merge s1 s2 : perm_eql (merge s1 s2) (s1 ++ s2). Proof. -apply/perm_eqlP; rewrite perm_eq_sym; elim: s1 s2 => //= x1 s1 IHs1. +apply/permPl; rewrite perm_sym; elim: s1 s2 => //= x1 s1 IHs1. elim=> [|x2 s2 IHs2]; rewrite /= ?cats0 //. case: ifP => _ /=; last by rewrite perm_cons. by rewrite (perm_catCA (_ :: _) [::x2]) perm_cons. Qed. Lemma mem_merge s1 s2 : merge s1 s2 =i s1 ++ s2. -Proof. by apply: perm_eq_mem; rewrite perm_merge. Qed. +Proof. by apply: perm_mem; rewrite perm_merge. Qed. Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2). -Proof. by apply: perm_eq_size; rewrite perm_merge. Qed. +Proof. by apply: perm_size; rewrite perm_merge. Qed. Lemma merge_uniq s1 s2 : uniq (merge s1 s2) = uniq (s1 ++ s2). -Proof. by apply: perm_eq_uniq; rewrite perm_merge. Qed. +Proof. by apply: perm_uniq; rewrite perm_merge. Qed. Fixpoint merge_sort_push s1 ss := match ss with @@ -531,30 +531,30 @@ Qed. Lemma perm_sort s : perm_eql (sort s) s. Proof. -rewrite /sort; apply/perm_eqlP; pose catss := foldr (@cat T) [::]. -rewrite perm_eq_sym -{1}[s]/(catss [::] ++ s). +rewrite /sort; apply/permPl; pose catss := foldr (@cat T) [::]. +rewrite perm_sym -{1}[s]/(catss [::] ++ s). elim: {s}_.+1 {-2}s [::] (ltnSn (size s)) => // n IHn s ss. have: perm_eq (catss ss ++ s) (merge_sort_pop s ss). - elim: ss s => //= s2 ss IHss s1; rewrite -{IHss}(perm_eqrP (IHss _)). + elim: ss s => //= s2 ss IHss s1; rewrite -{IHss}(permPr (IHss _)). by rewrite perm_catC catA perm_catC perm_cat2l -perm_merge. case: s => // x1 [//|x2 s _]; move/ltnW; move/IHn=> {n IHn}IHs. -rewrite -{IHs}(perm_eqrP (IHs _)) ifE; set s1 := if_expr _ _ _. +rewrite -{IHs}(permPr (IHs _)) ifE; set s1 := if_expr _ _ _. rewrite (catA _ [:: _; _] s) {s}perm_cat2r. -apply: (@perm_eq_trans _ (catss ss ++ s1)). +apply: (@perm_trans _ (catss ss ++ s1)). by rewrite perm_cat2l /s1 -ifE; case: ifP; rewrite // (perm_catC [:: _]). elim: ss {x1 x2}s1 => /= [|s2 ss IHss] s1; first by rewrite cats0. rewrite perm_catC; case def_s2: {2}s2=> /= [|y s2']; first by rewrite def_s2. -by rewrite catA -{IHss}(perm_eqrP (IHss _)) perm_catC perm_cat2l -perm_merge. +by rewrite catA -{IHss}(permPr (IHss _)) perm_catC perm_cat2l -perm_merge. Qed. Lemma mem_sort s : sort s =i s. -Proof. by apply: perm_eq_mem; rewrite perm_sort. Qed. +Proof. by apply: perm_mem; rewrite perm_sort. Qed. Lemma size_sort s : size (sort s) = size s. -Proof. by apply: perm_eq_size; rewrite perm_sort. Qed. +Proof. by apply: perm_size; rewrite perm_sort. Qed. Lemma sort_uniq s : uniq (sort s) = uniq s. -Proof. by apply: perm_eq_uniq; rewrite perm_sort. Qed. +Proof. by apply: perm_uniq; rewrite perm_sort. Qed. Lemma perm_sortP : transitive leT -> antisymmetric leT -> forall s1 s2, reflect (sort s1 = sort s2) (perm_eq s1 s2). @@ -562,7 +562,7 @@ Proof. move=> leT_tr leT_asym s1 s2. apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. apply: eq_sorted; rewrite ?sort_sorted //. -by rewrite perm_sort (perm_eqlP eq12) -perm_sort. +by rewrite perm_sort (permPl eq12) -perm_sort. Qed. End SortSeq. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index bcb163c..16e44e2 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -569,8 +569,8 @@ rewrite mem_seq1 mem_primes prime_gt0 //=. by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2. Qed. -Lemma coprime_has_primes m n : m > 0 -> n > 0 -> - coprime m n = ~~ has (mem (primes m)) (primes n). +Lemma coprime_has_primes m n : + 0 < m -> 0 < n -> coprime m n = ~~ has (mem (primes m)) (primes n). Proof. move=> m_gt0 n_gt0; apply/eqnP/hasPn=> [mn1 p | no_p_mn]. rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n]. @@ -1344,8 +1344,8 @@ Proof. move=> co_mn; have [-> //| m_gt0] := posnP m. have [->|n_gt0] := posnP n; first by rewrite !muln0. rewrite !totientE ?muln_gt0 ?m_gt0 //. -have /(eq_big_perm _)->: perm_eq (primes (m * n)) (primes m ++ primes n). - apply: uniq_perm_eq => [||p]; first exact: primes_uniq. +have /(perm_big _)->: perm_eq (primes (m * n)) (primes m ++ primes n). + apply: uniq_perm => [||p]; first exact: primes_uniq. by rewrite cat_uniq !primes_uniq -coprime_has_primes // co_mn. by rewrite mem_cat primes_mul. rewrite big_cat /= !big_seq. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 5576355..9581a95 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -76,7 +76,15 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* find p s == the index of the first item in s for which p holds, *) (* or size s if no such item is found. *) (* count p s == the number of items of s for which p holds. *) -(* count_mem x s == the number of times x occurs in s := count (pred1 x) s. *) +(* count_mem x s == the multiplicity of x in s, i.e., count (pred1 x) s. *) +(* tally s == a tally of s, i.e., a sequence of (item, multiplicity) *) +(* pairs for all items in sequence s (without duplicates). *) +(* incr_tally bs x == increment the multiplicity of x in the tally bs, or add *) +(* x with multiplicity 1 at then end if x is not in bs. *) +(* bs \is a wf_tally <=> bs is well-formed tally, with no duplicate items or *) +(* null multiplicities. *) +(* tally_seq bs == the expansion of a tally bs into a sequence where each *) +(* (x, n) pair expands into a sequence of n x's. *) (* constant s <=> all items in s are identical (trivial if s = [::]). *) (* uniq s <=> all the items in s are pairwise different. *) (* subseq s1 s2 <=> s1 is a subsequence of s2, i.e., s1 = mask m s2 for *) @@ -84,11 +92,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* perm_eq s1 s2 <=> s2 is a permutation of s1, i.e., s1 and s2 have the *) (* items (with the same repetitions), but possibly in a *) (* different order. *) -(* permutations s == a duplicate-free list of all permutations of s. *) (* perm_eql s1 s2 <-> s1 and s2 behave identically on the left of perm_eq. *) (* perm_eqr s1 s2 <-> s1 and s2 behave identically on the right of perm_eq. *) (* --> These left/right transitive versions of perm_eq make it easier to *) (* chain a sequence of equivalences. *) +(* permutations s == a duplicate-free list of all permutations of s. *) (* ** Filtering: *) (* filter p s == the subsequence of s consisting of all the items *) (* for which the (boolean) predicate p holds. *) @@ -183,18 +191,16 @@ Open Scope seq_scope. (* Inductive seq (T : Type) : Type := Nil | Cons of T & seq T. *) Notation seq := list. -Prenex Implicits cons. +Bind Scope seq_scope with list. +Arguments cons {T%type} x s%SEQ : rename. +Arguments nil {T%type} : rename. Notation Cons T := (@cons T) (only parsing). Notation Nil T := (@nil T) (only parsing). -Bind Scope seq_scope with list. -Arguments cons _%type _ _%SEQ. - (* As :: and ++ are (improperly) declared in Init.datatypes, we only rebind *) (* them here. *) Infix "::" := cons : seq_scope. -(* GG - this triggers a camlp4 warning, as if this Notation had been Reserved *) Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope. Notation "[ :: x1 ]" := (x1 :: [::]) @@ -496,16 +502,20 @@ Proof. by elim: n => //= n ->; apply: orKb. Qed. Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x. Proof. by rewrite all_nseq eqb0 implybE. Qed. +Lemma filter_nseq n x : filter (nseq n x) = nseq (a x * n) x. +Proof. by elim: n => /= [|n ->]; case: (a x). Qed. + +Lemma count_nseq n x : count (nseq n x) = a x * n. +Proof. by rewrite -size_filter filter_nseq size_nseq. Qed. + Lemma find_nseq n x : find (nseq n x) = ~~ a x * n. -Proof. by elim: n => //= n ->; case: (a x). Qed. +Proof. by elim: n => /= [|n ->]; case: (a x). Qed. Lemma nth_find s : has s -> a (nth s (find s)). -Proof. by elim: s => //= x s IHs; case Hx: (a x). Qed. +Proof. by elim: s => //= x s IHs; case a_x: (a x). Qed. Lemma before_find s i : i < find s -> a (nth s i) = false. -Proof. -by elim: s i => //= x s IHs; case Hx: (a x) => [|] // [|i] //; apply: (IHs i). -Qed. +Proof. by elim: s i => //= x s IHs; case: ifP => // a'x [|i] // /(IHs i). Qed. Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2. Proof. by elim: s1 => //= x s1 ->; case (a x). Qed. @@ -782,9 +792,6 @@ Qed. Lemma rot_inj : injective (rot n0). Proof. exact (can_inj rotK). Qed. -Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x. -Proof. by rewrite /rot /= take0 drop0 -cats1. Qed. - (* (efficient) reversal *) Fixpoint catrev s1 s2 := if s1 is x :: s1' then catrev s1' (x :: s2) else s2. @@ -873,14 +880,37 @@ Proof. by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs. Qed. +Section RotRcons. + +Variable T : Type. +Implicit Types (x : T) (s : seq T). + +Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x. +Proof. by rewrite /rot /= take0 drop0 -cats1. Qed. + +Lemma rcons_inj s1 s2 x1 x2 : + rcons s1 x1 = rcons s2 x2 :> seq T -> (s1, x1) = (s2, x2). +Proof. by rewrite -!rot1_cons => /rot_inj[-> ->]. Qed. + +Lemma rcons_injl x : injective (rcons^~ x). +Proof. by move=> s1 s2 /rcons_inj[]. Qed. + +Lemma rcons_injr s : injective (rcons s). +Proof. by move=> x1 x2 /rcons_inj[]. Qed. + +End RotRcons. + +Arguments rcons_inj {T s1 x1 s2 x2} eq_rcons : rename. +Arguments rcons_injl {T} x [s1 s2] eq_rcons : rename. +Arguments rcons_injr {T} s [x1 x2] eq_rcons : rename. + (* Equality and eqType for seq. *) Section EqSeq. Variables (n0 : nat) (T : eqType) (x0 : T). Local Notation nth := (nth x0). -Implicit Type s : seq T. -Implicit Types x y z : T. +Implicit Types (x y z : T) (s : seq T). Fixpoint eqseq s1 s2 {struct s2} := match s1, s2 with @@ -928,7 +958,7 @@ Proof. by rewrite -size_eq0 size_filter has_count lt0n. Qed. Fixpoint mem_seq (s : seq T) := if s is y :: s' then xpredU1 y (mem_seq s') else xpred0. -Definition seq_eqclass := seq T. +Definition seq_eqclass := seq T. Identity Coercion seq_of_eqclass : seq_eqclass >-> seq. Coercion pred_of_seq (s : seq_eqclass) : {pred T} := mem_seq s. @@ -1098,10 +1128,11 @@ Proof. by case: s => //= y s /andP[/eqP->]. Qed. Lemma all_pred1_nseq x n : all (pred1 x) (nseq n x). Proof. by rewrite all_nseq /= eqxx orbT. Qed. +Lemma mem_nseq n x y : (y \in nseq n x) = (0 < n) && (y == x). +Proof. by rewrite -has_pred1 has_nseq eq_sym. Qed. + Lemma nseqP n x y : reflect (y = x /\ n > 0) (y \in nseq n x). -Proof. -by rewrite -has_pred1 has_nseq /= eq_sym andbC; apply: (iffP andP) => -[/eqP]. -Qed. +Proof. by rewrite mem_nseq andbC; apply: (iffP andP) => -[/eqP]. Qed. Lemma constant_nseq n x : constant (nseq n x). Proof. exact: all_pred1_constant (all_pred1_nseq x n). Qed. @@ -1141,8 +1172,8 @@ Proof. by rewrite -cats1 uniq_catC. Qed. Lemma filter_uniq s a : uniq s -> uniq (filter a s). Proof. -elim: s => [|x s IHs] //= /andP[Hx Hs]; case (a x); auto. -by rewrite /= mem_filter /= (negbTE Hx) andbF; auto. +elim: s => //= x s IHs /andP[s'x]; case: ifP => //= a_x /IHs->. +by rewrite mem_filter a_x s'x. Qed. Lemma rot_uniq s : uniq (rot n0 s) = uniq s. @@ -1160,7 +1191,7 @@ Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed. Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s). Proof. elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. -by rewrite in_cons eq_sym; case: eqP => // ->; rewrite s'y. +by rewrite in_cons; case: eqVneq => // <-; rewrite s'y. Qed. Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. @@ -1180,7 +1211,7 @@ Proof. by elim: s => //= x s IHs; case: (x \in s) => //=; apply: ltnW. Qed. Lemma mem_undup s : undup s =i s. Proof. move=> x; elim: s => //= y s IHs. -by case Hy: (y \in s); rewrite in_cons IHs //; case: eqP => // ->. +by case s_y: (y \in s); rewrite !inE IHs //; case: eqP => [->|]. Qed. Lemma undup_uniq s : uniq (undup s). @@ -1193,7 +1224,7 @@ Proof. by elim: s => //= x s IHs /andP[/negbTE-> /IHs->]. Qed. Lemma ltn_size_undup s : (size (undup s) < size s) = ~~ uniq s. Proof. -by elim: s => //= x s IHs; case Hx: (x \in s); rewrite //= ltnS size_undup. +by elim: s => //= x s IHs; case s_x: (x \in s); rewrite //= ltnS size_undup. Qed. Lemma filter_undup p s : filter p (undup s) = undup (filter p s). @@ -1222,13 +1253,15 @@ Lemma index_cat x s1 s2 : index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2. Proof. by rewrite /index find_cat has_pred1. Qed. -Lemma index_uniq i s : i < size s -> uniq s -> index (nth s i) s = i. +Lemma nthK s: uniq s -> {in gtn (size s), cancel (nth s) (index^~ s)}. Proof. -elim: s i => [|x s IHs] //= [|i]; rewrite /= ?eqxx // ltnS => lt_i_s. -case/andP=> not_s_x /(IHs i)-> {IHs}//. -by case: eqP not_s_x => // ->; rewrite mem_nth. +elim: s => //= x s IHs /andP[s'x Us] i; rewrite inE ltnS eq_sym -if_neg. +by case: i => /= [_|i lt_i_s]; rewrite ?eqxx ?IHs ?(memPn s'x) ?mem_nth. Qed. +Lemma index_uniq i s : i < size s -> uniq s -> index (nth s i) s = i. +Proof. by move/nthK. Qed. + Lemma index_head x s : index x (x :: s) = 0. Proof. by rewrite /= eqxx. Qed. @@ -1240,10 +1273,7 @@ Qed. Lemma nth_uniq s i j : i < size s -> j < size s -> uniq s -> (nth s i == nth s j) = (i == j). -Proof. -move=> lt_i_s lt_j_s Us; apply/eqP/eqP=> [eq_sij|-> //]. -by rewrite -(index_uniq lt_i_s Us) eq_sij index_uniq. -Qed. +Proof. by move=> lti ltj /nthK/can_in_eq->. Qed. Lemma uniqPn s : reflect (exists i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s). @@ -1254,11 +1284,11 @@ elim: s => // x s IHs /nandP[/negbNE | /IHs[i [j]]]; last by exists i.+1, j.+1. by exists 0, (index x s).+1; rewrite !ltnS index_mem /= nth_index. Qed. -Lemma uniqP s : reflect {in [pred i | i < size s] &, injective (nth s)} (uniq s). +Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s). Proof. -apply: (iffP idP) => [????? /eqP|]; first by rewrite nth_uniq // => /eqP. -move=> nth_inj; apply/uniqPn => -[i [j [ltij ltjs /nth_inj ]]]. -by move=> /(_ (ltn_trans ltij ltjs)) /(_ ltjs) eq_ij; rewrite eq_ij ltnn in ltij. +apply: (iffP idP) => [/nthK/can_in_inj// | nth_inj]. +apply/uniqPn => -[i [j [ltij ltjs /nth_inj/eqP/idPn]]]. +by rewrite !inE (ltn_trans ltij ltjs) ltn_eqF //=; case. Qed. Lemma mem_rot s : rot n0 s =i s. @@ -1273,7 +1303,7 @@ Lemma rot_to s x : x \in s -> rot_to_spec s x. Proof. move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s). rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs. -by rewrite eq_sym in_cons; case: eqP => // -> _; rewrite drop0. +by rewrite in_cons; case: eqVneq => // -> _; rewrite drop0. Qed. End EqSeq. @@ -1291,6 +1321,8 @@ Arguments allP {T a s}. Arguments allPn {T a s}. Arguments nseqP {T n x y}. Arguments count_memPn {T x s}. +Arguments uniqPn {T} x0 {s}. +Arguments uniqP {T} x0 {s}. Section NthTheory. @@ -1379,7 +1411,7 @@ Implicit Type s : seq T. Definition perm_eq s1 s2 := all [pred x | count_mem x s1 == count_mem x s2] (s1 ++ s2). -Lemma perm_eqP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2). +Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2). Proof. apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP. elim: {a}_.+1 {-2}a (ltnSn (count a (s1 ++ s2))) => // n IHn a le_an. @@ -1394,60 +1426,62 @@ apply: leq_trans le_an. by rewrite ltnS cnt_a' -add1n leq_add2r -has_count has_pred1. Qed. -Lemma perm_eq_refl s : perm_eq s s. -Proof. exact/perm_eqP. Qed. -Hint Resolve perm_eq_refl : core. +Lemma perm_refl s : perm_eq s s. +Proof. exact/permP. Qed. +Hint Resolve perm_refl : core. -Lemma perm_eq_sym : symmetric perm_eq. -Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed. +Lemma perm_sym : symmetric perm_eq. +Proof. by move=> s1 s2; apply/permP/permP=> eq_s12 a. Qed. -Lemma perm_eq_trans : transitive perm_eq. -Proof. by move=> s2 s1 s3 /perm_eqP-eq12 /perm_eqP/(ftrans eq12)/perm_eqP. Qed. +Lemma perm_trans : transitive perm_eq. +Proof. by move=> s2 s1 s3 /permP-eq12 /permP/(ftrans eq12)/permP. Qed. Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2). Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2). -Lemma perm_eqlE s1 s2 : perm_eql s1 s2 -> perm_eq s1 s2. Proof. by move->. Qed. +Lemma permEl s1 s2 : perm_eql s1 s2 -> perm_eq s1 s2. Proof. by move->. Qed. -Lemma perm_eqlP s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2). +Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2). Proof. -apply: (iffP idP) => [eq12 s3 | -> //]. -apply/idP/idP; last exact: perm_eq_trans. -by rewrite -!(perm_eq_sym s3); move/perm_eq_trans; apply. +apply: (iffP idP) => [eq12 s3 | -> //]; apply/idP/idP; last exact: perm_trans. +by rewrite -!(perm_sym s3) => /perm_trans; apply. Qed. -Lemma perm_eqrP s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2). +Lemma permPr s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2). Proof. -apply: (iffP idP) => [/perm_eqlP eq12 s3| <- //]. -by rewrite !(perm_eq_sym s3) eq12. +by apply/(iffP idP) => [/permPl eq12 s3| <- //]; rewrite !(perm_sym s3) eq12. Qed. Lemma perm_catC s1 s2 : perm_eql (s1 ++ s2) (s2 ++ s1). -Proof. by apply/perm_eqlP; apply/perm_eqP=> a; rewrite !count_cat addnC. Qed. +Proof. by apply/permPl/permP=> a; rewrite !count_cat addnC. Qed. Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3. Proof. -apply/perm_eqP/perm_eqP=> eq23 a; apply/eqP; +apply/permP/permP=> eq23 a; apply/eqP; by move/(_ a)/eqP: eq23; rewrite !count_cat eqn_add2l. Qed. -Lemma perm_catl s1 s2 s3 : perm_eq s2 s3 -> perm_eql (s1 ++ s2) (s1 ++ s3). -Proof. by move=> eq_s23; apply/perm_eqlP; rewrite perm_cat2l. Qed. +Lemma perm_catl s t1 t2 : perm_eq t1 t2 -> perm_eql (s ++ t1) (s ++ t2). +Proof. by move=> eq_t12; apply/permPl; rewrite perm_cat2l. Qed. Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2. Proof. exact: (perm_cat2l [::x]). Qed. Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3. -Proof. by do 2!rewrite perm_eq_sym perm_catC; apply: perm_cat2l. Qed. +Proof. by do 2!rewrite perm_sym perm_catC; apply: perm_cat2l. Qed. -Lemma perm_catr s1 s2 s3 : perm_eq s1 s2 -> perm_eql (s1 ++ s3) (s2 ++ s3). -Proof. by move=> eq_s12; apply/perm_eqlP; rewrite perm_cat2r. Qed. +Lemma perm_catr s1 s2 t : perm_eq s1 s2 -> perm_eql (s1 ++ t) (s2 ++ t). +Proof. by move=> eq_s12; apply/permPl; rewrite perm_cat2r. Qed. + +Lemma perm_cat s1 s2 t1 t2 : + perm_eq s1 s2 -> perm_eq t1 t2 -> perm_eq (s1 ++ t1) (s2 ++ t2). +Proof. by move=> /perm_catr-> /perm_catl->. Qed. Lemma perm_catAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2). -Proof. by apply/perm_eqlP; rewrite -!catA perm_cat2l perm_catC. Qed. +Proof. by apply/permPl; rewrite -!catA perm_cat2l perm_catC. Qed. Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3). -Proof. by apply/perm_eqlP; rewrite !catA perm_cat2r perm_catC. Qed. +Proof. by apply/permPl; rewrite !catA perm_cat2r perm_catC. Qed. Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s). Proof. by move=> /= s2; rewrite -cats1 perm_catC. Qed. @@ -1458,33 +1492,49 @@ Proof. by move=> /= s2; rewrite perm_catC cat_take_drop. Qed. Lemma perm_rotr n s : perm_eql (rotr n s) s. Proof. exact: perm_rot. Qed. -Lemma perm_eq_rev s : perm_eq s (rev s). -Proof. by apply/perm_eqP=> i; rewrite count_rev. Qed. +Lemma perm_rev s : perm_eql (rev s) s. +Proof. by apply/permPl/permP=> i; rewrite count_rev. Qed. -Lemma perm_filter s1 s2 P : - perm_eq s1 s2 -> perm_eq (filter P s1) (filter P s2). +Lemma perm_filter s1 s2 a : + perm_eq s1 s2 -> perm_eq (filter a s1) (filter a s2). Proof. -by move/perm_eqP=> s12_count; apply/perm_eqP=> Q; rewrite !count_filter. +by move/permP=> s12_count; apply/permP=> Q; rewrite !count_filter. Qed. Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s. Proof. -apply/perm_eqlP; elim: s => //= x s IHs. +apply/permPl; elim: s => //= x s IHs. by case: (a x); last rewrite /= -cat1s perm_catCA; rewrite perm_cons. Qed. -Lemma perm_eq_mem s1 s2 : perm_eq s1 s2 -> s1 =i s2. -Proof. by move/perm_eqP=> eq12 x; rewrite -!has_pred1 !has_count eq12. Qed. +Lemma perm_size s1 s2 : perm_eq s1 s2 -> size s1 = size s2. +Proof. by move/permP=> eq12; rewrite -!count_predT eq12. Qed. + +Lemma perm_mem s1 s2 : perm_eq s1 s2 -> s1 =i s2. +Proof. by move/permP=> eq12 x; rewrite -!has_pred1 !has_count eq12. Qed. + +Lemma perm_nilP s : reflect (s = [::]) (perm_eq s [::]). +Proof. by apply: (iffP idP) => [/perm_size/eqP/nilP | ->]. Qed. + +Lemma perm_consP x s t : + reflect (exists i u, rot i t = x :: u /\ perm_eq u s) + (perm_eq t (x :: s)). +Proof. +apply: (iffP idP) => [eq_txs | [i [u [Dt eq_us]]]]. + have /rot_to[i u Dt]: x \in t by rewrite (perm_mem eq_txs) mem_head. + by exists i, u; rewrite -(perm_cons x) -Dt perm_rot. +by rewrite -(perm_rot i) Dt perm_cons. +Qed. -Lemma perm_eq_all s1 s2 P : perm_eq s1 s2 -> all P s1 = all P s2. -Proof. by move/perm_eq_mem/eq_all_r. Qed. +Lemma perm_has s1 s2 a : perm_eq s1 s2 -> has a s1 = has a s2. +Proof. by move/perm_mem/eq_has_r. Qed. -Lemma perm_eq_size s1 s2 : perm_eq s1 s2 -> size s1 = size s2. -Proof. by move/perm_eqP=> eq12; rewrite -!count_predT eq12. Qed. +Lemma perm_all s1 s2 a : perm_eq s1 s2 -> all a s1 = all a s2. +Proof. by move/perm_mem/eq_all_r. Qed. -Lemma perm_eq_small s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2. +Lemma perm_small_eq s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2. Proof. -move=> s2_le1 eqs12; move/perm_eq_size: eqs12 s2_le1 (perm_eq_mem eqs12). +move=> s2_le1 eqs12; move/perm_size: eqs12 s2_le1 (perm_mem eqs12). by case: s2 s1 => [|x []] // [|y []] // _ _ /(_ x); rewrite !inE eqxx => /eqP->. Qed. @@ -1516,52 +1566,42 @@ move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12]. by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12). Qed. -Lemma leq_size_perm s1 s2 : +Lemma uniq_min_size s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> - s1 =i s2 /\ size s1 = size s2. + (size s1 = size s2) * (s1 =i s2). Proof. move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21. -suffices: s1 =i s2 by split; last by apply/eqP; rewrite -uniq_size_uniq. +suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq. move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x. rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //. by apply/allP; rewrite /= s2x; apply/allP. Qed. -Lemma perm_uniq s1 s2 : s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2. +Lemma eq_uniq s1 s2 : size s1 = size s2 -> s1 =i s2 -> uniq s1 = uniq s2. Proof. -move=> Es12 Esz12. -by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?Esz12 ?eqxx. +move=> eq_sz12 eq_s12. +by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?eq_sz12 ?eqxx. Qed. -Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2. -Proof. -by move=> eq_s12; apply: perm_uniq; [apply: perm_eq_mem | apply: perm_eq_size]. -Qed. +Lemma perm_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2. +Proof. by move=> eq_s12; apply/eq_uniq; [apply/perm_size | apply/perm_mem]. Qed. -Lemma uniq_perm_eq s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2. +Lemma uniq_perm s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2. Proof. move=> Us1 Us2 eq12; apply/allP=> x _; apply/eqP. by rewrite !count_uniq_mem ?eq12. Qed. -Lemma count_mem_uniq s : (forall x, count_mem x s = (x \in s)) -> uniq s. +Lemma perm_undup s1 s2 : s1 =i s2 -> perm_eq (undup s1) (undup s2). Proof. -move=> count1_s; have Uus := undup_uniq s. -suffices: perm_eq s (undup s) by move/perm_eq_uniq->. -by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup. +by move=> Es12; rewrite uniq_perm ?undup_uniq // => s; rewrite !mem_undup. Qed. -Lemma perm_eq_nilP s : reflect (s = [::]) (perm_eq s [::]). -Proof. by case: s => [|x s]; rewrite /perm_eq /= ?eqxx; constructor. Qed. - -Lemma perm_eq_consP x s t : - reflect (exists i t1, rot i t = x :: t1 /\ perm_eq s t1) - (perm_eq (x :: s) t). +Lemma count_mem_uniq s : (forall x, count_mem x s = (x \in s)) -> uniq s. Proof. -rewrite perm_eq_sym; apply: (iffP idP) => [eq_ts | [i [t1 [Dt eq_st]]]]. - have /rot_to[i t1 Dt]: x \in t by rewrite (perm_eq_mem eq_ts) mem_head. - by exists i, t1; rewrite -(perm_cons x) -Dt perm_eq_sym perm_rot. -by rewrite -(perm_rot i) Dt perm_cons perm_eq_sym. +move=> count1_s; have Uus := undup_uniq s. +suffices: perm_eq s (undup s) by move/perm_uniq->. +by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup. Qed. Lemma catCA_perm_ind P : @@ -1570,8 +1610,8 @@ Lemma catCA_perm_ind P : Proof. move=> PcatCA s1 s2 eq_s12; rewrite -[s1]cats0 -[s2]cats0. elim: s2 nil => [|x s2 IHs] s3 in s1 eq_s12 *. - by case: s1 {eq_s12}(perm_eq_size eq_s12). -have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_eq_mem eq_s12) mem_head. + by case: s1 {eq_s12}(perm_size eq_s12). +have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_mem eq_s12) mem_head. rewrite -(cat_take_drop i s1) -catA => /PcatCA. rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply. by rewrite -(perm_cons x) -def_s1 perm_rot. @@ -1590,16 +1630,16 @@ End PermSeq. Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2). Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2). -Arguments perm_eqP {T s1 s2}. -Arguments perm_eqlP {T s1 s2}. -Arguments perm_eqrP {T s1 s2}. +Arguments permP {T s1 s2}. +Arguments permPl {T s1 s2}. +Arguments permPr {T s1 s2}. Prenex Implicits perm_eq. -Hint Resolve perm_eq_refl : core. +Hint Resolve perm_refl : core. Section RotrLemmas. Variables (n0 : nat) (T : Type) (T' : eqType). -Implicit Type s : seq T. +Implicit Types (x : T) (s : seq T). Lemma size_rotr s : size (rotr n0 s) = size s. Proof. by rewrite size_rot. Qed. @@ -1908,13 +1948,13 @@ Qed. Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s). Proof. -elim: s => // y s IHs; rewrite inE /= eq_sym perm_eq_sym. +elim: s => // y s IHs; rewrite inE /= eq_sym perm_sym. case: eqP => [-> // | _ /IHs]. -by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_eq_sym. +by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_sym. Qed. Lemma size_rem s : x \in s -> size (rem s) = (size s).-1. -Proof. by move/perm_to_rem/perm_eq_size->. Qed. +Proof. by move/perm_to_rem/perm_size->. Qed. Lemma rem_subseq s : subseq (rem s) s. Proof. @@ -2067,8 +2107,8 @@ Lemma subseq_uniqP s1 s2 : Proof. move=> uniq_s2; apply: (iffP idP) => [ss12 | ->]; last exact: filter_subseq. apply/eqP; rewrite -size_subseq_leqif ?subseq_filter ?(introT allP) //. -apply/eqP/esym/perm_eq_size. -rewrite uniq_perm_eq ?filter_uniq ?(subseq_uniq ss12) // => x. +apply/eqP/esym/perm_size. +rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. @@ -2093,18 +2133,14 @@ Implicit Type s : seq T1. Lemma map_f s x : x \in s -> f x \in map f s. Proof. -elim: s => [|y s IHs] //=. -by case/predU1P=> [->|Hx]; [apply: predU1l | apply: predU1r; auto]. +by elim: s => //= y s IHs /predU1P[->|/IHs]; [apply: predU1l | apply: predU1r]. Qed. Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s). Proof. -elim: s => [|x s IHs]; first by right; case. -rewrite /= in_cons eq_sym; case Hxy: (f x == y). - by left; exists x; [rewrite mem_head | rewrite (eqP Hxy)]. -apply: (iffP IHs) => [[x' Hx' ->]|[x' Hx' Dy]]. - by exists x'; first apply: predU1r. -by move: Dy Hxy => ->; case/predU1P: Hx' => [->|]; [rewrite eqxx | exists x']. +elim: s => [|x s IHs]; [by right; case | rewrite /= inE]. +have [Dy | fx'y] := y =P f x; first by left; exists x; rewrite ?mem_head. +by apply: (iffP IHs) => [[z]|[z /predU1P[->|]]]; exists z; do ?apply: predU1r. Qed. Lemma map_uniq s : uniq (map f s) -> uniq s. @@ -2131,12 +2167,12 @@ Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x. Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. -move: s_x; rewrite inE eq_sym; case: eqP => [-> | _] //=; apply: IHs. +move: s_x; rewrite inE; case: eqVneq => [-> | _] //=; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed. Lemma perm_map s t : perm_eq s t -> perm_eq (map f s) (map f t). -Proof. by move/perm_eqP=> Est; apply/perm_eqP=> a; rewrite !count_map Est. Qed. +Proof. by move/permP=> Est; apply/permP=> a; rewrite !count_map Est. Qed. Hypothesis Hf : injective f. @@ -2151,7 +2187,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed. Lemma perm_map_inj s t : perm_eq (map f s) (map f t) -> perm_eq s t. Proof. -move/perm_eqP=> Est; apply/allP=> x _ /=. +move/permP=> Est; apply/allP=> x _ /=. have Dx: pred1 x =1 preim f (pred1 (f x)) by move=> y /=; rewrite inj_eq. by rewrite !(eq_count Dx) -!count_map Est. Qed. @@ -2342,14 +2378,14 @@ Variable T : eqType. Lemma mkseq_uniq (f : nat -> T) n : injective f -> uniq (mkseq f n). Proof. by move/map_inj_uniq->; apply: iota_uniq. Qed. -Lemma perm_eq_iotaP {s t : seq T} x0 (It := iota 0 (size t)) : +Lemma perm_iotaP {s t : seq T} x0 (It := iota 0 (size t)) : reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t). Proof. apply: (iffP idP) => [Est | [Is eqIst ->]]; last first. by rewrite -{2}[t](mkseq_nth x0) perm_map. elim: t => [|x t IHt] in s It Est *. - by rewrite (perm_eq_small _ Est) //; exists [::]. -have /rot_to[k s1 Ds]: x \in s by rewrite (perm_eq_mem Est) mem_head. + by rewrite (perm_small_eq _ Est) //; exists [::]. +have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head. have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot. exists (rotr k (0 :: map succn Is1)). by rewrite perm_rot /It /= perm_cons (iota_addl 1) perm_map. @@ -2358,7 +2394,7 @@ Qed. End MakeEqSeq. -Arguments perm_eq_iotaP {T s t}. +Arguments perm_iotaP {T s t}. Section FoldRight. @@ -2391,15 +2427,22 @@ Proof. by rewrite mulnC; elim: n => //= n ->. Qed. Lemma sumn_cat s1 s2 : sumn (s1 ++ s2) = sumn s1 + sumn s2. Proof. by elim: s1 => //= x s1 ->; rewrite addnA. Qed. -Lemma sumn_count T (P : pred T) s : - sumn [seq (P i : nat) | i <- s] = count P s. +Lemma sumn_count T (a : pred T) s : sumn [seq a i : nat | i <- s] = count a s. Proof. by elim: s => //= s0 s /= ->. Qed. Lemma sumn_rcons s n : sumn (rcons s n) = sumn s + n. Proof. by rewrite -cats1 sumn_cat /= addn0. Qed. +Lemma perm_sumn s1 s2 : perm_eq s1 s2 -> sumn s1 = sumn s2. +Proof. +by apply/catCA_perm_subst: s1 s2 => s1 s2 s3; rewrite !sumn_cat addnCA. +Qed. + +Lemma sumn_rot s n : sumn (rot n s) = sumn s. +Proof. by apply/perm_sumn; rewrite perm_rot. Qed. + Lemma sumn_rev s : sumn (rev s) = sumn s. -Proof. by elim: s => //= x s <-; rewrite rev_cons sumn_rcons addnC. Qed. +Proof. by apply/perm_sumn; rewrite perm_rev. Qed. Lemma natnseq0P s : reflect (s = nseq (size s) 0) (sumn s == 0). Proof. @@ -2753,7 +2796,7 @@ Qed. Lemma perm_flatten (ss1 ss2 : seq (seq T)) : perm_eq ss1 ss2 -> perm_eq (flatten ss1) (flatten ss2). Proof. -move=> eq_ss; apply/perm_eqP=> a; apply/catCA_perm_subst: ss1 ss2 eq_ss. +move=> eq_ss; apply/permP=> a; apply/catCA_perm_subst: ss1 ss2 eq_ss. by move=> ss1 ss2 ss3; rewrite !flatten_cat !count_cat addnCA. Qed. @@ -2762,20 +2805,6 @@ End EqFlatten. Arguments flattenP {T A x}. Arguments flatten_mapP {S T A s y}. -Lemma perm_undup_count (T : eqType) (s : seq T) : - perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s. -Proof. -pose N x r := count_mem x (flatten [seq nseq (count_mem y s) y | y <- r]). -apply/allP=> x _; rewrite /= -/(N x _). -have Nx0 r (r'x : x \notin r): N x r = 0. - by apply/count_memPn; apply: contra r'x => /flatten_mapP[y r_y /nseqP[->]]. -have [|s'x] := boolP (x \in s); last by rewrite Nx0 ?mem_undup ?(count_memPn _). -rewrite -mem_undup => /perm_to_rem/catCA_perm_subst->; last first. - by move=> s1 s2 s3; rewrite /N !map_cat !flatten_cat !count_cat addnCA. -rewrite /N /= count_cat -/(N x _) Nx0 ?mem_rem_uniq ?undup_uniq ?inE ?eqxx //. -by rewrite addn0 -{2}(size_nseq (_ s) x) -all_count all_pred1_nseq. -Qed. - Notation "[ 'seq' E | x <- s , y <- t ]" := (flatten [seq [seq E | y <- t] | x <- s]) (at level 0, E at level 99, x ident, y ident, @@ -2820,7 +2849,7 @@ Lemma allpairs_mapr f (g : forall x, T' x -> T x) s t : [seq f x y | x <- s, y <- map (g x) (t x)] = [seq f x (g x y) | x <- s, y <- t x]. Proof. by rewrite -(eq_map (fun=> map_comp _ _ _)). Qed. - + End AllPairsDep. Arguments allpairs_dep {S T R} f s t /. @@ -2949,68 +2978,248 @@ Qed. End EqAllPairs. Arguments allpairsP {S T R f s t z}. -Arguments perm_eq_nilP {T s}. -Arguments perm_eq_consP {T x s t}. +Arguments perm_nilP {T s}. +Arguments perm_consP {T x s t}. Section Permutations. Variable T : eqType. +Implicit Types (x : T) (s t : seq T) (bs : seq (T * nat)) (acc : seq (seq T)). + +Fixpoint incr_tally bs x := + if bs isn't b :: bs then [:: (x, 1)] else + if x == b.1 then (x, b.2.+1) :: bs else b :: incr_tally bs x. + +Definition tally s := foldl incr_tally [::] s. + +Definition wf_tally := + [qualify a bs : seq (T * nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs)]. + +Definition tally_seq bs := flatten [seq nseq b.2 b.1 | b <- bs]. +Local Notation tseq := tally_seq. + +Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs). +Proof. +rewrite size_flatten /shape -map_comp; congr sumn. +by apply/eq_map=> b; apply: size_nseq. +Qed. + +Lemma tally_seqK : {in wf_tally, cancel tally_seq tally}. +Proof. +move=> bs /andP[]; elim: bs => [|[x [|n]] bs IHbs] //= /andP[bs'x Ubs] bs'0. +rewrite inE /tseq /tally /= -[n.+1]addn1 in bs'0 *. +elim: n 1 => /= [|n IHn] m; last by rewrite eqxx IHn addnS. +rewrite -{}[in RHS]IHbs {Ubs bs'0}// /tally /tally_seq add0n. +elim: bs bs'x [::] => [|[y n] bs IHbs] //=; rewrite inE => /norP[y'x bs'x]. +by elim: n => [|n IHn] bs1 /=; [rewrite IHbs | rewrite eq_sym ifN // IHn]. +Qed. + +Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}. +Proof. +move=> bs /andP[]; rewrite unfold_in. +elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs]; rewrite inE /= => bs'0. +rewrite eq_sym; case: ifP => [/eqP<- | y'x] /=; first by rewrite bs'y Ubs. +rewrite -andbA {}IHbs {Ubs bs'0}// andbT. +elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y]. +by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs. +Qed. + +Lemma tallyP s : tally s \is a wf_tally. +Proof. +rewrite /tally; set bs := [::]; have: bs \in wf_tally by []. +by elim: s bs => //= x s IHs bs /(incr_tallyP x)/IHs. +Qed. + +Lemma tallyK s : perm_eq (tally_seq (tally s)) s. +Proof. +rewrite -[s in perm_eq _ s]cats0 -[nil]/(tseq [::]) /tally. +elim: s [::] => //= x s IHs bs; rewrite {IHs}(permPl (IHs _)). +rewrite perm_sym -cat1s perm_catCA {s}perm_cat2l. +elim: bs => //= b bs IHbs; case: eqP => [-> | _] //=. +by rewrite -cat1s perm_catCA perm_cat2l. +Qed. + +Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s). +Proof. +have /andP[Ubs bs'0] := tallyP s; set bs := tally s in Ubs bs'0 *. +rewrite uniq_perm ?undup_uniq {Ubs}// => x. +rewrite mem_undup -(perm_mem (tallyK s)) -/bs. +elim: bs => [|[y [|m]] bs IHbs] //= in bs'0 *. +by rewrite inE IHbs // mem_cat mem_nseq. +Qed. + +Lemma tallyE s : perm_eq (tally s) [seq (x, count_mem x s) | x <- undup s]. +Proof. +have /andP[Ubs _] := tallyP s; pose b := [fun s x => (x, count_mem x (tseq s))]. +suffices /permPl->: perm_eq (tally s) (map (b (tally s)) (unzip1 (tally s))). + congr perm_eq: (perm_map (b (tally s)) (tallyEl s)). + by apply/eq_map=> x; rewrite /= (permP (tallyK s)). +elim: (tally s) Ubs => [|[x m] bs IH] //= /andP[bs'x /IH-IHbs {IH}]. +rewrite /tseq /= -/(tseq _) count_cat count_nseq /= eqxx mul1n. +rewrite (count_memPn _) ?addn0 ?perm_cons; last first. + apply: contra bs'x; elim: {b IHbs}bs => //= b bs IHbs. + by rewrite mem_cat mem_nseq inE andbC; case: (_ == _). +congr perm_eq: IHbs; apply/eq_in_map=> y bs_y; congr (y, _). +by rewrite count_cat count_nseq /= (negPf (memPnC bs'x y bs_y)). +Qed. + +Lemma perm_tally s1 s2 : perm_eq s1 s2 -> perm_eq (tally s1) (tally s2). +Proof. +move=> eq_s12; apply: (@perm_trans _ [seq (x, count_mem x s2) | x <- undup s1]). + by congr perm_eq: (tallyE s1); apply/eq_map=> x; rewrite (permP eq_s12). +by rewrite (permPr (tallyE s2)); apply/perm_map/perm_undup/(perm_mem eq_s12). +Qed. + +Lemma perm_tally_seq bs1 bs2 : + perm_eq bs1 bs2 -> perm_eq (tally_seq bs1) (tally_seq bs2). +Proof. by move=> Ebs12; rewrite perm_flatten ?perm_map. Qed. +Local Notation perm_tseq := perm_tally_seq. + +Lemma perm_count_undup s : + perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s. +Proof. +by rewrite -(permPr (tallyK s)) (permPr (perm_tseq (tallyE s))) /tseq -map_comp. +Qed. -Fixpoint permutations (s : seq T) := - if s isn't x :: s1 then [:: nil] else - let insert_x t i := take i t ++ x :: drop i t in - [seq insert_x t i | t <- permutations s1, i <- iota 0 (index x t + 1)]. +Local Fixpoint cons_perms_ perms_rec (s : seq T) bs bs2 acc := + if bs isn't b :: bs1 then acc else + if b isn't (x, m.+1) then cons_perms_ perms_rec s bs1 bs2 acc else + let acc_xs := perms_rec (x :: s) ((x, m) :: bs1 ++ bs2) acc in + cons_perms_ perms_rec s bs1 (b :: bs2) acc_xs. + +Local Fixpoint perms_rec n s bs acc := + if n isn't n.+1 then s :: acc else cons_perms_ (perms_rec n) s bs [::] acc. +Local Notation cons_perms n := (cons_perms_ (perms_rec n) [::]). + +Definition permutations s := perms_rec (size s) [::] (tally s) [::]. + +Let permsP s : exists n bs, + [/\ permutations s = perms_rec n [::] bs [::], + size (tseq bs) == n, perm_eq (tseq bs) s & uniq (unzip1 bs)]. +Proof. +have /andP[Ubs _] := tallyP s; exists (size s), (tally s). +by rewrite (perm_size (tallyK s)) tallyK. +Qed. + +Local Notation bsCA := (permEl (perm_catCA _ [:: _] _)). +Let cons_permsE : forall n x bs bs1 bs2, + let cp := cons_perms n bs bs2 in let perms s := perms_rec n s bs1 [::] in + cp (perms [:: x]) = cp [::] ++ [seq rcons t x | t <- perms [::]]. +Proof. +pose is_acc f := forall acc, f acc = f [::] ++ acc. (* f is accumulating. *) +have cpE: forall f & forall s bs, is_acc (f s bs), is_acc (cons_perms_ f _ _ _). + move=> s bs bs2 f fE acc; elim: bs => [|[x [|m]] bs IHbs] //= in s bs2 acc *. + by rewrite fE IHbs catA -IHbs. +have prE: is_acc (perms_rec _ _ _) by elim=> //= n IHn s bs; apply: cpE. +pose has_suffix f := forall s : seq T, f s = [seq t ++ s | t <- f [::]]. +suffices prEs n bs: has_suffix (fun s => perms_rec n s bs [::]). + move=> n x bs bs1 bs2 /=; rewrite cpE // prEs; congr (_ ++ _). + by apply/eq_map=> t; rewrite cats1. +elim: n bs => //= n IHn bs s; elim: bs [::] => [|[x [|m]] bs IHbs] //= bs1. +rewrite cpE // IHbs IHn [in RHS]cpE // [in RHS]IHn map_cat -map_comp. +by congr (_ ++ _); apply: eq_map => t /=; rewrite -catA. +Qed. Lemma mem_permutations s t : (t \in permutations s) = perm_eq t s. Proof. -elim: s => [|x s IHs] /= in t *; first by rewrite inE (sameP perm_eq_nilP eqP). -apply/allpairsPdep/idP=> [[t1 [i [Et1s _ ->]]] | Ets]. - by rewrite -cat1s perm_catCA /= cat_take_drop perm_cons -IHs. -pose i := index x t; pose t1 := take i t; pose t2 := drop i.+1 t. -have sz_t1: size t1 = i by rewrite size_takel ?index_size. -have t_x: x \in t by rewrite (perm_eq_mem Ets) mem_head. -have Dt: t = t1 ++ x :: t2. - by rewrite -(nth_index x t_x) -drop_nth ?index_mem ?cat_take_drop. -exists (t1 ++ t2), i; split; last by rewrite take_size_cat ?drop_size_cat. - by rewrite IHs -(perm_cons x) -cat1s perm_catCA /= -Dt. -rewrite mem_iota addn1 ltnS /= /i Dt !index_cat /= eqxx addn0. -by case: ifP; rewrite ?leq_addr. +have{s} [n [bs [-> Dn /permPr<- _]]] := permsP s. +elim: n => [|n IHn] /= in t bs Dn *. + by rewrite inE (nilP Dn); apply/eqP/perm_nilP. +rewrite -[bs in tseq bs]cats0 in Dn *; have x0 : T by case: (tseq _) Dn. +rewrite -[RHS](@andb_idl (last x0 t \in tseq bs)); last first. + case/lastP: t {IHn} => [|t x] Dt; first by rewrite -(perm_size Dt) in Dn. + by rewrite -[bs]cats0 -(perm_mem Dt) last_rcons mem_rcons mem_head. +elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn *. +rewrite cons_permsE -!cat_cons !mem_cat (mem_nseq m.+1) orbC andb_orl. +rewrite {}IHbs ?(perm_size (perm_tseq bsCA)) //= (permPr (perm_tseq bsCA)). +congr (_ || _); apply/mapP/andP=> [[t1 Dt1 ->] | [/eqP]]. + by rewrite last_rcons perm_rcons perm_cons IHn in Dt1 *. +case/lastP: t => [_ /perm_size//|t y]; rewrite last_rcons perm_rcons => ->. +by rewrite perm_cons; exists t; rewrite ?IHn. Qed. -Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s). +Lemma permutations_uniq s : uniq (permutations s). Proof. -by move=> Us; apply/allP=> t; rewrite mem_permutations => /perm_eq_uniq->. +have{s} [n [bs [-> Dn _ Ubs]]] := permsP s. +elim: n => //= n IHn in bs Dn Ubs *; rewrite -[bs]cats0 /unzip1 in Dn Ubs. +elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn Ubs *. + by case/andP: Ubs => _ /IHbs->. +rewrite /= cons_permsE cat_uniq has_sym andbCA andbC. +rewrite {}IHbs; first 1 last; first by rewrite (perm_size (perm_tseq bsCA)). + by rewrite (perm_uniq (perm_map _ bsCA)). +rewrite (map_inj_uniq (rcons_injl x)) {}IHn {Dn}//=. +have: x \notin unzip1 bs by apply: contraL Ubs; rewrite map_cat mem_cat => ->. +move: {bs2 m Ubs}(perms_rec n _ _ _) (_ :: bs2) => ts. +elim: bs => [|[y [|m]] bs IHbs] //=; rewrite inE => bs2 /norP[x'y /IHbs//]. +rewrite cons_permsE has_cat negb_or has_map => ->. +by apply/hasPn=> t _; apply: contra x'y => /mapP[t1 _ /rcons_inj[_ ->]]. +Qed. + +Notation perms := permutations. +Lemma permutationsE s : + 0 < size s -> + perm_eq (perms s) [seq x :: t | x <- undup s, t <- perms (rem x s)]. +Proof. +move=> nt_s; apply/uniq_perm=> [||t]; first exact: permutations_uniq. + apply/allpairs_uniq_dep=> [|x _|]; rewrite ?undup_uniq ?permutations_uniq //. + by case=> [_ _] [x t] _ _ [-> ->]. +rewrite mem_permutations; apply/idP/allpairsPdep=> [Dt | [x [t1 []]]]. + rewrite -(perm_size Dt) in nt_s; case: t nt_s => // x t _ in Dt *. + have s_x: x \in s by rewrite -(perm_mem Dt) mem_head. + exists x, t; rewrite mem_undup mem_permutations; split=> //. + by rewrite -(perm_cons x) (permPl Dt) perm_to_rem. +rewrite mem_undup mem_permutations -(perm_cons x) => s_x Dt1 ->. +by rewrite (permPl Dt1) perm_sym perm_to_rem. +Qed. + +Lemma permutationsErot x s (le_x := fun t => iota 0 (index x t + 1)) : + perm_eq (perms (x :: s)) [seq rot i (x :: t) | t <- perms s, i <- le_x t]. +Proof. +have take'x t i: i <= index x t -> i <= size t /\ x \notin take i t. + move=> le_i_x; have le_i_t: i <= size t := leq_trans le_i_x (index_size x t). + case: (nthP x) => // -[j lt_j_i /eqP]; rewrite size_takel // in lt_j_i. + by rewrite nth_take // [_ == _](before_find x (leq_trans lt_j_i le_i_x)). +pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)). +have xrotK t: {in le_x t, cancel (xrot t) xrotV}. + move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x]. + rewrite -rot_addn ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev. + by rewrite ifN // size_takel //= eqxx addn0. +apply/uniq_perm=> [||t]; first exact: permutations_uniq. + apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //. + move=> _ _ /allpairsPdep[t [i [_ ? ->]]] /allpairsPdep[u [j [_ ? ->]]] Etu. + have Eij: i = j by rewrite -(xrotK t i) // /xrot Etu xrotK. + by move: Etu; rewrite Eij => /rot_inj[->]. +rewrite mem_permutations; apply/esym; apply/allpairsPdep/idP=> [[u [i]] | Dt]. + rewrite mem_permutations => -[Du _ /(canLR (rotK i))]; rewrite /rotr. + by set j := (j in rot j _) => Dt; apply/perm_consP; exists j, u. +pose r := rev (rot 1 t); pose i := index x r; pose u := rev (take i r). +have r_x: x \in r by rewrite mem_rev mem_rot (perm_mem Dt) mem_head. +have [v Duv]: {v | rot i (x :: u ++ v) = t}; first exists (rev (drop i.+1 r)). + rewrite -rev_cat -rev_rcons -rot1_cons -cat_cons -(nth_index x r_x). + by rewrite -drop_nth ?index_mem // rot_rot !rev_rot revK rotK rotrK. +exists (u ++ v), i; rewrite mem_permutations -(perm_cons x) -(perm_rot i) Duv. +rewrite mem_iota addn1 ltnS /= index_cat mem_rev size_rev. +by have /take'x[le_i_t ti'x] := leqnn i; rewrite ifN ?size_takel ?leq_addr. Qed. Lemma size_permutations s : uniq s -> size (permutations s) = (size s)`!. Proof. -elim: s => //= x s IH /andP[s'x /IH-{IH}IHs]; rewrite factS -IHs mulnC. -rewrite -(size_allpairs mem _ (x :: s)) !size_allpairs_dep. -congr sumn; apply/eq_in_map => t; rewrite mem_permutations => Est. -rewrite size_iota -(cats0 t) index_cat (perm_eq_mem Est) addn1 ifN //. -by rewrite addn0 (perm_eq_size Est). +move Dn: (size s) => n Us; elim: n s => [[]|n IHn s] //= in Dn Us *. +rewrite (perm_size (permutationsE _)) ?Dn // undup_id // factS -Dn. +rewrite -(size_iota 0 n`!) -(size_allpairs (fun=>id)) !size_allpairs_dep. +by apply/congr1/eq_in_map=> x sx; rewrite size_iota IHn ?size_rem ?Dn ?rem_uniq. Qed. -Lemma permutations_uniq s : uniq (permutations s). +Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s). Proof. -elim: s => //= x s IHs. -rewrite allpairs_uniq_dep {IHs}// => [t _ |]; first exact: iota_uniq. -move=> _ _ /allpairsPdep[t [i [_ leix ->]]] /allpairsPdep[u [j [_ lejx ->]]] /=. -rewrite !mem_iota /= !addn1 !ltnS in leix lejx *; set tx := {-}(_ ++ _). -gen have Dj, Di: i t @tx leix / ((index x tx = i) * (size (take i t) = i))%type. - have Di: size (take i t) = i by apply/size_takel/(leq_trans leix)/index_size. - rewrite index_cat /= eqxx addn0 Di ifN //; apply: contraL leix => ti_x. - by rewrite -ltnNge -Di -{1}(cat_take_drop i t) index_cat ti_x index_mem. -move=> eq_tu; have eq_ij: i = j by rewrite -Di eq_tu Dj. -move/eqP: eq_tu; rewrite eqseq_cat ?Dj // eqseq_cons eqxx /= -eqseq_cat ?Dj //. -by rewrite !cat_take_drop eq_ij => /eqP->. +by move=> Us; apply/allP=> t; rewrite mem_permutations => /perm_uniq->. Qed. Lemma perm_permutations s t : perm_eq s t -> perm_eq (permutations s) (permutations t). Proof. -move=> Est; apply/uniq_perm_eq; try exact: permutations_uniq. -by move=> u; rewrite !mem_permutations (perm_eqrP Est). +move=> Est; apply/uniq_perm; try exact: permutations_uniq. +by move=> u; rewrite !mem_permutations (permPr Est). Qed. End Permutations. @@ -3056,3 +3265,41 @@ Coercion all_iffP : all_iff >-> Funclass. Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..)) (at level 0, format "[ '<->' '[' P0 ; '/' P1 ; '/' .. ; '/' Pn ']' ]") : form_scope. + +(* Temporary backward compatibility. *) +Notation perm_eqP := (deprecate perm_eqP permP) (only parsing). +Notation perm_eqlP := (deprecate perm_eqlP permPl) (only parsing). +Notation perm_eqrP := (deprecate perm_eqrP permPr) (only parsing). +Notation perm_eqlE := (deprecate perm_eqlE permEl _ _ _) (only parsing). +Notation perm_eq_refl := (deprecate perm_eq_refl perm_refl _) (only parsing). +Notation perm_eq_sym := (deprecate perm_eq_sym perm_sym _) (only parsing). +Notation "@ 'perm_eq_trans'" := (deprecate perm_eq_trans perm_trans) + (at level 10, only parsing). +Notation perm_eq_trans := (@perm_eq_trans _ _ _ _) (only parsing). +Notation perm_eq_size := (deprecate perm_eq_size perm_size _ _ _) + (only parsing). +Notation perm_eq_mem := (deprecate perm_eq_mem perm_mem _ _ _) + (only parsing). +Notation perm_eq_uniq := (deprecate perm_eq_uniq perm_uniq _ _ _) + (only parsing). +Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _) + (only parsing). +Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _) + (only parsing). +Notation perm_eq_all := (deprecate perm_eq_all perm_all _ _ _) + (only parsing). +Notation perm_eq_small := (deprecate perm_eq_small perm_small_eq _ _ _) + (only parsing). +Notation perm_eq_nilP := (deprecate perm_eq_nilP perm_nilP) (only parsing). +Notation perm_eq_consP := (deprecate perm_eq_consP perm_consP) (only parsing). +Notation leq_size_perm := + ((fun T s1 s2 Us1 ss12 les21 => + let: (Esz12, Es12) := + deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21 + in conj Es12 Esz12) _ _ _) + (only parsing). +Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) + (only parsing). +Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing). +Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _) + (only parsing). diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 7eb7fd9..54c74dd 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -1,6 +1,18 @@ From mathcomp Require Import ssreflect ssrfun. From Coq Require Export ssrbool. +(******************************************************************************) +(* Local additions: *) +(* {pred T} == a type convertible to pred T but that presents the *) +(* pred_sort coercion class. *) +(* PredType toP == the predType structure for toP : A -> pred T. *) +(* relpre f r == the preimage of r by f, simplifying to r (f x) (f y). *) +(* --> These will become part of the core SSReflect library with Coq 8.11. *) +(* This file also anticipates a v8.11 change in the definition of simpl_pred *) +(* to T -> simpl_pred T. This change ensures that inE expands the definition *) +(* of r : simpl_rel along with the \in, when rewriting in y \in r x. *) +(******************************************************************************) + Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0, format "{ 'pred' T }") : type_scope. @@ -37,4 +49,3 @@ Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0, Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)). Definition relpre {T rT} (f : T -> rT) (r : rel rT) := [rel x y | r (f x) (f y)]. - diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index fe06c0d..2925496 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -5,6 +5,31 @@ Global Set SsrOldRewriteGoalsOrder. Global Set Asymmetric Patterns. Global Set Bullet Behavior "None". +(******************************************************************************) +(* Local additions: *) +(* nonPropType == an interface for non-Prop Types: a nonPropType coerces *) +(* to a Type, and only types that do _not_ have sort *) +(* Prop are canonical nonPropType instances. This is *) +(* useful for applied views. *) +(* --> This will become standard with the Coq v8.11 SSReflect core library. *) +(* deprecate old new == new, but warning that old is deprecated and new *) +(* should be used instead. *) +(* --> Usage: Notation old := (deprecate old new) (only parsing). *) +(* --> Caveat: deprecate old new only inherits new's maximal implicits; *) +(* on-demand implicits should be added after : (deprecate old new _). *) +(* --> Caveat 2: if premises or conclusions need to be adjusted, of for *) +(* non-prenex implicits, use the idiom: *) +(* Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) *) +(* _ _ ... _) (only printing). *) +(* where all the implicit a_i's occur first, and correspond to the *) +(* trailing _'s, making sure deprecate old new is fully applied and *) +(* there are _no implicits_ inside the (fun .. => ..) expression. This *) +(* is to avoid triggering a bug in SSReflect elaboration that is *) +(* triggered by such evars under binders. *) +(* Import Deprecation.Silent :: turn off deprecation warning messages. *) +(* Import Deprecation.Reject :: raise an error instead of only warning. *) +(******************************************************************************) + Module NonPropType. Structure call_of (condition : unit) (result : bool) := Call {callee : Type}. @@ -33,3 +58,39 @@ End Exports. End NonPropType. Export NonPropType.Exports. +Module Deprecation. + +Definition hidden (T : Type) := T. +Definition exposed (T : Type) & unit -> unit -> unit := T. +Definition hide T u (v : exposed T u) : hidden T := v. + +Ltac warn old_id new_id := + idtac "Warning:" old_id "is deprecated; use" new_id "instead". + +Ltac stop old_id new_id := + fail 1 "Error:" old_id "is deprecated; use" new_id "instead". + +Structure hinted := Hint {statement; hint : statement}. +Ltac check cond := let test := constr:(hint _ : cond) in idtac. + +Variant reject := Reject. +Definition reject_hint := Hint reject Reject. +Module Reject. Canonical reject_hint. End Reject. + +Variant silent := Silent. +Definition silent_hint := Hint silent Silent. +Module Silent. Canonical silent_hint. End Silent. + +Ltac flag old_id new_id := + first [check reject; stop old_id new_id | check silent | warn old_id new_id]. + +Module Exports. +Arguments hide {T} u v /. +Coercion hide : exposed >-> hidden. +Notation deprecate old_id new_id := + (hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id) + (only parsing). +End Exports. + +End Deprecation. +Export Deprecation.Exports. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 86f8fb2..5b667f0 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -106,6 +106,10 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +(* Disable Coq prelude hints to improve proof script robustness. *) + +Remove Hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm : core. + (* Declare legacy Arith operators in new scope. *) Delimit Scope coq_nat_scope with coq_nat. @@ -200,7 +204,7 @@ Lemma add1n n : 1 + n = n.+1. Proof. by []. Qed. Lemma addn0 : right_id 0 addn. Proof. by move=> n; apply/eqP; elim: n. Qed. -Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by elim: m. Qed. +Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by apply/eqP; elim: m. Qed. Lemma addSnnS m n : m.+1 + n = m + n.+1. Proof. by rewrite addnS. Qed. @@ -822,6 +826,9 @@ Proof. by elim: n => //= n ->. Qed. Lemma eq_iter f f' : f =1 f' -> forall n, iter n f =1 iter n f'. Proof. by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed. +Lemma iter_fix n f x : f x = x -> iter n f x = x. +Proof. by move=> fixf; elim: n => //= n ->. Qed. + Lemma eq_iteri f f' : f =2 f' -> forall n, iteri n f =1 iteri n f'. Proof. by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed. @@ -831,7 +838,7 @@ Proof. by move=> eq_op x; apply: eq_iteri; case. Qed. End Iteration. Lemma iter_succn m n : iter n succn m = m + n. -Proof. by elim: n => //= n ->. Qed. +Proof. by rewrite addnC; elim: n => //= n ->. Qed. Lemma iter_succn_0 n : iter n succn 0 = n. Proof. exact: iter_succn. Qed. @@ -1637,24 +1644,27 @@ case=> //=; elim=> //= p; case: (nat_of_pos p) => //= n [<-]. by rewrite natTrecE addnS /= addnS {2}addnn; elim: {1 3}n. Qed. -Lemma nat_of_succ_gt0 p : Pos.succ p = p.+1 :> nat. +Lemma nat_of_succ_pos p : Pos.succ p = p.+1 :> nat. Proof. by elim: p => //= p ->; rewrite !natTrecE. Qed. -Lemma nat_of_addn_gt0 p q : (p + q)%positive = p + q :> nat. +Lemma nat_of_add_pos p q : (p + q)%positive = p + q :> nat. Proof. apply: @fst _ (Pplus_carry p q = (p + q).+1 :> nat) _. elim: p q => [p IHp|p IHp|] [q|q|] //=; rewrite !natTrecE //; - by rewrite ?IHp ?nat_of_succ_gt0 ?(doubleS, doubleD, addn1, addnS). + by rewrite ?IHp ?nat_of_succ_pos ?(doubleS, doubleD, addn1, addnS). +Qed. + +Lemma nat_of_mul_pos p q : (p * q)%positive = p * q :> nat. +Proof. +elim: p => [p IHp|p IHp|] /=; rewrite ?mul1n //; + by rewrite ?nat_of_add_pos /= !natTrecE IHp doubleMl. Qed. Lemma nat_of_add_bin b1 b2 : (b1 + b2)%num = b1 + b2 :> nat. -Proof. by case: b1 b2 => [|p] [|q] //=; apply: nat_of_addn_gt0. Qed. +Proof. by case: b1 b2 => [|p] [|q]; rewrite ?addn0 //= nat_of_add_pos. Qed. Lemma nat_of_mul_bin b1 b2 : (b1 * b2)%num = b1 * b2 :> nat. -Proof. -case: b1 b2 => [|p] [|q] //=; elim: p => [p IHp|p IHp|] /=; - by rewrite ?(mul1n, nat_of_addn_gt0, mulSn) //= !natTrecE IHp doubleMl. -Qed. +Proof. by case: b1 b2 => [|p] [|q]; rewrite ?muln0 //= nat_of_mul_pos. Qed. Lemma nat_of_exp_bin n (b : N) : n ^ b = pow_N 1 muln n b. Proof. diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v index 4c55514..dbc7f3d 100644 --- a/mathcomp/ssreflect/ssrnotations.v +++ b/mathcomp/ssreflect/ssrnotations.v @@ -1,6 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +(******************************************************************************) (* - Reserved notation for various arithmetic and algebraic operations: *) (* e.[a1, ..., a_n] evaluation (e.g., polynomials). *) (* e`_i indexing (number list, integer pi-part). *) @@ -27,6 +28,7 @@ (* [rec a1, ..., an] standard shorthand for hidden recursor (see prime.v). *) (* The interpretation of these notations is not defined here, but the *) (* declarations help maintain consistency across the library. *) +(******************************************************************************) (* Reserved notation for evaluation *) Reserved Notation "e .[ x ]" |