| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Coq currently fails to resolve Miller patterns against open evars
(issue coq/#9663), in particular it fails to unify `T -> ?R` with
`forall x : T, ?dR x` even when `?dR` does not have `x` in its context.
As a result canonical structures and constructor notations for the
new generalised dependent `finfun`s fail for the non-dependent use
cases, which is an unacceptable regression.
This commit mitigates the problem by specialising the canonical
instances and most of the constructor notation to the non-dependent
case, and introducing an alias of the `finfun_of` type that has
canonical instances for the dependent case, to allow experimentation
with that feature.
With this fix the whole `MathComp` library compiles, with a few
minor changes. The change in `integral_char` fixes a performance issue
that appears to be the consequence of insufficient locking of both
`finfun_eqType` and `cfIirr`; this will be explored in a further commit.
|
|
Clarified that the sample use provided is an example rather than a
misplaced unit test.
Added the definition of generic recursors to the examples, for both
non-dependent and dependent use cases.
|
|
Construct `finfun_of` directly from a bespoke indexed inductive type,
which both makes it structurally positive (and therefore usable as a
container in an `Inductive` definition), and accommodates naturally
dependent functions.
This is still WIP, because this PR exposed a serious shortcoming of
the Coq unification algorithm’s implantation of Miller patterns. This
bug defeats the inference of `Canonical` structures for `{ffun S -> T}`
when the instances are defined in the dependent case!
This causes unmanageable regressions starting in `matrix.v`, so I
have not been able to check for any impact past that. I’m pushing this
commit so that the Coq issue may be addressed.
Made `fun_of_fin` structurally decreasing: Changed the primitive
accessor of `finfun_of` from `tfgraph` to the `Funclass` coercion
`fun_of_fin`. This will make it possible to define recursive functions
on inductive types built using finite functions. While`tfgraph` is
still useful to transport the tuple canonical structures to
`finfun_of`, it is no longer central to the theory so its role has
been reduced.
|
|
Add extra eta lemmas for the under tactic
|
|
|
|
compat sumn with bigop
|
