aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
AgeCommit message (Collapse)Author
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
- In the definition of structures in order.v, displays are removed from parameters of mixins and fields of classes internally and now only appear in parameters of structures. Consequently, each mixin is now parameterized by a class rather than a structure, and the corresponding factory parameterized by a structure is provided to replace the use of the mixin. These factories have the same names as in the mixins before this change except that `bLatticeMixin` and `tbLatticeMixin` have been renamed to `bottomMixin` and `topMixin` respectively. - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`.
2020-08-11fix notation-incompatible-format warningsChristian Doczkal
2020-08-11Merge pull request #507 from pi8027/test-guard-condCyril Cohen
Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition
2020-08-11Merge pull request #542 from chdoc/nothing-to-injectCyril Cohen
fix "Nothing to inject" warnings
2020-08-11Merge pull request #541 from chdoc/properCCyril Cohen
lemmas for proper and setC
2020-06-27Fix some Makefile issues and rename `hierarchy_test.v` to `test_hierarchy_all.v`Kazuhiko Sakaguchi
2020-06-26fix "Nothing to inject" warningsChristian Doczkal
2020-06-26lemmas for proper and setCChristian Doczkal
2020-06-24Merge pull request #540 from thery/docCyril Cohen
fix the doc for ubnP in ssrnat
2020-06-24Merge pull request #539 from thery/sum_nat_constCyril Cohen
simpler proof of sum_nat_const_nat in bigop.v
2020-06-24missing lemmas discovered while developing mathcomp-analysisReynald Affeldt
2020-06-24fix the doc for ubnP in ssrnatthery
2020-06-24simpler proofthery
2020-06-18conform to 80 chars limitChristian Doczkal
2020-06-18fixup spacingCyril Cohen
2020-06-18Apply suggestions from code reviewChristian Doczkal
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
2020-06-18drop_uniq / CHANGELOGChristian Doczkal
2020-06-18add fcard_gt?P lemmas found in fourcolorChristian Doczkal
2020-06-18cards_eqP and cards2PChristian Doczkal
2020-06-18cardinality lemmas for #|A| <= 1 and n <= #|A|Christian Doczkal
2020-06-17contra lemmas involving propositionsChristian Doczkal
2020-06-13Add more test cases for higher-order recursive functions in seq.v w.r.t. the ↵Kazuhiko Sakaguchi
guard condition
2020-06-09add lua&sed to shell and switch to coq 8.11 + fixing docCyril Cohen
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-08turning let into local definitionCyril Cohen
2020-06-08Merge pull request #528 from CohenCyril/silence_warningsCyril Cohen
silencing warnings in individual packages
2020-06-08silencing warnings in individual packagesCyril Cohen
2020-06-08Documenting addition policy to coq.Cyril Cohen
2020-06-06bugfixCyril Cohen
2020-06-06Missing homo_mono lemmasCyril Cohen
2020-06-06ImprovementsCyril Cohen
- deprecating `fintype.arg_(min|max)P` - removing dangling comments connecting min max and meet join - better compatibility module - removing broken notations with `\min` and `\max` (no neutral available) - fixing `incompare` and `incomparel` in order.v - adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`) - adding missing `(comparable|real)_arg(min|max)P` - CHANGELOG update
2020-06-06tentative changelogReynald Affeldt
- mostly gathered the changes from previous commits - add `minrC` - minor doc addition to `order.v`
2020-06-06General theory of min and max, and use in ssrnumCyril Cohen
- min and max can now be used in a partial order (sometimes under preconditions) - min and max can now be used in a numDomainType (sometimes under preconditions)
2020-06-06Increasing definitional equalitiesCyril Cohen
- `Order.max` and `Order.min` are now convertible to `maxn` and `minn` - Inserting `(fun _ _ => erefl)` in `LeOrderMixin` and `LtOrderMixin` gives `meet`/`join` which are convertible to `min`/`max` - `Order.max` and `Order.min` are not convertible to former `Num.max` and `Num.min`
2020-06-06Generalizing max and min to porderTypeCyril Cohen
- max and min are not defined in terms or meet and join anymore - extremum_inP is a generalization of extremum suitable for a partial order - arg_min and arg_max are usable in a porderType - equivalences between min and meet, and max and join are proven for orderType - leP, ltP, ltgtP, and `[l]?comparable_.*P` lemmas have been generalized to take this into account - total_display was completely removed
2020-06-05Merge pull request #514 from affeldt-aist/lemmas_from_analysis_20200521Yves Bertot
Lemma addition to ssrnum
2020-06-05fix namingReynald Affeldt
2020-06-05Missing mono lemmas (#513)Cyril Cohen
* Missing mono lemmas
2020-06-04fix namingReynald Affeldt
2020-06-03add real_* variantsReynald Affeldt
2020-06-02another lemma about norm from mathcomp-analysisReynald Affeldt
2020-05-22tentative change of naming convention and add variantsReynald Affeldt
2020-05-21three lemmas that we found useful in the context of theReynald Affeldt
mathcomp-analysis project
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-05-04Merge pull request #493 from pi8027/rm-tuple-lemmas-in-orderCyril Cohen
Remove the tuple extensions in order.v that is available in tuple.v
2020-05-04Remove the tuple extensions in order.v that is available in tuple.vKazuhiko Sakaguchi
2020-04-21Add dual_finLatticeType and fix dual_finDistrLatticeTypeKazuhiko Sakaguchi
This fixes two issues: - dual_finLatticeType was missing, and - dual_finDistrLatticeType was just an identity function.
2020-04-15reworked new lemmas in perm and action and added missing onesCyril Cohen
In particular: rephrased permS0 and permS1 with all_equal_to
2020-04-15addressing comments about PR#221 of mathcompReynald Affeldt
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-09 21:42:02 +0000