diff options
| -rw-r--r-- | .gitlab-ci.yml | 87 | ||||
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 54 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 29 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 398 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 289 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 8 |
10 files changed, 632 insertions, 251 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 99fe690..7b7ae64 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,15 +1,15 @@ # Design: -# - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.7 .) +# - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.12 .) # - all branches (not tags) => push on GitLab registry # - GitHub PRs => push on GitLab and report back thanks to @coqbot # - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.7) # - script template foreach project (custom CONTRIB_URL, script) # - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION) -# - deploy stage (only branch "master" and environment "deployment") +# - deploy stage (only branch "master" and environment deployments "mathcomp/*") # - pull each built image from GitLab registry => push to Docker Hub # + scheduled build & deploy for mathcomp/mathcomp-dev:coq-dev # -# Config for protected environment "deployment": +# Config for protected environment deployments "mathcomp/*": # - set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN # # Remark: @@ -47,9 +47,12 @@ stages: script: - docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}" -t "${IMAGE}" . except: - - tags - - merge_requests - - schedules + refs: + - tags + - merge_requests + - schedules + variables: + - $CRON_MODE == "nightly" make-coq-latest: extends: .make-build @@ -72,15 +75,19 @@ make-coq-latest: - docker push "${IMAGE}" - docker logout "${CI_REGISTRY}" except: - - tags - - merge_requests + refs: + - tags + - merge_requests .opam-build-once: extends: .opam-build except: - - tags - - merge_requests - - schedules + refs: + - tags + - merge_requests + - schedules + variables: + - $CRON_MODE == "nightly" coq-8.9: extends: .opam-build-once @@ -125,16 +132,20 @@ coq-dev: - cd mathcomp - make test-suite TEST_SKIP_BUILD=1 except: - - tags - - merge_requests + refs: + - tags + - merge_requests # run "make test-suite" only for push pipelines (not for scheduled pipelines) .test-once: extends: .test except: - - tags - - merge_requests - - schedules + refs: + - tags + - merge_requests + - schedules + variables: + - $CRON_MODE == "nightly" test-coq-dev: extends: .test @@ -188,9 +199,12 @@ test-coq-8.9: - git rev-parse --verify HEAD - git describe --all --long --abbrev=40 --always --dirty except: - - tags - - merge_requests - - schedules + refs: + - tags + - merge_requests + - schedules + variables: + - $CRON_MODE == "nightly" # Guidelines to add a library to mathcomp CI: # - Add a hidden job (starting with a .) .ci-lib that extends the .ci job, @@ -207,10 +221,6 @@ test-coq-8.9: script: - make -j "${NJOBS}" - make install - except: - - tags - - merge_requests - - schedules ci-fourcolor-8.9: extends: .ci-fourcolor @@ -246,10 +256,6 @@ ci-fourcolor-dev: script: - make -j "${NJOBS}" - make install - except: - - tags - - merge_requests - - schedules ci-odd-order-8.9: extends: .ci-odd-order @@ -466,14 +472,15 @@ ci-fcsl-pcm-dev: services: - docker:dind environment: - name: deployment + # here, CI_JOB_NAME must not contain any ':', hence the use of '_' + name: "mathcomp/${CI_JOB_NAME}" url: https://hub.docker.com/r/mathcomp/mathcomp-dev variables: GIT_STRATEGY: none - HUB_IMAGE: "mathcomp/${CI_JOB_NAME}" IMAGE_PREFIX: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}" script: - - export IMAGE="${IMAGE_PREFIX}_${CI_JOB_NAME##*:}" + - export IMAGE="${IMAGE_PREFIX}_${CI_JOB_NAME##*_}" + - export HUB_IMAGE="mathcomp/${CI_JOB_NAME/_/:}" - echo "${IMAGE}" - docker pull "${IMAGE}" - echo "${HUB_IMAGE}" @@ -484,29 +491,33 @@ ci-fcsl-pcm-dev: - docker push "${HUB_IMAGE}" - docker logout "${HUB_REGISTRY}" only: - - master + refs: + - master .docker-deploy-once: extends: .docker-deploy except: - - schedules + refs: + - schedules + variables: + - $CRON_MODE == "nightly" -mathcomp-dev:coq-8.9: +mathcomp-dev_coq-8.9: extends: .docker-deploy-once -mathcomp-dev:coq-8.10: +mathcomp-dev_coq-8.10: extends: .docker-deploy-once -mathcomp-dev:coq-8.11: +mathcomp-dev_coq-8.11: extends: .docker-deploy-once -mathcomp-dev:coq-8.12: +mathcomp-dev_coq-8.12: extends: .docker-deploy-once # to uncomment when 8.13+alpha available -# mathcomp-dev:coq-8.13: +# mathcomp-dev_coq-8.13: # # to be replaced with .docker-deploy-once when 8.13.0 available # extends: .docker-deploy -mathcomp-dev:coq-dev: +mathcomp-dev_coq-dev: extends: .docker-deploy diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e78d37d..f6f8eca 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -228,9 +228,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `all_comm_mx_cons`, `comm_mx_scalar`, and `comm_scalar_mx`. The common arguments of these lemmas `R` and `n` are maximal implicits. - - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. - - in `fintype.v`, added `mask_enum_ord`. - - in `bigop.v`, added `big_mask_tuple` and `big_mask`. +- in `seq.v`, added `drop_index`, `in_mask`, `cons_subseq`, + `undup_subseq`, `leq_count_mask`, `leq_count_subseq`, + `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, + `rem_cons`, `remE`, `subseq_rem`, `leq_uniq_countP`, and + `leq_uniq_count`. +- in `fintype.v`, added `mask_enum_ord`. +- in `bigop.v`, added `big_mask_tuple` and `big_mask`. - in `mxalgebra.v`, new notation `stablemx V f` asserting that `f` stabilizes `V`, with new theorems: `eigenvectorP`, `eqmx_stable`, `stablemx_row_base`, `stablemx_full`, `stablemxM`, `stablemxD`, @@ -244,7 +248,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `comm_horner_mx2`, `horner_mx_stable`, `comm_mx_stable_kermxpoly`, and `comm_mx_stable_geigenspace`. -- in `ssralg.v`: +- in `ssralg.v`: + Lemma `expr_sum` : equivalent for ring of `expn_sum` + Lemma `prodr_natmul` : generalization of `prodrMn_const`. Its name will become `prodrMn` in the next release when this name will become available (cf. Renamed section) @@ -252,11 +256,32 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `polydiv.v`, new lemma `dvdpNl`. - in `perm.v` new lemma `permS01`. -- in `seq.v`, new definition `rot_add` and new lemmas `rot_minn`, `leq_rot_add`, `rot_addC`, `rot_rot_add`. +- in `seq.v`, new definition `rot_add` and new lemmas `rot_minn`, + `leq_rot_add`, `rot_addC`, `rot_rot_add`. + +- in `seq.v`, new lemmas `perm_catACA`, `allpairs0l`, `allpairs0r`, + `allpairs1l`, `allpairs1r`, `allpairs_cons`, `eq_allpairsr`, + `allpairs_rcons`, `perm_allpairs_catr`, `perm_allpairs_consr`, + `mem_allpairs_rconsr`, and `allpairs_rconsr` (with the alias + `perm_allpairs_rconsr` for the sake of uniformity, but which is + already deprecated in favor of `allpairs_rconsr`, cf renamed + section). + +- in `seq.v`, new lemmas `allss` and `all_mask`. + +- in `path.v`, new lemmas `sub_cycle(_in)`, `eq_cycle_in`, + `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`, + `(homo|mono)_cycle(_in)`. + +- in `seq.v` new lemmas `index_pivot`, `take_pivot`, `rev_pivot`, + `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr` + `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons`, `rev_mask`, + `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and + `uniq_subseq_pivot`. ### Changed -- in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 +- in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 - in `ssrAC.v`, fix `non-reversible-notation` warnings - In the definition of structures in order.v, displays are removed from @@ -325,11 +350,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). weaker hypothesis (i.e. `#|T| >= #|T'|` instead of `#|T| = #|T'|` thanks to `leq_card` under injectivity assumption). +- in `path.v`, generalized lemmas `sub_path_in`, `sub_sorted_in`, and + `eq_path_in` for non-`eqType`s. + +- in `order.v`, generalized `sort_le_id` for any `porderType`. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) - `mem_imset` -> `imset_f` (with deprecation alias, cf. Added section) -- `mem_imset2` -> imset2_f` (with deprecation alias, cf. Added section) +- `mem_imset2` -> `imset2_f` (with deprecation alias, cf. Added section) - in `interval.v`, we deprecate, rename, and relocate to `order.v` the following: + `lersif_(trans|anti)` -> `lteif_(trans|anti)` @@ -366,7 +396,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `odd_(opp|mul|exp)` -> `odd(N|M|X)` + `sqrn_sub` -> `sqrnB` -- in `seq.v`, `iota_add(|l)` -> `iotaD(|l)` +- in `seq.v`, + + `iota_add(|l)` -> `iotaD(|l)` + + `allpairs_(cons|cat)r` -> `mem_allpairs_(cons|cat)r` + (`allpairs_consr` and `allpairs_catr` are now deprecated alias, + and will be attributed to the new `perm_allpairs_catr`). + +- in `path.v`, `eq_sorted(_irr)` -> `(irr_)sorted_eq` - in `div.v` + `coprime_mul(l|r)` -> `coprimeM(l|r)` @@ -382,6 +418,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `primes_(mul|exp)` -> `primes(M|X)` + `pnat_(mul|exp)` -> `pnat(M|X)` +- in `order.v`, `eq_sorted_(le|lt)` -> `(le|lt)_sorted_eq` + - in `ssralg.v` + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section) diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index a2a2395..185d5c1 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1584,7 +1584,7 @@ Arguments ltr01 {R}. Arguments normr_idP {R x}. Arguments normr0P {R V v}. Hint Resolve ler01 ltr01 ltr0Sn ler0n : core. -Hint Extern 0 (is_true (0 <= norm _)) => exact: normr_ge0 : core. +Hint Extern 0 (is_true (0 <= norm _)) => apply: normr_ge0 : core. Section NumDomainOperationTheory. @@ -2977,7 +2977,7 @@ Definition lter_nnormr := (ler_nnorml, ltr_nnorml). End NormedZmoduleTheory. -Hint Extern 0 (is_true (norm _ \is real)) => exact: normr_real : core. +Hint Extern 0 (is_true (norm _ \is real)) => apply: normr_real : core. Lemma real_ler_norml x y : x \is real -> (`|x| <= y) = (- y <= x <= y). Proof. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index e8293ae..0ece733 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -990,7 +990,7 @@ Lemma big_nat_widen m n1 n2 (P : pred nat) F : = \big[op/idx]_(m <= i < n2 | P i && (i < n1)) F i. Proof. move=> len12; symmetry; rewrite -big_filter filter_predI big_filter. -have [ltn_trans eq_by_mem] := (ltn_trans, eq_sorted_irr ltn_trans ltnn). +have [ltn_trans eq_by_mem] := (ltn_trans, irr_sorted_eq ltn_trans ltnn). congr bigop; apply: eq_by_mem; rewrite ?sorted_filter ?iota_ltn_sorted // => i. rewrite mem_filter !mem_index_iota andbCA andbA andb_idr => // /andP[_]. by move/leq_trans->. diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 836c323..cd3ec87 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -468,7 +468,7 @@ have ft_m: #|f_t t| = m. rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj). exact: (sorted_uniq ltn_trans ltnn). rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=. -apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y. +apply/eqP/(irr_sorted_eq ltn_trans ltnn) => // y. by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *. Qed. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index da4d59d..1546a55 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -2741,7 +2741,7 @@ Proof. by rewrite andbC lt_le_asym. Qed. Definition lte_anti := (=^~ eq_le, lt_asym, lt_le_asym, le_lt_asym). -Lemma lt_sorted_uniq_le s : sorted lt s = uniq s && sorted le s. +Lemma lt_sorted_uniq_le s : sorted <%O s = uniq s && sorted <=%O s. Proof. case: s => //= n s; elim: s n => //= m s IHs n. rewrite inE lt_neqAle negb_or IHs -!andbA. @@ -2750,12 +2750,15 @@ rewrite andbF; apply/and5P=> [[ne_nm lenm _ _ le_ms]]; case/negP: ne_nm. by rewrite eq_le lenm /=; apply: (allP (order_path_min le_trans le_ms)). Qed. -Lemma eq_sorted_lt s1 s2 : sorted lt s1 -> sorted lt s2 -> s1 =i s2 -> s1 = s2. -Proof. by apply: eq_sorted_irr => //; apply: lt_trans. Qed. +Lemma lt_sorted_eq s1 s2 : sorted <%O s1 -> sorted <%O s2 -> s1 =i s2 -> s1 = s2. +Proof. by apply: irr_sorted_eq => //; apply: lt_trans. Qed. -Lemma eq_sorted_le s1 s2 : sorted le s1 -> sorted le s2 -> - perm_eq s1 s2 -> s1 = s2. -Proof. by apply: eq_sorted; [apply: le_trans|apply: le_anti]. Qed. +Lemma le_sorted_eq s1 s2 : + sorted <=%O s1 -> sorted <=%O s2 -> perm_eq s1 s2 -> s1 = s2. +Proof. exact/sorted_eq/le_anti/le_trans. Qed. + +Lemma sort_le_id s : sorted <=%O s -> sort <=%O s = s. +Proof. exact/sorted_sort/le_trans. Qed. Lemma comparable_leNgt x y : x >=< y -> (x <= y) = ~~ (y < x). Proof. @@ -3419,6 +3422,13 @@ Proof. exact: anti_mono_in. Qed. End POrderMonotonyTheory. +Notation "@ 'eq_sorted_lt'" := (deprecate eq_sorted_lt lt_sorted_eq) + (at level 10, only parsing) : fun_scope. +Notation "@ 'eq_sorted_le'" := (deprecate eq_sorted_le le_sorted_eq) + (at level 10, only parsing) : fun_scope. +Notation eq_sorted_lt := (@eq_sorted_lt _ _ _ _) (only parsing). +Notation eq_sorted_le := (@eq_sorted_le _ _ _ _) (only parsing). + End POrderTheory. Hint Resolve lexx le_refl ltxx lt_irreflexive ltW lt_eqF : core. @@ -3728,14 +3738,9 @@ Lemma sort_le_sorted s : sorted <=%O (sort <=%O s). Proof. exact: sort_sorted. Qed. Hint Resolve sort_le_sorted : core. -Lemma sort_lt_sorted s : sorted lt (sort le s) = uniq s. +Lemma sort_lt_sorted s : sorted <%O (sort <=%O s) = uniq s. Proof. by rewrite lt_sorted_uniq_le sort_uniq sort_le_sorted andbT. Qed. -Lemma sort_le_id s : sorted le s -> sort le s = s. -Proof. -by move=> ss; apply: eq_sorted_le; rewrite ?sort_le_sorted // perm_sort. -Qed. - Lemma leNgt x y : (x <= y) = ~~ (y < x). Proof. exact: comparable_leNgt. Qed. Lemma ltNge x y : (x < y) = ~~ (y <= x). Proof. exact: comparable_ltNge. Qed. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 0965b14..93521d7 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -137,55 +137,247 @@ Qed. Lemma rotr_cycle p : cycle (rotr n0 p) = cycle p. Proof. by rewrite -rot_cycle rotrK. Qed. +Definition sorted s := if s is x :: s' then path x s' else true. + +Lemma path_sorted x s : path x s -> sorted s. +Proof. by case: s => //= y s /andP[]. Qed. + +Lemma path_min_sorted x s : all (e x) s -> path x s = sorted s. +Proof. by case: s => //= y s /andP [->]. Qed. + End Path. -Lemma eq_path e e' : e =2 e' -> path e =2 path e'. -Proof. by move=> ee' x p; elim: p x => //= y p IHp x; rewrite ee' IHp. Qed. +Section SubPath_in. -Lemma eq_cycle e e' : e =2 e' -> cycle e =1 cycle e'. -Proof. by move=> ee' [|x p] //=; apply: eq_path. Qed. +Variable (P : {pred T}) (e e' : rel T). +Hypothesis (ee' : {in P &, subrel e e'}). -Lemma sub_path e e' : subrel e e' -> forall x p, path e x p -> path e' x p. -Proof. by move=> ee' x p; elim: p x => //= y p IHp x /andP[/ee'-> /IHp]. Qed. +Lemma sub_path_in x s : all P (x :: s) -> path e x s -> path e' x s. +Proof. +by elim: s x => //= y s ihs x /and3P [? ? ?] /andP [/ee' -> //]; apply/ihs/andP. +Qed. -Lemma rev_path e x p : - path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p. +Lemma sub_cycle_in s : all P s -> cycle e s -> cycle e' s. Proof. -elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC. -by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons. +case: s => //= x s /andP [Px Ps]. +by apply: sub_path_in; rewrite /= all_rcons Px. +Qed. + +Lemma sub_sorted_in s : all P s -> sorted e s -> sorted e' s. +Proof. by case: s => //; apply: sub_path_in. Qed. + +End SubPath_in. + +Section EqPath_in. + +Variable (P : {pred T}) (e e' : rel T). +Hypothesis (ee' : {in P &, e =2 e'}). + +Let e_e' : {in P &, subrel e e'}. Proof. by move=> ? ? ? ?; rewrite ee'. Qed. +Let e'_e : {in P &, subrel e' e}. Proof. by move=> ? ? ? ?; rewrite ee'. Qed. + +Lemma eq_path_in x s : all P (x :: s) -> path e x s = path e' x s. +Proof. by move=> Pxs; apply/idP/idP; apply: sub_path_in Pxs. Qed. + +Lemma eq_cycle_in s : all P s -> cycle e s = cycle e' s. +Proof. by move=> Ps; apply/idP/idP; apply: sub_cycle_in Ps. Qed. + +End EqPath_in. + +Section SubPath. + +Variables e e' : rel T. + +Lemma sub_path : subrel e e' -> forall x p, path e x p -> path e' x p. +Proof. by move=> ? ? ?; apply/sub_path_in/all_predT; apply: in2W. Qed. + +Lemma sub_cycle : subrel e e' -> subpred (cycle e) (cycle e'). +Proof. by move=> ee' [] // ? ?; apply: sub_path. Qed. + +Lemma sub_sorted : subrel e e' -> subpred (sorted e) (sorted e'). +Proof. by move=> ee' [] //=; apply: sub_path. Qed. + +Lemma eq_path : e =2 e' -> path e =2 path e'. +Proof. by move=> ? ? ?; apply/eq_path_in/all_predT; apply: in2W. Qed. + +Lemma eq_cycle : e =2 e' -> cycle e =1 cycle e'. +Proof. by move=> ee' [] // ? ?; apply: eq_path. Qed. + +End SubPath. + +Section Transitive_in. + +Variables (P : {pred T}) (leT : rel T). +Hypothesis leT_tr : {in P & &, transitive leT}. + +Lemma path_mask_in x m s : + all P (x :: s) -> path leT x s -> path leT x (mask m s). +Proof. +elim: m s x => [|[] m ih] [|y s] x //=. + by case/and3P=> ? ? ? /andP [-> /ih ->] //; apply/andP. +case/andP=> Px Pys /andP [xy ys]; case/andP: (Pys) => Py Ps. +case: (mask _ _) (all_mask m Ps) (ih s y Pys ys) => //=. +by move=> z t /andP [Pz Pt] /andP [] /(leT_tr Py Px Pz xy) ->. Qed. +Lemma path_filter_in x a s : + all P (x :: s) -> path leT x s -> path leT x (filter a s). +Proof. by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed. + +Lemma sorted_mask_in m s : all P s -> sorted leT s -> sorted leT (mask m s). +Proof. +elim: m s => [|[] m ih] [|x s] //= Pxs; first exact: path_mask_in. +by move/path_sorted/ih; apply; case/andP: Pxs. +Qed. + +Lemma sorted_filter_in a s : all P s -> sorted leT s -> sorted leT (filter a s). +Proof. rewrite filter_mask; exact: sorted_mask_in. Qed. + +End Transitive_in. + +Section Transitive. + +Variable (leT : rel T). +Hypothesis leT_tr : transitive leT. + +Let leT_tr' : {in predT & &, transitive leT}. Proof. exact: in3W. Qed. + +Lemma path_mask x m s : path leT x s -> path leT x (mask m s). +Proof. exact/path_mask_in/all_predT. Qed. + +Lemma path_filter x a s : path leT x s -> path leT x (filter a s). +Proof. by rewrite filter_mask; exact: path_mask. Qed. + +Lemma sorted_mask m s : sorted leT s -> sorted leT (mask m s). +Proof. exact/sorted_mask_in/all_predT. Qed. + +Lemma sorted_filter a s : sorted leT s -> sorted leT (filter a s). +Proof. rewrite filter_mask; exact: sorted_mask. Qed. + +End Transitive. + End Paths. +Arguments pathP {T e x p}. +Arguments path_sorted {T e x s}. +Arguments path_min_sorted {T e x s}. +Arguments path_mask_in {T P leT} leT_tr {x m s}. +Arguments path_filter_in {T P leT} leT_tr {x a s}. +Arguments sorted_mask_in {T P leT} leT_tr {m s}. +Arguments sorted_filter_in {T P leT} leT_tr {a s}. +Arguments path_mask {T leT} leT_tr {x} m {s}. +Arguments path_filter {T leT} leT_tr {x} a {s}. +Arguments sorted_mask {T leT} leT_tr m {s}. +Arguments sorted_filter {T leT} leT_tr a {s}. + Lemma cycle_catC (T : Type) (e : rel T) (p q : seq T) : cycle e (p ++ q) = cycle e (q ++ p). Proof. by rewrite -rot_size_cat rot_cycle. Qed. -Arguments pathP {T e x p}. +Section RevPath. + +Variables (T : Type) (e : rel T). + +Lemma rev_path x p : + path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p. +Proof. +elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC. +by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons. +Qed. + +Lemma rev_cycle p : cycle e (rev p) = cycle (fun z => e^~ z) p. +Proof. +case: p => //= x p; rewrite -rev_path last_rcons belast_rcons rev_cons. +by rewrite -[in LHS]cats1 cycle_catC. +Qed. + +Lemma rev_sorted p : sorted e (rev p) = sorted (fun z => e^~ z) p. +Proof. by case: p => //= x p; rewrite -rev_path lastI rev_rcons. Qed. + +End RevPath. Section HomoPath. -Variables (T T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). +Variables (T T' : Type) (P : {pred T}) (f : T -> T') (e : rel T) (e' : rel T'). -Lemma path_map x s : path leT' (f x) (map f s) = path (relpre f leT') x s. +Lemma path_map x s : path e' (f x) (map f s) = path (relpre f e') x s. Proof. by elim: s x => //= y s <-. Qed. -Lemma homo_path x s : {homo f : x y / leT x y >-> leT' x y} -> - path leT x s -> path leT' (f x) (map f s). -Proof. by move=> f_homo xs; rewrite path_map (sub_path _ xs). Qed. +Lemma cycle_map s : cycle e' (map f s) = cycle (relpre f e') s. +Proof. by case: s => //= ? ?; rewrite -map_rcons path_map. Qed. + +Lemma sorted_map s : sorted e' (map f s) = sorted (relpre f e') s. +Proof. by case: s; last apply: path_map. Qed. + +Lemma homo_path_in x s : {in P &, {homo f : x y / e x y >-> e' x y}} -> + all P (x :: s) -> path e x s -> path e' (f x) (map f s). +Proof. by move=> f_mono; rewrite path_map; apply: sub_path_in. Qed. + +Lemma homo_cycle_in s : {in P &, {homo f : x y / e x y >-> e' x y}} -> + all P s -> cycle e s -> cycle e' (map f s). +Proof. by move=> f_mono; rewrite cycle_map; apply: sub_cycle_in. Qed. + +Lemma homo_sorted_in s : {in P &, {homo f : x y / e x y >-> e' x y}} -> + all P s -> sorted e s -> sorted e' (map f s). +Proof. by move=> f_mono; rewrite sorted_map; apply: sub_sorted_in. Qed. + +Lemma mono_path_in x s : {in P &, {mono f : x y / e x y >-> e' x y}} -> + all P (x :: s) -> path e' (f x) (map f s) = path e x s. +Proof. by move=> f_mono; rewrite path_map; apply: eq_path_in. Qed. + +Lemma mono_cycle_in s : {in P &, {mono f : x y / e x y >-> e' x y}} -> + all P s -> cycle e' (map f s) = cycle e s. +Proof. by move=> f_mono; rewrite cycle_map; apply: eq_cycle_in. Qed. -Lemma mono_path x s : {mono f : x y / leT x y >-> leT' x y} -> - path leT' (f x) (map f s) = path leT x s. +Lemma mono_sorted_in s : {in P &, {mono f : x y / e x y >-> e' x y}} -> + all P s -> sorted e' (map f s) = sorted e s. +Proof. by case: s => // x s; apply: mono_path_in. Qed. + +Lemma homo_path x s : {homo f : x y / e x y >-> e' x y} -> + path e x s -> path e' (f x) (map f s). +Proof. by move=> f_homo; rewrite path_map; apply: sub_path. Qed. + +Lemma homo_cycle : {homo f : x y / e x y >-> e' x y} -> + {homo map f : s / cycle e s >-> cycle e' s}. +Proof. by move=> f_homo s hs; rewrite cycle_map (sub_cycle _ hs). Qed. + +Lemma homo_sorted : {homo f : x y / e x y >-> e' x y} -> + {homo map f : s / sorted e s >-> sorted e' s}. +Proof. by move/homo_path => ? []. Qed. + +Lemma mono_path x s : {mono f : x y / e x y >-> e' x y} -> + path e' (f x) (map f s) = path e x s. Proof. by move=> f_mon; rewrite path_map; apply: eq_path. Qed. +Lemma mono_cycle : {mono f : x y / e x y >-> e' x y} -> + {mono map f : s / cycle e s >-> cycle e' s}. +Proof. by move=> ? ?; rewrite cycle_map; apply: eq_cycle. Qed. + +Lemma mono_sorted : {mono f : x y / e x y >-> e' x y} -> + {mono map f : s / sorted e s >-> sorted e' s}. +Proof. by move=> f_mon [] //= x s; apply: mono_path. Qed. + End HomoPath. -Arguments homo_path {T T' f leT leT' x s}. -Arguments mono_path {T T' f leT leT' x s}. +Arguments path_map {T T' f e'}. +Arguments cycle_map {T T' f e'}. +Arguments sorted_map {T T' f e'}. +Arguments homo_path_in {T T' P f e e' x s}. +Arguments homo_cycle_in {T T' P f e e' s}. +Arguments homo_sorted_in {T T' P f e e' s}. +Arguments mono_path_in {T T' P f e e' x s}. +Arguments mono_cycle_in {T T' P f e e' s}. +Arguments mono_sorted_in {T T' P f e e' s}. +Arguments homo_path {T T' f e e' x s}. +Arguments homo_cycle {T T' f e e'}. +Arguments homo_sorted {T T' f e e'}. +Arguments mono_path {T T' f e e' x s}. +Arguments mono_cycle {T T' f e e'}. +Arguments mono_sorted {T T' f e e'}. Section EqPath. -Variables (n0 : nat) (T : eqType) (x0_cycle : T) (e : rel T). +Variables (n0 : nat) (T : eqType) (e : rel T). Implicit Type p : seq T. Variant split x : seq T -> seq T -> seq T -> Type := @@ -405,40 +597,15 @@ Qed. End EqPath. -Section EqHomoPath. - -Variables (T : eqType) (T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). - -Lemma sub_path_in (e e' : rel T) x s : {in x :: s &, subrel e e'} -> - path e x s -> path e' x s. -Proof. -elim: s x => //= y s IHs x ee' /andP[/ee'->//=]; rewrite ?(eqxx,in_cons,orbT)//. -by apply: IHs => z t zys tys; apply: ee'; rewrite in_cons (zys, tys) orbT. -Qed. - -Lemma eq_path_in (e e' : rel T) x s : {in x :: s &, e =2 e'} -> - path e x s = path e' x s. -Proof. by move=> ee'; apply/idP/idP => /sub_path_in->// y z /ee' P/P->. Qed. - -Lemma homo_path_in x s : {in x :: s &, {homo f : x y / leT x y >-> leT' x y}} -> - path leT x s -> path leT' (f x) (map f s). -Proof. by move=> f_homo xs; rewrite path_map (sub_path_in _ xs). Qed. - -Lemma mono_path_in x s : {in x :: s &, {mono f : x y / leT x y >-> leT' x y}} -> - path leT' (f x) (map f s) = path leT x s. -Proof. by move=> f_mono; rewrite path_map; apply: eq_path_in. Qed. - -End EqHomoPath. - -Arguments homo_path_in {T T' f leT leT' x s}. -Arguments mono_path_in {T T' f leT leT' x s}. - (* Ordered paths and sorting. *) Section SortSeq. Variables (T : Type) (leT : rel T). +Local Notation path := (path leT). +Local Notation sorted := (sorted leT). + Fixpoint merge s1 := if s1 is x1 :: s1' then let fix merge_s1 s2 := @@ -482,15 +649,9 @@ rewrite /sort; move: [::] {2}_.+1 (ltnSn (size s)./2) => ss n. by elim: n => // n IHn in ss s *; case: s => [|x [|y s]] //= /IHn->. Qed. -Definition sorted s := if s is x :: s' then path leT x s' else true. - -Lemma path_sorted x s : path leT x s -> sorted s. -Proof. by case: s => //= y s /andP[]. Qed. - Hypothesis leT_total : total leT. -Lemma merge_path x s1 s2 : - path leT x s1 -> path leT x s2 -> path leT x (merge s1 s2). +Lemma merge_path x s1 s2 : path x s1 -> path x s2 -> path x (merge s1 s2). Proof. elim: s1 s2 x => //= x1 s1 IHs1. elim=> //= x2 s2 IHs2 x /andP[le_x_x1 ord_s1] /andP[le_x_x2 ord_s2]. @@ -517,9 +678,6 @@ elim: s [::] => /= [|x s ihs] ss allss. [rewrite /= ht | apply/ihss/merge_sorted]. Qed. -Lemma path_min_sorted x s : all (leT x) s -> path leT x s = sorted s. -Proof. by case: s => //= y s /andP [->]. Qed. - Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2). Proof. rewrite size_cat; elim: s1 s2 => // x s1 IH1. @@ -527,7 +685,7 @@ elim=> //= [|y s2 IH2]; first by rewrite addn0. by case: leT; rewrite /= ?IH1 ?IH2 !addnS. Qed. -Lemma order_path_min x s : transitive leT -> path leT x s -> all (leT x) s. +Lemma order_path_min x s : transitive leT -> path x s -> all (leT x) s. Proof. move=> leT_tr; elim: s => //= y [//|z s] ihs /andP[xy yz]; rewrite xy {}ihs//. by move: yz => /= /andP [/(leT_tr _ _ _ xy) ->]. @@ -535,7 +693,7 @@ Qed. Hypothesis leT_tr : transitive leT. -Lemma path_sortedE x s : path leT x s = all (leT x) s && sorted s. +Lemma path_sortedE x s : path x s = all (leT x) s && sorted s. Proof. apply/idP/idP => [xs|/andP[/path_min_sorted<-//]]. by rewrite order_path_min//; apply: path_sorted xs. @@ -567,46 +725,25 @@ rewrite -{1 3}[s]/(catss [::] ++ s) sortE; elim: s [::] => /= [|x s ihs] ss. by elim: (catss ss) h_sorted => //= ? ? ih /path_sorted. Qed. -Lemma path_mask x m s : path leT x s -> path leT x (mask m s). -Proof. -elim: m s x => [|[] m ih] [|y s] x //=; first by case/andP=> -> /ih. -by case/andP => xy /ih; case: (mask _ _) => //= ? ? /andP [] /(leT_tr xy) ->. -Qed. - -Lemma path_filter x a s : path leT x s -> path leT x (filter a s). -Proof. by rewrite filter_mask; exact: path_mask. Qed. - -Lemma sorted_mask m s : sorted s -> sorted (mask m s). -Proof. -by elim: m s => [|[] m ih] [|x s] //=; [apply/path_mask | move/path_sorted/ih]. -Qed. - -Lemma sorted_filter a s : sorted s -> sorted (filter a s). -Proof. rewrite filter_mask; exact: sorted_mask. Qed. - End SortSeq. -Arguments path_sorted {T leT x s}. -Arguments order_path_min {T leT x s}. -Arguments path_min_sorted {T leT x s}. Arguments merge {T} relT !s1 !s2 : rename. +Arguments merge_path {T leT} leT_total {x s1 s2}. +Arguments merge_sorted {T leT} leT_total {s1 s2}. +Arguments sort_sorted {T leT} leT_total s. +Arguments order_path_min {T leT x s}. +Arguments path_sortedE {T leT} leT_tr x s. +Arguments sorted_merge {T leT} leT_tr {s t}. +Arguments sorted_sort {T leT} leT_tr {s}. Section SortMap. Variables (T T' : Type) (f : T' -> T). Section Monotonicity. -Variables (leT' : rel T') (leT : rel T). - -Lemma homo_sorted : {homo f : x y / leT' x y >-> leT x y} -> - {homo map f : s / sorted leT' s >-> sorted leT s}. -Proof. by move=> /homo_path f_path [|//= x s]. Qed. -Section Strict. +Variables (leT' : rel T') (leT : rel T). Hypothesis f_mono : {mono f : x y / leT' x y >-> leT x y}. -Lemma mono_sorted : {mono map f : s / sorted leT' s >-> sorted leT s}. -Proof. by case=> //= x s; rewrite (mono_path f_mono). Qed. - Lemma map_merge : {morph map f : s1 s2 / merge leT' s1 s2 >-> merge leT s1 s2}. Proof. elim=> //= x s1 IHs1; elim => [|y s2 IHs2] //=; rewrite f_mono. @@ -622,59 +759,39 @@ rewrite ihs -/(map f [:: x]); congr sort_rec1. by elim: ss [:: x] => {x s ihs} [|[|x s] ss ihss] //= ?; rewrite ihss map_merge. Qed. -End Strict. End Monotonicity. -Variable (leT : rel T). -Local Notation leTf := (relpre f leT). +Variable leT : rel T. -Lemma merge_map s1 s2 : merge leT (map f s1) (map f s2) = - map f (merge leTf s1 s2). +Lemma merge_map s1 s2 : + merge leT (map f s1) (map f s2) = map f (merge (relpre f leT) s1 s2). Proof. exact/esym/map_merge. Qed. -Lemma sort_map s : sort leT (map f s) = map f (sort leTf s). +Lemma sort_map s : sort leT (map f s) = map f (sort (relpre f leT) s). Proof. exact/esym/map_sort. Qed. -Lemma sorted_map s : sorted leT (map f s) = sorted leTf s. -Proof. exact: mono_sorted. Qed. - -Lemma sub_sorted (leT' : rel T) : - subrel leT leT' -> forall s, sorted leT s -> sorted leT' s. -Proof. by move=> leTT'; case => //; apply: sub_path. Qed. - End SortMap. -Arguments homo_sorted {T T' f leT' leT}. -Arguments mono_sorted {T T' f leT' leT}. Arguments map_merge {T T' f leT' leT}. Arguments map_sort {T T' f leT' leT}. Arguments merge_map {T T' f leT}. Arguments sort_map {T T' f leT}. -Arguments sorted_map {T T' f leT}. - -Lemma rev_sorted (T : Type) (leT : rel T) s : - sorted leT (rev s) = sorted (fun y x => leT x y) s. -Proof. by case: s => //= x p; rewrite -rev_path lastI rev_rcons. Qed. Section EqSortSeq. Variable T : eqType. Variable leT : rel T. -Lemma sub_sorted_in (leT' : rel T) (s : seq T) : - {in s &, subrel leT leT'} -> sorted leT s -> sorted leT' s. -Proof. by case: s => //; apply: sub_path_in. Qed. - +Local Notation path := (path leT). +Local Notation sorted := (sorted leT). Local Notation merge := (merge leT). Local Notation sort := (sort leT). -Local Notation sorted := (sorted leT). Section Transitive. Hypothesis leT_tr : transitive leT. -Lemma subseq_order_path x s1 s2 : - subseq s1 s2 -> path leT x s2 -> path leT x s1. +Lemma subseq_order_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1. Proof. by case/subseqP => m _ ->; apply/path_mask. Qed. Lemma subseq_sorted s1 s2 : subseq s1 s2 -> sorted s2 -> sorted s1. @@ -687,7 +804,7 @@ rewrite (IHs (path_sorted s_ord)) andbT; apply/negP=> s_x. by case/allPn: (order_path_min leT_tr s_ord); exists x; rewrite // leT_irr. Qed. -Lemma eq_sorted : antisymmetric leT -> +Lemma sorted_eq : 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. @@ -702,13 +819,13 @@ case/predU1P=> [eq_x12 | s1_x2]; first by case ne_x12. by rewrite (allP (order_path_min _ ord_s1)). Qed. -Lemma eq_sorted_irr : irreflexive leT -> +Lemma irr_sorted_eq : irreflexive leT -> forall s1 s2, sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2. 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 => //; apply: sorted_uniq. +by move/sorted_eq; apply=> //; apply: uniq_perm => //; apply: sorted_uniq. Qed. End Transitive. @@ -750,7 +867,7 @@ Lemma perm_sortP : Proof. move=> leT_total leT_tr leT_asym s1 s2. apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort. -apply: eq_sorted; rewrite ?sort_sorted //. +apply: sorted_eq; rewrite ?sort_sorted //. by rewrite perm_sort (permPl eq12) -perm_sort. Qed. @@ -771,23 +888,6 @@ case: s => [|x s] //; have [s1 pp qq] := perm_iota_sort leT x (x :: s). by rewrite qq size_map (perm_size pp) size_iota. Qed. -Section EqHomoSortSeq. - -Variables (T : eqType) (T' : Type) (f : T -> T') (leT : rel T) (leT' : rel T'). - -Lemma homo_sorted_in s : {in s &, {homo f : x y / leT x y >-> leT' x y}} -> - sorted leT s -> sorted leT' (map f s). -Proof. by case: s => //= x s /homo_path_in. Qed. - -Lemma mono_sorted_in s : {in s &, {mono f : x y / leT x y >-> leT' x y}} -> - sorted leT' (map f s) = sorted leT s. -Proof. by case: s => // x s /mono_path_in /= ->. Qed. - -End EqHomoSortSeq. - -Arguments homo_sorted_in {T T' f leT leT'}. -Arguments mono_sorted_in {T T' f leT leT'}. - Lemma ltn_sorted_uniq_leq s : sorted ltn s = uniq s && sorted leq s. Proof. case: s => //= n s; elim: s n => //= m s IHs n. @@ -905,7 +1005,8 @@ Lemma sort_stable s : Proof. move=> sorted_s; case Ds: s => // [x s1]; rewrite -{s1}Ds. rewrite -(mkseq_nth x s) sort_map. -apply/(homo_sorted_in (f := nth x s)): (sort_iota_stable x s (size s)). +move: (sort_iota_stable x s (size s)). +apply/(homo_sorted_in (f := nth x s) _ (allss _)). move=> /= y z; rewrite !mem_sort !mem_iota !leq0n add0n /= => y_le_s z_le_s. case/andP => -> /= /implyP yz; apply/implyP => /yz {yz} y_le_z. elim: s y z sorted_s y_le_z y_le_s z_le_s => // y s ih [|n] [|m] //=; @@ -937,7 +1038,7 @@ Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s). Proof. case Ds: s => // [x s1]; rewrite -{s1}Ds. rewrite -(mkseq_nth x s) !(filter_map, sort_map). -congr map; apply/(@eq_sorted_irr _ (le_lex x s)) => //. +congr map; apply/(@irr_sorted_eq _ (le_lex x s)) => //. - by move=> ?; rewrite /= ltnn implybF andbN. - exact/sorted_filter/sort_stable/iota_ltn_sorted/ltn_trans. - exact/sort_stable/sorted_filter/iota_ltn_sorted/ltn_trans/ltn_trans. @@ -1339,8 +1440,7 @@ Qed. Lemma ltn_index (s : seq T) : sorted r s -> {in s &, forall x y, index x s < index y s -> r x y}. Proof. -case: s => [//|x0 s'] r_sorted x y xs ys. -move=> /(@sorted_lt_nth x0 (x0 :: s')). +case: s => // x0 s' r_sorted x y xs ys /(@sorted_lt_nth x0 (x0 :: s')). by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. Qed. @@ -1350,15 +1450,23 @@ Lemma sorted_le_nth x0 (s : seq T) : sorted r s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> r i j}}. Proof. move=> s_sorted x y xs ys. -by rewrite leq_eqVlt=> /orP[/eqP->//|/sorted_lt_nth]; apply. +by rewrite leq_eqVlt=> /predU1P[->//|]; apply: sorted_lt_nth. Qed. Lemma leq_index (s : seq T) : sorted r s -> {in s &, forall x y, index x s <= index y s -> r x y}. Proof. -case: s => [//|x0 s'] r_sorted x y xs ys. -move=> /(@sorted_le_nth x0 (x0 :: s')). +case: s => // x0 s' r_sorted x y xs ys /(@sorted_le_nth x0 (x0 :: s')). by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply. Qed. End Monotonicity. + +Notation "@ 'eq_sorted'" := + (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope. +Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq) + (at level 10, only parsing) : fun_scope. +Notation eq_sorted := + (fun le_tr le_asym => @eq_sorted _ _ le_tr le_asym _ _) (only parsing). +Notation eq_sorted_irr := + (fun le_tr le_irr => @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing). diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 8e94ef6..389b1c2 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -454,7 +454,7 @@ Qed. Lemma eq_primes m n : (primes m =i primes n) <-> (primes m = primes n). Proof. split=> [eqpr| -> //]. -by apply: (eq_sorted_irr ltn_trans ltnn); rewrite ?sorted_primes. +by apply: (irr_sorted_eq ltn_trans ltnn); rewrite ?sorted_primes. Qed. Lemma primes_uniq n : uniq (primes n). @@ -565,7 +565,7 @@ Qed. Lemma primes_prime p : prime p -> primes p = [::p]. Proof. -move=> pr_p; apply: (eq_sorted_irr ltn_trans ltnn) => // [|q]. +move=> pr_p; apply: (irr_sorted_eq ltn_trans ltnn) => // [|q]. exact: sorted_primes. rewrite mem_seq1 mem_primes prime_gt0 //=. by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2. @@ -862,7 +862,7 @@ Proof. by move=> eq_pi n; rewrite 3!inE /= eq_pi. Qed. Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n). Proof. -rewrite /pi_of; have eqs := eq_sorted_irr ltn_trans ltnn. +rewrite /pi_of; have eqs := irr_sorted_eq ltn_trans ltnn. by split=> [|-> //] /(eqs _ _ (sorted_primes m) (sorted_primes n)) ->. Qed. @@ -954,7 +954,7 @@ Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed. Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n). Proof. have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0. -apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //. +apply: (irr_sorted_eq ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //. move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=. apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]]. rewrite /partn; apply big_ind => [|n1 n2 IHn1 IHn2|q pi_q]. @@ -970,7 +970,7 @@ Qed. Lemma filter_pi_of n m : n < m -> filter \pi(n) (index_iota 0 m) = primes n. Proof. -move=> lt_n_m; have ltnT := ltn_trans; apply: (eq_sorted_irr ltnT ltnn). +move=> lt_n_m; have ltnT := ltn_trans; apply: (irr_sorted_eq ltnT ltnn). - by rewrite sorted_filter // iota_ltn_sorted. - exact: sorted_primes. move=> p; rewrite mem_filter mem_index_iota /= mem_primes; case: and3P => //. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 1e9e1c9..9747171 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1119,6 +1119,8 @@ Proof. by rewrite -all_predC; apply: allP. Qed. Lemma allPn a s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s). Proof. by rewrite -has_predC; apply: hasP. Qed. +Lemma allss s : all (mem s) s. Proof. exact/allP. Qed. + Lemma mem_filter a x s : (x \in filter a s) = a x && (x \in s). Proof. rewrite andbC; elim: s => //= y s IHs. @@ -1269,6 +1271,17 @@ elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. by rewrite in_cons; case: (eqVneq y x) => // <-; rewrite s'y. Qed. +Lemma leq_uniq_countP x s1 s2 : uniq s1 -> + reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2). +Proof. +move/count_uniq_mem->; case: (boolP (_ \in _)) => //= _; last by constructor. +by rewrite -has_pred1 has_count; apply: (iffP idP) => //; apply. +Qed. + +Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} -> + (forall x, count_mem x s1 <= count_mem x s2). +Proof. by move=> s1_uniq s1_s2 x; apply/leq_uniq_countP/s1_s2. Qed. + Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. Proof. move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)). @@ -1393,6 +1406,60 @@ Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed. Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2). Proof. exact/inj_eq/rot_inj. Qed. +Lemma drop_index s (n := index x0 s) : x0 \in s -> drop n s = x0 :: drop n.+1 s. +Proof. by move=> xs; rewrite (drop_nth x0) ?index_mem ?nth_index. Qed. + +(* lemmas about the pivot pattern [_ ++ _ :: _] *) + +Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 -> + index x s = size s1. +Proof. by rewrite index_cat/= eqxx addn0; case: ifPn. Qed. + +Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 -> + take (index x s) s = s1. +Proof. by move=> /index_pivot->; rewrite take_size_cat. Qed. + +Lemma rev_pivot x s1 s2 : rev (s1 ++ x :: s2) = rev s2 ++ x :: rev s1. +Proof. by rewrite rev_cat rev_cons cat_rcons. Qed. + +Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs1 xNs3; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. +suff S : size s1 = size s3 by rewrite eqseq_cat// eqseq_cons eqxx in E. +by rewrite -(index_pivot s2 xNs1) (eqP E) index_pivot. +Qed. + +Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 -> x \notin s4 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs2 xNs4; rewrite -(can_eq revK) !rev_pivot. +by rewrite eqseq_pivot2l ?mem_rev // !(can_eq revK) andbC. +Qed. + +Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +move=> xNs1 xNs2; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//]. +rewrite -(@eqseq_pivot2l x)//; have /eqP/(congr1 (count_mem x)) := E. +rewrite !count_cat/= eqxx !addnS (count_memPn _ _ xNs1) (count_memPn _ _ xNs2). +by move=> -[/esym/eqP]; rewrite addn_eq0 => /andP[/eqP/count_memPn]. +Qed. + +Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. by move=> *; rewrite eq_sym eqseq_pivotl//; case: eqVneq => /=. Qed. + +Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2) -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. +by rewrite uniq_catC/= mem_cat => /andP[/norP[? ?] _]; rewrite eqseq_pivotl. +Qed. + +Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) -> + (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4). +Proof. by move=> ?; rewrite eq_sym uniq_eqseq_pivotl//; case: eqVneq => /=. Qed. + End EqSeq. Section RotIndex. @@ -1401,9 +1468,7 @@ Implicit Types x y z : T. Lemma rot_index s x (i := index x s) : x \in s -> rot i s = x :: (drop i.+1 s ++ take i s). -Proof. -by move=> x_s; rewrite /rot (drop_nth x) ?index_mem ?nth_index// cat_cons. -Qed. +Proof. by move=> x_s; rewrite /rot drop_index. Qed. Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'. @@ -1472,7 +1537,7 @@ Definition bitseq := seq bool. Canonical bitseq_eqType := Eval hnf in [eqType of bitseq]. Canonical bitseq_predType := Eval hnf in [predType of bitseq]. -(* Generalized versions of splitP (from path.v): split_find_nth and split_find *) +(* Generalizations of splitP (from path.v): split_find_nth and split_find *) Section FindNth. Variables (T : Type). Implicit Types (x : T) (p : pred T) (s : seq T). @@ -1623,6 +1688,10 @@ 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/permPl; rewrite !catA perm_cat2r perm_catC. Qed. +Lemma perm_catACA s1 s2 s3 s4 : + perm_eql ((s1 ++ s2) ++ (s3 ++ s4)) ((s1 ++ s3) ++ (s2 ++ s4)). +Proof. by apply/permPl; rewrite perm_catAC !catA perm_catAC. Qed. + Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s). Proof. by move=> /= s2; rewrite -cats1 perm_catC. Qed. @@ -1920,14 +1989,24 @@ Lemma mask_cat m1 m2 s1 s2 : size m1 = size s1 -> mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2. Proof. by move: m1 s1; apply: seq_ind2 => // -[] m1 x1 s1 /= _ ->. Qed. +Lemma mask_rcons b m x s : size m = size s -> + mask (rcons m b) (rcons s x) = mask m s ++ nseq b x. +Proof. by move=> ms; rewrite -!cats1 mask_cat//; case: b. Qed. + +Lemma all_mask a m s : all a s -> all a (mask m s). +Proof. by elim: s m => [|x s IHs] [|[] m]//= /andP[ax /IHs->]; rewrite ?ax. Qed. + Lemma has_mask_cons a b m x s : has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s). Proof. by case: b. Qed. Lemma has_mask a m s : has a (mask m s) -> has a s. +Proof. by apply/contraTT; rewrite -!all_predC; apply: all_mask. Qed. + +Lemma rev_mask m s : size m = size s -> rev (mask m s) = mask (rev m) (rev s). Proof. -elim: m s => [|b m IHm] [|x s] //; rewrite has_mask_cons /= andbC. -by case: (a x) => //= /IHm. +move: m s; apply: seq_ind2 => //= b x m s eq_size_sm IH. +by case: b; rewrite !rev_cons mask_rcons ?IH ?size_rev// (cats1, cats0). Qed. Lemma mask_rot m s : size m = size s -> @@ -2102,6 +2181,27 @@ elim: s => //= x s; case: (_ \in _); last by rewrite eqxx. by case: (undup s) => //= y u; case: (_ == _) => //=; apply: cons_subseq. Qed. +Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2. +Proof. +wlog suff W : s1 s2 / subseq s1 s2 -> subseq (rev s1) (rev s2). + by apply/idP/idP => /W //; rewrite !revK. +by case/subseqP => m size_m ->; rewrite rev_mask // mask_subseq. +Qed. + +Lemma subseq_cat2l s s1 s2 : subseq (s ++ s1) (s ++ s2) = subseq s1 s2. +Proof. by elim: s => // x s IHs; rewrite !cat_cons /= eqxx. Qed. + +Lemma subseq_cat2r s s1 s2 : subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2. +Proof. by rewrite -subseq_rev !rev_cat subseq_cat2l subseq_rev. Qed. + +Lemma subseq_rot p s n : + subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s). +Proof. +move=> /subseqP[m size_m ->]. +exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. +by rewrite (leq_trans (count_size _ _))// size_take; case: ltnP. +Qed. + End Subseq. Prenex Implicits subseq. @@ -2115,16 +2215,19 @@ Variables (T : eqType) (x : T). Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s. +Lemma rem_cons y s : rem (y :: s) = if y == x then s else y :: rem s. +Proof. by []. Qed. + +Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 s. +Proof. by elim: s => //= y s ->; case: eqVneq; rewrite ?drop0. Qed. + Lemma rem_id s : x \notin s -> rem s = s. -Proof. -by elim: s => //= y s IHs /norP[neq_yx /IHs->]; rewrite eq_sym (negbTE neq_yx). -Qed. +Proof. by elim: s => //= y s IHs /norP[neq_yx /IHs->]; case: eqVneq neq_yx. 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_sym. -case: eqP => [-> // | _ /IHs]. -by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_sym. +move=> xs; rewrite remE -[X in perm_eq X](cat_take_drop (index x s)). +by rewrite drop_index// -cat1s perm_catCA cat1s. Qed. Lemma size_rem s : x \in s -> size (rem s) = (size s).-1. @@ -2154,6 +2257,18 @@ Proof. by move/rem_filter=> -> y; rewrite mem_filter. Qed. Lemma mem_rem_uniqF s : uniq s -> x \in rem s = false. Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed. +Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x. +Proof. +have [/perm_to_rem/permP->|xNs]/= := boolP (x \in s); first by rewrite addKn. +by rewrite subn0 rem_id. +Qed. + +Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y). +Proof. +rewrite count_rem; have []//= := boolP (x \in s). +by case: eqP => // <- /count_memPn->. +Qed. + End Rem. Section Map. @@ -2259,8 +2374,18 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" := Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s. Proof. by elim: s => //= x s <-; case: (a x). Qed. -Lemma mask_filter (T : eqType) (s : seq T) (m : bitseq) : - uniq s -> mask m s = [seq i <- s | i \in mask m s]. +Section MiscMask. + +Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s. +Proof. +by elim: s m => [|x s IHs] [|[] m]//=; + rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl. +Qed. + +Variable (T : eqType). +Implicit Types (s : seq T) (m : bitseq). + +Lemma mask_filter s m : uniq s -> mask m s = [seq i <- s | i \in mask m s]. Proof. elim: m s => [|[] m ih] [|x s] //=. - by move=> _; elim: s. @@ -2269,6 +2394,33 @@ elim: m s => [|[] m ih] [|x s] //=. - by case: ifP => [/mem_mask -> // | _ /andP [] _ /ih]. Qed. +Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2. +Proof. by move=> /subseqP[m _ ->]; rewrite leq_count_mask. Qed. + +Lemma count_maskP s1 s2 : + (forall x, count_mem x s1 <= count_mem x s2) <-> + exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2). +Proof. +split=> [s1_le|[m _ /permP s1ms2 x]]; last by rewrite s1ms2 leq_count_mask. +suff [m mP]: exists m, perm_eq s1 (mask m s2). + by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. +elim: s2 => [|x s2 IHs]//= in s1 s1_le *. + by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le. +have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. +exists ((x \in s1) :: m); have [|/rem_id<-//] := boolP (x \in s1). +by move/perm_to_rem/permPl->; rewrite perm_cons. +Qed. + +Lemma count_subseqP s1 s2 : + (forall x, count_mem x s1 <= count_mem x s2) <-> + exists2 s, subseq s s2 & perm_eq s1 s. +Proof. +rewrite count_maskP; split=> [[m _]|[_/subseqP[m sm ->]]]; last by exists m. +by exists (mask m s2); rewrite ?mask_subseq. +Qed. + +End MiscMask. + Section FilterSubseq. Variable T : eqType. @@ -2294,6 +2446,18 @@ rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12). Qed. +Lemma uniq_subseq_pivot x (s1 s2 s3 s4 : seq T) (s := s3 ++ x :: s4) : + uniq s -> subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4). +Proof. +move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first. + by rewrite cat_subseq //= eqxx. +have uniq_s' := subseq_uniq sub_s'_s uniq_s. +have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s. +rewrite !filter_cat /= mem_cat inE eqxx orbT /=. +rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->]. +by rewrite !filter_subseq. +Qed. + Lemma perm_to_subseq s1 s2 : subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)}. Proof. @@ -2303,15 +2467,12 @@ case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}. by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r. Qed. -Lemma subset_maskP s1 s2 : uniq s1 -> {subset s1 <= s2} -> - exists2 m : seq bool, size m = size s2 & perm_eq s1 (mask m s2). +Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}. Proof. -move=> s1_uniq sub_s1_s2; pose s1' := [seq x <- undup s2 | x \in s1]. -have /subseqP[m sm s1'_eq] : subseq s1' s2. - by apply: subseq_trans (undup_subseq _); apply: filter_subseq. -exists m; rewrite // -s1'_eq; apply: uniq_perm => // [|x]. - by rewrite filter_uniq ?undup_uniq. -by rewrite mem_filter mem_undup; have [/sub_s1_s2|] := boolP (x \in s1). +move=> s1 s2; elim: s2 s1 => [|x2 s2 IHs2] [|x1 s1]; rewrite ?sub0seq //=. +have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx. +move=> /IHs2/subseq_trans->//. +by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed. End FilterSubseq. @@ -3063,16 +3224,45 @@ Lemma size_allpairs_dep f s t : size [seq f x y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s]. Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed. +Lemma allpairs0l f t : [seq f x y | x <- [::], y <- t x] = [::]. +Proof. by []. Qed. + +Lemma allpairs0r f s : [seq f x y | x <- s, y <- [::]] = [::]. +Proof. by elim: s. Qed. + +Lemma allpairs1l f x t : + [seq f x y | x <- [:: x], y <- t x] = [seq f x y | y <- t x]. +Proof. exact: cats0. Qed. + +Lemma allpairs1r f s y : + [seq f x y | x <- s, y <- [:: y x]] = [seq f x (y x) | x <- s]. +Proof. exact: flatten_map1. Qed. + +Lemma allpairs_cons f x s t : + [seq f x y | x <- x :: s, y <- t x] = + [seq f x y | y <- t x] ++ [seq f x y | x <- s, y <- t x]. +Proof. by []. Qed. + Lemma eq_allpairs (f1 f2 : forall x, T x -> R) s t : (forall x, f1 x =1 f2 x) -> [seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x]. -Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. +Proof. by move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed. + +Lemma eq_allpairsr (f : forall x, T x -> R) s t1 t2 : (forall x, t1 x = t2 x) -> + [seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 x]. +(* From Coq 8.10 Proof. by move=> eq_t; under eq_map do rewrite eq_t. Qed. *) +Proof. by move=> eq_t; congr flatten; apply: eq_map => x; rewrite eq_t. Qed. Lemma allpairs_cat f s1 s2 t : [seq f x y | x <- s1 ++ s2, y <- t x] = [seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x]. Proof. by rewrite map_cat flatten_cat. Qed. +Lemma allpairs_rcons f x s t : + [seq f x y | x <- rcons s x, y <- t x] = + [seq f x y | x <- s, y <- t x] ++ [seq f x y | y <- t x]. +Proof. by rewrite -cats1 allpairs_cat allpairs1l. Qed. + Lemma allpairs_mapl f (g : S' -> S) s t : [seq f x y | x <- map g s, y <- t x] = [seq f (g x) y | x <- s, y <- t (g x)]. Proof. by rewrite -map_comp. Qed. @@ -3165,21 +3355,44 @@ Section MemAllPairs. Variables (S : Type) (T : S -> Type) (R : eqType). Implicit Types (f : forall x, T x -> R) (s : seq S). -Lemma allpairs_catr f s t1 t2 : - [seq f x y | x <- s, y <- t1 x ++ t2 x] =i - [seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]. +Lemma perm_allpairs_catr f s t1 t2 : + perm_eql [seq f x y | x <- s, y <- t1 x ++ t2 x] + ([seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]). +Proof. +apply/permPl; rewrite perm_sym; elim: s => //= x s ihs. +by rewrite perm_catACA perm_cat ?map_cat. +Qed. + +Lemma mem_allpairs_catr f s y0 t : + [seq f x y | x <- s, y <- y0 x ++ t x] =i + [seq f x y | x <- s, y <- y0 x] ++ [seq f x y | x <- s, y <- t x]. +Proof. exact/perm_mem/permPl/perm_allpairs_catr. Qed. + +Lemma perm_allpairs_consr f s y0 t : + perm_eql [seq f x y | x <- s, y <- y0 x :: t x] + ([seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]). Proof. -move=> z; rewrite mem_cat; elim: s => //= x s ih. -by rewrite map_cat !mem_cat ih !orbA; congr orb; rewrite orbAC. +by apply/permPl; rewrite (perm_allpairs_catr _ _ (fun=> [:: _])) allpairs1r. Qed. -Lemma allpairs_consr f s t1 t2 : - [seq f x y | x <- s, y <- t1 x :: t2 x] =i - [seq f x (t1 x) | x <- s] ++ [seq f x y | x <- s, y <- t2 x]. +Lemma mem_allpairs_consr f s t y0 : + [seq f x y | x <- s, y <- y0 x :: t x] =i + [seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]. +Proof. exact/perm_mem/permPl/perm_allpairs_consr. Qed. + +Lemma allpairs_rconsr f s y0 t : + perm_eql [seq f x y | x <- s, y <- rcons (t x) (y0 x)] + ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]). Proof. -by move=> z; rewrite (allpairs_catr f s (fun x => [:: t1 x])) /= flatten_map1. +apply/permPl; rewrite -(eq_allpairsr _ _ (fun=> cats1 _ _)). +by rewrite perm_allpairs_catr allpairs1r. Qed. +Lemma mem_allpairs_rconsr f s t y0 : + [seq f x y | x <- s, y <- rcons (t x) (y0 x)] =i + ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]). +Proof. exact/perm_mem/permPl/allpairs_rconsr. Qed. + End MemAllPairs. Lemma all_allpairsP @@ -3596,6 +3809,14 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) 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). - -Notation iota_add := (deprecate iota_add iotaD) (only parsing). +(* TODO: restore when Coq 8.10 is no longer supported *) +(* #[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")] *) +Notation iota_add := iotaD (only parsing). Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing). + +Notation allpairs_catr := + (deprecate allpairs_catr mem_allpairs_catr _ _ _) (only parsing). +Notation allpairs_consr := + (deprecate allpairs_consr mem_allpairs_consr _ _ _) (only parsing). +Notation perm_allpairs_rconsr := + (deprecate perm_allpairs_rconsr allpairs_rconsr _ _ _) (only parsing). diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 568f8b0..0a2fbcd 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -2030,15 +2030,13 @@ Notation "@ 'decr_inj_in'" := (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope. Notation decr_inj_in := (@decr_inj_in _ _) (only parsing). +Notation "@ 'iter_add'" := + (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope. Notation "@ 'odd_opp'" := (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope. Notation "@ 'sqrn_sub'" := (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. - -(* TODO: restore when Coq 8.10 is no longer supported *) -(* #[deprecated(since="mathcomp 1.13.0", note="Use iterD instead.")] *) -Notation iter_add := iterD (only parsing). - +Notation iter_add := (@iterD _) (only parsing). Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing). Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing). Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing). |