| Age | Commit message (Collapse) | Author |
|---|
|
Non-distributive lattice structures
|
|
|
|
|
|
|
|
Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)
|
|
This reverts commit a03e0cb0ff40afabcaccba7f764076355ca82962.
|
|
|
|
Renaming converse to dual in order.v
|
|
|
|
|
|
Indeed, the name converse and notation ^c were already taken in
https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L989-L990
We are renaming to dual.
|
|
Add FCSL-PCM library to CI
|
|
|
|
FCSL-PCM is in Coq's CI, so this will prevent breaking Coq's CI, see
https://github.com/imdea-software/fcsl-pcm/issues/17
|
|
Refactoring and linting proofs especially in polydiv.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 CI overlay for PR #270
|
|
|
|
[ci] add missing "except:" rules to fix the nightly build on GitLab CI
|
|
It seems adding an "except:" rule in a job that "extends:" another one
*overwrites* the except rule, so we were getting too many jobs in the
mathcomp-dev scheduled pipeline.
Once merged, this patch should fix this.
|
|
take advantage of opam variables and their default values
|
|
Dispatching order and norm, and anticipating normed modules.
|
|
|
|
|
|
* 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
|
|
|
|
- adding a doc paragraph on displays
- Changelog
- better proofs for new logn, gcdn, lcmn, partn facts
- Putting comments in the example of nat
|
|
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.
|
|
|
|
|
|
|
|
needed lemmas (#261)
* adds relevant theorems when fcycle f (orbit f x) and the needed lemmas
* Generalize f_step lemmas
* Generalizations, shorter proofs, bugfixes, CHANGELOG
- changelog, renamings and comments
- renaming `homo_cycle` to `mem_fcycle` and other small renamings
- name swap `mem_orbit` and `in_orbit`
- simplifications
- generalization following @pi8027's comment
- Getting rid of many uniquness condition in `fingraph.v`
- added cases to the equivalence `orbitPcycle`
- added `cycle_catC`
|
|
Fix the doc-clean target of Makefile
|
|
|
|
remove duplicated sentence in CHANGELOG_UNRELEASED
|
|
Big enum
|
|
Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more
explicitly big ops iterating over explicit enumerations in a `finType`.
The previous practice was to rely on the convertibility between
`enum A` and `filter A (index_enum T)`, sometimes explicitly via the
`filter_index_enum` equality, more often than not implicitly.
Both are likely to fail after the integration of `finmap`, as the
`choiceType` theory can’t guarantee that the order in selected
enumerations is consistent.
For this reason `big_enum` and the related (but currently unused)
`big_image` lemmas are restricted to the abelian case. The `big_enumP`
lemma can be used to handle enumerations in the non-abelian case, as
explained in the `bigop.v` internal documentation.
The Changelog entry enjoins clients to stop relying on either
`filter_index_enum` and convertibility (though this PR still provides
both), and warns about the restriction of the `big_image` lemma set to
the abelian case, as it it a possible source of incompatibility.
|
