coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2020-11-19	Removing duplicate clears and turning the warning into an error	Cyril Cohen

2020-10-29	Switch from long suffixes to short suffixes	Kazuhiko Sakaguchi

2019-12-28	Refactoring and linting especially polydiv	Kazuhiko Sakaguchi
	- 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`.
2019-11-22	New generalised induction idiom (#434)	Georges Gonthier
	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.
2019-04-26	Cleaning Require and Require Imports	Cyril Cohen

2018-12-04	Document parameter names whenever possible	Anton Trunov
	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.
2018-11-21	Merge Arguments and Prenex Implicits	Anton Trunov
	See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
2018-03-04	Change deprecated Arguments Scope to Arguments	Jasper Hugunin

2018-02-06	running semi-automated linting on the whole library	Cyril Cohen

2016-11-07	update copyright banner	Assia Mahboubi

2015-07-28	update copyright banner	Enrico Tassi

2015-07-17	Updating files + reorganizing everything	Cyril Cohen

2015-04-09	adapting solvable to 8.5	Cyril Cohen

2015-03-09	Initial commit	Enrico Tassi