coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
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-13	Adjust implicits of cancellation lemmas	Georges Gonthier
	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.
2018-02-06	running semi-automated linting on the whole library	Cyril Cohen

2017-10-30	Fix obsolete vernacular syntax for locality.	Maxime Dénès
	It was emitting a deprecation warning and will soon be removed from Coq.
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