| Age | Commit message (Collapse) | Author |
|---|
|
* renaming
NormedZmoduleType -> NormedZmodType
NormedZmoduleMixin -> NormedZmodMixin
that looks more homogeneous with regard to naming conventions used so far
* update .gitlab-ci.yml
* typo
|
|
|
|
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
|
|
#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.
|
|
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.
|
|
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.
|
|
|
|
add existsPn/forallPn lemmas
|
|
Commutative Algebras
|
|
|
|
|
|
Initial properties of polynomials in R-algebras
|
|
from
`ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)`
to
`ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`,
to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.
|
|
- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas
|
|
- add notation support for lemma renaming PRs, helping clients adjust
to the name change by emitting warning or raising errors when the old
name is used. The default is to emit warnings, but clients can change
this to silence (if electing to delay migration) or errors (to help
with actual migration). Usage:
Notation old_id := (deprecate old_id new_id) (only parsing).
—> Caveat 1: only prenex maximal implicit of `new_id` are preserved, so,
as `Notation` does not support on-demand implicits, the latter should
be added explicitly as in `(deprecate old new _ _)`.
—> Caveat 2: the warnings are emitted by a tactic-in-term, which
is interpreted during type elaboration. As the SSReflect elaborator may
re-infer type in arguments multiple times (notably, views and arguments
to `apply` and `rewrite`), clients may see duplicate warnings.
- use the `deprecate` facility to introduce the first part of the
refactoring of `seq` permutation lemmas : only lemmas concerning
`perm_eq` should have `perm` as a component of their name.
- document local additions in `ssreflect.v` and `ssrbool.v`
- add 8.8 `odd-order` regression
- the explicit beta-redex idiom use in the `perm_uniq` and
`leq_min_perm` aliases avoids a strange name-sensitive bug of view
interpretation in Coq 8.7.
|
|
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`).
|
|
|
|
|
|
* (Update make's path accordingly)
* This patch is required for opam 2.0 pinning
* As a result, these *.opam files are now similar to the opam files in
https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-*/coq-mathcomp-*.dev/
|
|
Like injectivity lemmas, instances of cancellation lemmas (whose
conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or
`ocancel`) are passed to
generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should
not have trailing on-demand implicits _just before_ the `cancel`
conclusion, as these would be inconvenient to insert (requiring
essentially an explicit eta-expansion).
We therefore use `Arguments` or `Prenex Implicits` directives to make
all such arguments maximally inserted implicits. We don’t, however make
other arguments implicit, so as not to spoil direct instantiation of
the lemmas (in, e.g., `rewrite -[y](invmK injf)`).
We have also tried to do this with lemmas whose statement matches a
`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern
unification will pick up `f = fun x => E[x]`).
We also adjusted implicits of a few stray injectivity
lemmas, and defined constants.
We provide a shorthand for reindexing a bigop with a permutation.
Finally we used the new implicit signatures to simplify proofs that
use injectivity or cancellation lemmas.
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
This increases performance 10% - 15% for Coq v8.6.1 - v8.9.dev.
Tested on a Debain-based 16-core build server and
a Macbook Pro laptop with 2,3 GHz Intel Core i5.
| | Compilation time, old | Compilation | Speedup |
| | (mathcomp commit 967088a6f87) | time, new | |
| Coq 8.6.1 | 10min 33s | 9min 10s | 15% |
| Coq 8.7.2 | 10min 12s | 8min 50s | 15% |
| Coq 8.8.2 | 9min 39s | 8min 32s | 13% |
| Coq 8.9.dev(05d827c800544) | 9min 12s | 8min 16s | 11% |
| | | | |
It seems Coq at some point fixed the problem `_ : Type` was
supposed to solve.
|
|
Document parameter names whenever possible
|
|
As suggested by @ggonthier
[here](https://github.com/math-comp/math-comp/pull/249#pullrequestreview-177938295)
> One of the design ideas for the `Arguments` command was that it would allow
to centralise the documentation of the application of constants.
In that spirit it would be in my opinion better to make as much use of this
as possible, and to document the parameter names whenever possible,
especially that of implicit parameters.
and
[here](https://github.com/math-comp/math-comp/pull/253#discussion_r237434163):
> As a general rule, defined functional constants should have maximal prenex
implicit arguments, as this facilitates their use as arguments to functionals,
because this mimics the way function constants are treated in functional
programming languages with Hindley-Milner type inference. Conversely, lemmas and
theorems should have on-demand implicit arguments, possibly interspersed with
explicit ones, as it's fairly common for other lemmas to have universally
quantified premises; also, this makes it easier to specify such arguments with
the apply: tactic. This policy may be amended for lemmas that are used as
functional arguments, such as reflection or cancellation lemmas. Unfortunately
there is currently no easy way to tell Coq to use different defaults for
definitions and lemmas, so MathComp sticks to the on-demand default, as there
are significantly more lemmas than definition, and use the Prenex Implicits to
redress matters in bulk for definitions. However, this is not completely
systematic, and is sometimes omitted for constants that are not used as
functional arguments in the library, or inside the sections in which the
definition occur, since such commands need to be repeated after the section is
closed. Since Arguments commands should document the intended constant usage as
best as possible, they should follow the implicits policy - even in cases such
as this where the Prenex Implicits had been skipped.
|
|
Documentation of FieldUnitMixin and FieldMixin corrected to reflect
actual arguments, with mulVf and inv0 made explicit arguments for
FieldMixin (they were implicit due to the extended signature of
Field.mixin_of). Type of FieldMixin changed to a convertible variant to
facilitate construction of on-the-fly in-proof construction of
fieldType instances, exposing an idomainType instance.
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
should fix #238
|
|
- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style
|
|
This commit fixes the following issue:
```shell
$ opam pin add coq-mathcomp-ssreflect --dev
[ERROR] "dev-repo" field missing in coq-mathcomp-ssreflect metadata,
you'll need to specify the pinning location
```
This commit also changes http to https for the homepage links.
|
|
|
|
- Cleanup, refactoring and generalize the makefile architecture
- Reuses @strub math-comp/analysis Makefile / Makefile.common organization
- As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
|
|
|
|
|
|
Dear devs, in an attempt to simplify the code of intro patterns we came up with a proposal that:
- simplifies the code of the plugin
- breaks only one line in the entire mathcomp, the one fixed by this patch.
The code we want to simplify is the one deferring clear switches inside an intro pattern.
The implementation is tricky because just delaying the clear switch until the end of the pattern is not enough, for example:
```
move=> {x} /andP[x y].
```
In this case `x` is both cleared and used. In order to be able to use `x`, given that the clear has not been performed yet, we rename `x` into `_x_` (when `{x}` is executed) so that when `x` is later executed we can use the name `x`, and then `.` is executed clear `_x_` instead of `x`.
So systematically "always rename now & clear later" seem to be OK, but it is not. The extra complication is that "rename" may break later intro pattern using terms as views. Eg
```
move=> {x} /andP[Ha Hb] /x.
```
What the code does today is:
- when `{x}` is execute look-ahead in the patter and see if `x` is used as a name to be introduced
- if so, "rename"
- otherwise don't rename (just delay)
This way of doing things is not only complicated but also incomplete, Eg
```
move=> {x} /orP[x | /x].
```
would misbehave, since the look-ahead is not "semantic".
Anyway, the proposed behavior is:
- `{x}` always renames now and clears (the renamed) later
- `{clears}/views` is always "compiled" as `/views{clears}` (most of the occurrences in the library are ok with this simpler rule, but for the one fixed in this PR).
- bonus: support `{}/view` (as in `rewrite {}rule`) to signal that the immediately following `view` has to be cleared, that is `{}/v` compiled as `/v{v}`.
What do you think?
```
```
|
|
|
|
|
|
|
|
|
|
It was emitting a deprecation warning and will soon be removed from Coq.
|
|
|
|
New packager
|
|
|
|
Fixes #139
|
|
|
|
Simple `Definition` should work fine here.
This avoids the problem:
`Error: Library Coq.Program.Tactics has to be required first.`
in math-comp versions that depends on a minimal (or no) Coq stdlib.
Tested on 8.5/8.6
|
|
complex and algC.
The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.
|
|
|
