| Age | Commit message (Collapse) | Author |
|---|
|
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
|
|
- Added helper lemmas about `rem`: `rem_cons` (to control unfolding),
`remE`, `count_rem`, `count_mem_rem`, and `subseq_mem`.
(New lemma `drop_index` briges the gap between `cat_take_drop` and `remE`).
- `subset_maskP`, which was not released yet is generalized with
hypothesis `(forall x, count_mem x s1 <= count_mem x s2)`, instead of
`uniq s1` and `{subset s1 <= s2}`, the previous behaviour can be
restored with helper lemma `leq_uniq_count`
- Its trivial consequence `subset_subseqP` has been added too.
|
|
Deprecation of iota_add delayed, and not the one of iter_add
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
|
|
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
|
|
|
|
|
|
Reorganize, generalize, and add lemmas about `path`, `cycle`, and `sorted`
|
|
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
- Add `allss` and `all_mask` lemmas.
- Since `path`, `cycle`, and `sorted` share similar properties, these lemmas
have been relocated in the same place to improve the visibility. Some missing
lemmas have also been discovered and added.
- Generalize `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType` T
by introducing a predicate `P : {pred T}`.
|
|
|
|
|
|
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
|
|
fixes #469
|
|
+ `odd_add` -> `oddD`
+ `odd_sub` -> `oddB`
+ `take_addn` -> `takeD`
+ `rot_addn` -> `rotD`
+ `nseq_addn` -> `nseqD`
fixes #359
|
|
remove deprecated commands whose deprecation was introduced in 1.9.0
|
|
Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v
|
|
fixes #418
|
|
|
|
|
|
|
|
- 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`.
|
|
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`
|
|
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.
|
|
Add all_filter, all_pmap, and all_allpairsP in seq.v
|
|
|
|
|
|
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`.
|
|
* 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
|
|
|
|
|
|
Also changed eqsVneq.
|
|
|
|
|
|
- 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.
|
|
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`).
|
