# Changelog All notable changes to this project will be documented in this file. Last releases: [[1.12.0] - 2020-11-26](#1120---2020-11-26), [[1.11.0] - 2020-06-09](#1110---2020-06-09), and [[1.10.0] - 2019-11-29](#1100---2019-11-29). The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ## [1.12.0] - 2020-11-26 This release is compatible with Coq versions 8.10, 8.11, and 8.12. ### Added - Contraposition lemmas involving propositions: + in `ssrbool.v`: `contra_not`, `contraPnot`, `contraTnot`, `contraNnot`, `contraPT`, `contra_notT`, `contra_notN`, `contraPN`, `contraFnot`, `contraPF` and `contra_notF`. + in `eqtype.v`: `contraPeq`, `contra_not_eq`, `contraPneq`, and `contra_neq_not`, `contra_not_neq`, `contra_eq_not`. - Contraposition lemmas involving inequalities: + in `ssrnat.v`: `contraTleq`, `contraTltn`, `contraNleq`, `contraNltn`, `contraFleq`, `contraFltn`, `contra_leqT`, `contra_ltnT`, `contra_leqN`, `contra_ltnN`, `contra_leqF`, `contra_ltnF`, `contra_leq`, `contra_ltn`, `contra_leq_ltn`, `contra_ltn_leq`, `contraPleq`, `contraPltn`, `contra_not_leq`, `contra_not_ltn`, `contra_leq_not`, `contra_ltn_not` + in `order.v`: `comparable_contraTle`, `comparable_contraTlt`, `comparable_contraNle`, `comparable_contraNlt`, `comparable_contraFle`, `comparable_contraFlt`, `contra_leT`, `contra_ltT`, `contra_leN`, `contra_ltN`, `contra_leF`, `contra_ltF`, `comparable_contra_leq_le`, `comparable_contra_leq_lt`, `comparable_contra_ltn_le`, `comparable_contra_ltn_lt`, `contra_le_leq`, `contra_le_ltn`, `contra_lt_leq`, `contra_lt_ltn`, `comparable_contra_le`, `comparable_contra_le_lt`, `comparable_contra_lt_le`, `comparable_contra_lt`, `contraTle`, `contraTlt`, `contraNle`, `contraNlt`, `contraFle`, `contraFlt`, `contra_leq_le`, `contra_leq_lt`, `contra_ltn_le`, `contra_ltn_lt`, `contra_le`, `contra_le_lt`, `contra_lt_le`, `contra_lt`, `contra_le_not`, `contra_lt_not`, `comparable_contraPle`, `comparable_contraPlt`, `comparable_contra_not_le`, `comparable_contra_not_lt`, `contraPle`, `contraPlt`, `contra_not_le`, `contra_not_lt` - in `ssreflect.v`, added intro pattern ltac views for dup, swap, apply: `/[apply]`, `/[swap]` and `/[dup]`. - in `ssrbool.v` (waiting to be integrated in Coq) + generic lemmas about interaction between `{in _, _}` and `{on _, _}`: `in_on1P`, `in_on1lP`, `in_on2P`, `on1W_in`, `on1lW_in`, `on2W_in`, `in_on1W`, `in_on1lW`, `in_on2W`, `on1S`, `on1lS`, `on2S`, `on1S_in`, `on1lS_in`, `on2S_in`, `in_on1S`, `in_on1lS`, `in_on2S`. + lemmas about interaction between `{in _, _}` and `sig`: `in1_sig`, `in2_sig`, and `in3_sig`. - in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl`, `oddS`, `subnA`, `addnBn`, `addnCAC`, `addnACl`, `iterM`, `iterX` - in `seq.v`, + new lemmas `take_uniq`, `drop_uniq` + new lemma `mkseqP` to abstract a sequence `s` with `mkseq f n`, where `f` and `n` are fresh variables. + new high-order relation `allrel r xs ys` which asserts that `r x y` holds whenever `x` is in `xs` and `y` is in `ys`, new notation `all2rel r xs (:= allrel r xs xs)` which asserts that `r` holds on all pairs of elements of `xs`, and * lemmas `allrel0(l|r)`, `allrel_cons(l|r|2)`, `allrel1(l|r)`, `allrel_cat(l|r)`, `allrel_allpairsE`, `eq_in_allrel`, `eq_allrel`, `allrelC`, `allrel_map(l|r)`, `allrelP`, * new lemmas `all2rel1`, `all2rel2`, and `all2rel_cons` under assumptions of symmetry of `r`. + new lemmas `allss`, `all_mask`, and `all_sigP`. `allss` has also been declared as a hint. + new lemmas `index_pivot`, `take_pivot`, `rev_pivot`, `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr` `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons`, `rev_mask`, `subseq_rev`, `subseq_cat2l`, `subseq_cat2r`, `subseq_rot`, and `uniq_subseq_pivot`. + new lemmas `find_ltn`, `has_take`, `has_take_leq`, `index_ltn`, `in_take`, `in_take_leq`, `split_find_nth`, `split_find` and `nth_rcons_cat_find`. + added `drop_index`, `in_mask`, `mask0s`, `cons_subseq`, `undup_subseq`, `leq_count_mask`, `leq_count_subseq`, `count_maskP`, `count_subseqP`, `count_rem`, `count_mem_rem`, `rem_cons`, `remE`, `subseq_rem`, `leq_uniq_countP`, and `leq_uniq_count`. + new definition `rot_add` and new lemmas `rot_minn`, `leq_rot_add`, `rot_addC`, `rot_rot_add`. + new lemmas `perm_catACA`, `allpairs0l`, `allpairs0r`, `allpairs1l`, `allpairs1r`, `allpairs_cons`, `eq_allpairsr`, `allpairs_rcons`, `perm_allpairs_catr`, `perm_allpairs_consr`, `mem_allpairs_rconsr`, and `allpairs_rconsr` (with the alias `perm_allpairs_rconsr` for the sake of uniformity, but which is already deprecated in favor of `allpairs_rconsr`, cf renamed section). - in `path.v`, + new lemmas `sub_cycle(_in)`, `eq_cycle_in`, `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`, `(homo|mono)_cycle(_in)`. + new lemma `sort_iota_stable`. + new lemmas `order_path_min_in`, `path_sorted_inE`, `sorted_(leq|ltn)_nth_in`, `subseq_path_in`, `subseq_sorted_in`, `sorted_(leq|ltn)_index_in`, `sorted_uniq_in`, `sorted_eq_in`, `irr_sorted_eq_in`, `sort_sorted_in`, `sorted_sort_in`, `perm_sort_inP`, `all_sort`, `sort_stable_in`, `filter_sort_in`, `(sorted_)mask_sort_in`, `(sorted_)subseq_sort_in`, and `mem2_sort_in`. + added `size_merge_sort_push`, which documents an invariant of `merge_sort_push`. - in `fintype.v`, + new lemmas `card_geqP`, `card_gt1P`, `card_gt2P`, `card_le1_eqP` (generalizes `fintype_le1P`), + adds lemma `split_ordP`, a variant of `splitP` which introduces ordinal equalities between the index and `lshift`/`rshift`, rather than equalities in `nat`, which in some proofs makes the reasoning easier (cf `matrix.v`), especially together with the new lemma `eq_shift` (which is a multi-rule for new lemmas `eq_lshift`, `eq_rshift`, `eq_lrshift` and `eq_rlshift`). + new lemmas `eq_liftF` and `lift_eqF`. + new lemmas `disjointFr`, `disjointFl`, `disjointWr`, `disjointW` + new (pigeonhole) lemmas `leq_card_in`, `leq_card`, + added `mask_enum_ord`. - in `finset.v` + new lemmas `set_enum`, `cards_eqP`, `cards2P` + new lemmas `properC`, `properCr`, `properCl` + new lemmas `mem_imset_eq`, `mem_imset2_eq`. These lemmas will lose the `_eq` suffix in the next release, when the shortende names will become available (cf. Renamed section) + new lemma `disjoints1` - in `order.v` + new lemmas `comparable_bigl` and `comparable_bigr`. + added a factory `distrLatticePOrderMixin` to build a `distrLatticeType` from a `porderType`. + new notations `0^d` and `1^d` for bottom and top elements of dual lattices. + new definition `lteif` and notations ` v = 0` for all `v`. + new notation `stablemx V f` asserting that `f` stabilizes `V`, with new theorems: `eigenvectorP`, `eqmx_stable`, `stablemx_row_base`, `stablemx_full`, `stablemxM`, `stablemxD`, `stablemxN`, `stablemxC`, `stablemx0`, `stableDmx`, `stableNmx`, `stable0mx`, `stableCmx`, `stablemx_sums`, and `stablemx_unit`. + added `comm_mx_stable`, `comm_mx_stable_ker`, and `comm_mx_stable_eigenspace`. + new definitions `maxrankfun`, `fullrankfun` which are "subset function" to be plugged in `rowsub`, with lemmas: `maxrowsub_free`, `eq_maxrowsub`, `maxrankfun_inj`, `maxrowsub_full`, `fullrowsub_full`, `fullrowsub_unit`, `fullrowsub_free`, `mxrank_fullrowsub`, `eq_fullrowsub`, and `fullrankfun_inj`. - in `mxpoly.v`, + new lemmas `mxminpoly_minP` and `dvd_mxminpoly`. + new lemmas `horner_mx_diag` and `char_poly_trig`, `root_mxminpoly`, and `mxminpoly_diag` + new definitions `kermxpoly g p` (the kernel of polynomial $p(g)$). * new elementary theorems: `kermxpolyC`, `kermxpoly1`, `kermxpolyX`, `kermxpoly_min` * kernel lemmas: `mxdirect_kermxpoly`, `kermxpolyM`, `kermxpoly_prod`, and `mxdirect_sum_kermx` * correspondance between `eigenspace` and `kermxpoly`: `eigenspace_poly` + generalized eigenspace `geigenspace` and a generalization of eigenvalues called `eigenpoly g` (i.e. polynomials such that `kermxpoly g p` is nonzero, e.g. eigen polynomials of degree 1 are of the form `'X - a%:P` where `a` are eigenvalues), and * correspondance with `kermx`: `geigenspaceE`, * application of kernel lemmas `mxdirect_sum_geigenspace`, * new lemmas: `eigenpolyP`, `eigenvalue_poly`, `eigenspace_sub_geigen`, + new `map_mx` lemmas: `map_kermxpoly`, `map_geigenspace`, `eigenpoly_map`. + new lemma `horner_mx_stable`. + added `comm_mx_horner`, `comm_horner_mx`, `comm_horner_mx2`, `horner_mx_stable`, `comm_mx_stable_kermxpoly`, and `comm_mx_stable_geigenspace`. - in `ssrnum.v`, + new lemma `ler_sum_nat` + new lemmas `big_real`, `sum_real`, `prod_real`, `max_real`, `min_real`, `bigmax_real`, and `bigmin_real`. + new lemma `real_lteif_distl`. - in `interval.v`, + intervals and their bounds of `T` now have canonical ordered type instances whose ordering relations are the subset relation and the left to right ordering respectively. They form partially ordered types if `T` is a `porderType`. If `T` is a `latticeType`, they also form `tbLatticeType` where the join and meet are intersection and convex hull respectively. If `T` is an `orderType`, they are distributive, and the interval bounds are totally ordered. (cf Changed section) + new lemmas `bound_ltxx`, `subitvE`, `in_itv`, `itv_ge`, `in_itvI`, `itv_total_meet3E`, and `itv_total_join3E`. ### Changed - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 - in `seq.v`, `mask` will only expand if both arguments are constructors, the case `mask [::] s` can be dealt with using `mask0s` or explicit conversion. - in `path.v`, + generalized lemmas `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType`s. + generalized lemmas `sorted_ltn_nth` and `sorted_leq_nth` (formerly `sorted_lt_nth` and `sorted_le_nth`, cf Renamed section) for non-`eqType`s. - in `fintype.v`, + added lemma `ord1`, it is the same as `zmodp.ord1`, except `fintype.ord1` does not rely on `'I_n` zmodType structure. + rename `disjoint_trans` to `disjointWl` + lemmas `inj_card_onto` and `inj_card_bij` take a weaker hypothesis (i.e. `#|T| >= #|T'|` instead of `#|T| = #|T'|` thanks to `leq_card` under injectivity assumption). - in `finset.v`, fixed printing of notation `[set E | x in A , y in B & P ]` - in `bigop.v`, lemma `big_rmcond` is deprecated and has been renamed `big_rmcomd_in` (and aliased `big_uncond_in`, see Added). The variant which does not require an `eqType` is currently named `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the next release. - in `ssrAC.v`, fix `non-reversible-notation` warnings - in `order.v`, + in the definition of structures, displays are removed from parameters of mixins and fields of classes internally and now only appear in parameters of structures. Consequently, each mixin is now parameterized by a class rather than a structure, and the corresponding factory parameterized by a structure is provided to replace the use of the mixin. These factories have the same names as in the mixins before this change except that `bLatticeMixin` and `tbLatticeMixin` have been renamed to `bottomMixin` and `topMixin` respectively. + the `dual_*` notations such as `dual_le` are now qualified with the `Order` module. + `\join^d_` and `\meet^d_` notations are now properly specialized for `dual_display`. + rephrased `comparable_(min|max)[rl]` in terms of `{in _, forall x y, _}`, hence reordering the arguments. Made them hints for smoother combination with `comparable_big[lr]`. + `>=< y` now stands for `[pred x | x >=< y]` + `>< y` now stands for `[pred x | x >< y]` + and the same holds for the dual `>=<^d`, `><^d`, the product `>=<^p`, `><^p`, and lexicographic `>=<^l`, `><^l`. The previous meanings can be obtained through `>=<%O x` and `><%O x`. + generalized `sort_le_id` for any `porderType`. + the names of lemmas `join_idPl` and `join_idPr` are transposed to follow the naming convention. - In `ssrnum.v`, + `>=< y` now stands for `[pred x | x >=< y]` + fixed notations `@minr` and `@maxr` to point `Order.min` and `Order.max` respectively. - in `ssrint.v`, generalized `mulpz` for any `ringType`. - in `interval.v`: + `x <= y ?< if c` (`lersif`) has been generalized to `porderType`, relocated to `order.v`, and replaced with `x < y ?<= if c'` (`lteif`) where `c'` is negation of `c`. + Many definitions and lemmas on intervals such as the membership test are generalized from numeric domains to ordered types. + Interval bounds `itv_bound : Type -> Type` are redefined with two constructors `BSide : bool -> T -> itv_bound T` and `BInfty : bool -> itv_bound T`. New notations `BLeft` and `BRight` are aliases for `BSide true` and `BSide false` respectively. `BInfty false` and `BInfty true` respectively means positive and negative infinity. `BLeft x` and `BRight x` respectively mean close and open bounds as left bounds, and they respectively mean open and close bounds as right bounds. This change gives us the canonical "left to right" ordering of interval bounds. + Lemmas `mid_in_itv(|oo|cc)` have been generalized from `realFieldType` to `numFieldType`. - In `matrix.v`, generalized `diag_mx_comm` and `scalar_mx_comm` to all `n`, instead of `n'.+1`, thanks to `commmmx`. ### Renamed - in `ssrnat.v` + `iter_add` -> `iterD` + `maxn_mul(l|r)` -> `maxnM(l|r)` + `minn_mul(l|r)` -> `minnM(l|r)` + `odd_(opp|mul|exp)` -> `odd(N|M|X)` + `sqrn_sub` -> `sqrnB` - in `div.v` + `coprime_mul(l|r)` -> `coprimeM(l|r)` + `coprime_exp(l|r)` -> `coprimeX(l|r)` - in `prime.v` + `primes_(mul|exp)` -> `primes(M|X)` + `pnat_(mul|exp)` -> `pnat(M|X)` - in `seq.v`, + `iota_add(|l)` -> `iotaD(|l)` + `allpairs_(cons|cat)r` -> `mem_allpairs_(cons|cat)r` (`allpairs_consr` and `allpairs_catr` are now deprecated alias, and will be attributed to the new `perm_allpairs_catr`). - in `path.v`, + `eq_sorted(_irr)` -> `(irr_)sorted_eq` + `sorted_(lt|le)_nth` -> `sorted_(ltn|leq)_nth` + `(ltn|leq)_index` -> `sorted_(ltn|leq)_index` + `subseq_order_path` -> `subseq_path` - in `fintype.v` + `bump_addl` -> `bumpDl` + `unbump_addl` -> `unbumpDl` - in `finset.v`, + `mem_imset` -> `imset_f` (with deprecation alias, cf. Added section) + `mem_imset2` -> `imset2_f` (with deprecation alias, cf. Added section) - in `bigop.v` + `big_rmcond` -> `big_rmcond_in` (cf Changed section) + `mulm_add(l|r)` -> `mulmD(l|r)` - in `order.v`, `eq_sorted_(le|lt)` -> `(le|lt)_sorted_eq` - in `interval.v`, we deprecate, rename, and relocate to `order.v` the following: + `lersif_(trans|anti)` -> `lteif_(trans|anti)` + `lersif(xx|NF|S|T|F|W)` -> `lteif(xx|NF|S|T|F|W)` + `lersif_(andb|orb|imply)` -> `lteif_(andb|orb|imply)` + `ltrW_lersif` -> `ltrW_lteif` + `lersifN` -> `lteifNE` + `lersif_(min|max)(l|r)` -> ` lteif_(min|max)(l|r)` - in `interval.v`, we deprecate, rename, and relocate to `ssrnum.v` the following: + `subr_lersif(r0|0r|0)` -> `subr_lteif(r0|0r|0)` + `lersif01` -> `lteif01` + `lersif_(oppl|oppr|0oppr|oppr0|opp2|oppE)` -> `lteif_(oppl|oppr|0oppr|oppr0|opp2|oppE)` + `lersif_add2(|l|r)` -> `lteif_add2(|l|r)` + `lersif_sub(l|r)_add(l|r)` -> `lteif_sub(l|r)_add(l|r)` + `lersif_sub_add(l|r)` -> `lteif_sub_add(l|r)` + `lersif_(p|n)mul2(l|r)` -> `lteif_(p|n)mul2(l|r)` + `real_lersifN` -> `real_lteifNE` + `real_lersif_norm(l|r)` -> `real_lteif_norm(l|r)` + `lersif_nnormr` -> `lteif_nnormr` + `lersif_norm(l|r)` -> `lteif_norm(l|r)` + `lersif_distl` -> `lteif_distl` + `lersif_(p|n)div(l|r)_mul(l|r)` -> `lteif_(p|n)div(l|r)_mul(l|r)` - in `interval.v`, we deprecate and replace the following: + `lersif_in_itv` -> `lteif_in_itv` + `itv_gte` -> `itv_ge` + `l(t|e)r_in_itv` -> `lt_in_itv` - in `ssralg.v`, `prodrMn`-> `prodrMn_const` (with deprecation alias, cf. Added section) - in `ssrint.v`, `polyC_mulrz` -> `polyCMz` - in `poly.v` + `polyC_(add|opp|sub|muln|mul|inv)` -> `polyC(D|N|B|Mn|M|V)` + `lead_coef_opp` -> `lead_coefN` + `derivn_sub` -> `derivnB` - in `polydiv.v` + `rdivp_add(l|r)` -> `rdivpD(l|r)` + `rmodp_add` -> `rmodpD` + `dvdp_scale(l|r)` -> `dvdpZ(l|r)` + `dvdp_opp` -> `dvdpNl` + `coprimep_scale(l|r)` -> `coprimepZ(l|r)` + `coprimep_mul(l|r)` -> `coprimepM(l|r)` + `modp_scale(l|r)` -> `modpZ(l|r)` + `modp_(opp|add|scalel|scaler)` -> `modp(N|D|Zl|Zr)` + `divp_(opp|add|scalel|scaler)` -> `divp(N|D|Zl|Zr)` - in `matrix.v`, `map_mx_sub` -> `map_mxB` - in `mxalgebra.v`, `mulsmx_add(l|r)` -> `mulsmxD(l|r)` - in `vector.v`, `limg_add` -> `limgD` - in `intdiv.v` + `coprimez_mul(l|r)` -> `coprimezM(l|r)` + `coprimez_exp(l|r)` -> `coprimezX(l|r)` ### Removed - in `ssrnat.v`, we remove the compatibility module `mc_1_9`. - in `interval.v`, we remove the following: + `le_bound(l|r)` (use `Order.le` instead) + `le_bound(l|r)_refl` (use `lexx` instead) + `le_bound(l|r)_anti` (use `eq_le` instead) + `le_bound(l|r)_trans` (use `le_trans` instead) + `le_bound(l|r)_bb` (use `bound_lexx` instead) + `le_bound(l|r)_total` (use `le_total` instead) - in `interval.v`, we deprecate the following: + `itv_intersection` (use `Order.meet` instead) + `itv_intersection1i` (use `meet1x` instead) + `itv_intersectioni1` (use `meetx1` instead) + `itv_intersectionii` (use `meetxx` instead) + `itv_intersectionC` (use `meetC` instead) + `itv_intersectionA` (use `meetA` instead) - in `mxpoly.v`, we deprecate `scalar_mx_comm`, and advise to use `comm_mxC` instead (with maximal implicit arguments `R` and `n`). ### Infrastructure - in all the hierarchies (in `eqtype.v`, `choice.v`, `order.v`, `ssralg.v`,...), the `class_of` records of structures are turned into primitive records to prevent prevent potential issues of ambiguous paths and convertibility of structure instances. - across the library, the following constants have been tuned to only reduce when they do not expose a match: `subn_rec`, `decode_rec`, `nth` (thus avoiding a notorious problem of ``p`_0`` expanding too eagerly), `set_nth`, `take`, `drop`, `eqseq`, `incr_nth`, `elogn2`, `binomial_rec`, `sumpT`. ## [1.11.0] - 2020-06-09 This release is compatible with Coq versions 8.7, 8.8, 8.9, 8.10, and 8.11. - Added lemmas about monotony of functions `nat -> T` where `T` is an ordered type: `homo_ltn_lt_in`, `incn_inP`, `nondecn_inP`, `nhomo_ltn_lt_in`, `decn_inP`, `nonincn_inP`, `homo_ltn_lt`, `incnP`, `nondecnP`, `nhomo_ltn_lt`, `decnP`, `nonincnP` in file `order.v`. - Added lemmas for swaping arguments of homomorphisms and monomorphisms: `homo_sym`, `mono_sym`, `homo_sym_in`, `mono_sym_in`, `homo_sym_in11`, `mono_sym_in11` in `ssrbool.v` ### Added - in `ssrnum.v`, new lemmas: + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW` + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`, `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl` - in `order.v`, defining `min` and `max` independently from `meet` and `join`, and providing a theory about for min and max, hence generalizing the theory of `Num.min` and `Num.max` from versions <= `1.10`, instead of specializing to total order as in `1.11+beta1`: ``` Definition min (T : porderType) (x y : T) := if x < y then x else y. Definition max (T : porderType) (x y : T) := if x < y then y else x. ``` + Lemmas: `min_l`, `min_r`, `max_l`, `max_r`, `minxx`, `maxxx`, `eq_minl`, `eq_maxr`, `min_idPl`, `max_idPr`, `min_minxK`, `min_minKx`, `max_maxxK`, `max_maxKx`, `comparable_minl`, `comparable_minr`, `comparable_maxl`, and `comparable_maxr` + Lemmas about interaction with lattice operations: `meetEtotal`, `joinEtotal`, + Lemmas under condition of pairwise comparability of a (sub)set of their arguments: `comparable_minC`, `comparable_maxC`, `comparable_eq_minr`, `comparable_eq_maxl`, `comparable_le_minr`, `comparable_le_minl`, `comparable_min_idPr`, `comparable_max_idPl`, `comparableP`, `comparable_lt_minr`, `comparable_lt_minl`, `comparable_le_maxr`, `comparable_le_maxl`, `comparable_lt_maxr`, `comparable_lt_maxl`, `comparable_minxK`, `comparable_minKx`, `comparable_maxxK`, `comparable_maxKx`, `comparable_minA`, `comparable_maxA`, `comparable_max_minl`, `comparable_min_maxl`, `comparable_minAC`, `comparable_maxAC`, `comparable_minCA`, `comparable_maxCA`, `comparable_minACA`, `comparable_maxACA`, `comparable_max_minr`, `comparable_min_maxr` + and the same but in a total order: `minC`, `maxC`, `minA`, `maxA`, `minAC`, `maxAC`, `minCA`, `maxCA`, `minACA`, `maxACA`, `eq_minr`, `eq_maxl`, `min_idPr`, `max_idPl`, `le_minr`, `le_minl`, `lt_minr`, `lt_minl`, `le_maxr`,`le_maxl`, `lt_maxr`, `lt_maxl`, `minxK`, `minKx`, `maxxK`, `maxKx`, `max_minl`, `min_maxl`, `max_minr`, `min_maxr` - in `ssrnum.v`, theory about `min` and `max` extended to `numDomainType`: + Lemmas: `real_oppr_max`, `real_oppr_min`, `real_addr_minl`, `real_addr_minr`, `real_addr_maxl`, `real_addr_maxr`, `minr_pmulr`, `maxr_pmulr`, `real_maxr_nmulr`, `real_minr_nmulr`, `minr_pmull`, `maxr_pmull`, `real_minr_nmull`, `real_maxr_nmull`, `real_maxrN`, `real_maxNr`, `real_minrN`, `real_minNr` - the compatibility module `ssrnum.mc_1_10` was extended to support definitional compatibility with `min` and `max` which had been lost in `1.11+beta1` for most instances. - in `fintype.v`, new lemmas: `seq_sub_default`, `seq_subE` - in `order.v`, new "unfolding" lemmas: `minEnat` and `maxEnat` - in `ssrbool.v` + lemmas about the `cancel` predicate and `{in _, _}`/`{on _, _}` notations: * `onW_can`, `onW_can_in`, `in_onW_can`, `onS_can`, `onS_can_in`, `in_onS_can` + lemmas about the `cancel` predicate and injective functions: * `inj_can_sym_in_on`, `inj_can_sym_on`, `inj_can_sym_in` ### Changed - in `order.v`, `le_xor_gt`, `lt_xor_ge`, `compare`, `incompare`, `lel_xor_gt`, `ltl_xor_ge`, `comparel`, `incomparel` have more parameters, so that the the following now deal with `min` and `max` + `comparable_ltgtP`, `comparable_leP`, `comparable_ltP`, `comparableP` + `lcomparableP`, `lcomparable_ltgtP`, `lcomparable_leP`, `lcomparable_ltP`, `ltgtP` - in `order.v`: + `[arg min_(i < i0 | P) M]` now for `porderType` (was for `orderType`) + `[arg max_(i < i0 | P) M]` now for `porderType` (was for `orderType`) + added `comparable_arg_minP`, `comparable_arg_maxP`, `real_arg_minP`, `real_arg_maxP`, in order to take advantage of the former generalizations. - in `ssrnum.v`, `maxr` is a notation for `(@Order.max ring_display _)` (was `Order.join`) (resp. `minr` is a notation for `(@Order.min ring_display _)`) - in `ssrnum.v`, `ler_xor_gt`, `ltr_xor_ge`, `comparer`, `ger0_xor_lt0`, `ler0_xor_gt0`, `comparer0` have now more parameters, so that the following now deal with min and max: + `real_leP`, `real_ltP x y`, `real_ltgtP`, `real_ge0P`, `real_le0P`, `real_ltgt0P` + `lerP`, `ltrP`, `ltrgtP`, `ger0P`, `ler0P`, `ltrgt0P` - in `ssrnum.v`, the following have been restated (which were formerly derived from `order.v` and stated with specializations of the `meet` and `join` operators): + `minrC`, `minrr`, `minr_l`, `minr_r`, `maxrC`, `maxrr`, `maxr_l`, `maxr_r`, `minrA`, `minrCA`, `minrAC`, `maxrA`, `maxrCA`, `maxrAC` + `eqr_minl`, `eqr_minr`, `eqr_maxl`, `eqr_maxr`, `ler_minr`, `ler_minl`, `ler_maxr`, `ler_maxl`, `ltr_minr`, `ltr_minl`, `ltr_maxr`, `ltr_maxl` + `minrK`, `minKr`, `maxr_minl`, `maxr_minr`, `minr_maxl`, `minr_maxr` - The new definitions of `min` and `max` may require the following rewrite rules changes when dealing with `max` and `min` instead of `meet` and `join`: + `ltexI` -> `(le_minr,lt_minr)` + `lteIx` -> `(le_minl,lt_minl)` + `ltexU` -> `(le_maxr,lt_maxr)` + `lteUx` -> `(le_maxl,lt_maxl)` + `lexU` -> `le_maxr` + `ltxU` -> `lt_maxr` + `lexU` -> `le_maxr` - in `ssrbool.v` + lemmas about monotone functions and the `{in _, _}` notation: * `homoRL_in`, `homoLR_in`, `homo_mono_in`, `monoLR_in`, `monoRL_in`, `can_mono_in` ### Renamed - in `fintype` we deprecate and rename the following: + `arg_minP` -> `arg_minnP` + `arg_maxP` -> `arg_maxnP` - in `order.v`, in module `NatOrder`, renamings: + `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat`, `meetEnat` -> `minEnat`, `joinEnat` -> `maxEnat` ### Removed - in `order.v`, removed `total_display` (was used to provide the notation `max` for `join` and `min` for `meet`). - in `order.v`, removed `minnE` and `maxnE` - in `order.v`, + removed `meetEnat` (in favor of `meetEtotal` followed by `minEnat`) + removed `joinEnat` (in favor of `joinEtotal` followed by `maxEnat`) ## [1.11+beta1] - 2020-04-15 This release is compatible with Coq versions 8.7, 8.8, 8.9 and 8.10. ### Added - Arithmetic theorems in ssrnat, div and prime about `logn`, `coprime`, `gcd`, `lcm` and `partn`: `logn_coprime`, `logn_gcd`, `logn_lcm`, `eq_partn_from_log` and `eqn_from_log`. - Lemmas `ltnNleqif`, `eq_leqif`, `eqTleqif` in `ssrnat` - Lemmas `eqEtupe`, `tnthS` and `tnth_nseq` in `tuple` - Ported `order.v` from the finmap library, which provides structures of ordered sets (`porderType`, `latticeType`, `distrLatticeType`, `orderType`, etc.) and its theory. - Lemmas `path_map`, `eq_path_in`, `sub_path_in`, `path_sortedE`, `sub_sorted` and `sub_sorted_in` in `path` (and refactored related proofs) - Added lemmas `hasNfind`, `memNindex` and `findP` in `seq` - Added lemmas `foldr_rcons`, `foldl_rcons`, `scanl_rcons` and `nth_cons_scanl` in `seq` - ssrAC tactics, see header of `ssreflect/ssrAC.v` for documentation of `(AC patternshape reordering)`, `(ACl reordering)` `(ACof reordering reordering)`, `op.[AC patternshape reordering]`, `op.[ACl reordering]` and `op.[ACof reordering reordering]`. - Added definition `cast_perm` with a group morphism canonical structure, and lemmas `permX_fix`, `imset_perm1`, `permS0`, `permS1`, `cast_perm_id`, `cast_ord_permE`, `cast_permE`, `cast_perm_comp`, `cast_permK`, `cast_permKV`, `cast_perm_inj`, `cast_perm_sym`,`cast_perm_morphM`, and `isom_cast_perm` in `perm` and `restr_perm_commute` in `action`. - Added `card_porbit_neq0`, `porbitP`, and `porbitPmin` in `perm` - Added definition `Sym` with a group set canonical structure and lemmas `card_Sn` and `card_Sym` in `perm` and `SymE` in `action` ### Changed - Reorganized the algebraic hierarchy and the theory of `ssrnum.v`. + `numDomainType` and `realDomainType` get inheritances respectively from `porderType` and `orderType`. + `normedZmodType` is a new structure for `numDomainType` indexed normed additive abelian groups. + `[arg minr_( i < n | P ) F]` and `[arg maxr_( i < n | P ) F]` notations are removed. Now `[arg min_( i < n | P ) F]` and `[arg max_( i < n | P ) F]` notations are defined in `nat_scope` (specialized for `nat`), `order_scope` (general one), and `ring_scope` (specialized for `ring_display`). Lemma `fintype.arg_minP` is aliased to `arg_minnP` and the same for `arg_maxnP`. + The following lemmas are generalized, renamed, and relocated to `order.v`: * `ltr_def` -> `lt_def` * `(ger|gtr)E` -> `(ge|gt)E` * `(le|lt|lte)rr` -> `(le|lt|lte)xx` * `ltrW` -> `ltW` * `ltr_neqAle` -> `lt_neqAle` * `ler_eqVlt` -> `le_eqVlt` * `(gtr|ltr)_eqF` -> `(gt|lt)_eqF` * `ler_anti`, `ler_asym` -> `le_anti` * `eqr_le` -> `eq_le` * `(ltr|ler_lt|ltr_le|ler)_trans` -> `(lt|le_lt|lt_le|le)_trans` * `lerifP` -> `leifP` * `(ltr|ltr_le|ler_lt)_asym` -> `(lt|lt_le|le_lt)_asym` * `lter_anti` -> `lte_anti` * `ltr_geF` -> `lt_geF` * `ler_gtF` -> `le_gtF` * `ltr_gtF` -> `lt_gtF` * `lt(r|nr|rn)W_(n)homo(_in)` -> `ltW_(n)homo(_in)` * `inj_(n)homo_lt(r|nr|rn)(_in)` -> `inj_(n)homo_lt(_in)` * `(inc|dec)(r|nr|rn)_inj(_in)` -> `(inc_dec)_inj(_in)` * `le(r|nr|rn)W_(n)mono(_in)` -> `leW_(n)mono(_in)` * `lenr_(n)mono(_in)` -> `le_(n)mono(_in)` * `lerif_(refl|trans|le|eq)` -> `leif_(refl|trans|le|eq)` * `(ger|ltr)_lerif` -> `(ge|lt)_leif` * `(n)mono(_in)_lerif` -> `(n)mono(_in)_leif` * `(ler|ltr)_total` -> `(le|lt)_total` * `wlog_(ler|ltr)` -> `wlog_(le|lt)` * `ltrNge` -> `ltNge` * `lerNgt` -> `leNgt` * `neqr_lt` -> `neq_lt` * `eqr_(le|lt)(LR|RL)` -> `eq_(le|lt)(LR|RL)` * `eqr_(min|max)(l|r)` -> `eq_(meet|join)(l|r)` * `ler_minr` -> `lexI` * `ler_minl` -> `leIx` * `ler_maxr` -> `lexU` * `ler_maxl` -> `leUx` * `lt(e)r_min(r|l)` -> `lt(e)(xI|Ix)` * `lt(e)r_max(r|l)` -> `lt(e)(xU|Ux)` * `minrK` -> `meetUKC` * `minKr` -> `joinKIC` * `maxr_min(l|r)` -> `joinI(l|r)` * `minr_max(l|r)` -> `meetU(l|r)` * `minrP`, `maxrP` -> `leP`, `ltP` Replacing `minrP` and `maxrP` with `leP` and `ltP` may require to provide some arguments explicitly. The former ones respectively try to match with `minr` and `maxr` first but the latter ones try that in the order of `<`, `<=`, `maxr`, and `minr`. * `(minr|maxr)(r|C|A|CA|AC)` -> `(meet|join)(xx|C|A|CA|AC)` * `minr_(l|r)` -> `meet_(l|r)` * `maxr_(l|r)` -> `join_(l|r)` * `arg_minrP` -> `arg_minP` * `arg_maxrP` -> `arg_maxP` + Generalized the following lemmas as properties of `normedDomainType`: `normr0`, `normr0P`, `normr_eq0`, `distrC`, `normr_id`, `normr_ge0`, `normr_le0`, `normr_lt0`, `normr_gt0`, `normrE`, `normr_real`, `ler_norm_sum`, `ler_norm_sub`, `ler_dist_add`, `ler_sub_norm_add`, `ler_sub_dist`, `ler_dist_dist`, `ler_dist_norm_add`, `ler_nnorml`, `ltr_nnorml`, `lter_nnormr`. + The compatibility layer for the version 1.10 is provided as the `ssrnum.mc_1_10` module. One may compile proofs compatible with the version 1.10 in newer versions by using the `mc_1_10.Num` module instead of the `Num` module. However, instances of the number structures may require changes. - Extended comparison predicates `leqP`, `ltnP`, and `ltngtP` in ssrnat to allow case analysis on `minn` and `maxn`. + The compatibility layer for the version 1.10 is provided as the `ssrnat.mc_1_10` module. One may compile proofs compatible with the version 1.10 in newer versions by using this module. - The definition of `all2` was slightly altered for a better interaction with the guard condition (#469) ### Renamed - `real_lerP` -> `real_leP` - `real_ltrP` -> `real_ltP` - `real_ltrNge` -> `real_ltNge` - `real_lerNgt` -> `real_leNgt` - `real_ltrgtP` -> `real_ltgtP` - `real_ger0P` -> `real_ge0P` - `real_ltrgt0P` -> `real_ltgt0P` - `lerif_nat` -> `leif_nat_r` - Replaced `lerif` with `leif` in the following names of lemmas: + `lerif_subLR`, `lerif_subRL`, `lerif_add`, `lerif_sum`, `lerif_0_sum`, `real_lerif_norm`, `lerif_pmul`, `lerif_nmul`, `lerif_pprod`, `real_lerif_mean_square_scaled`, `real_lerif_AGM2_scaled`, `lerif_AGM_scaled`, `real_lerif_mean_square`, `real_lerif_AGM2`, `lerif_AGM`, `relif_mean_square_scaled`, `lerif_AGM2_scaled`, `lerif_mean_square`, `lerif_AGM2`, `lerif_normC_Re_Creal`, `lerif_Re_Creal`, `lerif_rootC_AGM`. - The following naming inconsistencies have been fixed in `ssrnat.v`: + `homo_inj_lt(_in)` -> `inj_homo_ltn(_in)` + `(inc|dec)r_inj(_in)` -> `(inc|dec)n_inj(_in)` - switching long suffixes to short suffixes + `odd_add` -> `oddD` + `odd_sub` -> `oddB` + `take_addn` -> `takeD` + `rot_addn` -> `rotD` + `nseq_addn` -> `nseqD` - Replaced `cycle` by `orbit` in `perm/action`: + `pcycle` -> `porbit` + `pcycles` -> `porbits` + `pcycleE` -> `porbitE` + `pcycle_actperm` -> `porbit_actperm` + `mem_pcycle` -> `mem_porbit` + `pcycle_id` -> `porbit_id` + `uniq_traject_pcycle` -> `uniq_traject_porbit` + `pcycle_traject` -> `porbit_traject` + `iter_pcycle` -> `iter_porbit` + `eq_pcycle_mem` -> `eq_porbit_mem` + `pcycle_sym` -> `porbit_sym` + `pcycle_perm` -> `porbit_perm` + `ncycles_mul_tperm` -> `porbits_mul_tperm` ### Removed The following were deprecated since release 1.9.0 - `tuple_perm_eqP` (use `tuple_permP` instead, from `perm.v`) - `eq_big_perm` (use `perm_big` instead, from `bigop.v`) - `perm_eqP` (use `permP` instead, from seq.v) - `perm_eqlP` (use `permPl` instead) - `perm_eqrP` (use `permPr` instead) - `perm_eqlE` (use `permEl` instead) - `perm_eq_refl` (use `perm_refl` instead) - `perm_eq_sym` (use `perm_sym` instead) - `perm_eq_trans` (use `perm_trans` instead) - `perm_eq_size` (use `perm_size` instead) - `perm_eq_mem` (use `perm_mem` instead) - `perm_eq_uniq` (use `perm_uniq` instead) ## [1.10.0] - 2019-11-29 This release is compatible with Coq versions 8.9 and 8.10. ### Added - Added a `void` notation for the `Empty_set` type of the standard library, the canonical injection `of_void` and its cancellation lemma `of_voidK`, and `eq`, `choice`, `count` and `fin` instances. - Added `ltn_ind` general induction principle for `nat` variables, helper lemmas `ubnP`, `ltnSE`, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for `nat` measures that does not rely on the `{-2}` numerical occurrence selector, and purged this idiom from the `mathcomp` library (see below). - Added fixpoint and cofixpoint constructions to `finset`: `fixset`, `cofixset` and `fix_order`, with a few theorems about them - Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their "cancellation" lemmas. - Added theorems `totient_prime` and `Euclid_dvd_prod` in `prime.v` - Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little` in `binomial.v` - Added theorems `flatten_map1`, `allpairs_consr`, `mask_filter`, `all_filter`, `all_pmap`, and `all_allpairsP` in `seq.v`. - Added theorems `nth_rcons_default`, `undup_rcons`, `undup_cat` and `undup_flatten_nseq` in `seq.v` - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`, `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`, `eq_enum_rank_in`, `enum_rank_in_inj`, `lshift_inj`, and `rshift_inj`. - Bigop theorems: `index_enum_uniq`, `big_rmcond`, `bigD1_seq`, `big_enum_val_cond`, `big_enum_rank_cond`, `big_enum_val`, `big_enum_rank`, `big_set`, `big_enumP`, `big_enum_cond`, `big_enum` - Arithmetic theorems in ssrnat and div: - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`, `ltn_subrR`, `leq_subrR`, `ltn_subrL` 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`, - some commutations between modulo and division: `modn_divl` and `divn_modl`, - 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 `sort_rec1` and `sortE` to help inductive reasoning on `sort`. - Added map/parametricity theorems about `path`, `sort`, and `sorted`: `homo_path`, `mono_path`, `homo_path_in`, `mono_path_in`, `homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`, `sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`. - Extracting lemma `fpathE` from `fpathP`, and shortening the proof of the latter. - Added the theorem `perm_iota_sort` to express that the sorting of any sequence `s` is equal to a mapping of `iota 0 (size s)` to the nth elements of `s`, so that one can still reason on `nat`, even though the elements of `s` are not in an `eqType`. - Added stability theorems about `merge` and `sort`: `sorted_merge`, `merge_stable_path`, `merge_stable_sorted`, `sorted_sort`, `sort_stable`, `filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`, `sorted_subseq_sort`, and `mem2_sort`. - New algebraic interfaces in `ssralg.v`: comAlgebra and comUnitAlgebra for commutative and commutative-unitary algebras. - Initial property for polynomials in algebras: New canonical lrMoprphism `horner_alg` evaluating a polynomial in an element of an algebra. The theory include the lemmas `in_alg_comm`, `horner_algC`, `horner_algX`, `poly_alg_initial`. - Added lemmas on commutation with difference, big sum and prod: `commrB`, `commr_sum`, `commr_prod`. - Added a few basic seq lemmas about `nseq`, `take` and `drop`: `nseq_addn`, `take_take`, `take_drop`, `take_addn`, `takeC`, `take_nseq`, `drop_nseq`, `rev_nseq`, `take_iota`, `drop_iota`. - Added ssrfun theorem `inj_compr`. - Added theorems `mem2E`, `nextE`, `mem_fcycle`, `inj_cycle`, `take_traject`, `trajectD` and `cycle_catC` in `path.v` - Added lemmas about `cycle`, `connect`, `fconnect`, `order` and `orbit` in `fingraph.v`: - lemma `connect_cycle`, - lemmas `in_orbit`, `order_gt0`, `findex_eq0`, `mem_orbit`, `image_orbit`, - lemmas `fcycle_rconsE`, `fcycle_consE`, `fcycle_consEflatten` and `undup_cycle_cons` which operate under the precondition that the sequence `x :: p` is a cycle for f (i.e. `fcycle f (x :: p)`). - lemmas which operate under the precondition there is a sequence `p` which is a cycle for `f` (i.e. `fcycle f p`): `order_le_cycle`, `finv_cycle`, `f_finv_cycle`, `finv_f_cycle`, `finv_inj_cycle`, `iter_finv_cycle`, `cycle_orbit_cycle`, `fpath_finv_cycle`, `fpath_finv_f_cycle`, `fpath_f_finv_cycle`, `prevE`, `fcycleEflatten`, `fcycle_undup`, `in_orbit_cycle`, `eq_order_cycle`, `iter_order_cycle`, - lemmas `injectivePcycle`, `orbitPcycle`, `fconnect_eqVf`, `order_id_cycle`, `orderPcycle`, `fconnect_f`, `fconnect_findex`. - Added lemma `rot_index` which explicits the index given by `rot_to`. - Added tactic `tfae` to split an equivalence between n+1 propositions into n+1 goals, and referenced orbitPcycle as a reference of use. ### Changed - Replaced the legacy generalised induction idiom with a more robust one that does not rely on the `{-2}` numerical occurrence selector, using new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`, ...., (see above). The new idiom is documented in `ssrnat`. This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release (see [PR #434](https://github.com/math-comp/math-comp/pull/434) for examples). - Replaced the use of the accidental convertibility between `enum A` and `filter A (index_enum T)` with more explicit lemmas `big_enumP`, `big_enum`, `big_enum_cond`, `big_image` added to the `bigop` library, and deprecated the `filter_index_enum` lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future `mathcomp` releases when sets over `finType`s are generalised to finite sets over `choiceType`s, so client libraries should stop relying on this identity. File `bigop.v` has some boilerplate to help with the port; also see [PR #441](https://github.com/math-comp/math-comp/pull/441) for examples. - Restricted `big_image`, `big_image_cond`, `big_image_id` and `big_image_cond_id` to `bigop`s over _abelian_ monoids, anticipating the change in the definition of `enum`. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of `big_map` and `big_enumP`. - `eqVneq` lemma is changed from `{x = y} + {x != y}` to `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs simultaneous replacement of expressions of the form `x == y` and `y == x` by `true` or `false`, while keeping the ability to use it in the way it was used before. - Generalized the `allpairs_catr` lemma to the case where the types of `s`, `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`. - Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`. - Generalized `sort` to non-`eqType`s (as well as `merge`, `merge_sort_push`, `merge_sort_pop`), together with all the lemmas that did not really rely on an `eqType`: `size_merge`, `size_sort`, `merge_path`, `merge_sorted`, `sort_sorted`, `path_min_sorted` (which statement was modified to remove the dependency in `eqType`), and `order_path_min`. - `compare_nat` type family and `ltngtP` comparison predicate are changed from `compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)` to `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`. + The compatibility layer for the version 1.9 is provided as the `ssrnat.mc_1_9` module. One may compile proofs compatible with the version 1.9 in newer versions by using this module. - Moved `iter_in` to ssrnat and reordered its arguments. - Notation `[<-> P0 ; .. ; Pn]` now forces `Pi` to be of type `Prop`. ### Removed - `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma from `fintype` library. ### Infrastructure - `Makefile` now supports the `test-suite` and `only` targets. Currently, `make test-suite` will verify the implementation of mathematical structures and their inheritances of MathComp automatically, by using the `hierarchy.ml` utility. One can use the `only` target to build the sub-libraries of MathComp specified by the `TGTS` variable, e.g., `make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo"`. - `Makefile`now supports a `doc` target to build the documentation as made available on https://mathcomp.github.io/htmldoc/index.html ## [1.9.0] - 2019-05-22 MathComp 1.9.0 is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1. Minor releases will remain compatible with Coq 8.9 and 8.10; compatibility with earlier versions may be dropped. ### Added - `nonPropType`, an interface for non-`Prop` types, and `{pred T}` and `relpre f r`, all of which will be in the Coq 8.10 core SSreflect library. - `deprecate old_id new_id`, notation for `new_id` that prints a deprecation warning for `old_id`; `Import Deprecation.Silent` turns off those warnings, `Import Deprecation.Reject` raises errors instead of only warning. - `filter_nseq`, `count_nseq`, `mem_nseq`, `rcons_inj`, `rcons_injl`, `rcons_injr`, `nthK`, `sumn_rot`. - some `perm_eq` lemmas: `perm_cat[lr]`, `perm_nilP`, `perm_consP`, `perm_has`, `perm_flatten`, `perm_sumn`. - computing (efficiently) (item, multiplicity) tallies of sequences over an `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`. ### Changed - definition of `PredType` which now takes only a `P -> pred T` function; definition of `simpl_rel` to improve simplification by `inE`. Both these changes will be in the Coq 8.10 SSReflect core library. - definition of `permutations s` now uses an optimal algorithm (in space _and_ time) to generate all permutations of s back-to-front, using `tally s`. ### Renamed - `perm_eqP` -> `permP` (`seq.permP` if `perm.v` is also imported) - `perm_eqlP` -> `permPl` - `perm_eqrP` -> `permPr` - `perm_eqlE` -> `permEl` - `perm_eq_refl` -> `perm_refl` - `perm_eq_sym` -> `perm_sym` - `perm_eq_trans` -> `perm_trans` - `perm_eq_size` -> `perm_size` - `perm_eq_mem` -> `perm_mem` - `perm_eq_uniq` -> `perm_uniq` - `perm_eq_rev` -> `perm_rev` - `perm_eq_flatten` -> `perm_flatten` - `perm_eq_all` -> `perm_all` - `perm_eq_small` -> `perm_small_eq` - `perm_eq_nilP` -> `perm_nilP` - `perm_eq_consP` -> `perm_consP` - `leq_size_perm` -> `uniq_min_size` (permuting conclusions) - `perm_uniq` -> `eq_uniq` (permuting assumptions) --> beware `perm_uniq` now means `perm_eq_uniq` - `uniq_perm_eq` -> `uniq_perm` - `perm_eq_iotaP` -> `perm_iotaP` - `perm_undup_count` -> `perm_count_undup` - `tuple_perm_eqP` -> `tuple_permP` - `eq_big_perm` -> `perm_big` - `perm_eq_abelian_type` -> `abelian_type_pgroup` ### Misc - removed Coq prelude hints `plus_n_O` `plus_n_Sm` `mult_n_O` `mult_n_Sm`, to improve robustness of `by ...`; scripts may need to invoke `addn0`, `addnS`, `muln0` or `mulnS` explicitly where these hints were used accidentally. ## [1.8.0] - 2019-04-08 Drop compatibility with Coq 8.6 (OCaml plugin removed). MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. ### Added - Companion matrix of a polynomial `companionmx p` and the theorems: `companionmxK`, `map_mx_companion` and `companion_map_poly` - `homoW_in`, `inj_homo_in`, `mono_inj_in`, `anti_mono_in`, `total_homo_mono_in`, `homoW`, `inj_homo`, `monoj`, `anti_mono`, `total_homo_mono` - `sorted_lt_nth`, `ltn_index`, `sorted_le_nth`, `leq_index`. - `[arg minr_( i < n | P ) F]` and `[arg maxr_( i < n | P ) F]` with all their variants, following the same convention as for `nat` - `contra_neqN`, `contra_neqF`, `contra_neqT`, `contra_neq_eq`, `contra_eq_neq` - `take_subseq`, `drop_subseq` - `big_imset_cond`,`big_map_id`, `big_image_cond` `big_image`, `big_image_cond_id` and `big_image_id` - `foldrE`, `foldlE`, `foldl_idx` and `sumnE` to turn "seq statements" into "bigop statements" - `all_iff` with notation `[<-> P0; P1; ..; Pn]` to talk about circular implication `P0 -> P1 -> ... -> Pn -> P0`. Related theorems are `all_iffLR` and `all_iffP` - support for casts in map comprehension notations, e.g., `[seq E : T | s <- s]`. - a predicate `all2`, a parallel double `seq` version of `all`. - some `perm_eq` lemmas: `perm_cat[lr]`, `perm_eq_nilP`, `perm_eq_consP`, `perm_eq_flatten`. - a function `permutations` that computes a duplicate-free list of all permutations of a given sequence `s` over an `eqType`, along with its theory: `mem_permutations`, `size_permutations`, `permutations_uniq`, `permutations_all_uniq`, `perm_permutations`. - `eq_mktuple`, `eq_ffun`, `eq_finset`, `eq_poly`, `ex_mx` that can be used with the `under` tactic from the Coq 8.10 SSReflect plugin (cf. [coq/coq#9651](https://github.com/coq/coq/pull/9651)) ### Changed - Theory of `lersif` and intervals: + Many `lersif` related lemmas are ported from `ssrnum` + Changed: `prev_of_itv`, `itv_decompose`, and `itv_rewrite` + New theory of intersections of intervals - Generalized `extremum_spec` and its theory, added `extremum` and `extremumP`, generalizing `arg_min` for an arbitrary `eqType` with an order relation on it (rather than `nat`). Redefined `arg_min` and `arg_max` with it. - Reshuffled theorems inside files and packages: + `countalg` goes from the field to the algebra package + `finalg` inherits from countalg + `closed_field` contains the construction of algebraic closure for countable fields that used to be in the file `countalg`. - Maximal implicits applied to reflection, injectivity and cancellation lemmas so that they are easier to pass to combinator lemmas such as `sameP`, `inj_eq` or `canLR`. - Added `reindex_inj s` shorthand for reindexing a bigop with a permutation `s`. - Added lemma `eqmxMunitP`: two matrices with the same shape represent the same subspace iff they differ only by a change of basis. - Corrected implicits and documentation of `MatrixGenField`. - Rewritten proof of quantifier elimination for closed field in a monadic style. - Specialized `bool_irrelevance` so that the statement reflects the name. - Changed the shape of the type of `FieldMixin` to allow one-line in-proof definition of bespoke `fieldType` structure. - Refactored and extended Arguments directives to provide more comprehensive signature information. - Generalized the notation `[seq E | i <- s, j <- t]` to the case where `t` may depend on `i`. The notation is now primitive and expressed using `flatten` and `map` (see documentation of seq). `allpairs` now expands to this notation when fully applied. + Added `allpairs_dep` and made it self-expanding as well. + Generalized some lemmas in a backward compatible way. + Some strictly more general lemmas now have suffix `_dep`. + Replaced `allpairs_comp` with its converse `map_allpairs`. + Added `allpairs` extensionality lemmas for the following cases: non-localised (`eq_allpairs`), dependent localised (`eq_in_allpairs_dep`) and non-dependent localised (`eq_in_allpairs`); as per `eq_in_map`, the latter two are equivalences. - Generalized `{ffun A -> R}` to handle dependent functions, and to be structurally positive so it can be used in recursive inductive type definitions. Minor backward incompatibilities: `fgraph f` is no longer a field accessor, and no longer equal to `val f` as `{ffun A -> R}` is no longer a `subType`; some instances of `finfun`, `ffunE`, `ffunK` may not unify with a generic non-dependent function type `A -> ?R` due to a bug in Coq version 8.9 or below. - Renamed double `seq` induction lemma from `seq2_ind` to `seq_ind2`, and weakened its induction hypothesis. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive. - Many corrections in implicits declarations. - fixed missing joins in `ssralg`, `ssrnum`, `finalg` and `countalg` ### Renamed Renamings also involve the `_in` suffix counterpart when applicable - `mono_inj` -> `incr_inj` - `nmono_inj` -> `decr_inj` - `leq_mono_inj` -> `incnr_inj` - `leq_nmono_inj` -> `decnr_inj` - `homo_inj_ltn_lt` -> `incnr_inj` - `nhomo_inj_ltn_lt` -> `decnr_inj` - `homo_inj_in_lt` -> `inj_homo_ltr_in` - `nhomo_inj_in_lt` -> `inj_nhomo_ltr_in` - `ltn_ltrW_homo` -> `ltnrW_homo` - `ltn_ltrW_nhomo` -> `ltnrW_nhomo` - `leq_lerW_mono` -> `lenrW_mono` - `leq_lerW_nmono` -> `lenrW_nmono` - `homo_leq_mono` -> `lenr_mono` - `nhomo_leq_mono` -> `lenr_nmono` - `homo_inj_lt` -> `inj_homo_ltr` - `nhomo_inj_lt` -> `inj_nhomo_ltr` - `homo_inj_ltn_lt` -> `inj_homo_ltnr` - `nhomo_inj_ltn_lt` -> `inj_nhomo_ltnr` - `homo_mono` -> `ler_mono` - `nhomo_mono` -> `ler_nmono` - `big_setIDdep` -> `big_setIDcond` - `sum_nat_dep_const` -> `sum_nat_cond_const` ### Misc - Removed trailing `_ : Type` field from packed classes. This performance optimization is not strictly necessary with modern Coq versions. - Removed duplicated definitions of `tag`, `tagged` and `Tagged` from `eqtype.v`. They are already in `ssrfun.v`. - Miscellaneous improvements to proof scripts and file organisation. ## [1.7.0] - 2018-04-24 Compatibility with Coq 8.8 and lost compatibility with Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8. - Integration in Coq startng from version 8.7 of: + OCaml plugin (plugin for 8.6 still in the archive for backward compatibility) + `ssreflect.v`, `ssrbool.v`, `ssrfun.v` and `ssrtest/` - Cleaning up the github repository: the math-comp repository is now dedicated to the released material (as in the present release). For instance, directories `real-closed/` and `odd-order/` now have their own repository. ### Changed - Library refactoring: `algC` and `ssrnum`. Library `ssrnum.v` provides an interface `numClosedFieldType`, which abstracts the theory of algebraic numbers. In particular, `Re`, `Im`, `'i`, `conjC`, `n.-root` and `sqrtC`, previously defined in library `algC.v`, are now part of this generic interface. In case of ambiguity, a cast to type `algC`, of complex algebraic numbers, can be used to disambiguate via typing constraints. Some theory was thus made more generic, and the corresponding lemmas, previously defined in library `algC.v` (e.g. `conjCK`) now feature an extra, non maximal implicit, parameter of type `numClosedFieldType`. This could break some proofs. Every theorem from `ssrnum` that used to be in `algC` changed statement. - `ltngtP`, `contra_eq`, `contra_neq`, `odd_opp`, `nth_iota` ### Added - `iter_in`, `finv_in`, `inv_f_in`, `finv_inj_in`, `fconnect_sym_in`, `iter_order_in`, `iter_finv_in`, `cycle_orbit_in`, `fpath_finv_in`, `fpath_finv_f_in`, `fpath_f_finv_in` - `big_allpairs` - `uniqP, uniqPn` - `dec_factor_theorem`, `mul_bin_down`, `mul_bin_left` - `abstract_context` (`in ssreflect.v`, now merged in Coq proper) ### Renamed - Lemma `dvdn_fact` was moved from library `prime.v` to library `div.v` - `mul_Sm_binm -> mul_bin_diag - `divn1` -> `divz1` (in intdiv) - `rootC` -> `nthroot` - `algRe` -> `Re` - `algIm` -> `Im` - `algCi` -> `imaginaryC` - `reshape_index_leq` -> `reshape_leq` ## [1.6.0] - 2015-11-24 (ssreflect + mathcomp) Major reorganization of the archive. - Files split into sub-directories: `ssreflect/`, `algebra/`, `fingroup/`, `solvable/`, `field/` and `character/`. In this way the user can decide to compile only the subset of the Mathematical Components library that is relevant to her. Note that this introduces a possible incompatibility for users of the previous version. A replacement scheme is suggested in the installation notes. - The archive is now open and based on git. Public mirror at: https://github.com/math-comp/math-comp - Sources of the reference manual of the Ssreflect tactic language are also open and available at: https://github.com/math-comp/ssr-manual Pull requests improving the documentation are welcome. ### Renamed - `conjC_closed` -> `cfConjC_closed` - `class_transr` -> `class_eqP` - `cfclass_transl` -> `cfclass_transr` - `nontrivial_ideal` -> `proper_ideal` - `zchar_orthonormalP` -> `vchar_orthonormalP` ### Changed - `seq_sub` - `orbit_in_transl`, `orbit_sym`, `orbit_trans`, `orbit_transl`, `orbit_transr`, `cfAut_char`, `cfConjC_char`, `invg_lcosets`, `lcoset_transl`, `lcoset_transr`, `rcoset_transl`, `rcoset_transr`, `mem2_last`, `bind_unless`, `unless_contra`, `all_and2`, `all_and3`, `all_and4`, `all_and5`, `ltr0_neq0`, `ltr_prod`, `Zisometry_of_iso` ### Added - `adhoc_seq_sub_choiceMixin`, `adhoc_seq_sub_[choice|fin]Type` - `orbit_in_eqP`, `cards_draws`, `cfAut_lin_char`, `cfConjC_lin_char`, `extend_cfConjC_subset`, `isometry_of_free`, `cfAutK`, `cfAutVK`, `lcoset_eqP`, `rcoset_eqP`, `class_eqP`, `gFsub_trans`, `gFnorms`, `gFchar_trans`, `gFnormal_trans`, `gFnorm_trans`, `mem2_seq1`, `dvdn_fact`, `prime_above`, `subKr`, `subrI`, `subIr`, `subr0_eq`, `divrI`, `divIr`, `divKr`, `divfI`, `divIf`, `divKf`, `impliesP`, `impliesPn`, `unlessL`, `unlessR`, `unless_sym`, `unlessP` (coercion), `classicW`, `ltr_prod_nat` - Notation `\unless C, P` ## [1.5.0] - 2014-03-12 (ssreflect + mathcomp) Split the archive in SSReflect and MathComp - With this release "ssreflect" has been split into two packages. The Ssreflect one contains the proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. The Mathematical Components one contains advanced theory files covering a wider spectrum of mathematics. - With respect to version 1.4 the proof language got a few new features related to forward reasoning and some bug fixes. The Mathematical Components library features 16 new theory files and in particular: some field and Galois theory, advanced character theory and a construction of algebraic numbers. ## [1.4.0] - 2012-09-05 (ssreflect) - With this release the plugin code received many bug fixes and the existing libraries relevant updates. This release also includes some new libraries on the following topics: rational numbers, divisibility of integers, F-algebras, finite dimensional field extensions and Euclidean division for polynomials over a ring. - The release includes a major code refactoring of the plugin for Coq 8.4. In particular a documented ML API to access the pattern matching facilities of Ssreflect from third party plugins has been introduced. ## [1.3.0] - 2011-03-14 (ssreflect) - The tactic language has been extended with several new features, inspired by the five years of intensive use in our project. However we have kept the core of the language unchanged; the new library compiles with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" line in ssreflect.v to properly compile the 1.3 library. We will continue supporting new releases of Coq in due course. - The new library adds general linear algebra (matrix rank, subspaces) and all of the advanced finite group that was developed in the course of completing the Local Analysis part of the Odd Order Theorem, starting from the Sylow and Hall theorems and including full structure theorems for abelian, extremal and extraspecial groups, and general (modular) linear representation theory. ## [1.2.0] - 2009-08-14 (ssreflect) No change log ## [1.1.0] - 2008-03-18 (ssreflect) First public release