aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-25Stability proofs of sort (#358)Kazuhiko Sakaguchi
* Modified the definition of sort to work on any type * Other Generalizations, fixes and CHANGELOG entry * Add stability lemmas for `path.sort` - Inverse the comparison in `merge` and swap arguments of it everywhere. - Add `sort_rec1` and `sortE` to simplify inductive proofs on `sort`. - Add `seq.mask_filter`, `mem2E`, `path_mask`, `path_filter`, and `sorted_mask`. - Generalize `sorted_filter`, `homo_path_in`, `mono_path_in`, `homo_sorted_in`, and `mono_sorted_in` to non-`eqType`s. - Add the following lemmas to state the stability of `path.merge` and `path.sort`. sorted_merge : forall (T : Type) (leT : rel T), transitive leT -> forall s t : seq T, sorted leT (s ++ t) -> merge leT s t = s ++ t merge_stable_path : forall (T : Type) (leT leT' : rel T), total leT -> forall (x : T) (s1 s2 : seq T), all (fun y : T => all (leT' y) s2) s1 -> path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s1 -> path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s2 -> path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x (merge leT s1 s2) merge_stable_sorted : forall (T : Type) (leT leT' : rel T), total leT -> forall s1 s2 : seq T, all (fun x : T => all (leT' x) s2) s1 -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s1 -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s2 -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (merge leT s1 s2) sorted_sort : forall (T : Type) (leT : rel T), transitive leT -> forall s : seq T, sorted leT s -> sort leT s = s sort_stable : forall (T : Type) (leT leT' : rel T), total leT -> transitive leT' -> forall s : seq T, sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s) filter_sort : forall (T : Type) (leT : rel T), total leT -> transitive leT -> forall (p : pred T) (s : seq T), [seq x <- sort leT s | p x] = sort leT [seq x <- s | p x] mask_sort : forall (T : Type) (leT : rel T), total leT -> transitive leT -> forall (s : seq T) (m : bitseq), {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)} mask_sort' : forall (T : Type) (leT : rel T), total leT -> transitive leT -> forall (s : seq T) (m : bitseq), sorted leT (mask m s) -> {m_s : bitseq | mask m_s (sort leT s) = mask m s} subseq_sort : forall (T : eqType) (leT : rel T), total leT -> transitive leT -> {homo sort leT : t s / subseq t s} subseq_sort' : forall (T : eqType) (leT : rel T), total leT -> transitive leT -> forall t s : seq T, subseq t s -> sorted leT t -> subseq t (sort leT s) mem2_sort : forall (T : eqType) (leT : rel T), total leT -> transitive leT -> forall (s : seq T) (x y : T), leT x y -> mem2 s x y -> mem2 (sort leT s) x y * Avoid some eta-expansions * Get the proper fix of `order_path_min` and remove `sort_map_in` * Update documentation and CHANGELOG entries
2019-10-24Added and generalized arithmetic theorems. (#394)Cyril Cohen
- Added: `modn_divl` and `divn_modl`. - Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
2019-10-21Merge pull request #365 from math-comp/ghpages-redirectMaxime Dénès
Redirects to math-comp.github.io
2019-10-18Add build for mathcomp/mathcomp-dev:coq-8.10 (#391)Erik Martin-Dorel
* feat: Add build for mathcomp/mathcomp-dev:coq-8.10 * fix(coq-mathcomp-ssreflect.opam): Bump coq upper bound * fix(*.opam): Remove "remove" directive href: coq/opam-coq-archive#703
2019-10-16Merge pull request #203 from CohenCyril/improving_fintype_bigopMaxime Dénès
Improving fintype and bigop
2019-10-16shifting to CHANGELOG_UNRELEASEDCyril Cohen
2019-10-16renaming new `reindex_` lemmas with prefix `big_`Cyril Cohen
2019-10-16Improving fintype and bigopCyril Cohen
### Added - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. - Bigop theorems: `big_rmcond`, `bigD1_seq`, `reindex_enum_val_cond`, `reindex_enum_rank_cond`, `reindex_enum_val`, `reindex_enum_rank`, `big_set`.
2019-10-16removing everything but index which redirects to the new pageCyril Cohen
2019-10-15Merge pull request #390 from thery/docCyril Cohen
typo in ssralg
2019-10-14typothery
2019-10-07Merge pull request #384 from pi8027/hierarchyCyril Cohen
Fix and improve the test suite and Makefile
2019-10-07Merge pull request #387 from pi8027/seq-lemmasCyril Cohen
Add `flatten_map1` and `allpairs_consr`
2019-10-05Add flatten_map1 and allpairs_consrKazuhiko Sakaguchi
2019-10-02Fix and improve the test suite and MakefileKazuhiko Sakaguchi
- improve an error message produced by the `check_join` tactic, - fix the build of the test suite: `make test-suite`, and - add a new rule `only` to build a subset of MathComp.
2019-10-01Merge pull request #386 from pi8027/allpairsCyril Cohen
Generalize `allpairs_catr` to non-`eqType`s
2019-09-30Generalize `allpairs_catr` to non-`eqType`sKazuhiko Sakaguchi
2019-09-30Euclid theorem for product (#375)Laurent Théry
2019-09-30ffact as a product similar to fact_prod (#374)Laurent Théry
Thanks!
2019-09-28maxn comment fix (#385)Antonio Nikishaev
2019-09-24Merge pull request #380 from pi8027/ring-core-scopeCyril Cohen
Fix a typo: `ring_core_scope`
2019-09-18Fix a typo: ring_core_scope -> ring_scopeKazuhiko Sakaguchi
2019-09-16fermat little theoremthery
2019-09-05Redirects to math-comp.github.ioCyril Cohen
Merge only after solving issue https://github.com/math-comp/math-comp/issues/361
2019-08-12Merge pull request #376 from erikmd/fix-gitlab-yamlCyril Cohen
[ci] fix .gitlab-ci.yml regarding "GIT_STRATEGY: none"
2019-08-10fix(.gitlab-ci.yml): duplicated "variables:" entryErik Martin-Dorel
This could explain why the change in b8eadb8603b83c053a313b39c2a8f268385d8942 was not taken into account.
2019-08-02Merge pull request #373 from erikmd/improve-ciCyril Cohen
[ci] a few improvements of the GitLab CI setup
2019-07-30[ci] Adapt the GitLab CI config to allow scheduled builds for coq-devErik Martin-Dorel
* Normal builds (branches & GitHub PRs) are not impacted * Triggering a scheduled pipeline will only run {coq-dev, mathcomp-dev:coq-dev} to build and deploy the corresponding image to mathcomp/mathcomp-dev:coq-dev. * href: https://docs.gitlab.com/ce/user/project/pipelines/schedules.html
2019-07-30[ci] Add jobs {ci-fourcolor-8.9, ci-odd-order-8.9}Erik Martin-Dorel
* Add {fourcolor, odd-order} test builds with latest Coq release (8.9) * As a result, the math-comp CI config w.r.t. {fourcolor, odd-order} will be similar to that of the upstream repos: - https://github.com/math-comp/fourcolor/blob/master/.travis.yml - https://github.com/math-comp/odd-order/pull/16
2019-07-30refactor: deploy jobs need not clone the repoErik Martin-Dorel
* Set "GIT_STRATEGY: none" accordingly
2019-07-29style: fix indentation detailErik Martin-Dorel
2019-07-11Merge pull request #369 from thery/totientCyril Cohen
totient for prime
2019-07-10totient for primethery
2019-07-05feat(finfun.v): Add tuple_of_finfun, finfun_of_tuple & cancel lemmasCyril Cohen
2019-06-26Merge pull request #364 from erikmd/update/changelogCyril Cohen
docs: Add missing entry in CHANGELOG.md regarding #292
2019-06-26docs: Add missing entry in CHANGELOG.mdErik Martin-Dorel
href: math-comp/math-comp#292
2019-06-18Merge pull request #340 from pi8027/hierarchyEnrico
Reimplement the hierarchy related tools in OCaml
2019-06-11Merge pull request #302 from CohenCyril/fixsetGeorges Gonthier
Fixpoint theorems in finset
2019-06-04Fixpoint theorems in finsetCyril Cohen
2019-05-29Merge pull request #353 from anton-trunov/update-ciCyril Cohen
Remove support for Travis CI (mathcomp switched to Gitlab CI)
2019-05-29Replace eqVneq to destruct both x == y, but also y == x (#351)Cyril Cohen
2019-05-29Remove support for Travis CIAnton Trunov
Mathcomp switched to Gitlab CI via coqbot, see here: https://github.com/math-comp/math-comp/pull/353#issuecomment-497017174
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Merge pull request #352 from CohenCyril/pr_tempateCyril Cohen
PR template
2019-05-29reword entry in CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29Update pull_request_template.mdCyril Cohen
2019-05-29Move unreleased changelog entries to CHANGELOG_UNRELEASED.mdAnton Trunov
2019-05-29pr templateCyril Cohen
2019-05-29incorporate new suggestions by @CohenCyrilAnton Trunov
2019-05-29Replace eqVneq with eqPsymAnton Trunov
Also changed eqsVneq.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 17:03:50 +0000