| Age | Commit message (Collapse) | Author |
|---|
|
Cancel lemmas implicit
|
|
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.
|
|
|
|
fix TFAE
|
|
Fix some new warnings emitted by Coq 8.10
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
Adding lemma `eqmxMunitP`
|
|
|
|
|
|
Remove `_ : Type` from packed classes
|
|
|
|
|
|
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.
|
|
Merge Arguments and Prenex Implicits
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
Point out the use of id/idfun to control printing of notation.
(as suggested by @anton-trunov - see #247)
|
|
Document and review the usage of canonical Equality mixins
|
|
Add a section on documenting code
|
|
Remove some unused canonical mixins.
Change simplification behavior of concrete comparison functions to allow for
better simplification using unfolding and sebsequent folding back e.g. with
`rewrite !eqE /= -!eqE`.
A bit of cleanup for `Prenex Implicits` declarations.
Document some explanations by G. Gonthier.
|
|
Based on the discussion here:
https://github.com/math-comp/math-comp/pull/242
|
|
Adding missing documentation for mixin and class constructors for
Equality, Choice, Countable, and Finite.
Renaming Equality mixin constructor comparableClass to the more
consistent comparableMixin.
|
|
|
|
fix issue #240
|
|
|
|
fixing local Makefiles
|
|
should fix #238
|
|
Revert "Adding allsigs, the dependent version of allpairs"
|
|
This reverts commit 044634dcc2f645e3afbdad6cb8dcc66f3eb4a87e.
See issue https://github.com/math-comp/odd-order/pull/5
|
|
fix some bugs in Makefile
|
|
Statement of `bool_irrelevance` more consistent with its name.
|
|
|
|
|
|
Moving countalg and closed_field around
|
|
- 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
|
|
removing multiple definitions of [tT]ag*
|
|
they are already defined in ssrfun
ChangeLog updated
|
|
bump ocaml version in travis
|
|
|
|
[opam]: add dev-repo links
|
|
Adding `allsigs`, the dependent version of `allpairs`
|
|
|
|
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.
|
|
Added the definition of all2.
This definition of all2 has the useful computational behaviour, and all2E unfolds an equivalent one.
|
|
Small scale tool for proving circular implications, and using any pair of statements as an equivalence
|
|
Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
|
|
Fixes the doc of rat
|
|
|
