diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/Make | 2 | ||||
| -rw-r--r-- | mathcomp/_CoqProject | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/inertia.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/vcharacter.v | 10 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 14 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 17 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 20 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 25 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 36 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 597 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 9 |
20 files changed, 517 insertions, 265 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index 4becdcb..bbb6433 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -95,3 +95,5 @@ test_suite/hierarchy_test.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/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 65167b5..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. @@ -2413,7 +2413,7 @@ 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] := uniq_min_size uniqSu sSuS; first by rewrite size_map. -by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)). +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 ae54fa1..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 /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..b610c36 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 _). @@ -577,5 +577,6 @@ 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..a51cbf2 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -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/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/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/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 76acaca..00e0a27 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. 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 @@ -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. @@ -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. @@ -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 t : perm_eq s1 s2 -> perm_eql (s1 ++ t) (s2 ++ t). +Proof. by move=> eq_s12; apply/permPl; rewrite perm_cat2r. 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_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_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_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_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_nilP s : reflect (s = [::]) (perm_eq s [::]). +Proof. by apply: (iffP idP) => [/perm_size/eqP/nilP | ->]. Qed. -Lemma perm_eq_small s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2. +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. -move=> s2_le1 eqs12; move/perm_eq_size: eqs12 s2_le1 (perm_eq_mem eqs12). +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_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_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_small_eq s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2. +Proof. +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. @@ -1533,35 +1583,25 @@ 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/eq_uniq; [apply: perm_eq_size | apply: perm_eq_mem]. -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. @@ -2136,7 +2172,7 @@ 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. -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)]. +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. + +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. @@ -3057,14 +3266,40 @@ 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 perm_uniq := - ((fun T s1 s2 eq_s12 eq_sz12 => - deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12) - _ _ _) +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/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 95da9cd..2925496 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -17,6 +17,15 @@ Global Set Bullet Behavior "None". (* --> 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. *) (******************************************************************************) |