| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
refactor `seq` permutation theory
|
|
- 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
|
|
remove dependence on Arith lemmas
|
|
|
|
add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names
|
|
- 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.
|
|
Restore CI with `finmap master`
|
|
Following merge of math-comp/finmap#36
|
|
Fix compatibility for #237
|
|
- reprove rather than specialize `Some_inj` to allow for redefinition
of `nonPropType` in `mathcomp.ssreflect.ssreflect`
- retarget finmap CI to coq-9995-compatibility
|
|
Generalise use of `{pred T}` from coq/coq#9995
|
|
Appears to be needed fo v8.7 compatibility, to avert some bug in early
`only printing` implementation whose fix was not back ported.
|
|
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`).
|
|
Cleaning Require and Require Imports
|
|
|
|
remove deprecated use of `if ... return`
|
|
Replace improper use of non-dependent `return` clause in `if` with a
type cast; an upcoming coq-side PR will discontinue support for this,
in order to support dependent return clauses with an implicit `as`
annotation.
|
|
Remove unused `Require`s and a hint directive from interval.v
|
|
|
|
ssrnum doesn't use zmodp theory
|
|
|
|
[ci] Extend the test-suite
|
|
Refactor CI with separate deploy jobs
|
|
- coq-mathcomp-odd-order.dev + coq.dev
- coq-mathcomp-bigenough.dev, coq-{8.7, 8.8, 8.9, dev}
- coq-mathcomp-finmap.dev, coq-{8.7, 8.8, 8.9, dev}
The configs below are commented-out as the upstream repos' opam is not
yet marked as compatible with mathcomp.dev (and Travis CI doesn't test
it with mathcomp-dev images)
# - coq-mathcomp-real-closed.dev, coq-{8.7, 8.8, 8.9, dev}
# - coq-mathcomp-analysis.dev, coq-{8.8, 8.9, dev}
Close math-comp/math-comp#245
|
|
|
|
|
|
so the images:
- mathcomp/mathcomp-dev:coq-8.7
- mathcomp/mathcomp-dev:coq-8.8
- mathcomp/mathcomp-dev:coq-8.9
- mathcomp/mathcomp-dev:coq-dev
will be pushed to Docker Hub even if a third-party library CI fails.
|
|
|
|
* The latter template job is trusted and only runs:
- in branch master,
- if all build *and* test jobs were successful
(major change in the deployment's condition)
* The other jobs are not tagged with "environment: name: deployment",
so they won't be able to read scoped protected variables.
* href: https://gitlab.com/help/ci/variables/README.md#limiting-environment-scopes-of-variables-premium
|
|
|
|
switching to opam 2.0 format
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Least common childen
|
|
Seq refactoring; adding `permutations`, extending `allpairs`
|
|
Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an
intermediate file for `hierarchy_test.py`. So the typical usage is:
$ python3.5 etc/utils/hierarchy_test.py \
<(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \
> mathcomp/test_suite/hierarchy_test.v
|
|
- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet
in #299 (except the link to the coq lib `Permutation` predicate).
Use insertions to construct permutations. This definition is closer
to the one proposed by @MrSet, than one using rotations (it adds one
line to the definition of `permutations` but the proofs become a
little simpler.)
- Added support for casts on `map` comprehension general terms.
- Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with
equational proofs; changed `allpairs_comp` to its converse
`map_allpairs` for consistency.
- Add three `allpairs` extensionality lemmas: for the non-localised,
dependent localised and non-dependent localised cases; as per
`eq_in_map`, the latter two are equivalences.
- Documented the `all2` predicate added in #224, and the view
combinators added in #202.
- Renamed `seq2_ind` to `seq_ind2`, and weakened the induction
hypothesis, adding a `size` equality assumption.
- Corrected the header to use `<=>` for `bool` predicate
documentation, and `<->` for `Prop` predicates, following the
library’s general convention.
- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
directive, making it possible to merge the `Rev` section into the
main `Sequences` section.
- Miscellaneous improvements to proof scripts and file organisation.
- Correct maximal implicits of `constant`.
- Fixes omitted `Prenex Implicit` declaration.
- Other implicits fixes.
- Fix apparent `done` regression It appears `done` now does a weaker
form of intros, and this broke the `dtuple_onP` proof. Updated the
proof to eliminate the issue.
(Commit log edited by @CohenCyril during the squash.)
|
|
|
|
|
|
|
|
|
|
remove support for Coq 8.6
|
|
|
|
rename test-suite -> test_suite to make coq happy
|
