aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
AgeCommit message (Collapse)Author
2020-09-05Adding contra lemmas with ordersCyril Cohen
- Adding contra lemmas between `leq`, `ltn`, `Order.le` ("le"), `Order.lt` ("lt"), `b` ("T"), `~~ b` ("N"), `b = false` ("F"), and `~ P` ("not"). - Changelog for contra lemmas with orders Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
2020-09-03compat Coq < 8.10Cyril Cohen
2020-09-03Lemmas reindex_omap and bigD1_ordCyril Cohen
+ eq_liftF and lift_eqF + proof simplificaions
2020-09-03Merge pull request #558 from CohenCyril/are_allpairsEnrico Tassi
Adding allrel predicate
2020-09-03Adding allrel predicateCyril Cohen
2020-09-03New `big_uncond` and `big_rmcond -> big_rmcond_in`Cyril Cohen
- Lemma `big_rmcond` has been renamed `big_rmcomd_in` and the variant which does not require an `eqType` has been added and named `big_uncond`. - The name `big_rmcond` is deprecated and will be reused for `big_uncond` in the next version of math-comp - Additionally `big_uncond_in` is made available for uniformity, but is already deprecated.
2020-09-03Expliciting relation between split and [lr]shiftCyril Cohen
2020-09-01fix for Coq 8.7Cyril Cohen
2020-09-01Adding sig_big_dep lemmaCyril Cohen
2020-08-25Adding lemma `oddS`Cyril Cohen
2020-08-17Qualify the dual_* notations with the Order moduleKazuhiko Sakaguchi
2020-08-16Merge pull request #517 from thery/minnCyril Cohen
Extra theorems about subn minn and maxn
2020-08-15Extra theorems about subn min and maxthery
2020-08-13Merge pull request #553 from chdoc/non-reversible-notationCyril Cohen
fix non-reversible-notation warnings
2020-08-13fix non-reversible-notation warningsChristian Doczkal
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 #542 from chdoc/nothing-to-injectCyril Cohen
fix "Nothing to inject" warnings
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-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-09add lua&sed to shell and switch to coq 8.11 + fixing docCyril Cohen
2020-06-09fix coq 8.12 warningsCyril 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-05Missing mono lemmas (#513)Cyril Cohen
* Missing mono lemmas
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-15Merge pull request #475 from CohenCyril/ssrnat_deprecated_symbolsaffeldt-aist
adding deprecations in ssrnat
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:13:15 +0000