| Age | Commit message (Collapse) | Author |
|---|
|
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`).
|
|
|
|
- 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.)
|
|
|
|
|
|
pmap_cat, pmap_perm and perm_map_inj added
|
|
|
|
fix TFAE
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
|
|
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.
|
|
This reverts commit 044634dcc2f645e3afbdad6cb8dcc66f3eb4a87e.
See issue https://github.com/math-comp/odd-order/pull/5
|
|
|
|
Added the definition of all2.
This definition of all2 has the useful computational behaviour, and all2E unfolds an equivalent one.
|
|
Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
|
|
small generalizations and extensions in poly
|
|
|
|
|
|
|
|
Change deprecated Arguments Scope to Arguments
|
|
generalize the default value of nth in nth_iota
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reflection lemmas for `seq.uniq`
|
|
It was emitting a deprecation warning and will soon be removed from Coq.
|
|
|
|
subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2.
|
|
|
|
|
|
|
|
|
