| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- Generalizing `ltn_subr`
- Adding `ltn_subl` and `ltn_subr`
- Changing conclusion of `ltn_predl` to `0 < n` instead of `n != 0`
|
|
More lemmas on seqs
|
|
|
|
* missing exports of lemmas `commrB`, `commr_sum` and `commr_prod`
* missing `regular_*` canonical exports
|
|
|
|
typo
|
|
|
|
|
|
* Lemmas on commutation with big sum and prod
* Added commrB Lemma
* @CohenCyril review
* apply -> apply:
|
|
|
|
|
|
|
|
|
|
Update README.md
|
|
add existsPn/forallPn lemmas
|
|
Commutative Algebras
|
|
|
|
|
|
|
|
|
|
|
|
Initial properties of polynomials in R-algebras
|
|
Reorder the arguments in `compare_nat` and `ltngtP`
|
|
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`.
|
|
Add an explicit type annotation to GRing.scale
|
|
`V` was wrongly eta-expanded before:
GRing.scale
: forall (R : ringType) (V : lmodType R),
R -> GRing.Zmodule.Pack (GRing.Lmodule.class V) ->
GRing.Zmodule.Pack (GRing.Lmodule.class V)
|
|
Removing duplicate lemma `addnKC` (= `addKn`)
|
|
|
|
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`.
|
|
Redirects to math-comp.github.io
|
|
* feat: Add build for mathcomp/mathcomp-dev:coq-8.10
* fix(coq-mathcomp-ssreflect.opam): Bump coq upper bound
* fix(*.opam): Remove "remove" directive
href: coq/opam-coq-archive#703
|
|
Improving fintype and bigop
|
|
|
|
|
|
### 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`.
|
|
|
|
typo in ssralg
|
|
|
|
Fix and improve the test suite and Makefile
|
|
Add `flatten_map1` and `allpairs_consr`
|
|
|
|
- improve an error message produced by the `check_join` tactic,
- fix the build of the test suite: `make test-suite`, and
- add a new rule `only` to build a subset of MathComp.
|
|
Generalize `allpairs_catr` to non-`eqType`s
|
|
|
|
|
