| 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`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Add new lemmas iterM and iterX in ssrnat
|
|
|
|
|
|
|
|
- Adding contra lemmas between `leq`, `ltn`, `Order.le` ("le"),
`Order.lt` ("lt"), `b` ("T"), `~~ b` ("N"), `b = false` ("F"),
and `~ P` ("not").
- Changelog for contra lemmas with orders
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
|
|
|
|
|
|
|
|
|
|
This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
|
|
|
|
switching long suffixes to short suffixes
|
|
+ `odd_add` -> `oddD`
+ `odd_sub` -> `oddB`
+ `take_addn` -> `takeD`
+ `rot_addn` -> `rotD`
+ `nseq_addn` -> `nseqD`
fixes #359
|
|
Documentation typos
|
|
the->this
Co-Authored-By: Yves Bertot <yves.bertot@inria.fr>
|
|
|
|
|
|
- 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
|
|
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`
|
|
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.
|
|
|
|
|
|
- Generalizing `ltn_subr`
- Adding `ltn_subl` and `ltn_subr`
- Changing conclusion of `ltn_predl` to `0 < n` instead of `n != 0`
|
|
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`.
|
|
|
|
In ssrnat:
- some trivial results in ssrnat `addnKC`, `ltn_predl`, `ltn_predr`, `ltn_subr` and `predn_sub`
- theorems about `n <=/< p +/- m` and `m +/- n <=/< p`
`leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`,
`leq_subCl`, `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and `ltn_subCl`
In div:
- theorems about the euclidean division of additions and subtraction,
+ without preconditions of divisibility:
`edivnD`, `edivnB`, `divnD`, `divnB`, `modnD`, `modnB`
+ with divisibility of one argument:
`divnDMl`, `divnMBl`, `divnBMl`, `divnBl` and `divnBr`
+ specialization of the former theorems for .+1 and .-1:
`edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and `modn_pred`
|
|
|
|
|
|
|
|
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`).
|
|
|
|
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
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.
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
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.
|
|
|
|
Proofs by Cyril Cohen
|
|
|
|
I had put this for compatibility with mathcomp 1.6 when we were still using svn, but I am afraid it got under the radar.
We should decide
- if we revert the change of `ltngtP`,
- if we document (and extend) the compatibility module
- or if we just remove the module and keep the change to `ltngtP`
I am personally in favour of the last
|
|
This was the proof does not depend on the lemma name.
|
|
|
