| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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`
|
|
Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more
explicitly big ops iterating over explicit enumerations in a `finType`.
The previous practice was to rely on the convertibility between
`enum A` and `filter A (index_enum T)`, sometimes explicitly via the
`filter_index_enum` equality, more often than not implicitly.
Both are likely to fail after the integration of `finmap`, as the
`choiceType` theory can’t guarantee that the order in selected
enumerations is consistent.
For this reason `big_enum` and the related (but currently unused)
`big_image` lemmas are restricted to the abelian case. The `big_enumP`
lemma can be used to handle enumerations in the non-abelian case, as
explained in the `bigop.v` internal documentation.
The Changelog entry enjoins clients to stop relying on either
`filter_index_enum` and convertibility (though this PR still provides
both), and warns about the restriction of the `big_image` lemma set to
the abelian case, as it it a possible source of incompatibility.
|
|
|
|
|
|
|
|
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.
|
|
More arithmetic theorems
|
|
Add all_filter, all_pmap, and all_allpairsP in seq.v
|
|
|
|
|
|
- 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`.
|
|
|
|
More arithmetic theorems
|
|
* Add notation and instances for empty type.
* Update change log.
* Mention void in fintype header.
* Remove unnecessary explicit argument.
* Documentation header for void.
|
|
* Modified the definition of sort to work on any type
* Other Generalizations, fixes and CHANGELOG entry
* Add stability lemmas for `path.sort`
- Inverse the comparison in `merge` and swap arguments of it everywhere.
- Add `sort_rec1` and `sortE` to simplify inductive proofs on `sort`.
- Add `seq.mask_filter`, `mem2E`, `path_mask`, `path_filter`, and `sorted_mask`.
- Generalize `sorted_filter`, `homo_path_in`, `mono_path_in`, `homo_sorted_in`,
and `mono_sorted_in` to non-`eqType`s.
- Add the following lemmas to state the stability of `path.merge` and `path.sort`.
sorted_merge
: forall (T : Type) (leT : rel T),
transitive leT ->
forall s t : seq T, sorted leT (s ++ t) -> merge leT s t = s ++ t
merge_stable_path
: forall (T : Type) (leT leT' : rel T),
total leT ->
forall (x : T) (s1 s2 : seq T),
all (fun y : T => all (leT' y) s2) s1 ->
path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s1 ->
path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x s2 ->
path [rel x0 y | leT x0 y && (leT y x0 ==> leT' x0 y)] x
(merge leT s1 s2)
merge_stable_sorted
: forall (T : Type) (leT leT' : rel T),
total leT ->
forall s1 s2 : seq T,
all (fun x : T => all (leT' x) s2) s1 ->
sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s1 ->
sorted [rel x y | leT x y && (leT y x ==> leT' x y)] s2 ->
sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (merge leT s1 s2)
sorted_sort
: forall (T : Type) (leT : rel T),
transitive leT -> forall s : seq T, sorted leT s -> sort leT s = s
sort_stable
: forall (T : Type) (leT leT' : rel T),
total leT -> transitive leT' ->
forall s : seq T,
sorted leT' s ->
sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s)
filter_sort
: forall (T : Type) (leT : rel T),
total leT -> transitive leT ->
forall (p : pred T) (s : seq T),
[seq x <- sort leT s | p x] = sort leT [seq x <- s | p x]
mask_sort
: forall (T : Type) (leT : rel T),
total leT -> transitive leT ->
forall (s : seq T) (m : bitseq),
{m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}
mask_sort'
: forall (T : Type) (leT : rel T),
total leT -> transitive leT ->
forall (s : seq T) (m : bitseq),
sorted leT (mask m s) ->
{m_s : bitseq | mask m_s (sort leT s) = mask m s}
subseq_sort
: forall (T : eqType) (leT : rel T),
total leT -> transitive leT -> {homo sort leT : t s / subseq t s}
subseq_sort'
: forall (T : eqType) (leT : rel T),
total leT -> transitive leT ->
forall t s : seq T, subseq t s -> sorted leT t -> subseq t (sort leT s)
mem2_sort
: forall (T : eqType) (leT : rel T),
total leT -> transitive leT ->
forall (s : seq T) (x y : T),
leT x y -> mem2 s x y -> mem2 (sort leT s) x y
* Avoid some eta-expansions
* Get the proper fix of `order_path_min` and remove `sort_map_in`
* Update documentation and CHANGELOG entries
|
|
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`
|
|
- Added: `modn_divl` and `divn_modl`.
- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
|
|
|
|
### Added
- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
`card1P`, `fintype_le1P`, `fintype1`, `fintype1P`.
- Bigop theorems: `big_rmcond`, `bigD1_seq`,
`reindex_enum_val_cond`, `reindex_enum_rank_cond`,
`reindex_enum_val`, `reindex_enum_rank`, `big_set`.
|
|
|
|
|
|
|
|
Thanks!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also changed eqsVneq.
|
|
Addressing a suggestion by @CohenCyril
|
|
|
|
|
|
- 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
|
|
|
|
- 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.
|
|
- reprove rather than specialize `Some_inj` to allow for redefinition
of `nonPropType` in `mathcomp.ssreflect.ssreflect`
- retarget finmap CI to coq-9995-compatibility
|
|
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`).
|
|
|
|
|
|
- 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.)
|
|
|
|
Line 426 in `integral.v` diverged to over 40 minutes with the new
`finfun.v`, because matching `mod_Iirr` to `quo_Iirr` goes into
exponential backtracking. This is currently averted by limiting the
repetition of `mod_IirrE` in this `rewrite` line.
Making `finfun` mixing opaque brings this down to 40 seconds, and
locking `cfIirr` to a tractable 0.15 seconds, hopefully improving the
instances. This line also takes 47 seconds to execute in the master
branch, so this is likely an undetected Coq performance regression.
|
