| Age | Commit message (Collapse) | Author |
|---|
|
- 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`.
|
|
|
|
`order.v`
|
|
|
|
Intro pattern extensions for dup, swap and apply
|
|
since `exact` might call `ssrdone` which calls use of level 0 hints, potentially
causing a loop in some weird cases.
|
|
|
|
Adding bigop lemmas for ring : expr_sum and prodr_natmul
|
|
|
|
|
|
|
|
Co-authored-by: Cyril Cohen <cohen@crans.org>
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
|
|
|
|
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
- 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`.
|
|
|
|
|
|
- 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
|
|
- mostly gathered the changes from previous commits
- add `minrC`
- minor doc addition to `order.v`
|
|
- 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)
|
|
|
|
|
|
|
|
|
|
|
|
mathcomp-analysis project
|
|
%AC annotation are for backward compatilibity with coq <= 8.9
|
|
Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v
|
|
|
|
|
|
|
|
- Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`:
The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and
introduces a hypothesis in the form of `x != y` in the second case. Thus,
`case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms
can be replaced with `case: eqVneq`, `case: (eqVneq x)` and
`case: (eqVneq x y)` respectively. This replacement slightly simplifies and
reduces proof scripts.
- use `have [] :=` rather than `case` if it is better.
- `by apply:` -> `exact:`.
- `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`.
- `move/lem1; move/lem2` -> `move/lem1/lem2`.
- Remove `GRing.` prefix if applicable.
- `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`.
|
|
|
|
* remove ProdNormedZmodule from ssrnum.v, it made its way to mathcomp-analysis in a generalized form (branch analysis_270) at the time of this writing
* update gitlab-ci
|
|
* renaming
NormedZmoduleType -> NormedZmodType
NormedZmoduleMixin -> NormedZmodMixin
that looks more homogeneous with regard to naming conventions used so far
* update .gitlab-ci.yml
* typo
|
|
|
|
amounts to the difference being real, and consequences
|
|
|
|
|
|
scopes
|
|
* Redefine `normedDomainType` (now `normedZmodType`)
- Redefine `normedDomainType` to drop ring and integral domain axioms.
- Add canonical instance of `normedZmodType` for `prod`.
|
|
- Rename `totalLatticeMixin` to `totalPOrderMixin`.
- Refactor num mixins.
- Use `Num.min` and `Num.max` rather than lattice notations if applicable.
|
|
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
|
|
The comparison predicates (for nat, ordered types, ordered integral domains)
must have the following order of arguments:
- leP x y : le_xor_gt x y ... (x <= y) (y < x) ... .
- ltP x y : lt_xor_ge x y ... (y <= x) (x < y) ... .
- ltgtP x y : compare x y ... (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) ... .
|
|
- comparer -> compare (in order.v)
- eq constructor of compare goes last
- "x < y" is matched before "x > y"
- "x <= y" is matched before "x >= y"
- adding prod and lexi ordering on tuple
- adding missing CS
- edit CHANGELOG
|
|
|
|
#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.
|
|
|
|
Replaced the legacy generalised induction idiom with a more robust one
that does not rely on the `{-2}` numerical occurrence selector, using
either new helper lemmas `ubnP` and `ltnSE` or a specific `nat`
induction principle `ltn_ind`.
Added (non-strict in)equality induction helper lemmas
Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression
along with some (in)equality, in preparation for some generalised
induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed
`ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember
that the inductive value remains below the initial one.
Used the change log to give notice to users to update the generalised
induction idioms in their proofs to one of the new forms before
Mathcomp 1.11.
|
