aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/seq.v
AgeCommit message (Collapse)Author
2021-03-07Adding Order.enum and related definitions and theoremsCyril Cohen
2021-01-22Remove deprecation aliases introduced in 1.9.0Kazuhiko Sakaguchi
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
- The `deprecate` notation and `iota_add` have been deprecated. All the uses of the `deprecate` notation have been replaced with the `deprecated` attribute. - Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1 have been removed. - Remove `VDFILE` related hacks from `Makefile.common`.
2020-12-16Add `pairwise r xs` predicateKazuhiko Sakaguchi
which asserts that the relation `r` holds for any i-th and j-th element of `xs` such that i < j.
2020-11-25Rename `all1rel` to `all2rel`, restate `eq_allrel`, and add CHANGELOG entriesKazuhiko Sakaguchi
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-11-25Apply suggestions from code reviewKazuhiko Sakaguchi
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-11-25Apply suggestions from code reviewKazuhiko Sakaguchi
Co-authored-by: Christian Doczkal <christian.doczkal@inria.fr>
2020-11-25Generalize `allrel` to take two lists as argumentsKazuhiko Sakaguchi
2020-11-24Add more `_in` lemmas and CHANGELOG entriesKazuhiko Sakaguchi
2020-11-24factoring out in_sigCyril Cohen
2020-11-24Add `_in` lemmas for `sort`Kazuhiko Sakaguchi
2020-11-23Merge pull request #667 from CohenCyril/ssrcoq8.10Enrico Tassi
Using Coq 8.10 ssreflect new features
2020-11-20Tuning simplifications using Arguments simpl nomatchCyril Cohen
2020-11-20Using Coq 8.10 ssreflect new featuresCyril Cohen
2020-11-20typo in documentation of allpairs_depYves Bertot
2020-11-19add declare scopesReynald Affeldt
2020-11-12Apply suggestions from KazuhikoCyril Cohen
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2020-11-12Equivalences instead of implications for `count_maskP` and `count_subseqP`Cyril Cohen
2020-11-12Shorter proofs and suggestions by KazuhikoCyril Cohen
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2020-11-12Adding some theory for `rem` and generalizing `subset_maskP`Cyril Cohen
- Added helper lemmas about `rem`: `rem_cons` (to control unfolding), `remE`, `count_rem`, `count_mem_rem`, and `subseq_mem`. (New lemma `drop_index` briges the gap between `cat_take_drop` and `remE`). - `subset_maskP`, which was not released yet is generalized with hypothesis `(forall x, count_mem x s1 <= count_mem x s2)`, instead of `uniq s1` and `{subset s1 <= s2}`, the previous behaviour can be restored with helper lemma `leq_uniq_count` - Its trivial consequence `subset_subseqP` has been added too.
2020-11-11Merge pull request #640 from CohenCyril/fix_iota_addCyril Cohen
Deprecation of iota_add delayed, and not the one of iter_add
2020-11-11make pivot the first argument in uniq_subseq_pivotChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-11-11turn uniq_subseq_pivot into equalityChristian Doczkal
2020-11-11Apply suggestions from code reviewChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com> Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2020-11-11fixup after feedback from CyrilChristian Doczkal
2020-11-11Apply suggestions from code reviewChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-11-11suggestions from CyrilChristian Doczkal
2020-11-11lemmas on subseq and rotChristian Doczkal
2020-11-11Deprecation of iota_add delayed, and not the one of iter_addCyril Cohen
2020-11-11Merge pull request #632 from pi8027/path-cycle-sortedCyril Cohen
Reorganize, generalize, and add lemmas about `path`, `cycle`, and `sorted`
2020-11-11New lemmas about allpairsCyril Cohen
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2020-11-11Apply suggestions from code reviewKazuhiko Sakaguchi
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-11-10Reorganize, generalize, and add lemmas about `path`, `cycle`, and `sorted`Kazuhiko Sakaguchi
- Add `allss` and `all_mask` lemmas. - Since `path`, `cycle`, and `sorted` share similar properties, these lemmas have been relocated in the same place to improve the visibility. Some missing lemmas have also been discovered and added. - Generalize `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType` T by introducing a predicate `P : {pred T}`.
2020-11-02lemmas for reasoing about "rot n (rot m s)"Christian Doczkal
2020-10-29Switch from long suffixes to short suffixesKazuhiko Sakaguchi
2020-10-10generalization and shorter proofsCyril Cohen
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
2020-10-09Added results about `mask` and `subseq`Cyril Cohen
2020-09-08split_find_nth and split_find lemmasCyril Cohen
2020-09-03Adding allrel predicateCyril Cohen
2020-06-18drop_uniq / CHANGELOGChristian Doczkal
2020-06-18cardinality lemmas for #|A| <= 1 and n <= #|A|Christian Doczkal
2020-05-16A few more revisionsKazuhiko Sakaguchi
2020-05-13Revise proofs in ssreflect/*.vKazuhiko Sakaguchi
This change reduces - use of numerical occurrence selectors (#436) and - use of non ssreflect tactics such as `auto`, and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`, `ltngtP`, and `eqVneq`.
2020-04-10Make `all2` better wrt the guard conditionCyril Cohen
fixes #469
2020-04-09- switching long suffixes to short suffixesReynald Affeldt
+ `odd_add` -> `oddD` + `odd_sub` -> `oddB` + `take_addn` -> `takeD` + `rot_addn` -> `rotD` + `nseq_addn` -> `nseqD` fixes #359
2020-04-02Merge pull request #468 from ybertot/remove-deprecated-from-1.9Enrico Tassi
remove deprecated commands whose deprecation was introduced in 1.9.0
2020-04-01Merge pull request #429 from pi8027/extend-nat-comparisonYves Bertot
Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v
2020-03-31remove deprecated commands whose deprecation was introduced in release 1.9.0Yves Bertot
fixes #418
2020-03-15Extend comparison predicates for nat with minn and maxnKazuhiko Sakaguchi
2020-01-28Added lemmas about foldl, scanl, foldr and rcons and consCyril Cohen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:32:04 +0000