| Age | Commit message (Collapse) | Author |
|---|
|
Drop support for Coq 8.10
|
|
|
|
- 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`.
|
|
|
|
- Generalize `mem0_itv(cc|oo)_xNx` and `oppr_itv(|oo|co|oc|cc)` lemmas from
`numFieldType` to `numDomainType`, which have been specialized in PR #458
accidentally.
- Generalize `mid_in_itv(|oo|cc)` lemmas from `realFieldType` to `numFieldType`.
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
|
|
- `x <= y ?< if c` (lersif) has been replaced with `x < y ?<= if c'` (lteif)
where `c'` is negation of `c`. This change makes statements of several lemmas
(e.g., `lteif_orb`) easily comprehensible.
- The first constructor `BOpen_if` of `itv_bound` has been replaced with
`BClose_if` where the first argument is inverted. Now `pred_of_itv` is defined
by using `lteif` instead of `lersif`.
- Intervals of `T : porderType` form a `porderType` where the ordering relation
is the subset relation. If `T` is a `latticeType`, intervals also form a
`latticeType` where the join and meet are intersection and convex hull
respectively. They are distributive if `T` is an `orderType`.
|
|
- 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)
|
|
scopes
|
|
New lemmas:
- meet_l, meet_r, join_l, join_r.
Renamings:
- Order.BLatticeTheory.lexUl -> disjoint_lexUl,
- Order.BLatticeTheory.lexUr -> disjoint_lexUr,
- Order.TBLatticeTheory.lexIl -> cover_leIxl,
- Order.TBLatticeTheory.lexIr -> cover_leIxr.
Use `Order.TTheory` instead of `Order.Theory` if applicable
|
|
#283, #285, #286, #288, #296, #330, #334, and #341)
ssrnum related changes:
- Redefine the intermediate structure between `idomainType` and `numDomainType`,
which is `normedDomainType` (normed integral domain without an order).
- Generalize (by using `normedDomainType` or the order structures), relocate
(to order.v), and rename ssrnum related definitions and lemmas.
- Add a compatibility module `Num.mc_1_9` and export it to check compilation.
- Remove the use of the deprecated definitions and lemmas from entire theories.
- Implement factories mechanism to construct several ordered and num structures
from fewer axioms.
order related changes:
- Reorganize the hierarchy of finite lattice structures. Finite lattices have
top and bottom elements except for empty set. Therefore we removed finite
lattice structures without top and bottom.
- Reorganize the theory modules in order.v:
+ `LTheory` (lattice and partial order, without complement and totality)
+ `CTheory` (`LTheory` + complement)
+ `Theory` (all)
- Give a unique head symbol for `Total.mixin_of`.
- Replace reverse and `^r` with converse and `^c` respectively.
- Fix packing and cloning functions and notations.
- Provide more ordered type instances:
Products and lists can be ordered in two different ways: the lexicographical
ordering and the pointwise ordering. Now their canonical instances are not
exported to make the users choose them.
- Export `Order.*.Exports` modules by default.
- Specify the core hint database explicitly in order.v. (see #252)
- Apply 80 chars per line restriction.
General changes:
- Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle`
like lemmas:
lt_def x y : (x < y) = (y != x) && (x <= y),
lt_neqAle x y : (x < y) = (x != y) && (x <= y).
- Enable notation overloading by using scopes and displays:
+ Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as
aliases of `meet` and `join` specialized for `total_display`.
+ Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and
`comparable` notations and their explicit variants in `Num.Def`.
+ Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]`
notations in `nat_scope` (specialized for nat), `order_scope` (general
version), and `ring_scope` (specialized for `ring_display`).
- Update documents and put CHANGELOG entries.
|
|
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
|
|
|
|
|
|
itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend itv_rewrite, simplify proofs (#271)
|
|
* Add some theorems on lersif and intervals
* Add more theorems on lersif
* Remove needless parens
* ChangeLog
* Move lersifN
* Add lersif_anti
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
